# HG changeset patch # User wenzelm # Date 1348597727 -7200 # Node ID ea4308b7ef0ff0c54d5791f2ce768552cbfb2db7 # Parent 03381c41235b547737e2b8e454160826b79bb7b0 ML support for generic graph display, with browser and graphview backends (via print modes); reverse graph layout (again), according to the graph orientation provided by ML; simplified scala types -- eliminated unused type parameters; more explicit Model.Info, Model.Graph; renamed isabelle.graphview.Graphview_Frame to isabelle.graphview.Frame in accordance to file name; removed obsolete Graph_XML and Tooltips; tuned graphview command line; more generous JVM resources via GRAPHVIEW_JAVA_OPTIONS; diff -r 03381c41235b -r ea4308b7ef0f src/Pure/General/graph_display.ML --- a/src/Pure/General/graph_display.ML Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Pure/General/graph_display.ML Tue Sep 25 20:28:47 2012 +0200 @@ -1,7 +1,7 @@ (* Title: Pure/General/graph_display.ML Author: Makarius -Graph display. +Generic graph display, with browser and graphview backends. *) signature GRAPH_DISPLAY = @@ -10,7 +10,9 @@ {name: string, ID: string, dir: string, unfold: bool, path: string, parents: string list, content: Pretty.T list} type graph = node list - val write_graph: Path.T -> graph -> unit + val write_graph_browser: Path.T -> graph -> unit + val browserN: string + val graphviewN: string val display_graph: graph -> unit end; @@ -25,20 +27,45 @@ type graph = node list; -fun write_graph path (graph: graph) = + +(* print modes *) + +val browserN = "browser"; +val graphviewN = "graphview"; + +fun write_graph_browser path (graph: graph) = File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} => "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^ path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph)); +val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks; + +fun encode_graphview (graph: graph) = + Graph.empty + |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph + |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph + |> let open XML.Encode in Graph.encode string (pair string encode_content) end; + +fun write_graph_graphview path graph = + File.write path (YXML.string_of_body (encode_graphview graph)); + + (* display graph *) fun display_graph graph = let + val browser = + (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of + SOME m => m = browserN + | NONE => true); + val (write, tool) = + if browser then (write_graph_browser, "browser") else (write_graph_graphview, "graphview"); + + val _ = writeln "Displaying graph ..."; val path = Isabelle_System.create_tmp_path "graph" ""; - val _ = write_graph path graph; - val _ = writeln "Displaying graph ..."; - val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &"); + val _ = write path graph; + val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &"); in () end; end; diff -r 03381c41235b -r ea4308b7ef0f src/Pure/General/pretty.ML --- a/src/Pure/General/pretty.ML Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Pure/General/pretty.ML Tue Sep 25 20:28:47 2012 +0200 @@ -61,6 +61,7 @@ val output: int option -> T -> Output.output val string_of_margin: int -> T -> string val string_of: T -> string + val symbolic_string_of: T -> string val str_of: T -> string val writeln: T -> unit val to_ML: T -> ML_Pretty.pretty @@ -324,6 +325,7 @@ val output = Buffer.content oo output_buffer; fun string_of_margin margin = Output.escape o output (SOME margin); val string_of = Output.escape o output NONE; +val symbolic_string_of = Output.escape o Buffer.content o symbolic; val str_of = Output.escape o Buffer.content o unformatted; val writeln = Output.writeln o string_of; diff -r 03381c41235b -r ea4308b7ef0f src/Pure/Thy/present.ML --- a/src/Pure/Thy/present.ML Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Pure/Thy/present.ML Tue Sep 25 20:28:47 2012 +0200 @@ -324,7 +324,7 @@ val pdf_path = Path.append dir graph_pdf_path; val eps_path = Path.append dir graph_eps_path; val graph_path = Path.append dir graph_path; - val _ = Graph_Display.write_graph graph_path graph; + val _ = Graph_Display.write_graph_browser graph_path graph; val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path; in if Isabelle_System.isabelle_tool "browser" args = 0 andalso @@ -371,7 +371,7 @@ create_index html_prefix; if length path > 1 then update_index parent_html_prefix name else (); (case readme of NONE => () | SOME path => File.copy path html_prefix); - Graph_Display.write_graph (Path.append html_prefix graph_path) sorted_graph; + Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph; Isabelle_System.isabelle_tool "browser" "-b"; File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix; List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt) diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/etc/settings --- a/src/Tools/Graphview/etc/settings Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/etc/settings Tue Sep 25 20:28:47 2012 +0200 @@ -2,5 +2,7 @@ GRAPHVIEW_HOME="$COMPONENT" +GRAPHVIEW_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m" + ISABELLE_TOOLS="$ISABELLE_TOOLS:$GRAPHVIEW_HOME/lib/Tools" diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/lib/Tools/graphview --- a/src/Tools/Graphview/lib/Tools/graphview Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/lib/Tools/graphview Tue Sep 25 20:28:47 2012 +0200 @@ -11,7 +11,6 @@ "src/floating_dialog.scala" "src/frame.scala" "src/graph_panel.scala" - "src/graph_xml.scala" "src/layout_pendulum.scala" "src/main_panel.scala" "src/model.scala" @@ -21,7 +20,6 @@ "src/parameters.scala" "src/popups.scala" "src/shapes.scala" - "src/tooltips.scala" "src/visualizer.scala" "../jEdit/src/html_panel.scala" ) @@ -60,15 +58,15 @@ # options -BUILD_ONLY=false -CLEAN="" +BUILD_ONLY="false" +CLEAN="false" BUILD_JARS="jars" while getopts "bcf" OPT do case "$OPT" in b) - BUILD_ONLY=true + BUILD_ONLY="true" ;; c) CLEAN="true" @@ -88,15 +86,9 @@ # args GRAPH_FILE="" - -if [ "$#" -eq 0 -a "$BUILD_ONLY" = false ]; then - usage -elif [ "$#" -eq 1 ]; then - GRAPH_FILE="$1" - shift -else - usage -fi +[ "$#" -gt 0 ] && { GRAPH_FILE="$1"; shift; } +[ "$#" -ne 0 ] && usage +[ -z "$GRAPH_FILE" -a "$BUILD_ONLY" = false ] && usage ## build @@ -182,13 +174,13 @@ if [ "$BUILD_ONLY" = false ]; then PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$""$(basename "$GRAPH_FILE")" - if [ "$CLEAN" = true ]; then + if [ "$CLEAN" = "true" ]; then mv -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPH_FILE" else cp -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPH_FILE" fi - "$ISABELLE_TOOL" java isabelle.graphview.Graphview_Frame "$(jvmpath "$PRIVATE_FILE")" + "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Frame "$PRIVATE_FILE" RC="$?" rm -f "$PRIVATE_FILE" diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/frame.scala --- a/src/Tools/Graphview/src/frame.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/frame.scala Tue Sep 25 20:28:47 2012 +0200 @@ -14,39 +14,25 @@ import javax.swing.border.EmptyBorder -object Graphview_Frame extends SwingApplication +object Frame extends SwingApplication { def startup(args : Array[String]) { - try { - Platform.init_laf() - Isabelle_System.init() - } - catch { case exn: Throwable => println(Exn.message(exn)); System.exit(1) } + // FIXME avoid I/O etc. on Swing thread + val graph: Model.Graph = + try { + Platform.init_laf() + Isabelle_System.init() - val opt_xml: Option[XML.Tree] = - try { - Some(YXML.parse_body( - Symbol.decode(io.Source.fromFile(args(0)).mkString)).head) - } catch { - case _ : ArrayIndexOutOfBoundsException => None - case _ : java.io.FileNotFoundException => None + args.toList match { + case List(arg) => + Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg)))) + case _ => error("Bad arguments:\n" + cat_lines(args)) + } } - - //Textfiles will still be valid and result in an empty frame - //since they are valid to YXML. - opt_xml match { - case None => - println("No valid YXML-File given.\n" + - "Usage: java -jar graphview.jar ") - System.exit(1) - case Some(xml) => - val top = frame(xml) - top.pack() - top.visible = true - } + catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) } - def frame(xml: XML.Tree): Window = new MainFrame { + val top = new MainFrame { title = "Graphview" minimumSize = new Dimension(640, 480) preferredSize = new Dimension(800, 600) @@ -54,8 +40,11 @@ contents = new BorderPanel { border = new EmptyBorder(5, 5, 5, 5) - add(new Main_Panel(xml), BorderPanel.Position.Center) + add(new Main_Panel(graph), BorderPanel.Position.Center) } } + + top.pack() + top.visible = true } } \ No newline at end of file diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/graph_xml.scala --- a/src/Tools/Graphview/src/graph_xml.scala Tue Sep 25 18:24:49 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,74 +0,0 @@ -/* Title: Tools/Graphview/src/graph_xml.scala - Author: Markus Kaiser, TU Muenchen - -XML to graph conversion. -*/ - -package isabelle.graphview - - -import isabelle._ - - -case class Locale(val axioms: List[XML.Body], val parameters: List[(String, XML.Body)]) - -object Graph_XML -{ - type Entry = Option[Locale] - type Nodes = List[(String, (Entry, List[String]))] - - def apply(xml: XML.Tree): Graph[String, Entry] = { - val nodes : Nodes = - { - try { - xml match { - case XML.Elem(Markup("thy_deps", Nil), ts) => thy_deps(ts) - case XML.Elem(Markup("locale_deps", Nil), ts) => locale_deps(ts) - case _ => Nil - } - } - } - - // Add nodes - val node_graph = - (Graph.string[Entry] /: nodes) { - case (graph, (key, (info, _))) => graph.new_node(key, info) - } - - // Add edges - (node_graph /: nodes) { - case (graph, (from, (_, tos))) => - (graph /: tos) { - (graph, to) => graph.add_edge(from, to) - } - } - } - - private def thy_deps(ts: XML.Body) : Nodes = { - val strings : List[(String, List[String])] = { - import XML.Decode._ - - list(pair(string, list(string)))(ts) - } - - strings.map({case (key, tos) => (key, (None, tos))}) - } - - private def locale_deps(ts: XML.Body) : Nodes = { - // Identity functions return (potential) term-xmls - val strings = { - import XML.Decode._ - val node = pair(list(x=>x),pair(list(pair(string,x=>x)),list(list(x=>x)))) - val graph = list(pair(pair(string, node), list(string))) - def symtab[A](f: T[A]) = list(pair(x=>x, f)) - val dependencies = symtab(symtab(list(list(x=>x)))) - pair(graph, dependencies)(ts) - } - - strings._1.map({ - case ((key, (axioms, (parameters, _))), tos) => - (key, (Some(Locale(axioms, parameters)), tos)) - } - ) - } -} diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/layout_pendulum.scala --- a/src/Tools/Graphview/src/layout_pendulum.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/layout_pendulum.scala Tue Sep 25 20:28:47 2012 +0200 @@ -12,26 +12,25 @@ object Layout_Pendulum { type Key = String - type Entry = Option[Locale] type Point = (Double, Double) type Coordinates = Map[Key, Point] type Level = List[Key] type Levels = List[Level] type Layout = (Coordinates, Map[(Key, Key), List[Point]]) - type Dummies = (Graph[Key, Entry], List[Key], Map[Key, Int]) + type Dummies = (Model.Graph, List[Key], Map[Key, Int]) val x_distance = 350 val y_distance = 350 val pendulum_iterations = 10 - def apply(graph: Graph[Key, Entry]): Layout = { + def apply(graph: Model.Graph): Layout = { if (graph.entries.isEmpty) (Map[Key, Point](), Map[(Key, Key), List[Point]]()) else { val (dummy_graph, dummies, dummy_levels) = { val initial_levels = level_map(graph) - def add_dummies(graph: Graph[Key, Entry], from: Key, to: Key, + def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies = { val ds = ((levels(from) + 1) until levels(to)) @@ -44,7 +43,7 @@ val next_nodes = (graph /: ds) { - (graph, d) => graph.new_node(d, None) + (graph, d) => graph.new_node(d, Model.empty_info) } val next = @@ -89,7 +88,7 @@ } } - def level_map(graph: Graph[Key, Entry]): Map[Key, Int] = + def level_map(graph: Model.Graph): Map[Key, Int] = (Map[Key, Int]() /: graph.topological_order){ (levels, key) => { val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1) @@ -108,7 +107,7 @@ } }.map(_._2) - def count_crossings(graph: Graph[Key, Entry], levels: Levels): Int = { + def count_crossings(graph: Model.Graph, levels: Levels): Int = { def in_level(ls: Levels): Int = ls match { case List(top, bot) => top.zipWithIndex.map{ @@ -131,7 +130,7 @@ levels.sliding(2).map(in_level).sum } - def minimize_crossings(graph: Graph[Key, Entry], levels: Levels): Levels = { + def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = { def resort_level(parent: Level, child: Level, top_down: Boolean): Level = child.map(k => { val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k) @@ -167,7 +166,7 @@ } def initial_coordinates(levels: Levels): Coordinates = - (Map[Key, Point]() /: levels.reverse.zipWithIndex){ + (Map[Key, Point]() /: levels.zipWithIndex){ case (coords, (level, yi)) => (coords /: level.zipWithIndex) { case (coords, (node, xi)) => @@ -175,7 +174,7 @@ } } - def pendulum(graph: Graph[Key, Entry], + def pendulum(graph: Model.Graph, levels: Levels, coords: Map[Key, Point]): Coordinates = { type Regions = List[List[Region]] @@ -260,7 +259,7 @@ }._2 } - protected class Region(val graph: Graph[Key, Entry], node: Key) { + protected class Region(val graph: Model.Graph, node: Key) { var nodes: List[Key] = List(node) def left(coords: Coordinates): Double = diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/main_panel.scala --- a/src/Tools/Graphview/src/main_panel.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/main_panel.scala Tue Sep 25 20:28:47 2012 +0200 @@ -18,12 +18,12 @@ import java.io.File -class Main_Panel(xml: XML.Tree) extends BorderPanel +class Main_Panel(graph: Model.Graph) extends BorderPanel { focusable = true requestFocus() - val model = new Model(Graph_XML(xml)) + val model = new Model(graph) val visualizer = new Visualizer(model) val graph_panel = new Graph_Panel(visualizer) diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/model.scala --- a/src/Tools/Graphview/src/model.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/model.scala Tue Sep 25 20:28:47 2012 +0200 @@ -14,8 +14,8 @@ import scala.actors.Actor._ -class Mutator_Container(val available: List[Mutator[String, Option[Locale]]]) { - type Mutator_Markup = (Boolean, Color, Mutator[String, Option[Locale]]) +class Mutator_Container(val available: List[Mutator]) { + type Mutator_Markup = (Boolean, Color, Mutator) val events = new Event_Bus[Mutator_Event.Message] @@ -34,7 +34,33 @@ } } -class Model(private val graph: Graph[String, Option[Locale]]) { + +object Model +{ + /* node info */ + + sealed case class Info(name: String, content: XML.Body) + + val empty_info: Info = Info("", Nil) + + val decode_info: XML.Decode.T[Info] = (body: XML.Body) => + { + import XML.Decode._ + + val (name, content) = pair(string, x => x)(body) + Info(name, content) + } + + + /* graph */ + + type Graph = isabelle.Graph[String, Info] + + val decode_graph: XML.Decode.T[Graph] = + isabelle.Graph.decode(XML.Decode.string, decode_info) +} + +class Model(private val graph: Model.Graph) { val Mutators = new Mutator_Container( List( Node_Expression(".*", false, false, false), @@ -57,7 +83,7 @@ current.keys.map(k => current.imm_succs(k).map((k, _))).flatten def complete = graph - def current: Graph[String, Option[Locale]] = + def current: Model.Graph = (graph /: Mutators()) { case (g, (enabled, _, mutator)) => { if (!enabled) g diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/mutator.scala --- a/src/Tools/Graphview/src/mutator.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/mutator.scala Tue Sep 25 20:28:47 2012 +0200 @@ -13,60 +13,57 @@ import scala.collection.immutable.SortedSet -trait Mutator[Key, Entry] +trait Mutator { val name: String val description: String - def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry] + def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph override def toString() = name } -trait Filter[Key, Entry] -extends Mutator[Key, Entry] +trait Filter extends Mutator { - def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]) = filter(sub) - def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry] + def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub) + def filter(sub: Model.Graph) : Model.Graph } object Mutators { - type Key = String - type Entry = Option[Locale] - type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry]) + type Mutator_Markup = (Boolean, Color, Mutator) val Enabled = true val Disabled = false - def create(m: Mutator[Key, Entry]): Mutator_Markup = + def create(m: Mutator): Mutator_Markup = (Mutators.Enabled, Parameters.Colors.next, m) - class Graph_Filter[Key, Entry](val name: String, val description: String, - pred: Graph[Key, Entry] => Graph[Key, Entry]) - extends Filter[Key, Entry] + class Graph_Filter(val name: String, val description: String, + pred: Model.Graph => Model.Graph) + extends Filter { - def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry] = pred(sub) + def filter(sub: Model.Graph) : Model.Graph = pred(sub) } - class Graph_Mutator[Key, Entry](val name: String, val description: String, - pred: (Graph[Key, Entry], Graph[Key, Entry]) => Graph[Key, Entry]) - extends Mutator[Key, Entry] + class Graph_Mutator(val name: String, val description: String, + pred: (Model.Graph, Model.Graph) => Model.Graph) + extends Mutator { - def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry] = + def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph = pred(complete, sub) } - class Node_Filter[Key, Entry](name: String, description: String, - pred: (Graph[Key, Entry], Key) => Boolean) - extends Graph_Filter[Key, Entry] ( + class Node_Filter(name: String, description: String, + pred: (Model.Graph, String) => Boolean) + extends Graph_Filter ( name, description, g => g.restrict(pred(g, _)) ) - class Edge_Filter[Key, Entry](name: String, description: String, - pred: (Graph[Key, Entry], Key, Key) => Boolean) - extends Graph_Filter[Key, Entry] ( + class Edge_Filter(name: String, description: String, + pred: (Model.Graph, String, String) => Boolean) + extends Graph_Filter ( name, description, @@ -80,10 +77,10 @@ } ) - class Node_Family_Filter[Key, Entry](name: String, description: String, + class Node_Family_Filter(name: String, description: String, reverse: Boolean, parents: Boolean, children: Boolean, - pred: (Graph[Key, Entry], Key) => Boolean) - extends Node_Filter[Key, Entry]( + pred: (Model.Graph, String) => Boolean) + extends Node_Filter( name, description, @@ -95,7 +92,7 @@ ) case class Identity() - extends Graph_Filter[Key, Entry]( + extends Graph_Filter( "Identity", "Does not change the graph.", @@ -104,7 +101,7 @@ case class Node_Expression(regex: String, reverse: Boolean, parents: Boolean, children: Boolean) - extends Node_Family_Filter[Key, Entry]( + extends Node_Family_Filter( "Filter by Name", "Only shows or hides all nodes with any family member's name matching " + @@ -117,7 +114,7 @@ case class Node_List(list: List[String], reverse: Boolean, parents: Boolean, children: Boolean) - extends Node_Family_Filter[Key, Entry]( + extends Node_Family_Filter( "Filter by Name List", "Only shows or hides all nodes with any family member's name matching " + @@ -129,7 +126,7 @@ ) case class Edge_Endpoints(source: String, dest: String) - extends Edge_Filter[Key, Entry]( + extends Edge_Filter( "Hide edge", "Hides the edge whose endpoints match strings.", @@ -137,7 +134,7 @@ ) case class Edge_Transitive() - extends Edge_Filter[Key, Entry]( + extends Edge_Filter( "Hide transitive edges", "Hides all transitive edges.", @@ -147,8 +144,8 @@ } ) - private def add_node_group(from: Graph[Key, Entry], to: Graph[Key, Entry], - keys: List[Key]) = { + private def add_node_group(from: Model.Graph, to: Model.Graph, + keys: List[String]) = { // Add Nodes val with_nodes = @@ -159,7 +156,7 @@ // Add Edges (with_nodes /: keys) { (gv, key) => { - def add_edges(g: Graph[Key, Entry], keys: SortedSet[Key], succs: Boolean) = + def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) = (g /: keys) { (graph, end) => { if (!graph.keys.contains(end)) graph @@ -180,7 +177,7 @@ } case class Add_Node_Expression(regex: String) - extends Graph_Mutator[Key, Entry]( + extends Graph_Mutator( "Add by name", "Adds every node whose name matches the regex. " + @@ -193,7 +190,7 @@ ) case class Add_Transitive_Closure(parents: Boolean, children: Boolean) - extends Graph_Mutator[Key, Entry]( + extends Graph_Mutator( "Add transitive closure", "Adds all family members of all current nodes.", diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/mutator_dialog.scala --- a/src/Tools/Graphview/src/mutator_dialog.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/mutator_dialog.scala Tue Sep 25 20:28:47 2012 +0200 @@ -25,9 +25,7 @@ reverse_caption: String = "Inverse", show_color_chooser: Boolean = true) extends Dialog { - type Key = String - type Entry = Option[Locale] - type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry]) + type Mutator_Markup = (Boolean, Color, Mutator) title = caption @@ -112,7 +110,7 @@ val filterPanel = new BoxPanel(Orientation.Vertical) {} - private val mutatorBox = new ComboBox[Mutator[Key, Entry]](container.available) + private val mutatorBox = new ComboBox[Mutator](container.available) private val addButton: Button = new Button{ action = Action("Add") { diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/mutator_event.scala --- a/src/Tools/Graphview/src/mutator_event.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/mutator_event.scala Tue Sep 25 20:28:47 2012 +0200 @@ -12,9 +12,7 @@ object Mutator_Event { - type Key = String - type Entry = Option[Locale] - type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry]) + type Mutator_Markup = (Boolean, Color, Mutator) sealed abstract class Message case class Add(m: Mutator_Markup) extends Message diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/tooltips.scala --- a/src/Tools/Graphview/src/tooltips.scala Tue Sep 25 18:24:49 2012 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,93 +0,0 @@ -/* Title: Tools/Graphview/src/graph_components.scala - Author: Markus Kaiser, TU Muenchen - -Tooltip generation for graph components. -*/ - -package isabelle.graphview - - -import isabelle._ -import java.awt.FontMetrics - - -object Tooltips { - // taken (and modified slightly) from html_panel.scala - private def make_HTML(term: XML.Body, fm: FontMetrics): String = { - XML.string_of_body ( term.flatMap(div => - Pretty.formatted(List(div), 76, Pretty.font_metric(fm)) - .map( t=> - HTML.spans(t, false)) - ).head - ) - } - - def locale(key: String, model: Model, fm: FontMetrics): String = { - val locale = model.complete.get_node(key) - val parsed_name = key.split('.') - - if (!locale.isDefined) { - """| - | - |%s - | - |""".stripMargin.format(parsed_name.reduceLeft("%s
%s".format(_,_))) - } else { - val Some(Locale(axioms, parameters)) = locale - - val parms = { - if (parameters.size > 0) { - """| - |

Parameters:

- | - |""".stripMargin.format(parameters.map( - y => "
  • %s :: %s
    • ".format( - y._1, - make_HTML(y._2, fm)) - ).reduceLeft(_+_)) - } else "" - } - val axms = { - if (axioms.size > 0) { - """| - |

    Axioms:

    - | - |""".stripMargin.format(axioms.map( - y => "
  • %s
    • ".format( - make_HTML(y, fm)) - ).reduceLeft(_+_)) - } else "" - } - - """| - | - | - |
    %s
    - |
    - |%s - |%s - | - | - |""".stripMargin.format(Parameters.tooltip_css, - parsed_name.reduceLeft("%s
    %s".format(_,_)), - axms, - parms).replace("'", "'") - } - } -} \ No newline at end of file diff -r 03381c41235b -r ea4308b7ef0f src/Tools/Graphview/src/visualizer.scala --- a/src/Tools/Graphview/src/visualizer.scala Tue Sep 25 18:24:49 2012 +0200 +++ b/src/Tools/Graphview/src/visualizer.scala Tue Sep 25 20:28:47 2012 +0200 @@ -6,6 +6,7 @@ package isabelle.graphview +import isabelle._ import java.awt.{RenderingHints, Graphics2D} @@ -142,8 +143,14 @@ object Tooltip { import java.awt.FontMetrics - - def apply(l: String, fm: FontMetrics) = Tooltips.locale(l, model, fm) + + def apply(l: String, fm: FontMetrics): String = + { + val info = model.complete.get_node(l) + XML.string_of_body( + Pretty.formatted(info.content, 76, Pretty.font_metric(fm)) + .map(t => XML.Elem(Markup(HTML.PRE, Nil), HTML.spans(t, false)))) + } } object Font {