ML support for generic graph display, with browser and graphview backends (via print modes);
authorwenzelm
Tue Sep 25 20:28:47 2012 +0200 (2012-09-25)
changeset 49565ea4308b7ef0f
parent 49564 03381c41235b
child 49566 66cbf8bb4693
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;
src/Pure/General/graph_display.ML
src/Pure/General/pretty.ML
src/Pure/Thy/present.ML
src/Tools/Graphview/etc/settings
src/Tools/Graphview/lib/Tools/graphview
src/Tools/Graphview/src/frame.scala
src/Tools/Graphview/src/graph_xml.scala
src/Tools/Graphview/src/layout_pendulum.scala
src/Tools/Graphview/src/main_panel.scala
src/Tools/Graphview/src/model.scala
src/Tools/Graphview/src/mutator.scala
src/Tools/Graphview/src/mutator_dialog.scala
src/Tools/Graphview/src/mutator_event.scala
src/Tools/Graphview/src/tooltips.scala
src/Tools/Graphview/src/visualizer.scala
     1.1 --- a/src/Pure/General/graph_display.ML	Tue Sep 25 18:24:49 2012 +0200
     1.2 +++ b/src/Pure/General/graph_display.ML	Tue Sep 25 20:28:47 2012 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/graph_display.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Graph display.
     1.8 +Generic graph display, with browser and graphview backends.
     1.9  *)
    1.10  
    1.11  signature GRAPH_DISPLAY =
    1.12 @@ -10,7 +10,9 @@
    1.13     {name: string, ID: string, dir: string, unfold: bool,
    1.14      path: string, parents: string list, content: Pretty.T list}
    1.15    type graph = node list
    1.16 -  val write_graph: Path.T -> graph -> unit
    1.17 +  val write_graph_browser: Path.T -> graph -> unit
    1.18 +  val browserN: string
    1.19 +  val graphviewN: string
    1.20    val display_graph: graph -> unit
    1.21  end;
    1.22  
    1.23 @@ -25,20 +27,45 @@
    1.24  
    1.25  type graph = node list;
    1.26  
    1.27 -fun write_graph path (graph: graph) =
    1.28 +
    1.29 +(* print modes *)
    1.30 +
    1.31 +val browserN = "browser";
    1.32 +val graphviewN = "graphview";
    1.33 +
    1.34 +fun write_graph_browser path (graph: graph) =
    1.35    File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.36      "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.37      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
    1.38  
    1.39  
    1.40 +val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
    1.41 +
    1.42 +fun encode_graphview (graph: graph) =
    1.43 +  Graph.empty
    1.44 +  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
    1.45 +  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.46 +  |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
    1.47 +
    1.48 +fun write_graph_graphview path graph =
    1.49 +  File.write path (YXML.string_of_body (encode_graphview graph));
    1.50 +
    1.51 +
    1.52  (* display graph *)
    1.53  
    1.54  fun display_graph graph =
    1.55    let
    1.56 +    val browser =
    1.57 +      (case find_first (fn m => m = browserN orelse m = graphviewN) (print_mode_value ()) of
    1.58 +        SOME m => m = browserN
    1.59 +      | NONE => true);
    1.60 +    val (write, tool) =
    1.61 +      if browser then (write_graph_browser, "browser") else (write_graph_graphview, "graphview");
    1.62 +
    1.63 +    val _ = writeln "Displaying graph ...";
    1.64      val path = Isabelle_System.create_tmp_path "graph" "";
    1.65 -    val _ = write_graph path graph;
    1.66 -    val _ = writeln "Displaying graph ...";
    1.67 -    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    1.68 +    val _ = write path graph;
    1.69 +    val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
    1.70    in () end;
    1.71  
    1.72  end;
     2.1 --- a/src/Pure/General/pretty.ML	Tue Sep 25 18:24:49 2012 +0200
     2.2 +++ b/src/Pure/General/pretty.ML	Tue Sep 25 20:28:47 2012 +0200
     2.3 @@ -61,6 +61,7 @@
     2.4    val output: int option -> T -> Output.output
     2.5    val string_of_margin: int -> T -> string
     2.6    val string_of: T -> string
     2.7 +  val symbolic_string_of: T -> string
     2.8    val str_of: T -> string
     2.9    val writeln: T -> unit
    2.10    val to_ML: T -> ML_Pretty.pretty
    2.11 @@ -324,6 +325,7 @@
    2.12  val output = Buffer.content oo output_buffer;
    2.13  fun string_of_margin margin = Output.escape o output (SOME margin);
    2.14  val string_of = Output.escape o output NONE;
    2.15 +val symbolic_string_of = Output.escape o Buffer.content o symbolic;
    2.16  val str_of = Output.escape o Buffer.content o unformatted;
    2.17  val writeln = Output.writeln o string_of;
    2.18  
     3.1 --- a/src/Pure/Thy/present.ML	Tue Sep 25 18:24:49 2012 +0200
     3.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 25 20:28:47 2012 +0200
     3.3 @@ -324,7 +324,7 @@
     3.4      val pdf_path = Path.append dir graph_pdf_path;
     3.5      val eps_path = Path.append dir graph_eps_path;
     3.6      val graph_path = Path.append dir graph_path;
     3.7 -    val _ = Graph_Display.write_graph graph_path graph;
     3.8 +    val _ = Graph_Display.write_graph_browser graph_path graph;
     3.9      val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    3.10    in
    3.11      if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    3.12 @@ -371,7 +371,7 @@
    3.13          create_index html_prefix;
    3.14          if length path > 1 then update_index parent_html_prefix name else ();
    3.15          (case readme of NONE => () | SOME path => File.copy path html_prefix);
    3.16 -        Graph_Display.write_graph (Path.append html_prefix graph_path) sorted_graph;
    3.17 +        Graph_Display.write_graph_browser (Path.append html_prefix graph_path) sorted_graph;
    3.18          Isabelle_System.isabelle_tool "browser" "-b";
    3.19          File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
    3.20          List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
     4.1 --- a/src/Tools/Graphview/etc/settings	Tue Sep 25 18:24:49 2012 +0200
     4.2 +++ b/src/Tools/Graphview/etc/settings	Tue Sep 25 20:28:47 2012 +0200
     4.3 @@ -2,5 +2,7 @@
     4.4  
     4.5  GRAPHVIEW_HOME="$COMPONENT"
     4.6  
     4.7 +GRAPHVIEW_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m"
     4.8 +
     4.9  ISABELLE_TOOLS="$ISABELLE_TOOLS:$GRAPHVIEW_HOME/lib/Tools"
    4.10  
     5.1 --- a/src/Tools/Graphview/lib/Tools/graphview	Tue Sep 25 18:24:49 2012 +0200
     5.2 +++ b/src/Tools/Graphview/lib/Tools/graphview	Tue Sep 25 20:28:47 2012 +0200
     5.3 @@ -11,7 +11,6 @@
     5.4    "src/floating_dialog.scala"
     5.5    "src/frame.scala"
     5.6    "src/graph_panel.scala"
     5.7 -  "src/graph_xml.scala"
     5.8    "src/layout_pendulum.scala"
     5.9    "src/main_panel.scala"
    5.10    "src/model.scala"
    5.11 @@ -21,7 +20,6 @@
    5.12    "src/parameters.scala"
    5.13    "src/popups.scala"
    5.14    "src/shapes.scala"
    5.15 -  "src/tooltips.scala"
    5.16    "src/visualizer.scala"
    5.17    "../jEdit/src/html_panel.scala"
    5.18  )
    5.19 @@ -60,15 +58,15 @@
    5.20  
    5.21  # options
    5.22  
    5.23 -BUILD_ONLY=false
    5.24 -CLEAN=""
    5.25 +BUILD_ONLY="false"
    5.26 +CLEAN="false"
    5.27  BUILD_JARS="jars"
    5.28  
    5.29  while getopts "bcf" OPT
    5.30  do
    5.31    case "$OPT" in
    5.32      b)
    5.33 -      BUILD_ONLY=true
    5.34 +      BUILD_ONLY="true"
    5.35        ;;
    5.36      c)
    5.37        CLEAN="true"
    5.38 @@ -88,15 +86,9 @@
    5.39  # args
    5.40  
    5.41  GRAPH_FILE=""
    5.42 -
    5.43 -if [ "$#" -eq 0 -a "$BUILD_ONLY" = false ]; then
    5.44 -  usage
    5.45 -elif [ "$#" -eq 1 ]; then
    5.46 -  GRAPH_FILE="$1"
    5.47 -  shift
    5.48 -else
    5.49 -  usage
    5.50 -fi
    5.51 +[ "$#" -gt 0 ] && { GRAPH_FILE="$1"; shift; }
    5.52 +[ "$#" -ne 0 ] && usage
    5.53 +[ -z "$GRAPH_FILE" -a "$BUILD_ONLY" = false ] && usage
    5.54  
    5.55  
    5.56  ## build
    5.57 @@ -182,13 +174,13 @@
    5.58  
    5.59  if [ "$BUILD_ONLY" = false ]; then
    5.60    PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$""$(basename "$GRAPH_FILE")"
    5.61 -  if [ "$CLEAN" = true ]; then
    5.62 +  if [ "$CLEAN" = "true" ]; then
    5.63      mv -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPH_FILE"
    5.64    else
    5.65      cp -f "$GRAPH_FILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPH_FILE"
    5.66    fi
    5.67  
    5.68 -  "$ISABELLE_TOOL" java isabelle.graphview.Graphview_Frame "$(jvmpath "$PRIVATE_FILE")"
    5.69 +  "$ISABELLE_TOOL" java $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Frame "$PRIVATE_FILE"
    5.70    RC="$?"
    5.71  
    5.72    rm -f "$PRIVATE_FILE"
     6.1 --- a/src/Tools/Graphview/src/frame.scala	Tue Sep 25 18:24:49 2012 +0200
     6.2 +++ b/src/Tools/Graphview/src/frame.scala	Tue Sep 25 20:28:47 2012 +0200
     6.3 @@ -14,39 +14,25 @@
     6.4  import javax.swing.border.EmptyBorder
     6.5  
     6.6  
     6.7 -object Graphview_Frame extends SwingApplication
     6.8 +object Frame extends SwingApplication
     6.9  {
    6.10    def startup(args : Array[String])
    6.11    {
    6.12 -    try {
    6.13 -      Platform.init_laf()
    6.14 -      Isabelle_System.init()
    6.15 -    }
    6.16 -    catch { case exn: Throwable => println(Exn.message(exn)); System.exit(1) }
    6.17 +    // FIXME avoid I/O etc. on Swing thread
    6.18 +    val graph: Model.Graph =
    6.19 +      try {
    6.20 +        Platform.init_laf()
    6.21 +        Isabelle_System.init()
    6.22  
    6.23 -    val opt_xml: Option[XML.Tree] =
    6.24 -      try {
    6.25 -        Some(YXML.parse_body(
    6.26 -            Symbol.decode(io.Source.fromFile(args(0)).mkString)).head)
    6.27 -      } catch {
    6.28 -        case _ : ArrayIndexOutOfBoundsException => None
    6.29 -        case _ : java.io.FileNotFoundException => None
    6.30 +        args.toList match {
    6.31 +          case List(arg) =>
    6.32 +            Model.decode_graph(YXML.parse_body(File.read(Path.explode(arg))))
    6.33 +          case _ => error("Bad arguments:\n" + cat_lines(args))
    6.34 +        }
    6.35        }
    6.36 -    
    6.37 -    //Textfiles will still be valid and result in an empty frame
    6.38 -    //since they are valid to YXML.
    6.39 -    opt_xml match {
    6.40 -      case None =>
    6.41 -        println("No valid YXML-File given.\n" +
    6.42 -          "Usage: java -jar graphview.jar <yxmlfile>")
    6.43 -        System.exit(1)
    6.44 -      case Some(xml) =>
    6.45 -        val top = frame(xml)
    6.46 -        top.pack()
    6.47 -        top.visible = true
    6.48 -    }
    6.49 +      catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
    6.50  
    6.51 -    def frame(xml: XML.Tree): Window = new MainFrame {
    6.52 +    val top = new MainFrame {
    6.53        title = "Graphview"
    6.54        minimumSize = new Dimension(640, 480)
    6.55        preferredSize = new Dimension(800, 600)
    6.56 @@ -54,8 +40,11 @@
    6.57        contents = new BorderPanel {
    6.58          border = new EmptyBorder(5, 5, 5, 5)
    6.59  
    6.60 -        add(new Main_Panel(xml), BorderPanel.Position.Center)
    6.61 +        add(new Main_Panel(graph), BorderPanel.Position.Center)
    6.62        }
    6.63      }
    6.64 +
    6.65 +    top.pack()
    6.66 +    top.visible = true
    6.67    }
    6.68  }
    6.69 \ No newline at end of file
     7.1 --- a/src/Tools/Graphview/src/graph_xml.scala	Tue Sep 25 18:24:49 2012 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,74 +0,0 @@
     7.4 -/*  Title:      Tools/Graphview/src/graph_xml.scala
     7.5 -    Author:     Markus Kaiser, TU Muenchen
     7.6 -
     7.7 -XML to graph conversion.
     7.8 -*/
     7.9 -
    7.10 -package isabelle.graphview
    7.11 -
    7.12 -
    7.13 -import isabelle._
    7.14 -
    7.15 -
    7.16 -case class Locale(val axioms: List[XML.Body], val parameters: List[(String, XML.Body)])
    7.17 -
    7.18 -object Graph_XML
    7.19 -{
    7.20 -  type Entry = Option[Locale]
    7.21 -  type Nodes = List[(String, (Entry, List[String]))]
    7.22 -  
    7.23 -  def apply(xml: XML.Tree): Graph[String, Entry] = {
    7.24 -    val nodes : Nodes =
    7.25 -    {
    7.26 -      try {
    7.27 -        xml match {
    7.28 -          case XML.Elem(Markup("thy_deps", Nil), ts) => thy_deps(ts)
    7.29 -          case XML.Elem(Markup("locale_deps", Nil), ts) => locale_deps(ts)
    7.30 -          case _ => Nil
    7.31 -        }
    7.32 -      }
    7.33 -    }
    7.34 -
    7.35 -    // Add nodes
    7.36 -    val node_graph =
    7.37 -      (Graph.string[Entry] /: nodes) {
    7.38 -        case (graph, (key, (info, _))) => graph.new_node(key, info)
    7.39 -      }
    7.40 -    
    7.41 -    // Add edges
    7.42 -    (node_graph /: nodes) {
    7.43 -      case (graph, (from, (_, tos))) =>
    7.44 -        (graph /: tos) {
    7.45 -          (graph, to) => graph.add_edge(from, to)
    7.46 -        }
    7.47 -    }
    7.48 -  }
    7.49 -
    7.50 -  private def thy_deps(ts: XML.Body) : Nodes = {
    7.51 -    val strings : List[(String, List[String])] = {
    7.52 -      import XML.Decode._
    7.53 -      
    7.54 -      list(pair(string, list(string)))(ts)
    7.55 -    }
    7.56 -
    7.57 -    strings.map({case (key, tos) => (key, (None, tos))})
    7.58 -  }
    7.59 -
    7.60 -  private def locale_deps(ts: XML.Body) : Nodes = {
    7.61 -    // Identity functions return (potential) term-xmls
    7.62 -    val strings = {
    7.63 -      import XML.Decode._
    7.64 -      val node = pair(list(x=>x),pair(list(pair(string,x=>x)),list(list(x=>x))))
    7.65 -      val graph = list(pair(pair(string, node), list(string)))
    7.66 -      def symtab[A](f: T[A]) = list(pair(x=>x, f))
    7.67 -      val dependencies = symtab(symtab(list(list(x=>x))))
    7.68 -      pair(graph, dependencies)(ts)
    7.69 -    }
    7.70 -
    7.71 -    strings._1.map({
    7.72 -        case ((key, (axioms, (parameters, _))), tos) =>
    7.73 -          (key, (Some(Locale(axioms, parameters)), tos))
    7.74 -      }
    7.75 -    )
    7.76 -  }
    7.77 -}
     8.1 --- a/src/Tools/Graphview/src/layout_pendulum.scala	Tue Sep 25 18:24:49 2012 +0200
     8.2 +++ b/src/Tools/Graphview/src/layout_pendulum.scala	Tue Sep 25 20:28:47 2012 +0200
     8.3 @@ -12,26 +12,25 @@
     8.4  
     8.5  object Layout_Pendulum {
     8.6    type Key = String
     8.7 -  type Entry = Option[Locale]
     8.8    type Point = (Double, Double)
     8.9    type Coordinates = Map[Key, Point]
    8.10    type Level = List[Key]
    8.11    type Levels = List[Level]
    8.12    type Layout = (Coordinates, Map[(Key, Key), List[Point]])
    8.13 -  type Dummies = (Graph[Key, Entry], List[Key], Map[Key, Int])
    8.14 +  type Dummies = (Model.Graph, List[Key], Map[Key, Int])
    8.15    
    8.16    val x_distance = 350
    8.17    val y_distance = 350
    8.18    val pendulum_iterations = 10
    8.19    
    8.20 -  def apply(graph: Graph[Key, Entry]): Layout = {
    8.21 +  def apply(graph: Model.Graph): Layout = {
    8.22      if (graph.entries.isEmpty)
    8.23        (Map[Key, Point](), Map[(Key, Key), List[Point]]())
    8.24      else {
    8.25        val (dummy_graph, dummies, dummy_levels) = {
    8.26          val initial_levels = level_map(graph)
    8.27  
    8.28 -        def add_dummies(graph: Graph[Key, Entry], from: Key, to: Key,
    8.29 +        def add_dummies(graph: Model.Graph, from: Key, to: Key,
    8.30                          levels: Map[Key, Int]): Dummies = {
    8.31            val ds = 
    8.32              ((levels(from) + 1) until levels(to))
    8.33 @@ -44,7 +43,7 @@
    8.34  
    8.35            val next_nodes = 
    8.36              (graph /: ds) {
    8.37 -              (graph, d) => graph.new_node(d, None)
    8.38 +              (graph, d) => graph.new_node(d, Model.empty_info)
    8.39              }
    8.40  
    8.41            val next =
    8.42 @@ -89,7 +88,7 @@
    8.43      }
    8.44    }
    8.45    
    8.46 -  def level_map(graph: Graph[Key, Entry]): Map[Key, Int] = 
    8.47 +  def level_map(graph: Model.Graph): Map[Key, Int] = 
    8.48      (Map[Key, Int]() /: graph.topological_order){
    8.49        (levels, key) => {
    8.50          val pred_levels = graph.imm_preds(key).map(levels(_)) + (-1)
    8.51 @@ -108,7 +107,7 @@
    8.52          }
    8.53      }.map(_._2)
    8.54    
    8.55 -  def count_crossings(graph: Graph[Key, Entry], levels: Levels): Int = {
    8.56 +  def count_crossings(graph: Model.Graph, levels: Levels): Int = {
    8.57      def in_level(ls: Levels): Int = ls match {
    8.58        case List(top, bot) =>
    8.59          top.zipWithIndex.map{
    8.60 @@ -131,7 +130,7 @@
    8.61      levels.sliding(2).map(in_level).sum
    8.62    }
    8.63    
    8.64 -  def minimize_crossings(graph: Graph[Key, Entry], levels: Levels): Levels = {
    8.65 +  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels = {
    8.66      def resort_level(parent: Level, child: Level, top_down: Boolean): Level = 
    8.67        child.map(k => {
    8.68            val ps = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
    8.69 @@ -167,7 +166,7 @@
    8.70    }
    8.71    
    8.72    def initial_coordinates(levels: Levels): Coordinates =
    8.73 -    (Map[Key, Point]() /: levels.reverse.zipWithIndex){
    8.74 +    (Map[Key, Point]() /: levels.zipWithIndex){
    8.75        case (coords, (level, yi)) =>
    8.76          (coords /: level.zipWithIndex) {
    8.77            case (coords, (node, xi)) => 
    8.78 @@ -175,7 +174,7 @@
    8.79          }
    8.80      }
    8.81    
    8.82 -  def pendulum(graph: Graph[Key, Entry],
    8.83 +  def pendulum(graph: Model.Graph,
    8.84                 levels: Levels, coords: Map[Key, Point]): Coordinates =
    8.85    {
    8.86      type Regions = List[List[Region]]
    8.87 @@ -260,7 +259,7 @@
    8.88      }._2
    8.89    }
    8.90    
    8.91 -  protected class Region(val graph: Graph[Key, Entry], node: Key) {
    8.92 +  protected class Region(val graph: Model.Graph, node: Key) {
    8.93      var nodes: List[Key] = List(node)
    8.94         
    8.95      def left(coords: Coordinates): Double =
     9.1 --- a/src/Tools/Graphview/src/main_panel.scala	Tue Sep 25 18:24:49 2012 +0200
     9.2 +++ b/src/Tools/Graphview/src/main_panel.scala	Tue Sep 25 20:28:47 2012 +0200
     9.3 @@ -18,12 +18,12 @@
     9.4  import java.io.File
     9.5  
     9.6  
     9.7 -class Main_Panel(xml: XML.Tree) extends BorderPanel
     9.8 +class Main_Panel(graph: Model.Graph) extends BorderPanel
     9.9  {
    9.10    focusable = true
    9.11    requestFocus()
    9.12    
    9.13 -  val model = new Model(Graph_XML(xml))
    9.14 +  val model = new Model(graph)
    9.15    val visualizer = new Visualizer(model)
    9.16    val graph_panel = new Graph_Panel(visualizer)
    9.17    
    10.1 --- a/src/Tools/Graphview/src/model.scala	Tue Sep 25 18:24:49 2012 +0200
    10.2 +++ b/src/Tools/Graphview/src/model.scala	Tue Sep 25 20:28:47 2012 +0200
    10.3 @@ -14,8 +14,8 @@
    10.4  import scala.actors.Actor._
    10.5  
    10.6  
    10.7 -class Mutator_Container(val available: List[Mutator[String, Option[Locale]]]) {
    10.8 -    type Mutator_Markup = (Boolean, Color, Mutator[String, Option[Locale]])
    10.9 +class Mutator_Container(val available: List[Mutator]) {
   10.10 +    type Mutator_Markup = (Boolean, Color, Mutator)
   10.11      
   10.12      val events = new Event_Bus[Mutator_Event.Message]
   10.13      
   10.14 @@ -34,7 +34,33 @@
   10.15      }
   10.16  }
   10.17  
   10.18 -class Model(private val graph: Graph[String, Option[Locale]]) {  
   10.19 +
   10.20 +object Model
   10.21 +{
   10.22 +  /* node info */
   10.23 +
   10.24 +  sealed case class Info(name: String, content: XML.Body)
   10.25 +
   10.26 +  val empty_info: Info = Info("", Nil)
   10.27 +
   10.28 +  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
   10.29 +  {
   10.30 +    import XML.Decode._
   10.31 +
   10.32 +    val (name, content) = pair(string, x => x)(body)
   10.33 +    Info(name, content)
   10.34 +  }
   10.35 +
   10.36 +
   10.37 +  /* graph */
   10.38 +
   10.39 +  type Graph = isabelle.Graph[String, Info]
   10.40 +
   10.41 +  val decode_graph: XML.Decode.T[Graph] =
   10.42 +    isabelle.Graph.decode(XML.Decode.string, decode_info)
   10.43 +}
   10.44 +
   10.45 +class Model(private val graph: Model.Graph) {  
   10.46    val Mutators = new Mutator_Container(
   10.47      List(
   10.48        Node_Expression(".*", false, false, false),
   10.49 @@ -57,7 +83,7 @@
   10.50      current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
   10.51    
   10.52    def complete = graph
   10.53 -  def current: Graph[String, Option[Locale]] =
   10.54 +  def current: Model.Graph =
   10.55        (graph /: Mutators()) {
   10.56          case (g, (enabled, _, mutator)) => {
   10.57            if (!enabled) g
    11.1 --- a/src/Tools/Graphview/src/mutator.scala	Tue Sep 25 18:24:49 2012 +0200
    11.2 +++ b/src/Tools/Graphview/src/mutator.scala	Tue Sep 25 20:28:47 2012 +0200
    11.3 @@ -13,60 +13,57 @@
    11.4  import scala.collection.immutable.SortedSet
    11.5  
    11.6  
    11.7 -trait Mutator[Key, Entry]
    11.8 +trait Mutator
    11.9  {
   11.10    val name: String
   11.11    val description: String
   11.12 -  def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry]
   11.13 +  def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
   11.14  
   11.15    override def toString() = name
   11.16  }
   11.17  
   11.18 -trait Filter[Key, Entry]
   11.19 -extends Mutator[Key, Entry]
   11.20 +trait Filter extends Mutator
   11.21  {
   11.22 -  def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]) = filter(sub)
   11.23 -  def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry]
   11.24 +  def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
   11.25 +  def filter(sub: Model.Graph) : Model.Graph
   11.26  }
   11.27  
   11.28  object Mutators {
   11.29 -  type Key = String
   11.30 -  type Entry = Option[Locale]
   11.31 -  type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
   11.32 +  type Mutator_Markup = (Boolean, Color, Mutator)
   11.33    
   11.34    val Enabled = true
   11.35    val Disabled = false
   11.36    
   11.37 -  def create(m: Mutator[Key, Entry]): Mutator_Markup =
   11.38 +  def create(m: Mutator): Mutator_Markup =
   11.39      (Mutators.Enabled, Parameters.Colors.next, m)
   11.40  
   11.41 -  class Graph_Filter[Key, Entry](val name: String, val description: String,
   11.42 -    pred: Graph[Key, Entry] => Graph[Key, Entry])
   11.43 -  extends Filter[Key, Entry]
   11.44 +  class Graph_Filter(val name: String, val description: String,
   11.45 +    pred: Model.Graph => Model.Graph)
   11.46 +  extends Filter
   11.47    {
   11.48 -    def filter(sub: Graph[Key, Entry]) : Graph[Key, Entry] = pred(sub)
   11.49 +    def filter(sub: Model.Graph) : Model.Graph = pred(sub)
   11.50    }
   11.51  
   11.52 -  class Graph_Mutator[Key, Entry](val name: String, val description: String,
   11.53 -    pred: (Graph[Key, Entry], Graph[Key, Entry]) => Graph[Key, Entry])
   11.54 -  extends Mutator[Key, Entry]
   11.55 +  class Graph_Mutator(val name: String, val description: String,
   11.56 +    pred: (Model.Graph, Model.Graph) => Model.Graph)
   11.57 +  extends Mutator
   11.58    {
   11.59 -    def mutate(complete: Graph[Key, Entry], sub: Graph[Key, Entry]): Graph[Key, Entry] =
   11.60 +    def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph =
   11.61            pred(complete, sub)
   11.62    }
   11.63  
   11.64 -  class Node_Filter[Key, Entry](name: String, description: String,
   11.65 -    pred: (Graph[Key, Entry], Key) => Boolean)
   11.66 -    extends Graph_Filter[Key, Entry] (
   11.67 +  class Node_Filter(name: String, description: String,
   11.68 +    pred: (Model.Graph, String) => Boolean)
   11.69 +    extends Graph_Filter (
   11.70  
   11.71      name,
   11.72      description,
   11.73      g => g.restrict(pred(g, _))
   11.74    )
   11.75  
   11.76 -  class Edge_Filter[Key, Entry](name: String, description: String,
   11.77 -    pred: (Graph[Key, Entry], Key, Key) => Boolean)
   11.78 -    extends Graph_Filter[Key, Entry] (
   11.79 +  class Edge_Filter(name: String, description: String,
   11.80 +    pred: (Model.Graph, String, String) => Boolean)
   11.81 +    extends Graph_Filter (
   11.82  
   11.83      name,
   11.84      description,
   11.85 @@ -80,10 +77,10 @@
   11.86      }
   11.87    )
   11.88  
   11.89 -  class Node_Family_Filter[Key, Entry](name: String, description: String,
   11.90 +  class Node_Family_Filter(name: String, description: String,
   11.91        reverse: Boolean, parents: Boolean, children: Boolean,
   11.92 -      pred: (Graph[Key, Entry], Key) => Boolean)
   11.93 -    extends Node_Filter[Key, Entry](
   11.94 +      pred: (Model.Graph, String) => Boolean)
   11.95 +    extends Node_Filter(
   11.96  
   11.97      name,
   11.98      description,
   11.99 @@ -95,7 +92,7 @@
  11.100    )  
  11.101    
  11.102    case class Identity()
  11.103 -    extends Graph_Filter[Key, Entry](
  11.104 +    extends Graph_Filter(
  11.105  
  11.106      "Identity",
  11.107      "Does not change the graph.",
  11.108 @@ -104,7 +101,7 @@
  11.109  
  11.110    case class Node_Expression(regex: String,
  11.111      reverse: Boolean, parents: Boolean, children: Boolean)
  11.112 -    extends Node_Family_Filter[Key, Entry](
  11.113 +    extends Node_Family_Filter(
  11.114  
  11.115      "Filter by Name",
  11.116      "Only shows or hides all nodes with any family member's name matching " +
  11.117 @@ -117,7 +114,7 @@
  11.118  
  11.119    case class Node_List(list: List[String],
  11.120      reverse: Boolean, parents: Boolean, children: Boolean)
  11.121 -    extends Node_Family_Filter[Key, Entry](
  11.122 +    extends Node_Family_Filter(
  11.123  
  11.124      "Filter by Name List",
  11.125      "Only shows or hides all nodes with any family member's name matching " +
  11.126 @@ -129,7 +126,7 @@
  11.127    )
  11.128  
  11.129    case class Edge_Endpoints(source: String, dest: String)
  11.130 -    extends Edge_Filter[Key, Entry](
  11.131 +    extends Edge_Filter(
  11.132  
  11.133      "Hide edge",
  11.134      "Hides the edge whose endpoints match strings.",
  11.135 @@ -137,7 +134,7 @@
  11.136    )
  11.137  
  11.138    case class Edge_Transitive()
  11.139 -    extends Edge_Filter[Key, Entry](
  11.140 +    extends Edge_Filter(
  11.141  
  11.142      "Hide transitive edges",
  11.143      "Hides all transitive edges.",
  11.144 @@ -147,8 +144,8 @@
  11.145      }
  11.146    )
  11.147  
  11.148 -  private def add_node_group(from: Graph[Key, Entry], to: Graph[Key, Entry],
  11.149 -    keys: List[Key]) = {
  11.150 +  private def add_node_group(from: Model.Graph, to: Model.Graph,
  11.151 +    keys: List[String]) = {
  11.152      
  11.153      // Add Nodes
  11.154      val with_nodes = 
  11.155 @@ -159,7 +156,7 @@
  11.156      // Add Edges
  11.157      (with_nodes /: keys) {
  11.158        (gv, key) => {
  11.159 -        def add_edges(g: Graph[Key, Entry], keys: SortedSet[Key], succs: Boolean) =
  11.160 +        def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
  11.161            (g /: keys) {
  11.162              (graph, end) => {
  11.163                if (!graph.keys.contains(end)) graph
  11.164 @@ -180,7 +177,7 @@
  11.165    }  
  11.166    
  11.167    case class Add_Node_Expression(regex: String)
  11.168 -    extends Graph_Mutator[Key, Entry](
  11.169 +    extends Graph_Mutator(
  11.170  
  11.171      "Add by name",
  11.172      "Adds every node whose name matches the regex. " +
  11.173 @@ -193,7 +190,7 @@
  11.174    )
  11.175    
  11.176    case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
  11.177 -    extends Graph_Mutator[Key, Entry](
  11.178 +    extends Graph_Mutator(
  11.179  
  11.180      "Add transitive closure",
  11.181      "Adds all family members of all current nodes.",
    12.1 --- a/src/Tools/Graphview/src/mutator_dialog.scala	Tue Sep 25 18:24:49 2012 +0200
    12.2 +++ b/src/Tools/Graphview/src/mutator_dialog.scala	Tue Sep 25 20:28:47 2012 +0200
    12.3 @@ -25,9 +25,7 @@
    12.4    reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
    12.5  extends Dialog
    12.6  {
    12.7 -  type Key = String
    12.8 -  type Entry = Option[Locale]
    12.9 -  type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
   12.10 +  type Mutator_Markup = (Boolean, Color, Mutator)
   12.11    
   12.12    title = caption
   12.13    
   12.14 @@ -112,7 +110,7 @@
   12.15  
   12.16    val filterPanel = new BoxPanel(Orientation.Vertical) {}
   12.17  
   12.18 -  private val mutatorBox = new ComboBox[Mutator[Key, Entry]](container.available)
   12.19 +  private val mutatorBox = new ComboBox[Mutator](container.available)
   12.20  
   12.21    private val addButton: Button = new Button{
   12.22      action = Action("Add") {
    13.1 --- a/src/Tools/Graphview/src/mutator_event.scala	Tue Sep 25 18:24:49 2012 +0200
    13.2 +++ b/src/Tools/Graphview/src/mutator_event.scala	Tue Sep 25 20:28:47 2012 +0200
    13.3 @@ -12,9 +12,7 @@
    13.4  
    13.5  object Mutator_Event
    13.6  {
    13.7 -  type Key = String
    13.8 -  type Entry = Option[Locale]
    13.9 -  type Mutator_Markup = (Boolean, Color, Mutator[Key, Entry])
   13.10 +  type Mutator_Markup = (Boolean, Color, Mutator)
   13.11    
   13.12    sealed abstract class Message
   13.13    case class Add(m: Mutator_Markup) extends Message
    14.1 --- a/src/Tools/Graphview/src/tooltips.scala	Tue Sep 25 18:24:49 2012 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,93 +0,0 @@
    14.4 -/*  Title:      Tools/Graphview/src/graph_components.scala
    14.5 -    Author:     Markus Kaiser, TU Muenchen
    14.6 -
    14.7 -Tooltip generation for graph components.
    14.8 -*/
    14.9 -
   14.10 -package isabelle.graphview
   14.11 -
   14.12 -
   14.13 -import isabelle._
   14.14 -import java.awt.FontMetrics
   14.15 -
   14.16 -
   14.17 -object Tooltips {
   14.18 -  // taken (and modified slightly) from html_panel.scala
   14.19 -  private def make_HTML(term: XML.Body, fm: FontMetrics): String = {
   14.20 -    XML.string_of_body ( term.flatMap(div =>
   14.21 -              Pretty.formatted(List(div), 76, Pretty.font_metric(fm))
   14.22 -                .map( t=>
   14.23 -                  HTML.spans(t, false))
   14.24 -      ).head
   14.25 -    )
   14.26 -  }  
   14.27 -  
   14.28 -  def locale(key: String, model: Model, fm: FontMetrics): String = {
   14.29 -    val locale = model.complete.get_node(key)
   14.30 -    val parsed_name = key.split('.')
   14.31 -    
   14.32 -    if (!locale.isDefined) {
   14.33 -      """|<html>
   14.34 -        |<body style="margin: 3px">
   14.35 -        |%s
   14.36 -        |</body>
   14.37 -        |""".stripMargin.format(parsed_name.reduceLeft("%s<br>%s".format(_,_)))      
   14.38 -    } else {
   14.39 -      val Some(Locale(axioms, parameters)) = locale
   14.40 -
   14.41 -      val parms = {
   14.42 -        if (parameters.size > 0) {
   14.43 -          """|
   14.44 -            |<p>Parameters:</p>
   14.45 -            |<ul>
   14.46 -            |%s
   14.47 -            |</ul>
   14.48 -            |""".stripMargin.format(parameters.map(
   14.49 -                                        y => "<li>%s :: %s</li>".format(
   14.50 -                                                y._1,
   14.51 -                                                make_HTML(y._2, fm))
   14.52 -                                    ).reduceLeft(_+_))
   14.53 -        } else ""
   14.54 -      }
   14.55 -      val axms = {
   14.56 -        if (axioms.size > 0) {
   14.57 -          """|
   14.58 -            |<p>Axioms:</p>
   14.59 -            |<ul>
   14.60 -            |%s
   14.61 -            |</ul>
   14.62 -            |""".stripMargin.format(axioms.map(
   14.63 -                                      y => "<li>%s</li>".format(
   14.64 -                                                make_HTML(y, fm))
   14.65 -                                    ).reduceLeft(_+_))
   14.66 -        } else ""
   14.67 -      }
   14.68 -
   14.69 -      """|<html>
   14.70 -        |<style type="text/css">
   14.71 -        |/* isabelle style */
   14.72 -        |%s
   14.73 -        |
   14.74 -        |/* tooltip specific style */
   14.75 -        |
   14.76 -        |body  { margin: 10px; font-size: 12px; }
   14.77 -        |hr    { margin: 12px 0 0 0; height: 2px; }
   14.78 -        |p     { margin: 6px 0 2px 0; }
   14.79 -        |ul    { margin: 0 0 0 4px; list-style-type: none; }
   14.80 -        |li    { margin: 0 0 4px; }
   14.81 -        |
   14.82 -        |</style>
   14.83 -        |<body>
   14.84 -        |<center>%s</center>
   14.85 -        |<hr>
   14.86 -        |%s
   14.87 -        |%s
   14.88 -        |</body>
   14.89 -        |</html>
   14.90 -        |""".stripMargin.format(Parameters.tooltip_css,
   14.91 -                                parsed_name.reduceLeft("%s<br>%s".format(_,_)),
   14.92 -                                axms,
   14.93 -                                parms).replace("&apos;", "'")
   14.94 -    }  
   14.95 -  }
   14.96 -}
   14.97 \ No newline at end of file
    15.1 --- a/src/Tools/Graphview/src/visualizer.scala	Tue Sep 25 18:24:49 2012 +0200
    15.2 +++ b/src/Tools/Graphview/src/visualizer.scala	Tue Sep 25 20:28:47 2012 +0200
    15.3 @@ -6,6 +6,7 @@
    15.4  
    15.5  package isabelle.graphview
    15.6  
    15.7 +import isabelle._
    15.8  
    15.9  import java.awt.{RenderingHints, Graphics2D}
   15.10  
   15.11 @@ -142,8 +143,14 @@
   15.12    
   15.13    object Tooltip {
   15.14      import java.awt.FontMetrics
   15.15 -    
   15.16 -    def apply(l: String, fm: FontMetrics) = Tooltips.locale(l, model, fm)
   15.17 +
   15.18 +    def apply(l: String, fm: FontMetrics): String =
   15.19 +    {
   15.20 +      val info = model.complete.get_node(l)
   15.21 +      XML.string_of_body(
   15.22 +        Pretty.formatted(info.content, 76, Pretty.font_metric(fm))
   15.23 +          .map(t => XML.Elem(Markup(HTML.PRE, Nil), HTML.spans(t, false))))
   15.24 +    }
   15.25    }
   15.26    
   15.27    object Font {