src/Tools/Graphview/src/model.scala
author wenzelm
Thu Feb 20 14:36:17 2014 +0100 (2014-02-20)
changeset 55618 995162143ef4
parent 50467 4b0e69dc9db8
child 56372 fadb0fef09d7
permissions -rw-r--r--
tuned imports;
markus@49557
     1
/*  Title:      Tools/Graphview/src/model.scala
markus@49557
     2
    Author:     Markus Kaiser, TU Muenchen
markus@49557
     3
markus@49557
     4
Internal graph representation.
markus@49557
     5
*/
markus@49557
     6
markus@49557
     7
package isabelle.graphview
markus@49557
     8
markus@49557
     9
markus@49557
    10
import isabelle._
markus@49557
    11
import isabelle.graphview.Mutators._
wenzelm@55618
    12
markus@49557
    13
import java.awt.Color
markus@49557
    14
markus@49557
    15
wenzelm@49565
    16
class Mutator_Container(val available: List[Mutator]) {
wenzelm@49565
    17
    type Mutator_Markup = (Boolean, Color, Mutator)
markus@49557
    18
    
wenzelm@49733
    19
    val events = new Mutator_Event.Bus
markus@49557
    20
    
markus@49557
    21
    private var _mutators : List[Mutator_Markup] = Nil
markus@49557
    22
    def apply() = _mutators
markus@49557
    23
    def apply(mutators: List[Mutator_Markup]){
markus@49557
    24
      _mutators = mutators
markus@49557
    25
      
markus@49557
    26
      events.event(Mutator_Event.NewList(mutators))
markus@49557
    27
    }    
markus@49557
    28
markus@49557
    29
    def add(mutator: Mutator_Markup) = {
markus@49557
    30
      _mutators = _mutators ::: List(mutator)
markus@49557
    31
      
markus@49557
    32
      events.event(Mutator_Event.Add(mutator))
markus@49557
    33
    }
markus@49557
    34
}
markus@49557
    35
wenzelm@49565
    36
wenzelm@49565
    37
object Model
wenzelm@49565
    38
{
wenzelm@49565
    39
  /* node info */
wenzelm@49565
    40
wenzelm@49565
    41
  sealed case class Info(name: String, content: XML.Body)
wenzelm@49565
    42
wenzelm@49565
    43
  val empty_info: Info = Info("", Nil)
wenzelm@49565
    44
wenzelm@49565
    45
  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
wenzelm@49565
    46
  {
wenzelm@49565
    47
    import XML.Decode._
wenzelm@49565
    48
wenzelm@49565
    49
    val (name, content) = pair(string, x => x)(body)
wenzelm@49565
    50
    Info(name, content)
wenzelm@49565
    51
  }
wenzelm@49565
    52
wenzelm@49565
    53
wenzelm@49565
    54
  /* graph */
wenzelm@49565
    55
wenzelm@49565
    56
  type Graph = isabelle.Graph[String, Info]
wenzelm@49565
    57
wenzelm@49565
    58
  val decode_graph: XML.Decode.T[Graph] =
wenzelm@49565
    59
    isabelle.Graph.decode(XML.Decode.string, decode_info)
wenzelm@49565
    60
}
wenzelm@49565
    61
wenzelm@49565
    62
class Model(private val graph: Model.Graph) {  
markus@49557
    63
  val Mutators = new Mutator_Container(
markus@49557
    64
    List(
markus@49557
    65
      Node_Expression(".*", false, false, false),
markus@49557
    66
      Node_List(Nil, false, false, false),
markus@49557
    67
      Edge_Endpoints("", ""),
markus@49557
    68
      Add_Node_Expression(""),
markus@49557
    69
      Add_Transitive_Closure(true, true)
markus@49557
    70
    ))
markus@49557
    71
  
markus@49557
    72
  val Colors = new Mutator_Container(
markus@49557
    73
    List(
markus@49557
    74
      Node_Expression(".*", false, false, false),
markus@49557
    75
      Node_List(Nil, false, false, false)
markus@49557
    76
    ))  
markus@49557
    77
  
markus@49557
    78
  def visible_nodes(): Iterator[String] = current.keys
markus@49557
    79
  
markus@49557
    80
  def visible_edges(): Iterator[(String, String)] =
wenzelm@49737
    81
    current.keys.map(k => current.imm_succs(k).map((k, _))).flatten  // FIXME iterator
markus@49557
    82
  
markus@49557
    83
  def complete = graph
wenzelm@49565
    84
  def current: Model.Graph =
markus@49557
    85
      (graph /: Mutators()) {
markus@49557
    86
        case (g, (enabled, _, mutator)) => {
markus@49557
    87
          if (!enabled) g
markus@49557
    88
          else mutator.mutate(graph, g)
markus@49557
    89
        }
markus@49557
    90
      }
markus@49557
    91
    
wenzelm@50467
    92
  private var _colors = Map.empty[String, Color]
markus@49557
    93
  def colors = _colors
markus@49557
    94
  
markus@49557
    95
  private def build_colors() {
markus@49854
    96
    _colors = 
wenzelm@50467
    97
      (Map.empty[String, Color] /: Colors()) ({
markus@49854
    98
          case (colors, (enabled, color, mutator)) => {
markus@49854
    99
              (colors /: mutator.mutate(graph, graph).keys) ({
markus@49854
   100
                  case (colors, k) => colors + (k -> color)
markus@49854
   101
                })
markus@49854
   102
            }
markus@49854
   103
      })
markus@49557
   104
  }
wenzelm@49733
   105
  Colors.events += { case _ => build_colors() }
markus@49854
   106
}