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;
--- 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;
--- 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;
--- 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)
--- 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"
--- 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"
--- 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 <yxmlfile>")
- 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
--- 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))
- }
- )
- }
-}
--- 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 =
--- 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)
--- 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
--- 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.",
--- 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") {
--- 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
--- 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) {
- """|<html>
- |<body style="margin: 3px">
- |%s
- |</body>
- |""".stripMargin.format(parsed_name.reduceLeft("%s<br>%s".format(_,_)))
- } else {
- val Some(Locale(axioms, parameters)) = locale
-
- val parms = {
- if (parameters.size > 0) {
- """|
- |<p>Parameters:</p>
- |<ul>
- |%s
- |</ul>
- |""".stripMargin.format(parameters.map(
- y => "<li>%s :: %s</li>".format(
- y._1,
- make_HTML(y._2, fm))
- ).reduceLeft(_+_))
- } else ""
- }
- val axms = {
- if (axioms.size > 0) {
- """|
- |<p>Axioms:</p>
- |<ul>
- |%s
- |</ul>
- |""".stripMargin.format(axioms.map(
- y => "<li>%s</li>".format(
- make_HTML(y, fm))
- ).reduceLeft(_+_))
- } else ""
- }
-
- """|<html>
- |<style type="text/css">
- |/* isabelle style */
- |%s
- |
- |/* tooltip specific style */
- |
- |body { margin: 10px; font-size: 12px; }
- |hr { margin: 12px 0 0 0; height: 2px; }
- |p { margin: 6px 0 2px 0; }
- |ul { margin: 0 0 0 4px; list-style-type: none; }
- |li { margin: 0 0 4px; }
- |
- |</style>
- |<body>
- |<center>%s</center>
- |<hr>
- |%s
- |%s
- |</body>
- |</html>
- |""".stripMargin.format(Parameters.tooltip_css,
- parsed_name.reduceLeft("%s<br>%s".format(_,_)),
- axms,
- parms).replace("'", "'")
- }
- }
-}
\ No newline at end of file
--- 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 {