1/* Title: Tools/Graphview/mutator.scala 2 Author: Markus Kaiser, TU Muenchen 3 Author: Makarius 4 5Filters and add-operations on graphs. 6*/ 7 8package isabelle.graphview 9 10 11import isabelle._ 12 13import java.awt.Color 14import scala.collection.immutable.SortedSet 15 16 17object Mutator 18{ 19 sealed case class Info(enabled: Boolean, color: Color, mutator: Mutator) 20 21 def make(graphview: Graphview, m: Mutator): Info = 22 Info(true, graphview.Colors.next, m) 23 24 class Graph_Filter( 25 val name: String, 26 val description: String, 27 pred: Graph_Display.Graph => Graph_Display.Graph) extends Filter 28 { 29 def filter(graph: Graph_Display.Graph): Graph_Display.Graph = pred(graph) 30 } 31 32 class Graph_Mutator( 33 val name: String, 34 val description: String, 35 pred: (Graph_Display.Graph, Graph_Display.Graph) => Graph_Display.Graph) extends Mutator 36 { 37 def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph = 38 pred(full_graph, graph) 39 } 40 41 class Node_Filter( 42 name: String, 43 description: String, 44 pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean) 45 extends Graph_Filter(name, description, g => g.restrict(pred(g, _))) 46 47 class Edge_Filter( 48 name: String, 49 description: String, 50 pred: (Graph_Display.Graph, Graph_Display.Edge) => Boolean) 51 extends Graph_Filter( 52 name, 53 description, 54 g => (g /: g.dest) { 55 case (graph, ((from, _), tos)) => 56 (graph /: tos)((gr, to) => 57 if (pred(gr, (from, to))) gr else gr.del_edge(from, to)) 58 }) 59 60 class Node_Family_Filter( 61 name: String, 62 description: String, 63 reverse: Boolean, 64 parents: Boolean, 65 children: Boolean, 66 pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean) 67 extends Node_Filter( 68 name, 69 description, 70 (g, k) => 71 reverse != 72 (pred(g, k) || 73 (parents && g.all_preds(List(k)).exists(pred(g, _))) || 74 (children && g.all_succs(List(k)).exists(pred(g, _))))) 75 76 case class Identity() 77 extends Graph_Filter( 78 "Identity", 79 "Does not change the graph.", 80 g => g) 81 82 case class Node_Expression( 83 regex: String, 84 reverse: Boolean, 85 parents: Boolean, 86 children: Boolean) 87 extends Node_Family_Filter( 88 "Filter by Name", 89 "Only shows or hides all nodes with any family member's name matching a regex.", 90 reverse, 91 parents, 92 children, 93 (g, node) => (regex.r findFirstIn node.toString).isDefined) 94 95 case class Node_List( 96 list: List[Graph_Display.Node], 97 reverse: Boolean, 98 parents: Boolean, 99 children: Boolean) 100 extends Node_Family_Filter( 101 "Filter by Name List", 102 "Only shows or hides all nodes with any family member's name matching any string in a comma separated list.", 103 reverse, 104 parents, 105 children, 106 (g, node) => list.contains(node)) 107 108 case class Edge_Endpoints(edge: Graph_Display.Edge) 109 extends Edge_Filter( 110 "Hide edge", 111 "Hides specified edge.", 112 (g, e) => e != edge) 113 114 private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph, 115 keys: List[Graph_Display.Node]) = 116 { 117 // Add Nodes 118 val with_nodes = 119 (to /: keys)((graph, key) => graph.default_node(key, from.get_node(key))) 120 121 // Add Edges 122 (with_nodes /: keys) { 123 (gv, key) => { 124 def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) = 125 (g /: keys) { 126 (graph, end) => { 127 if (!graph.keys_iterator.contains(end)) graph 128 else { 129 if (succs) graph.add_edge(key, end) 130 else graph.add_edge(end, key) 131 } 132 } 133 } 134 135 add_edges( 136 add_edges(gv, from.imm_preds(key), false), 137 from.imm_succs(key), true) 138 } 139 } 140 } 141 142 case class Add_Node_Expression(regex: String) 143 extends Graph_Mutator( 144 "Add by name", 145 "Adds every node whose name matches the regex. " + 146 "Adds all relevant edges.", 147 (full_graph, graph) => 148 add_node_group(full_graph, graph, 149 full_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList)) 150 151 case class Add_Transitive_Closure(parents: Boolean, children: Boolean) 152 extends Graph_Mutator( 153 "Add transitive closure", 154 "Adds all family members of all current nodes.", 155 (full_graph, graph) => { 156 val withparents = 157 if (parents) add_node_group(full_graph, graph, full_graph.all_preds(graph.keys)) 158 else graph 159 if (children) 160 add_node_group(full_graph, withparents, full_graph.all_succs(graph.keys)) 161 else withparents 162 }) 163} 164 165trait Mutator 166{ 167 val name: String 168 val description: String 169 def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph 170 171 override def toString: String = name 172} 173 174trait Filter extends Mutator 175{ 176 def mutate(full_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph) 177 def filter(graph: Graph_Display.Graph): Graph_Display.Graph 178} 179