1/* Title: Tools/Graphview/model.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5Internal graph representation. 6*/ 7 8package isabelle.graphview 9 10 11import isabelle._ 12 13import java.awt.Color 14 15 16class Mutator_Container(val available: List[Mutator]) 17{ 18 val events = new Mutator_Event.Bus 19 20 private var _mutators : List[Mutator.Info] = Nil 21 def apply() = _mutators 22 def apply(mutators: List[Mutator.Info]) 23 { 24 _mutators = mutators 25 events.event(Mutator_Event.New_List(mutators)) 26 } 27 28 def add(mutator: Mutator.Info) 29 { 30 _mutators = _mutators ::: List(mutator) 31 events.event(Mutator_Event.Add(mutator)) 32 } 33} 34 35 36class Model(val full_graph: Graph_Display.Graph) 37{ 38 val Mutators = 39 new Mutator_Container( 40 List( 41 Mutator.Node_Expression(".*", false, false, false), 42 Mutator.Node_List(Nil, false, false, false), 43 Mutator.Edge_Endpoints((Graph_Display.Node.dummy, Graph_Display.Node.dummy)), 44 Mutator.Add_Node_Expression(""), 45 Mutator.Add_Transitive_Closure(true, true))) 46 47 val Colors = 48 new Mutator_Container( 49 List( 50 Mutator.Node_Expression(".*", false, false, false), 51 Mutator.Node_List(Nil, false, false, false))) 52 53 def find_node(ident: String): Option[Graph_Display.Node] = 54 full_graph.keys_iterator.find(node => node.ident == ident) 55 56 def make_visible_graph(): Graph_Display.Graph = 57 (full_graph /: Mutators()) { 58 case (g, m) => if (!m.enabled) g else m.mutator.mutate(full_graph, g) 59 } 60 61 private var _colors = Map.empty[Graph_Display.Node, Color] 62 def colors = _colors 63 64 private def build_colors() 65 { 66 _colors = 67 (Map.empty[Graph_Display.Node, Color] /: Colors()) { 68 case (colors, m) => 69 (colors /: m.mutator.mutate(full_graph, full_graph).keys_iterator) { 70 case (colors, node) => colors + (node -> m.color) 71 } 72 } 73 } 74 Colors.events += { case _ => build_colors() } 75} 76