--- a/etc/components Wed Sep 26 10:41:36 2012 +0200
+++ b/etc/components Wed Sep 26 15:04:15 2012 +0200
@@ -1,5 +1,6 @@
src/Tools/Code
src/Tools/jEdit
+src/Tools/Graphview
src/Tools/WWW_Find
src/HOL/Mirabelle
src/HOL/Mutabelle
--- a/etc/isar-keywords-ZF.el Wed Sep 26 10:41:36 2012 +0200
+++ b/etc/isar-keywords-ZF.el Wed Sep 26 15:04:15 2012 +0200
@@ -96,6 +96,7 @@
"linear_undo"
"local_setup"
"locale"
+ "locale_deps"
"method_setup"
"moreover"
"next"
@@ -286,6 +287,7 @@
"full_prf"
"header"
"help"
+ "locale_deps"
"pr"
"pretty_setmargin"
"prf"
--- a/etc/isar-keywords.el Wed Sep 26 10:41:36 2012 +0200
+++ b/etc/isar-keywords.el Wed Sep 26 15:04:15 2012 +0200
@@ -139,6 +139,7 @@
"linear_undo"
"local_setup"
"locale"
+ "locale_deps"
"method_setup"
"moreover"
"next"
@@ -388,6 +389,7 @@
"full_prf"
"header"
"help"
+ "locale_deps"
"nitpick"
"pr"
"pretty_setmargin"
--- a/lib/Tools/browser Wed Sep 26 10:41:36 2012 +0200
+++ b/lib/Tools/browser Wed Sep 26 15:04:15 2012 +0200
@@ -72,9 +72,9 @@
if [ -n "$GRAPHFILE" ]; then
PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$"$(basename "$GRAPHFILE")
if [ -n "$CLEAN" ]; then
- mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $FILE"
+ mv -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot move file: $GRAPHFILE"
else
- cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $FILE"
+ cp -f "$GRAPHFILE" "$PRIVATE_FILE" || fail "Cannot copy file: $GRAPHFILE"
fi
PDF=""
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Sep 26 15:04:15 2012 +0200
@@ -315,8 +315,8 @@
|> commas;
val prgr = map (fn (consts, constss) =>
{ name = namify consts, ID = namify consts, dir = "", unfold = true,
- path = "", parents = map namify constss }) conn;
- in Present.display_graph prgr end;
+ path = "", parents = map namify constss, content = [] }) conn;
+ in Graph_Display.display_graph prgr end;
end;
--- a/src/Pure/General/graph.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/General/graph.ML Wed Sep 26 15:04:15 2012 +0200
@@ -22,7 +22,6 @@
val empty: 'a T
val is_empty: 'a T -> bool
val keys: 'a T -> key list
- val dest: 'a T -> (key * key list) list
val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*)
@@ -48,6 +47,8 @@
val add_edge: key * key -> 'a T -> 'a T (*exception UNDEF*)
val del_edge: key * key -> 'a T -> 'a T (*exception UNDEF*)
val restrict: (key -> bool) -> 'a T -> 'a T
+ val dest: 'a T -> ((key * 'a) * key list) list
+ val make: ((key * 'a) * key list) list -> 'a T (*exception DUP | UNDEF*)
val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
'a T * 'a T -> 'a T (*exception DUP*)
@@ -61,6 +62,8 @@
val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T (*exception CYCLES*)
exception DEP of key * key
val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list (*exception DEP*)
+ val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
+ val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
end;
functor Graph(Key: KEY): GRAPH =
@@ -108,7 +111,6 @@
val empty = Graph Table.empty;
fun is_empty (Graph tab) = Table.is_empty tab;
fun keys (Graph tab) = Table.keys tab;
-fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
fun get_first f (Graph tab) = Table.get_first f tab;
fun fold_graph f (Graph tab) = Table.fold f tab;
@@ -215,12 +217,22 @@
else G;
fun diff_edges G1 G2 =
- flat (dest G1 |> map (fn (x, ys) => ys |> map_filter (fn y =>
- if is_edge G2 (x, y) then NONE else SOME (x, y))));
+ fold_graph (fn (x, (_, (_, succs))) =>
+ Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
fun edges G = diff_edges G empty;
+(* dest and make *)
+
+fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
+
+fun make entries =
+ empty
+ |> fold (new_node o fst) entries
+ |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;
+
+
(* join and merge *)
fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
@@ -312,6 +324,19 @@
in map (the o Table.lookup results) xs end;
+(* XML data representation *)
+
+fun encode key info G =
+ dest G |>
+ let open XML.Encode
+ in list (pair (pair key info) (list key)) end;
+
+fun decode key info body =
+ body |>
+ let open XML.Decode
+ in list (pair (pair key info) (list key)) end |> make;
+
+
(*final declarations of this structure!*)
val map = map_nodes;
val fold = fold_graph;
--- a/src/Pure/General/graph.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/General/graph.scala Wed Sep 26 15:04:15 2012 +0200
@@ -21,9 +21,35 @@
def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
new Graph[Key, A](SortedMap.empty(ord))
+ def make[Key, A](entries: List[((Key, A), List[Key])])(implicit ord: Ordering[Key])
+ : Graph[Key, A] =
+ {
+ val graph1 =
+ (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
+ val graph2 =
+ (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
+ graph2
+ }
+
def string[A]: Graph[String, A] = empty(Ordering.String)
def int[A]: Graph[Int, A] = empty(Ordering.Int)
def long[A]: Graph[Long, A] = empty(Ordering.Long)
+
+
+ /* XML data representation */
+
+ def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
+ ((graph: Graph[Key, A]) => {
+ import XML.Encode._
+ list(pair(pair(key, info), list(key)))(graph.dest)
+ })
+
+ def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(implicit ord: Ordering[Key])
+ : XML.Decode.T[Graph[Key, A]] =
+ ((body: XML.Body) => {
+ import XML.Decode._
+ make(list(pair(pair(key, info), list(key)))(body))(ord)
+ })
}
@@ -44,11 +70,12 @@
def entries: Iterator[(Key, Entry)] = rep.iterator
def keys: Iterator[Key] = entries.map(_._1)
- def dest: List[(Key, List[Key])] =
- (for ((x, (_, (_, succs))) <- entries) yield (x, succs.toList)).toList
+ def dest: List[((Key, A), List[Key])] =
+ (for ((x, (i, (_, succs))) <- entries) yield ((x, i), succs.toList)).toList
override def toString: String =
- dest.map(p => p._1.toString + " -> " + p._2.map(_.toString).mkString("{", ", ", "}"))
+ dest.map({ case ((x, _), ys) =>
+ x.toString + " -> " + ys.iterator.map(_.toString).mkString("{", ", ", "}") })
.mkString("Graph(", ", ", ")")
private def get_entry(x: Key): Entry =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graph_display.ML Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,80 @@
+(* Title: Pure/General/graph_display.ML
+ Author: Makarius
+
+Generic graph display, with browser and graphview backends.
+*)
+
+signature GRAPH_DISPLAY =
+sig
+ type node =
+ {name: string, ID: string, dir: string, unfold: bool,
+ path: string, parents: string list, content: Pretty.T list}
+ type graph = node list
+ val write_graph_browser: Path.T -> graph -> unit
+ val browserN: string
+ val graphviewN: string
+ val graphview_reportN: string
+ val display_graph: graph -> unit
+end;
+
+structure Graph_Display: GRAPH_DISPLAY =
+struct
+
+(* external graph representation *)
+
+type node =
+ {name: string, ID: string, dir: string, unfold: bool,
+ path: string, parents: string list, content: Pretty.T list};
+
+type graph = node list;
+
+
+(* print modes *)
+
+val browserN = "browser";
+val graphviewN = "graphview";
+val graphview_reportN = "graphview_report";
+
+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 =
+ if print_mode_active graphview_reportN then
+ (Output.report
+ (YXML.string_of (XML.Elem ((Isabelle_Markup.graphviewN, []), encode_graphview graph)));
+ writeln "(see graphview)")
+ else
+ 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 path graph;
+ val _ = Isabelle_System.isabelle_tool tool ("-c " ^ File.shell_path path ^ " &");
+ in () end;
+
+end;
+
--- a/src/Pure/General/pretty.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/General/pretty.ML Wed Sep 26 15:04:15 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/Isar/isar_cmd.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Sep 26 15:04:15 2012 +0200
@@ -60,8 +60,9 @@
val print_trans_rules: Toplevel.transition -> Toplevel.transition
val print_methods: Toplevel.transition -> Toplevel.transition
val print_antiquotations: Toplevel.transition -> Toplevel.transition
+ val thy_deps: Toplevel.transition -> Toplevel.transition
+ val locale_deps: Toplevel.transition -> Toplevel.transition
val class_deps: Toplevel.transition -> Toplevel.transition
- val thy_deps: Toplevel.transition -> Toplevel.transition
val thm_deps: (Facts.ref * Attrib.src list) list -> Toplevel.transition -> Toplevel.transition
val unused_thms: (string list * string list option) option ->
Toplevel.transition -> Toplevel.transition
@@ -403,8 +404,19 @@
val parents = map Context.theory_name (Theory.parents_of node);
val session = Present.session_name node;
val unfold = (session = thy_session);
- in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
- in Present.display_graph gr end);
+ in
+ {name = name, ID = name, parents = parents, dir = session,
+ unfold = unfold, path = "", content = []}
+ end);
+ in Graph_Display.display_graph gr end);
+
+val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
+ let
+ val thy = Toplevel.theory_of state;
+ val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
+ {name = Locale.extern thy name, ID = name, parents = parents,
+ dir = "", unfold = true, path = "", content = [body]});
+ in Graph_Display.display_graph gr end);
val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
let
@@ -413,11 +425,11 @@
val classes = Sorts.classes_of algebra;
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
- dir = "", unfold = true, path = ""});
+ dir = "", unfold = true, path = "", content = []});
val gr =
Graph.fold (cons o entry) classes []
|> sort (int_ord o pairself #1) |> map #2;
- in Present.display_graph gr end);
+ in Graph_Display.display_graph gr end);
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
Thm_Deps.thm_deps (Toplevel.theory_of state)
--- a/src/Pure/Isar/isar_syn.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Isar/isar_syn.ML Wed Sep 26 15:04:15 2012 +0200
@@ -858,6 +858,10 @@
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
val _ =
+ Outer_Syntax.improper_command @{command_spec "locale_deps"} "visualize locale dependencies"
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.locale_deps));
+
+val _ =
Outer_Syntax.improper_command @{command_spec "class_deps"} "visualize class dependencies"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
--- a/src/Pure/Isar/locale.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Isar/locale.ML Wed Sep 26 15:04:15 2012 +0200
@@ -76,14 +76,11 @@
morphism -> theory -> theory
(* Diagnostic *)
- val all_locales: theory -> string list
val print_locales: theory -> unit
val print_locale: theory -> bool -> xstring * Position.T -> unit
val print_registrations: Proof.context -> xstring * Position.T -> unit
val print_dependencies: Proof.context -> bool -> morphism -> (string * morphism) list -> unit
- val locale_deps: theory ->
- {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
- * term list list Symtab.table Symtab.table
+ val pretty_locale_deps: theory -> {name: string, parents: string list, body: Pretty.T} list
end;
structure Locale: LOCALE =
@@ -610,16 +607,13 @@
(*** diagnostic commands and interfaces ***)
-val all_locales = Symtab.keys o snd o Locales.get;
-
fun print_locales thy =
Pretty.strs ("locales:" ::
map #1 (Name_Space.extern_table (Proof_Context.init_global thy) (Locales.get thy)))
|> Pretty.writeln;
-fun print_locale thy show_facts raw_name =
+fun pretty_locale thy show_facts name =
let
- val name = check thy raw_name;
val ctxt = init name thy;
fun cons_elem (elem as Notes _) = show_facts ? cons elem
| cons_elem elem = cons elem;
@@ -627,10 +621,14 @@
activate_all name thy cons_elem (K (Element.transfer_morphism thy)) (empty_idents, [])
|> snd |> rev;
in
- Pretty.big_list "locale elements:" (map (Pretty.chunks o Element.pretty_ctxt ctxt) elems)
- |> Pretty.writeln
+ Pretty.block
+ (Pretty.command "locale" :: Pretty.brk 1 :: Pretty.str (extern thy name) ::
+ maps (fn elem => [Pretty.fbrk, Pretty.chunks (Element.pretty_ctxt ctxt elem)]) elems)
end;
+fun print_locale thy show_facts raw_name =
+ Pretty.writeln (pretty_locale thy show_facts (check thy raw_name));
+
fun print_registrations ctxt raw_name =
let
val thy = Proof_Context.theory_of ctxt;
@@ -651,34 +649,12 @@
| deps => Pretty.big_list "dependencies:" (map (pretty_reg ctxt) (rev deps)))
end |> Pretty.writeln;
-fun locale_deps thy =
+fun pretty_locale_deps thy =
let
- val names = all_locales thy;
- fun add_locale_node name =
- let
- val params = params_of thy name;
- val axioms =
- these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
- val registrations =
- map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
- in
- Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
- end;
- fun add_locale_deps name =
- let
- val dependencies =
- map (apsnd (instance_of thy name o op $>) o fst) (dependencies_of thy name);
- in
- fold (fn (super, ts) => fn (gr, deps) =>
- (gr |> Graph.add_edge (super, name),
- deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
- dependencies
- end;
- in
- Graph.empty
- |> fold add_locale_node names
- |> rpair Symtab.empty
- |> fold add_locale_deps names
- end;
+ fun make_node name =
+ {name = name,
+ parents = map (fst o fst) (dependencies_of thy name),
+ body = pretty_locale thy false name};
+ in map make_node (Symtab.keys (#2 (Locales.get thy))) end;
end;
--- a/src/Pure/Isar/outer_syntax.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Sep 26 15:04:15 2012 +0200
@@ -275,7 +275,7 @@
fun cmts (t1 :: t2 :: toks) =
if Token.keyword_with (fn s => s = "--") t1 then t2 :: cmts toks
else cmts (t2 :: toks)
- | cmts toks = [];
+ | cmts _ = [];
in
--- a/src/Pure/PIDE/isabelle_markup.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.ML Wed Sep 26 15:04:15 2012 +0200
@@ -100,6 +100,7 @@
val reportN: string val report: Markup.T
val no_reportN: string val no_report: Markup.T
val badN: string val bad: Markup.T
+ val graphviewN: string
val functionN: string
val assign_execs: Properties.T
val removed_versions: Properties.T
@@ -296,6 +297,8 @@
val (badN, bad) = markup_elem "bad";
+val graphviewN = "graphview";
+
(* protocol message functions *)
--- a/src/Pure/PIDE/isabelle_markup.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Wed Sep 26 15:04:15 2012 +0200
@@ -254,6 +254,8 @@
val BAD = "bad"
+ val GRAPHVIEW = "graphview"
+
/* protocol message functions */
--- a/src/Pure/Pure.thy Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Pure.thy Wed Sep 26 15:04:15 2012 +0200
@@ -77,7 +77,7 @@
"print_theorems" "print_locales" "print_classes" "print_locale"
"print_interps" "print_dependencies" "print_attributes"
"print_simpset" "print_rules" "print_trans_rules" "print_methods"
- "print_antiquotations" "thy_deps" "class_deps" "thm_deps"
+ "print_antiquotations" "thy_deps" "locale_deps" "class_deps" "thm_deps"
"print_binds" "print_facts" "print_cases" "print_statement" "thm"
"prf" "full_prf" "prop" "term" "typ" "print_codesetup" "unused_thms"
:: diag
--- a/src/Pure/ROOT Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/ROOT Wed Sep 26 15:04:15 2012 +0200
@@ -67,6 +67,7 @@
"General/buffer.ML"
"General/file.ML"
"General/graph.ML"
+ "General/graph_display.ML"
"General/heap.ML"
"General/integer.ML"
"General/linear_set.ML"
--- a/src/Pure/ROOT.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/ROOT.ML Wed Sep 26 15:04:15 2012 +0200
@@ -50,7 +50,6 @@
use "General/same.ML";
use "General/ord_list.ML";
use "General/balanced_tree.ML";
-use "General/graph.ML";
use "General/linear_set.ML";
use "General/buffer.ML";
use "General/pretty.ML";
@@ -66,6 +65,8 @@
use "PIDE/xml.ML";
use "PIDE/yxml.ML";
+use "General/graph.ML";
+
(* concurrency within the ML runtime *)
@@ -249,6 +250,7 @@
use "Thy/thy_syntax.ML";
use "PIDE/command.ML";
use "Isar/outer_syntax.ML";
+use "General/graph_display.ML";
use "Thy/present.ML";
use "Thy/thy_load.ML";
use "Thy/thy_info.ML";
--- a/src/Pure/System/isabelle_process.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/System/isabelle_process.ML Wed Sep 26 15:04:15 2012 +0200
@@ -161,6 +161,10 @@
(* init *)
+val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN];
+val default_modes2 =
+ [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN, Graph_Display.graphview_reportN];
+
fun init rendezvous = ignore (Simple_Thread.fork false (fn () =>
let
val _ = OS.Process.sleep (seconds 0.5); (*yield to raw ML toplevel*)
@@ -174,9 +178,7 @@
val _ = Context.set_thread_data NONE;
val _ =
Unsynchronized.change print_mode
- (fn mode =>
- (mode @ [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN])
- |> fold (update op =) [Symbol.xsymbolsN, isabelle_processN, Pretty.symbolicN]);
+ (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2);
val channel = rendezvous ();
val _ = init_channels channel;
--- a/src/Pure/Thy/present.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Thy/present.ML Wed Sep 26 15:04:15 2012 +0200
@@ -13,10 +13,6 @@
sig
include BASIC_PRESENT
val session_name: theory -> string
- val write_graph: {name: string, ID: string, dir: string, unfold: bool,
- path: string, parents: string list} list -> Path.T -> unit
- val display_graph: {name: string, ID: string, dir: string, unfold: bool,
- path: string, parents: string list} list -> unit
datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
val dump_mode: string -> dump_mode
val read_variant: string -> string * string
@@ -82,24 +78,6 @@
(** graphs **)
-type graph_node =
- {name: string, ID: string, dir: string, unfold: bool,
- path: string, parents: string list};
-
-fun write_graph gr path =
- 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) ^ " ;") gr));
-
-fun display_graph gr =
- let
- val path = Isabelle_System.create_tmp_path "graph" "";
- val _ = write_graph gr path;
- val _ = writeln "Displaying graph ...";
- val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
- in () end;
-
-
fun ID_of sess s = space_implode "/" (sess @ [s]);
fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
@@ -118,10 +96,11 @@
(Path.append (Path.make session) (html_path name))))
else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
unfold = false,
- parents = map ID_of_thy (Theory.parents_of thy)};
+ parents = map ID_of_thy (Theory.parents_of thy),
+ content = []};
in (0, entry) end);
-fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
+fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
(i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
@@ -144,7 +123,8 @@
(* type browser_info *)
type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
- tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
+ tex_index: (int * string) list, html_index: (int * string) list,
+ graph: (int * Graph_Display.node) list};
fun make_browser_info (theories, files, tex_index, html_index, graph) =
{theories = theories, files = files, tex_index = tex_index, html_index = html_index,
@@ -344,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 _ = write_graph graph graph_path;
+ 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
@@ -391,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);
- write_graph sorted_graph (Path.append html_prefix graph_path);
+ 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)
@@ -509,7 +489,8 @@
val entry =
{name = name, ID = ID_of path name, dir = sess_name, unfold = true,
path = Path.implode (html_path name),
- parents = map ID_of_thy parents};
+ parents = map ID_of_thy parents,
+ content = []};
in
change_theory_info name prep_html_source;
add_graph_entry (update_time, entry);
--- a/src/Pure/Thy/thm_deps.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/Thy/thm_deps.ML Wed Sep 26 15:04:15 2012 +0200
@@ -38,10 +38,11 @@
dir = space_implode "/" (session @ prefix),
unfold = false,
path = "",
- parents = parents};
+ parents = parents,
+ content = []};
in cons entry end;
val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
- in Present.display_graph (sort_wrt #ID deps) end;
+ in Graph_Display.display_graph (sort_wrt #ID deps) end;
(* unused_thms *)
--- a/src/Pure/build-jars Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/build-jars Wed Sep 26 15:04:15 2012 +0200
@@ -126,8 +126,7 @@
[ "$#" -ne 0 ] && usage
-
-# build
+## build
TARGET_DIR="$ISABELLE_HOME/lib/classes"
TARGET="$TARGET_DIR/ext/Pure.jar"
--- a/src/Pure/display.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Pure/display.ML Wed Sep 26 15:04:15 2012 +0200
@@ -194,7 +194,8 @@
val classes = Sorts.classes_of class_algebra;
val arities = Sorts.arities_of class_algebra;
- val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
+ val clsses =
+ Name_Space.dest_table ctxt (class_space, Symtab.make (map (apfst fst) (Graph.dest classes)));
val tdecls = Name_Space.dest_table ctxt types;
val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities);
--- a/src/Tools/Code/code_thingol.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML Wed Sep 26 15:04:15 2012 +0200
@@ -1045,8 +1045,8 @@
|> commas;
val prgr = map (fn (consts, constss) =>
{ name = namify consts, ID = namify consts, dir = "", unfold = true,
- path = "", parents = map namify constss }) conn;
- in Present.display_graph prgr end;
+ path = "", parents = map namify constss, content = [] }) conn;
+ in Graph_Display.display_graph prgr end;
local
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/etc/settings Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,8 @@
+# -*- shell-script -*- :mode=shellscript:
+
+GRAPHVIEW_HOME="$COMPONENT"
+
+GRAPHVIEW_JAVA_OPTIONS="-Xms128m -Xmx1024m -Xss4m"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$GRAPHVIEW_HOME/lib/Tools"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/lib/Tools/graphview Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,174 @@
+#!/usr/bin/env bash
+#
+# Author: Markus Kaiser, TU Muenchen
+# Author: Makarius
+#
+# DESCRIPTION: graphview command-line tool wrapper
+
+## sources
+
+declare -a SOURCES=(
+ "src/floating_dialog.scala"
+ "src/graph_panel.scala"
+ "src/graphview.scala"
+ "src/layout_pendulum.scala"
+ "src/main_panel.scala"
+ "src/model.scala"
+ "src/mutator_dialog.scala"
+ "src/mutator_event.scala"
+ "src/mutator.scala"
+ "src/parameters.scala"
+ "src/popups.scala"
+ "src/shapes.scala"
+ "src/visualizer.scala"
+)
+
+
+## diagnostics
+
+PRG="$(basename "$0")"
+
+function usage()
+{
+ echo
+ echo "Usage: isabelle $PRG [OPTIONS] GRAPH_FILE"
+ echo
+ echo " Options are:"
+ echo " -b build only"
+ echo " -c cleanup -- remove GRAPH_FILE after use"
+ echo " -f fresh build"
+ echo
+ exit 1
+}
+
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+function failed()
+{
+ fail "Failed!"
+}
+
+
+## process command line
+
+# options
+
+BUILD_ONLY="false"
+CLEAN="false"
+BUILD_JARS="jars"
+
+while getopts "bcf" OPT
+do
+ case "$OPT" in
+ b)
+ BUILD_ONLY="true"
+ ;;
+ c)
+ CLEAN="true"
+ ;;
+ f)
+ BUILD_JARS="jars_fresh"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift $(($OPTIND - 1))
+
+
+# args
+
+GRAPH_FILE=""
+[ "$#" -gt 0 ] && { GRAPH_FILE="$1"; shift; }
+[ "$#" -ne 0 ] && usage
+[ -z "$GRAPH_FILE" -a "$BUILD_ONLY" = false ] && usage
+
+
+## build
+
+[ -e "$ISABELLE_HOME/Admin/build" ] && \
+ { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
+
+pushd "$GRAPHVIEW_HOME" >/dev/null || failed
+
+PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
+
+TARGET_DIR="$ISABELLE_HOME/lib/classes"
+TARGET="$TARGET_DIR/ext/Graphview.jar"
+
+declare -a UPDATED=()
+
+if [ "$BUILD_JARS" = jars_fresh ]; then
+ OUTDATED=true
+else
+ OUTDATED=false
+ if [ ! -e "$TARGET" ]; then
+ OUTDATED=true
+ else
+ if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+ declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}")
+ else
+ declare -a DEPS=()
+ fi
+ for DEP in "${DEPS[@]}"
+ do
+ [ ! -e "$DEP" ] && fail "Missing file: $DEP"
+ [ "$DEP" -nt "$TARGET" ] && {
+ OUTDATED=true
+ UPDATED["${#UPDATED[@]}"]="$DEP"
+ }
+ done
+ fi
+fi
+
+if [ "$OUTDATED" = true ]
+then
+ echo "### Building Isabelle/Graphview ..."
+
+ [ "${#UPDATED[@]}" -gt 0 ] && {
+ echo "Changed files:"
+ for FILE in "${UPDATED[@]}"
+ do
+ echo " $FILE"
+ done
+ }
+
+ rm -rf classes && mkdir classes
+
+ (
+ CLASSPATH="$CLASSPATH:$PURE_JAR"
+ CLASSPATH="$(jvmpath "$CLASSPATH")"
+ exec "$SCALA_HOME/bin/scalac" $ISABELLE_SCALA_BUILD_OPTIONS -d classes "${SOURCES[@]}"
+ ) || fail "Failed to compile sources"
+
+ cd classes
+ isabelle_jdk jar cf "$(jvmpath "$TARGET")" * || failed
+ cd ..
+ rm -rf classes
+fi
+
+popd >/dev/null
+
+
+## run
+
+if [ "$BUILD_ONLY" = false ]; then
+ PRIVATE_FILE="${ISABELLE_TMP:-/tmp}/$$""$(basename "$GRAPH_FILE")"
+ 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 $GRAPHVIEW_JAVA_OPTIONS isabelle.graphview.Graphview "$PRIVATE_FILE"
+ RC="$?"
+
+ rm -f "$PRIVATE_FILE"
+ echo "$RC"
+fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/floating_dialog.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,33 @@
+/* Title: Tools/Graphview/src/floating_dialog.scala
+ Author: Markus Kaiser, TU Muenchen
+
+PopUp Dialog containing node meta-information.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import scala.swing.{Dialog, BorderPanel, Component, TextArea}
+import java.awt.{Font, Point, Dimension}
+
+
+class Floating_Dialog(content: XML.Body, _title: String, _location: Point)
+extends Dialog
+{
+ location = _location
+ title = _title
+ //No adaptive size because we don't want to resize the Dialog about 1 sec
+ //after it is shown.
+ preferredSize = new Dimension(300, 300)
+ peer.setAlwaysOnTop(true)
+
+ private val text_font = new Font(Parameters.font_family, Font.PLAIN, Parameters.font_size)
+ private val text = new TextArea
+ text.peer.setFont(text_font)
+ text.editable = false
+
+ contents = new BorderPanel { add(text, BorderPanel.Position.Center) }
+ text.text = Pretty.string_of(content, 76, Pretty.font_metric(text.peer.getFontMetrics(text_font)))
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/graph_panel.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,320 @@
+/* Title: Tools/Graphview/src/graph_panel.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graphview Java2D drawing panel.
+*/
+
+package isabelle.graphview
+
+import isabelle._
+
+import java.awt.{Dimension, Graphics2D, Point, Rectangle}
+import java.awt.geom.{AffineTransform, Point2D}
+import javax.swing.ToolTipManager
+import scala.swing.{Panel, ScrollPane}
+import scala.swing.event._
+
+
+class Graph_Panel(private val vis: Visualizer) extends ScrollPane {
+ this.peer.setWheelScrollingEnabled(false)
+ focusable = true
+ requestFocus()
+
+ horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
+ verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
+
+ def visualizer = vis
+
+ def fit_to_window() = {
+ Transform.fit_to_window()
+ repaint()
+ }
+
+ def apply_layout() = vis.Coordinates.layout()
+
+ private val paint_panel = new Panel {
+ def set_preferred_size() {
+ val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+ val s = Transform.scale
+ val (px, py) = Transform.padding
+
+ preferredSize = new Dimension((math.abs(maxX - minX + px) * s).toInt,
+ (math.abs(maxY - minY + py) * s).toInt)
+
+ revalidate()
+ }
+
+ override def paint(g: Graphics2D) {
+ set_preferred_size()
+ super.paintComponent(g)
+ g.transform(Transform())
+
+ vis.Drawer.paint_all_visible(g, true)
+ }
+ }
+ contents = paint_panel
+
+ listenTo(keys)
+ listenTo(mouse.moves)
+ listenTo(mouse.clicks)
+ listenTo(mouse.wheel)
+ reactions += Interaction.Mouse.react
+ reactions += Interaction.Keyboard.react
+ reactions += {
+ case KeyTyped(_, _, _, _) => {repaint(); requestFocus()}
+ case MousePressed(_, _, _, _, _) => {repaint(); requestFocus()}
+ case MouseDragged(_, _, _) => {repaint(); requestFocus()}
+ case MouseWheelMoved(_, _, _, _) => {repaint(); requestFocus()}
+ case MouseClicked(_, _, _, _, _) => {repaint(); requestFocus()}
+ case MouseMoved(_, _, _) => repaint()
+ }
+ private val r = {
+ import scala.actors.Actor._
+
+ actor {
+ loop {
+ react {
+ // FIXME Swing thread!?
+ case _ => repaint()
+ }
+ }
+ }
+ }
+ vis.model.Colors.events += r
+ vis.model.Mutators.events += r
+ ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
+
+ apply_layout()
+ fit_to_window()
+
+ protected object Transform {
+ val padding = (4000, 2000)
+
+ private var _scale = 1d
+ def scale = _scale
+ def scale_= (s: Double) = {
+ _scale = math.max(math.min(s, 10), 0.01)
+ paint_panel.set_preferred_size()
+ }
+
+ def apply() = {
+ val (minX, minY, _, _) = vis.Coordinates.bounds()
+
+ val at = AffineTransform.getScaleInstance(scale, scale)
+ at.translate(-minX + padding._1 / 2, -minY + padding._2 / 2)
+ at
+ }
+
+ def fit_to_window() {
+ if (vis.model.visible_nodes().isEmpty)
+ scale = 1
+ else {
+ val (minX, minY, maxX, maxY) = vis.Coordinates.bounds()
+
+ val (dx, dy) = (maxX - minX + padding._1, maxY - minY + padding._2)
+ val (sx, sy) = (1d * size.width / dx, 1d * size.height / dy)
+ scale = math.min(sx, sy)
+ }
+ }
+
+ def pane_to_graph_coordinates(at: Point2D): Point2D = {
+ val s = Transform.scale
+ val p = Transform().inverseTransform(peer.getViewport.getViewPosition, null)
+
+ p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
+ p
+ }
+ }
+
+ private val panel = this
+ object Interaction {
+ object Keyboard {
+ import scala.swing.event.Key._
+
+ val react: PartialFunction[Event, Unit] = {
+ case KeyTyped(_, c, m, _) => typed(c, m)
+ }
+
+ def typed(c: Char, m: Modifiers) = (c, m) match {
+ case ('+', _) => {
+ Transform.scale *= 5d/4
+ }
+
+ case ('-', _) => {
+ Transform.scale *= 4d/5
+ }
+
+ case ('0', _) => {
+ Transform.fit_to_window()
+ }
+
+ case('1', _) => {
+ vis.Coordinates.layout()
+ }
+
+ case('2', _) => {
+ Transform.fit_to_window()
+ }
+
+ case _ =>
+ }
+ }
+
+ object Mouse {
+ import java.awt.image.BufferedImage
+ import scala.swing.event.Key.Modifier._
+ type Modifiers = Int
+ type Dummy = ((String, String), Int)
+
+ private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
+ private val g =
+ new BufferedImage(1, 1, BufferedImage.TYPE_INT_RGB).createGraphics
+ g.setFont(vis.Font())
+ g.setRenderingHints(vis.rendering_hints)
+
+ val react: PartialFunction[Event, Unit] = {
+ case MousePressed(_, p, _, _, _) => pressed(p)
+ case MouseDragged(_, to, _) => {
+ drag(draginfo, to)
+ val (_, p, d) = draginfo
+ draginfo = (to, p, d)
+ }
+ case MouseWheelMoved(_, p, _, r) => wheel(r, p)
+ case e@MouseClicked(_, p, m, n, _) => click(p, m, n, e)
+ case MouseMoved(_, p, _) => moved(p)
+ }
+
+ def node(at: Point2D): Option[String] =
+ vis.model.visible_nodes().find({
+ l => vis.Drawer.shape(g, Some(l)).contains(at)
+ })
+
+ def dummy(at: Point2D): Option[Dummy] =
+ vis.model.visible_edges().map({
+ i => vis.Coordinates(i).zipWithIndex.map((i, _))
+ }).flatten.find({
+ case (_, ((x, y), _)) =>
+ vis.Drawer.shape(g, None).contains(at.getX() - x, at.getY() - y)
+ }) match {
+ case None => None
+ case Some((name, (_, index))) => Some((name, index))
+ }
+
+ def moved(at: Point) {
+ val c = Transform.pane_to_graph_coordinates(at)
+ node(c) match {
+ case Some(l) => panel.tooltip = vis.Tooltip.text(l, g.getFontMetrics)
+ case None => panel.tooltip = null
+ }
+ }
+
+ def pressed(at: Point) {
+ val c = Transform.pane_to_graph_coordinates(at)
+ val l = node(c) match {
+ case Some(l) => if (vis.Selection(l))
+ vis.Selection()
+ else
+ List(l)
+
+ case None => Nil
+ }
+ val d = l match {
+ case Nil => dummy(c) match {
+ case Some(d) => List(d)
+ case None => Nil
+ }
+
+ case _ => Nil
+ }
+
+ draginfo = (at, l, d)
+ }
+
+ def click(at: Point, m: Modifiers, clicks: Int, e: MouseEvent) {
+ import javax.swing.SwingUtilities
+
+ val c = Transform.pane_to_graph_coordinates(at)
+ val p = node(c)
+
+ def left_click() {
+ (p, m) match {
+ case (Some(l), Control) => vis.Selection.add(l)
+ case (None, Control) =>
+
+ case (Some(l), Shift) => vis.Selection.add(l)
+ case (None, Shift) =>
+
+ case (Some(l), _) => vis.Selection.set(List(l))
+ case (None, _) => vis.Selection.clear
+ }
+ }
+
+ def right_click() {
+ val menu = Popups(panel, p, vis.Selection())
+ menu.show(panel.peer, at.x, at.y)
+ }
+
+ def double_click() {
+ p match {
+ case Some(l) => {
+ val p = at.clone.asInstanceOf[Point]
+ SwingUtilities.convertPointToScreen(p, panel.peer)
+ new Floating_Dialog(
+ vis.Tooltip.content(l),
+ vis.Caption(l),
+ at
+ ).open
+ }
+
+ case None =>
+ }
+ }
+
+ if (clicks < 2) {
+ if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
+ else left_click()
+ } else if (clicks == 2) {
+ if (SwingUtilities.isLeftMouseButton(e.peer)) double_click()
+ }
+ }
+
+ def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point) {
+ val (from, p, d) = draginfo
+
+ val s = Transform.scale
+ val (dx, dy) = (to.x - from.x, to.y - from.y)
+ (p, d) match {
+ case (Nil, Nil) => {
+ val r = panel.peer.getViewport.getViewRect
+ r.translate(-dx, -dy)
+
+ paint_panel.peer.scrollRectToVisible(r)
+ }
+
+ case (Nil, ds) =>
+ ds.foreach(d => vis.Coordinates.translate(d, (dx / s, dy / s)))
+
+ case (ls, _) =>
+ ls.foreach(l => vis.Coordinates.translate(l, (dx / s, dy / s)))
+ }
+ }
+
+ def wheel(rotation: Int, at: Point) {
+ val at2 = Transform.pane_to_graph_coordinates(at)
+ // > 0 -> up
+ Transform.scale *= (if (rotation > 0) 4d/5 else 5d/4)
+
+ // move mouseposition to center
+ Transform().transform(at2, at2)
+ val r = panel.peer.getViewport.getViewRect
+ val (width, height) = (r.getWidth, r.getHeight)
+ paint_panel.peer.scrollRectToVisible(
+ new Rectangle((at2.getX() - width / 2).toInt,
+ (at2.getY() - height / 2).toInt,
+ width.toInt,
+ height.toInt)
+ )
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/graphview.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,51 @@
+/* Title: Tools/Graphview/src/graphview.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graphview standalone application.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Dimension
+import scala.swing.{MainFrame, BorderPanel, Window, SwingApplication}
+import javax.swing.border.EmptyBorder
+
+
+object Graphview extends SwingApplication
+{
+ def startup(args : Array[String])
+ {
+ // FIXME avoid I/O etc. on Swing thread
+ val graph: Model.Graph =
+ try {
+ Platform.init_laf()
+ Isabelle_System.init()
+ Isabelle_System.install_fonts()
+
+ args.toList match {
+ case List(arg) =>
+ Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
+ case _ => error("Bad arguments:\n" + cat_lines(args))
+ }
+ }
+ catch { case exn: Throwable => println(Exn.message(exn)); sys.exit(1) }
+
+ val top = new MainFrame {
+ title = "Graphview"
+ minimumSize = new Dimension(640, 480)
+ preferredSize = new Dimension(800, 600)
+
+ contents = new BorderPanel {
+ border = new EmptyBorder(5, 5, 5, 5)
+
+ add(new Main_Panel(graph), BorderPanel.Position.Center)
+ }
+ }
+
+ top.pack()
+ top.visible = true
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/layout_pendulum.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,288 @@
+/* Title: Tools/Graphview/src/layout_pendulum.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Pendulum DAG layout algorithm.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+
+object Layout_Pendulum {
+ type Key = String
+ 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 = (Model.Graph, List[Key], Map[Key, Int])
+
+ val x_distance = 350
+ val y_distance = 350
+ val pendulum_iterations = 10
+
+ 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: Model.Graph, from: Key, to: Key,
+ levels: Map[Key, Int]): Dummies = {
+ val ds =
+ ((levels(from) + 1) until levels(to))
+ .map("%s$%s$%d" format (from, to, _)).toList
+
+ val ls =
+ (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
+ case (ls, (l, d)) => ls + (d -> l)
+ }
+
+ val next_nodes =
+ (graph /: ds) {
+ (graph, d) => graph.new_node(d, Model.empty_info)
+ }
+
+ val next =
+ (next_nodes.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
+ case (graph, List(f, t)) => graph.add_edge(f, t)
+ }
+ (next, ds, ls)
+ }
+
+ ((graph, Map[(Key, Key), List[Key]](), initial_levels) /: graph.keys) {
+ case ((graph, dummies, levels), from) => {
+ ((graph, dummies, levels) /: graph.imm_succs(from)) {
+ case ((graph, dummies, levels), to) => {
+ if (levels(to) - levels(from) <= 1) (graph, dummies, levels)
+ else add_dummies(graph, from, to, levels) match {
+ case (next, ds, ls) => (next, dummies + ((from, to) -> ds), ls)
+ }
+ }
+ }
+ }
+ }
+ }
+
+ val levels =
+ minimize_crossings(
+ dummy_graph,
+ level_list(dummy_levels)
+ )
+
+ val coords =
+ pendulum(dummy_graph,
+ levels,
+ initial_coordinates(levels)
+ )
+
+ val dummy_coords =
+ (Map[(Key, Key), List[Point]]() /: dummies.keys) {
+ case (map, key) => map + (key -> dummies(key).map(coords(_)))
+ }
+
+ (coords, dummy_coords)
+ }
+ }
+
+ 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)
+ levels + (key -> (pred_levels.max + 1))
+ }}
+
+ def level_list(map: Map[Key, Int]): Levels =
+ (map.toList.sortBy(_._2) :\ List[(Int, Level)]()){
+ case ((key, i), list) => {
+ if (list.isEmpty) (i, List(key)) :: list
+ else {
+ val (j, l) = list.head
+ if (i == j) (i, key :: l) :: list.tail
+ else (i, List(key)) :: list
+ }
+ }
+ }.map(_._2)
+
+ def count_crossings(graph: Model.Graph, levels: Levels): Int = {
+ def in_level(ls: Levels): Int = ls match {
+ case List(top, bot) =>
+ top.zipWithIndex.map{
+ case (outer_parent, outer_parent_index) =>
+ graph.imm_succs(outer_parent).map(bot.indexOf(_))
+ .map(outer_child => {
+ (0 until outer_parent_index)
+ .map(inner_parent =>
+ graph.imm_succs(top(inner_parent))
+ .map(bot.indexOf(_))
+ .filter(inner_child => outer_child < inner_child)
+ .size
+ ).sum
+ }).sum
+ }.sum
+
+ case _ => 0
+ }
+
+ levels.sliding(2).map(in_level).sum
+ }
+
+ 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)
+ val weight =
+ (0d /: ps) {
+ (w, p) => w + math.max(0, parent.indexOf(p))
+ } / math.max(ps.size, 1)
+ (k, weight)
+ }).sortBy(_._2).map(_._1)
+
+ def resort(levels: Levels, top_down: Boolean) = top_down match {
+ case true =>
+ (List[Level](levels.head) /: levels.tail) {
+ (tops, bot) => resort_level(tops.head, bot, top_down) :: tops
+ }.reverse
+
+ case false =>
+ (List[Level](levels.reverse.head) /: levels.reverse.tail) {
+ (bots, top) => resort_level(bots.head, top, top_down) :: bots
+ }
+ }
+
+ ((levels, count_crossings(graph, levels), true) /: (1 to 40)) {
+ case ((old_levels, old_crossings, top_down), _) => {
+ val new_levels = resort(old_levels, top_down)
+ val new_crossings = count_crossings(graph, new_levels)
+ if ( new_crossings < old_crossings)
+ (new_levels, new_crossings, !top_down)
+ else
+ (old_levels, old_crossings, !top_down)
+ }
+ }._1
+ }
+
+ def initial_coordinates(levels: Levels): Coordinates =
+ (Map[Key, Point]() /: levels.zipWithIndex){
+ case (coords, (level, yi)) =>
+ (coords /: level.zipWithIndex) {
+ case (coords, (node, xi)) =>
+ coords + (node -> (xi * x_distance, yi * y_distance))
+ }
+ }
+
+ def pendulum(graph: Model.Graph,
+ levels: Levels, coords: Map[Key, Point]): Coordinates =
+ {
+ type Regions = List[List[Region]]
+
+ def iteration(regions: Regions, coords: Coordinates,
+ top_down: Boolean): (Regions, Coordinates, Boolean) =
+ {
+ val (nextr, nextc, moved) =
+ ((List[List[Region]](), coords, false) /:
+ (if (top_down) regions else regions.reverse)) {
+ case ((tops, coords, prev_moved), bot) => {
+ val nextb = collapse(coords, bot, top_down)
+ val (nextc, this_moved) = deflect(coords, nextb, top_down)
+ (nextb :: tops, nextc, prev_moved || this_moved)
+ }
+ }
+
+ (nextr.reverse, nextc, moved)
+ }
+
+ def collapse(coords: Coordinates, level: List[Region],
+ top_down: Boolean): List[Region] =
+ if (level.size <= 1) level
+ else {
+ var next = level
+ var regions_changed = true
+ while (regions_changed) {
+ regions_changed = false
+ for (i <- (next.length to 1)) {
+ val (r1, r2) = (next(i-1), next(i))
+ val d1 = r1.deflection(coords, top_down)
+ val d2 = r2.deflection(coords, top_down)
+
+ if (
+ // Do regions touch?
+ r1.distance(coords, r2) <= x_distance &&
+ // Do they influence each other?
+ (d1 <= 0 && d2 < d1 || d2 > 0 && d1 > d2 || d1 > 0 && d2 < 0)
+ )
+ {
+ regions_changed = true
+ r1.nodes = r1.nodes ::: r2.nodes
+ next = next.filter(next.indexOf(_) != i)
+ }
+ }
+ }
+ next
+ }
+
+ def deflect(coords: Coordinates, level: List[Region],
+ top_down: Boolean): (Coordinates, Boolean) =
+ ((coords, false) /: (0 until level.length)) {
+ case ((coords, moved), i) => {
+ val r = level(i)
+ val d = r.deflection(coords, top_down)
+ val offset = {
+ if (i == 0 && d <= 0) d
+ else if (i == level.length - 1 && d >= 0) d
+ else if (d < 0) {
+ val prev = level(i-1)
+ math.max( -(r.distance(coords, prev) - x_distance), d )
+ }
+ else {
+ val next = level(i+1)
+ math.min( r.distance(coords, next) - x_distance, d )
+ }
+ }
+
+ (r.move(coords, offset), moved || (d != 0))
+ }
+ }
+
+ val regions = levels.map(level => level.map(new Region(graph, _)))
+
+ ((regions, coords, true, true) /: (1 to pendulum_iterations)) {
+ case ((regions, coords, top_down, moved), _) =>
+ if (moved) {
+ val (nextr, nextc, m) = iteration(regions, coords, top_down)
+ (nextr, nextc, !top_down, m)
+ }
+ else (regions, coords, !top_down, moved)
+ }._2
+ }
+
+ protected class Region(val graph: Model.Graph, node: Key) {
+ var nodes: List[Key] = List(node)
+
+ def left(coords: Coordinates): Double =
+ nodes.map(coords(_)._1).min
+ def right(coords: Coordinates): Double =
+ nodes.map(coords(_)._1).max
+ def distance(coords: Coordinates, to: Region): Double =
+ math.min(math.abs(left(coords) - to.left(coords)),
+ math.abs(right(coords) - to.right(coords)))
+
+ def deflection(coords: Coordinates, use_preds: Boolean) =
+ nodes.map(k => (coords(k)._1,
+ if (use_preds) graph.imm_preds(k).toList
+ else graph.imm_succs(k).toList))
+ .map({case (x, as) => as.map(coords(_)._1 - x).sum / math.max(as.length, 1)})
+ .sum / nodes.length
+
+ def move(coords: Coordinates, by: Double): Coordinates =
+ (coords /: nodes) {
+ (cs, node) => {
+ val (x, y) = cs(node)
+ cs + (node -> (x + by, y))
+ }
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/main_panel.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,133 @@
+/* Title: Tools/Graphview/src/main_panel.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graph Panel wrapper.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+
+import scala.collection.JavaConversions._
+import scala.swing.{BorderPanel, Button, BoxPanel,
+ Orientation, Swing, CheckBox, Action, FileChooser}
+import javax.swing.border.EmptyBorder
+import java.awt.Dimension
+import java.io.File
+
+
+class Main_Panel(graph: Model.Graph) extends BorderPanel
+{
+ focusable = true
+ requestFocus()
+
+ val model = new Model(graph)
+ val visualizer = new Visualizer(model)
+ val graph_panel = new Graph_Panel(visualizer)
+
+ listenTo(keys)
+ reactions += graph_panel.reactions
+
+ val mutator_dialog = new Mutator_Dialog(
+ model.Mutators,
+ "Filters",
+ "Hide",
+ false
+ )
+
+ val color_dialog = new Mutator_Dialog(
+ model.Colors,
+ "Colorations"
+ )
+
+ private val chooser = new FileChooser()
+ chooser.fileSelectionMode = FileChooser.SelectionMode.FilesOnly
+ chooser.title = "Graph export"
+
+ val options_panel = new BoxPanel(Orientation.Horizontal) {
+ border = new EmptyBorder(0, 0, 10, 0)
+
+ contents += Swing.HGlue
+ contents += new CheckBox(){
+ selected = Parameters.arrow_heads
+ action = Action("Arrow Heads"){
+ Parameters.arrow_heads = selected
+ graph_panel.repaint()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new CheckBox(){
+ selected = Parameters.long_names
+ action = Action("Long Names"){
+ Parameters.long_names = selected
+ graph_panel.repaint()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Save as PNG"){
+ chooser.showSaveDialog(this) match {
+ case FileChooser.Result.Approve => {
+ export(chooser.selectedFile)
+ }
+
+ case _ =>
+ }
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Apply Layout"){
+ graph_panel.apply_layout()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Fit to Window"){
+ graph_panel.fit_to_window()
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Colorations"){
+ color_dialog.open
+ }
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += new Button{
+ action = Action("Filters"){
+ mutator_dialog.open
+ }
+ }
+ }
+
+ add(graph_panel, BorderPanel.Position.Center)
+ add(options_panel, BorderPanel.Position.North)
+
+ private def export(file: File) {
+ import java.awt.image.BufferedImage
+ import javax.imageio.ImageIO
+ import java.awt.geom.Rectangle2D
+ import java.awt.Color
+
+ val (minX, minY, maxX, maxY) = visualizer.Coordinates.bounds
+ val img = new BufferedImage((math.abs(maxX - minX) + 400).toInt,
+ (math.abs(maxY - minY) + 200).toInt,
+ BufferedImage.TYPE_INT_RGB)
+ val g = img.createGraphics
+ g.setColor(Color.WHITE)
+ g.fill(new Rectangle2D.Double(0, 0, img.getWidth(), img.getHeight()))
+
+ g.translate(- minX + 200, - minY + 100)
+ visualizer.Drawer.paint_all_visible(g, false)
+ g.dispose()
+
+ try {
+ ImageIO.write(img, "png", file)
+ } catch {
+ case ex: Exception => ex.printStackTrace
+ }
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/model.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,113 @@
+/* Title: Tools/Graphview/src/model.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Internal graph representation.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+import java.awt.Color
+import scala.actors.Actor
+import scala.actors.Actor._
+
+
+class Mutator_Container(val available: List[Mutator]) {
+ type Mutator_Markup = (Boolean, Color, Mutator)
+
+ val events = new Event_Bus[Mutator_Event.Message]
+
+ private var _mutators : List[Mutator_Markup] = Nil
+ def apply() = _mutators
+ def apply(mutators: List[Mutator_Markup]){
+ _mutators = mutators
+
+ events.event(Mutator_Event.NewList(mutators))
+ }
+
+ def add(mutator: Mutator_Markup) = {
+ _mutators = _mutators ::: List(mutator)
+
+ events.event(Mutator_Event.Add(mutator))
+ }
+}
+
+
+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),
+ Node_List(Nil, false, false, false),
+ Edge_Endpoints("", ""),
+ Edge_Transitive(),
+ Add_Node_Expression(""),
+ Add_Transitive_Closure(true, true)
+ ))
+
+ val Colors = new Mutator_Container(
+ List(
+ Node_Expression(".*", false, false, false),
+ Node_List(Nil, false, false, false)
+ ))
+
+ def visible_nodes(): Iterator[String] = current.keys
+
+ def visible_edges(): Iterator[(String, String)] =
+ current.keys.map(k => current.imm_succs(k).map((k, _))).flatten
+
+ def complete = graph
+ def current: Model.Graph =
+ (graph /: Mutators()) {
+ case (g, (enabled, _, mutator)) => {
+ if (!enabled) g
+ else mutator.mutate(graph, g)
+ }
+ }
+
+ private var _colors = Map[String, Color]()
+ def colors = _colors
+
+ private def build_colors() {
+ (Map[String, Color]() /: Colors()) ({
+ case (colors, (enabled, color, mutator)) => {
+ (colors /: mutator.mutate(graph, graph).keys) ({
+ case (colors, k) => colors + (k -> color)
+ })
+ }
+ })
+ }
+ Colors.events += actor {
+ loop {
+ react {
+ case _ => build_colors()
+ }
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,211 @@
+/* Title: Tools/Graphview/src/mutator.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Filters and add-operations on graphs.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+
+import java.awt.Color
+import scala.collection.immutable.SortedSet
+
+
+trait Mutator
+{
+ val name: String
+ val description: String
+ def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph
+
+ override def toString() = name
+}
+
+trait Filter extends Mutator
+{
+ def mutate(complete: Model.Graph, sub: Model.Graph) = filter(sub)
+ def filter(sub: Model.Graph) : Model.Graph
+}
+
+object Mutators {
+ type Mutator_Markup = (Boolean, Color, Mutator)
+
+ val Enabled = true
+ val Disabled = false
+
+ def create(m: Mutator): Mutator_Markup =
+ (Mutators.Enabled, Parameters.Colors.next, m)
+
+ class Graph_Filter(val name: String, val description: String,
+ pred: Model.Graph => Model.Graph)
+ extends Filter
+ {
+ def filter(sub: Model.Graph) : Model.Graph = pred(sub)
+ }
+
+ class Graph_Mutator(val name: String, val description: String,
+ pred: (Model.Graph, Model.Graph) => Model.Graph)
+ extends Mutator
+ {
+ def mutate(complete: Model.Graph, sub: Model.Graph): Model.Graph =
+ pred(complete, sub)
+ }
+
+ 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(name: String, description: String,
+ pred: (Model.Graph, String, String) => Boolean)
+ extends Graph_Filter (
+
+ name,
+ description,
+ g => (g /: g.dest) {
+ case (graph, ((from, _), tos)) => {
+ (graph /: tos) {
+ (gr, to) => if (pred(gr, from, to)) gr
+ else gr.del_edge(from, to)
+ }
+ }
+ }
+ )
+
+ class Node_Family_Filter(name: String, description: String,
+ reverse: Boolean, parents: Boolean, children: Boolean,
+ pred: (Model.Graph, String) => Boolean)
+ extends Node_Filter(
+
+ name,
+ description,
+ (g, k) => reverse != (
+ pred(g, k) ||
+ (parents && g.all_preds(List(k)).exists(pred(g, _))) ||
+ (children && g.all_succs(List(k)).exists(pred(g, _)))
+ )
+ )
+
+ case class Identity()
+ extends Graph_Filter(
+
+ "Identity",
+ "Does not change the graph.",
+ g => g
+ )
+
+ case class Node_Expression(regex: String,
+ reverse: Boolean, parents: Boolean, children: Boolean)
+ extends Node_Family_Filter(
+
+ "Filter by Name",
+ "Only shows or hides all nodes with any family member's name matching " +
+ "a regex.",
+ reverse,
+ parents,
+ children,
+ (g, k) => (regex.r findFirstIn k).isDefined
+ )
+
+ case class Node_List(list: List[String],
+ reverse: Boolean, parents: Boolean, children: Boolean)
+ extends Node_Family_Filter(
+
+ "Filter by Name List",
+ "Only shows or hides all nodes with any family member's name matching " +
+ "any string in a comma separated list.",
+ reverse,
+ parents,
+ children,
+ (g, k) => list.exists(_ == k)
+ )
+
+ case class Edge_Endpoints(source: String, dest: String)
+ extends Edge_Filter(
+
+ "Hide edge",
+ "Hides the edge whose endpoints match strings.",
+ (g, s, d) => !(s == source && d == dest)
+ )
+
+ case class Edge_Transitive()
+ extends Edge_Filter(
+
+ "Hide transitive edges",
+ "Hides all transitive edges.",
+ (g, s, d) => {
+ !g.imm_succs(s).filter(_ != d)
+ .exists(p => !(g.irreducible_paths(p, d).isEmpty))
+ }
+ )
+
+ private def add_node_group(from: Model.Graph, to: Model.Graph,
+ keys: List[String]) = {
+
+ // Add Nodes
+ val with_nodes =
+ (to /: keys) {
+ (graph, key) => graph.default_node(key, from.get_node(key))
+ }
+
+ // Add Edges
+ (with_nodes /: keys) {
+ (gv, key) => {
+ def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
+ (g /: keys) {
+ (graph, end) => {
+ if (!graph.keys.contains(end)) graph
+ else {
+ if (succs) graph.add_edge(key, end)
+ else graph.add_edge(end, key)
+ }
+ }
+ }
+
+
+ add_edges(
+ add_edges(gv, from.imm_preds(key), false),
+ from.imm_succs(key), true
+ )
+ }
+ }
+ }
+
+ case class Add_Node_Expression(regex: String)
+ extends Graph_Mutator(
+
+ "Add by name",
+ "Adds every node whose name matches the regex. " +
+ "Adds all relevant edges.",
+ (complete, sub) => {
+ add_node_group(complete, sub, complete.keys.filter(
+ k => (regex.r findFirstIn k).isDefined
+ ).toList)
+ }
+ )
+
+ case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
+ extends Graph_Mutator(
+
+ "Add transitive closure",
+ "Adds all family members of all current nodes.",
+ (complete, sub) => {
+ val withparents =
+ if (parents)
+ add_node_group(complete, sub, complete.all_preds(sub.keys.toList))
+ else
+ sub
+
+ if (children)
+ add_node_group(complete, withparents,
+ complete.all_succs(sub.keys.toList))
+ else
+ withparents
+ }
+ )
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator_dialog.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,433 @@
+/* Title: Tools/Graphview/src/mutator_dialog.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Mutator selection and configuration dialog.
+*/
+
+package isabelle.graphview
+
+import isabelle._
+
+import java.awt.Color
+import java.awt.FocusTraversalPolicy
+import javax.swing.JColorChooser
+import javax.swing.border.EmptyBorder
+import scala.collection.JavaConversions._
+import scala.swing._
+import scala.actors.Actor
+import scala.actors.Actor._
+import isabelle.graphview.Mutators._
+import scala.swing.event.ValueChanged
+
+
+class Mutator_Dialog(
+ container: Mutator_Container, caption: String,
+ reverse_caption: String = "Inverse", show_color_chooser: Boolean = true)
+extends Dialog
+{
+ type Mutator_Markup = (Boolean, Color, Mutator)
+
+ title = caption
+
+ private var _panels: List[Mutator_Panel] = Nil
+ private def panels = _panels
+ private def panels_= (panels: List[Mutator_Panel]) {
+ _panels = panels
+ paintPanels
+ }
+
+ container.events += actor {
+ loop {
+ react {
+ case Mutator_Event.Add(m) => addPanel(new Mutator_Panel(m))
+ case Mutator_Event.NewList(ms) => {
+ panels = getPanels(ms)
+ }
+ }
+ }
+ }
+
+ override def open() {
+ if (!visible)
+ panels = getPanels(container())
+
+ super.open
+ }
+
+ minimumSize = new Dimension(700, 200)
+ preferredSize = new Dimension(1000, 300)
+ peer.setFocusTraversalPolicy(focusTraversal)
+
+ private def getPanels(m: List[Mutator_Markup]): List[Mutator_Panel] =
+ m.filter(_ match {case (_, _, Identity()) => false; case _ => true})
+ .map(m => new Mutator_Panel(m))
+
+ private def getMutators(panels: List[Mutator_Panel]): List[Mutator_Markup] =
+ panels.map(panel => panel.get_Mutator_Markup)
+
+ private def movePanelUp(m: Mutator_Panel) = {
+ def moveUp(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+ case x :: y :: xs => if (y == m) y :: x :: xs else x :: moveUp(y :: xs)
+ case _ => l
+ }
+
+ panels = moveUp(panels)
+ }
+
+ private def movePanelDown(m: Mutator_Panel) = {
+ def moveDown(l: List[Mutator_Panel]): List[Mutator_Panel] = l match {
+ case x :: y :: xs => if (x == m) y :: x :: xs else x :: moveDown(y :: xs)
+ case _ => l
+ }
+
+ panels = moveDown(panels)
+ }
+
+ private def removePanel(m: Mutator_Panel) = {
+ panels = panels.filter(_ != m).toList
+ }
+
+ private def addPanel(m: Mutator_Panel) = {
+ panels = panels ::: List(m)
+ }
+
+ def paintPanels = {
+ focusTraversal.clear
+ filterPanel.contents.clear
+ panels.map(x => {
+ filterPanel.contents += x
+ focusTraversal.addAll(x.focusList)
+ })
+ filterPanel.contents += Swing.VGlue
+
+ focusTraversal.add(mutatorBox.peer.asInstanceOf[java.awt.Component])
+ focusTraversal.add(addButton.peer)
+ focusTraversal.add(applyButton.peer)
+ focusTraversal.add(cancelButton.peer)
+ filterPanel.revalidate
+ filterPanel.repaint
+ }
+
+ val filterPanel = new BoxPanel(Orientation.Vertical) {}
+
+ private val mutatorBox = new ComboBox[Mutator](container.available)
+
+ private val addButton: Button = new Button{
+ action = Action("Add") {
+ addPanel(
+ new Mutator_Panel((true, Parameters.Colors.next,
+ mutatorBox.selection.item))
+ )
+ }
+ }
+
+ private val applyButton = new Button{
+ action = Action("Apply") {
+ container(getMutators(panels))
+ }
+ }
+
+ private val resetButton = new Button {
+ action = Action("Reset") {
+ panels = getPanels(container())
+ }
+ }
+
+ private val cancelButton = new Button{
+ action = Action("Close") {
+ close
+ }
+ }
+ defaultButton = cancelButton
+
+ private val botPanel = new BoxPanel(Orientation.Horizontal) {
+ border = new EmptyBorder(10, 0, 0, 0)
+
+ contents += mutatorBox
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += addButton
+
+ contents += Swing.HGlue
+ contents += Swing.RigidBox(new Dimension(30, 0))
+ contents += applyButton
+
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ contents += resetButton
+
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ contents += cancelButton
+ }
+
+ contents = new BorderPanel {
+ border = new EmptyBorder(5, 5, 5, 5)
+
+ add(new ScrollPane(filterPanel), BorderPanel.Position.Center)
+ add(botPanel, BorderPanel.Position.South)
+ }
+
+ private class Mutator_Panel(initials: Mutator_Markup)
+ extends BoxPanel(Orientation.Horizontal)
+ {
+ private val (_enabled, _color, _mutator) = initials
+
+ private val inputs: List[(String, Mutator_Input_Value)] = get_Inputs()
+ var focusList = List[java.awt.Component]()
+ private val enabledBox = new iCheckBox("Enabled", _enabled)
+
+ border = new EmptyBorder(5, 5, 5, 5)
+ maximumSize = new Dimension(Integer.MAX_VALUE, 30)
+ background = _color
+
+ contents += new Label(_mutator.name) {
+ preferredSize = new Dimension(175, 20)
+ horizontalAlignment = Alignment.Left
+ if (_mutator.description != "") tooltip = _mutator.description
+ }
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ contents += enabledBox
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ focusList = enabledBox.peer :: focusList
+ inputs.map( _ match {
+ case (n, c) => {
+ contents += Swing.RigidBox(new Dimension(10, 0))
+ if (n != "") {
+ contents += new Label(n)
+ contents += Swing.RigidBox(new Dimension(5, 0))
+ }
+ contents += c.asInstanceOf[Component]
+
+ focusList = c.asInstanceOf[Component].peer :: focusList
+ }
+ case _ =>
+ })
+
+ {
+ val t = this
+ contents += Swing.HGlue
+ contents += Swing.RigidBox(new Dimension(10, 0))
+
+ if (show_color_chooser) {
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Color") {
+ t.background =
+ JColorChooser.showDialog(t.peer, "Choose new Color", t.background)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ }
+
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Up") {
+ movePanelUp(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Down") {
+ movePanelDown(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ contents += Swing.RigidBox(new Dimension(2, 0))
+ contents += new Button {
+ maximumSize = new Dimension(20, 20)
+
+ action = Action("Del") {
+ removePanel(t)
+ }
+
+ focusList = this.peer :: focusList
+ }
+ }
+
+ focusList = focusList.reverse
+
+ private def isRegex(regex: String): Boolean = {
+ try {
+ regex.r
+
+ true
+ } catch {
+ case _: java.util.regex.PatternSyntaxException => false
+ }
+ }
+
+ def get_Mutator_Markup: Mutator_Markup = {
+ def regexOrElse(regex: String, orElse: String): String = {
+ if (isRegex(regex)) regex
+ else orElse
+ }
+
+ val m = _mutator match {
+ case Identity() =>
+ Identity()
+ case Node_Expression(r, _, _, _) =>
+ Node_Expression(
+ regexOrElse(inputs(2)._2.getString, r),
+ inputs(3)._2.getBool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.getBool,
+ inputs(0)._2.getBool
+ )
+ case Node_List(_, _, _, _) =>
+ Node_List(
+ inputs(2)._2.getString.split(',').filter(_ != "").toList,
+ inputs(3)._2.getBool,
+ // "Parents" means "Show parents" or "Matching Children"
+ inputs(1)._2.getBool,
+ inputs(0)._2.getBool
+ )
+ case Edge_Endpoints(_, _) =>
+ Edge_Endpoints(
+ inputs(0)._2.getString,
+ inputs(1)._2.getString
+ )
+ case Edge_Transitive() =>
+ Edge_Transitive()
+ case Add_Node_Expression(r) =>
+ Add_Node_Expression(
+ regexOrElse(inputs(0)._2.getString, r)
+ )
+ case Add_Transitive_Closure(_, _) =>
+ Add_Transitive_Closure(
+ inputs(0)._2.getBool,
+ inputs(1)._2.getBool
+ )
+ case _ =>
+ Identity()
+ }
+
+ (enabledBox.selected, background, m)
+ }
+
+ private def get_Inputs(): List[(String, Mutator_Input_Value)] = _mutator match {
+ case Node_Expression(regex, reverse, check_parents, check_children) =>
+ List(
+ ("", new iCheckBox("Parents", check_children)),
+ ("", new iCheckBox("Children", check_parents)),
+ ("Regex", new iTextField(regex, x => !isRegex(x))),
+ ("", new iCheckBox(reverse_caption, reverse))
+ )
+ case Node_List(list, reverse, check_parents, check_children) =>
+ List(
+ ("", new iCheckBox("Parents", check_children)),
+ ("", new iCheckBox("Children", check_parents)),
+ ("Names", new iTextField(list.mkString(","))),
+ ("", new iCheckBox(reverse_caption, reverse))
+ )
+ case Edge_Endpoints(source, dest) =>
+ List(
+ ("Source", new iTextField(source)),
+ ("Destination", new iTextField(dest))
+ )
+ case Add_Node_Expression(regex) =>
+ List(
+ ("Regex", new iTextField(regex, x => !isRegex(x)))
+ )
+ case Add_Transitive_Closure(parents, children) =>
+ List(
+ ("", new iCheckBox("Parents", parents)),
+ ("", new iCheckBox("Children", children))
+ )
+ case _ => Nil
+ }
+ }
+
+ private trait Mutator_Input_Value
+ {
+ def getString: String
+ def getBool: Boolean
+ }
+
+ private class iTextField(t: String, colorator: String => Boolean)
+ extends TextField(t) with Mutator_Input_Value
+ {
+ def this(t: String) = this(t, x => false)
+
+ preferredSize = new Dimension(125, 18)
+
+ reactions += {
+ case ValueChanged(_) =>
+ if (colorator(text))
+ background = Color.RED
+ else
+ background = Color.WHITE
+ }
+
+ def getString = text
+ def getBool = true
+ }
+
+ private class iCheckBox(t: String, s: Boolean)
+ extends CheckBox(t) with Mutator_Input_Value
+ {
+ selected = s
+
+ def getString = ""
+ def getBool = selected
+ }
+
+ private object focusTraversal
+ extends FocusTraversalPolicy
+ {
+ private var items = Vector[java.awt.Component]()
+
+ def add(c: java.awt.Component) {
+ items = items :+ c
+ }
+ def addAll(cs: TraversableOnce[java.awt.Component]) {
+ items = items ++ cs
+ }
+ def clear() {
+ items = Vector[java.awt.Component]()
+ }
+
+ def getComponentAfter(root: java.awt.Container,
+ c: java.awt.Component): java.awt.Component = {
+ val i = items.indexOf(c)
+ if (i < 0) {
+ getDefaultComponent(root)
+ } else {
+ items((i + 1) % items.length)
+ }
+ }
+
+ def getComponentBefore(root: java.awt.Container,
+ c: java.awt.Component): java.awt.Component = {
+ val i = items.indexOf(c)
+ if (i < 0) {
+ getDefaultComponent(root)
+ } else {
+ items((i - 1) % items.length)
+ }
+ }
+
+ def getFirstComponent(root: java.awt.Container): java.awt.Component = {
+ if (items.length > 0)
+ items(0)
+ else
+ null
+ }
+
+ def getDefaultComponent(root: java.awt.Container)
+ : java.awt.Component = getFirstComponent(root)
+
+ def getLastComponent(root: java.awt.Container): java.awt.Component = {
+ if (items.length > 0)
+ items.last
+ else
+ null
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/mutator_event.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,20 @@
+/* Title: Tools/Graphview/src/mutator_event.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Events for dialog synchronization.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.Color
+
+
+object Mutator_Event
+{
+ type Mutator_Markup = (Boolean, Color, Mutator)
+
+ sealed abstract class Message
+ case class Add(m: Mutator_Markup) extends Message
+ case class NewList(m: List[Mutator_Markup]) extends Message
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/parameters.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,45 @@
+/* Title: Tools/Graphview/src/parameters.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Visual parameters with fallbacks for non-jEdit-environment.
+*/
+
+package isabelle.graphview
+
+import isabelle._
+
+import java.awt.Color
+
+
+object Parameters
+{
+ val font_family: String = "IsabelleText"
+ val font_size: Int = 16
+
+ object Colors {
+ val Filter_Colors = List(
+
+ new Color(0xD9, 0xF2, 0xE2), //blue
+ new Color(0xFF, 0xE7, 0xD8), //orange
+ new Color(0xFF, 0xFF, 0xE5), //yellow
+ new Color(0xDE, 0xCE, 0xFF), //lilac
+ new Color(0xCC, 0xEB, 0xFF), //turquoise
+ new Color(0xFF, 0xE5, 0xE5), //red
+ new Color(0xE5, 0xE5, 0xD9) //green
+ )
+
+ private var curr : Int = -1
+ def next = {
+ this.synchronized {
+ curr = (curr + 1) % Filter_Colors.length
+ Filter_Colors(curr)
+ }
+ }
+
+ val Default = Color.WHITE
+ val No_Axioms = Color.LIGHT_GRAY
+ }
+
+ var long_names = true
+ var arrow_heads = false
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/popups.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,176 @@
+/* Title: Tools/Graphview/src/popups.scala
+ Author: Markus Kaiser, TU Muenchen
+
+PopupMenu generation for graph components.
+*/
+
+package isabelle.graphview
+
+
+import isabelle._
+import isabelle.graphview.Mutators._
+import javax.swing.JPopupMenu
+import scala.swing.{Action, Menu, MenuItem, Separator}
+
+
+object Popups {
+ def apply(panel: Graph_Panel, under_mouse: Option[String],
+ selected: List[String]): JPopupMenu =
+ {
+ val add_mutator = panel.visualizer.model.Mutators.add _
+ val curr = panel.visualizer.model.current
+
+ def filter_context(ls: List[String], reverse: Boolean,
+ caption: String, edges: Boolean) =
+ new Menu(caption) {
+ contents += new MenuItem(new Action("This") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, false, false)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Family") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, true, true)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Parents") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, false, true)
+ )
+ )
+ })
+
+ contents += new MenuItem(new Action("Children") {
+ def apply =
+ add_mutator(
+ Mutators.create(
+ Node_List(ls, reverse, true, false)
+ )
+ )
+ })
+
+
+ if (edges) {
+ val outs = ls.map(l => (l, curr.imm_succs(l)))
+ .filter(_._2.size > 0).sortBy(_._1)
+ val ins = ls.map(l => (l, curr.imm_preds(l)))
+ .filter(_._2.size > 0).sortBy(_._1)
+
+ if (outs.nonEmpty || ins.nonEmpty) {
+ contents += new Separator()
+
+ contents += new Menu("Edge") {
+ if (outs.nonEmpty) {
+ contents += new MenuItem("From...") {
+ enabled = false
+ }
+
+ outs.map( e => {
+ val (from, tos) = e
+ contents += new Menu(from) {
+ contents += new MenuItem("To..."){
+ enabled = false
+ }
+
+ tos.toList.sorted.distinct.map( to => {
+ contents += new MenuItem(new Action(to) {
+ def apply =
+ add_mutator(
+ Mutators.create(Edge_Endpoints(from, to))
+ )
+ })
+ })
+ }
+ })
+ }
+ if (outs.nonEmpty && ins.nonEmpty) {
+ contents += new Separator()
+ }
+ if (ins.nonEmpty) {
+ contents += new MenuItem("To...") {
+ enabled = false
+ }
+
+ ins.map( e => {
+ val (to, froms) = e
+ contents += new Menu(to) {
+ contents += new MenuItem("From..."){
+ enabled = false
+ }
+
+ froms.toList.sorted.distinct.map( from => {
+ contents += new MenuItem(new Action(from) {
+ def apply =
+ add_mutator(
+ Mutators.create(Edge_Endpoints(from, to))
+ )
+ })
+ })
+ }
+ })
+ }
+ }
+ }
+ }
+ }
+
+ val popup = new JPopupMenu()
+
+ popup.add(new MenuItem(new Action("Remove all filters") {
+ def apply = panel.visualizer.model.Mutators(Nil)
+ }).peer
+ )
+ popup.add(new MenuItem(new Action("Remove transitive edges") {
+ def apply = add_mutator(Mutators.create(Edge_Transitive()))
+ }).peer
+ )
+ popup.add(new JPopupMenu.Separator)
+
+ if (under_mouse.isDefined) {
+ val v = under_mouse.get
+ popup.add(new MenuItem("Mouseover: %s".format(panel.visualizer.Caption(v))) {
+ enabled = false
+ }.peer)
+
+ popup.add(filter_context(List(v), true, "Hide", true).peer)
+ popup.add(filter_context(List(v), false, "Show only", false).peer)
+
+ popup.add(new JPopupMenu.Separator)
+ }
+ if (!selected.isEmpty) {
+ val text = {
+ if (selected.length > 1) {
+ "Multiple"
+ } else {
+ panel.visualizer.Caption(selected.head)
+ }
+ }
+
+ popup.add(new MenuItem("Selected: %s".format(text)) {
+ enabled = false
+ }.peer)
+
+ popup.add(filter_context(selected, true, "Hide", true).peer)
+ popup.add(filter_context(selected, false, "Show only", false).peer)
+ popup.add(new JPopupMenu.Separator)
+ }
+
+
+ popup.add(new MenuItem(new Action("Fit to Window") {
+ def apply = panel.fit_to_window()
+ }).peer
+ )
+
+ popup
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/shapes.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,250 @@
+/* Title: Tools/Graphview/src/shapes.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Drawable shapes.
+*/
+
+package isabelle.graphview
+
+
+import java.awt.{BasicStroke, Graphics2D, Shape}
+import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D}
+
+
+object Shapes {
+ trait Node {
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]): Shape
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]): Unit
+ }
+
+ object Growing_Node extends Node {
+ private val stroke =
+ new BasicStroke(3, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]) = {
+ val caption = vis.Caption(peer.get)
+ val bounds = g.getFontMetrics.getStringBounds(caption, g)
+ val (x, y) = vis.Coordinates(peer.get)
+
+ new Rectangle2D.Double(
+ x -(bounds.getWidth / 2 + 25),
+ y -(bounds.getHeight / 2 + 5),
+ bounds.getWidth + 50,
+ bounds.getHeight + 10
+ )
+ }
+
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]) {
+ val caption = vis.Caption(peer.get)
+ val bounds = g.getFontMetrics.getStringBounds(caption, g)
+ val s = shape(g, vis, peer)
+
+ val (border, background, foreground) = vis.Color(peer)
+ g.setStroke(stroke)
+ g.setColor(border)
+ g.draw(s)
+ g.setColor(background)
+ g.fill(s)
+ g.setColor(foreground)
+ g.drawString(caption,
+ (s.getCenterX + (-bounds.getWidth / 2)).toFloat,
+ (s.getCenterY + 5).toFloat
+ )
+ }
+ }
+
+ object Dummy extends Node {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+ private val shape = new Rectangle2D.Double(-8, -8, 16, 16)
+ private val identity = new AffineTransform()
+
+ def shape(g: Graphics2D, vis: Visualizer, peer: Option[String]) = shape
+
+ def paint(g: Graphics2D, vis: Visualizer, peer: Option[String]) =
+ paint_transformed(g, vis, peer, identity)
+
+ def paint_transformed(g: Graphics2D, vis: Visualizer,
+ peer: Option[String], at: AffineTransform) = {
+ val (border, background, foreground) = vis.Color(peer)
+ g.setStroke(stroke)
+ g.setColor(border)
+ g.draw(at.createTransformedShape(shape))
+ }
+ }
+
+ trait Edge {
+ def paint(g: Graphics2D, vis: Visualizer, peer: (String, String),
+ head: Boolean, dummies: Boolean)
+ }
+
+ object Straight_Edge extends Edge {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+
+ def paint(g: Graphics2D, vis: Visualizer,
+ peer: (String, String), head: Boolean, dummies: Boolean) {
+ val ((fx, fy), (tx, ty)) =
+ (vis.Coordinates(peer._1), vis.Coordinates(peer._2))
+ val ds = {
+ val (min, max) = (math.min(fy, ty), math.max(fy, ty))
+
+ vis.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+ }
+ val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+
+ path.moveTo(fx, fy)
+ ds.foreach({case (x, y) => path.lineTo(x, y)})
+ path.lineTo(tx, ty)
+
+ if (dummies) {
+ ds.foreach({
+ case (x, y) => {
+ val at = AffineTransform.getTranslateInstance(x, y)
+ Dummy.paint_transformed(g, vis, None, at)
+ }
+ })
+ }
+
+ g.setStroke(stroke)
+ g.setColor(vis.Color(peer))
+ g.draw(path)
+
+ if (head) Arrow_Head.paint(g, path, vis.Drawer.shape(g, Some(peer._2)))
+ }
+ }
+
+ object Cardinal_Spline_Edge extends Edge {
+ private val stroke =
+ new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
+ private val slack = 0.1
+
+ def paint(g: Graphics2D, vis: Visualizer,
+ peer: (String, String), head: Boolean, dummies: Boolean) {
+ val ((fx, fy), (tx, ty)) =
+ (vis.Coordinates(peer._1), vis.Coordinates(peer._2))
+ val ds = {
+ val (min, max) = (math.min(fy, ty), math.max(fy, ty))
+
+ vis.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+ }
+
+ if (ds.isEmpty) Straight_Edge.paint(g, vis, peer, head, dummies)
+ else {
+ val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
+ path.moveTo(fx, fy)
+
+ val coords = ((fx, fy) :: ds ::: List((tx, ty)))
+ val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+
+ val (dx2, dy2) =
+ ((dx, dy) /: coords.sliding(3))({
+ case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
+ val (dx2, dy2) = (rx - lx, ry - ly)
+
+ path.curveTo(lx + slack * dx , ly + slack * dy,
+ mx - slack * dx2, my - slack * dy2,
+ mx , my)
+ (dx2, dy2)
+ }
+ })
+
+ val (lx, ly) = ds.last
+ path.curveTo(lx + slack * dx2, ly + slack * dy2,
+ tx - slack * dx2, ty - slack * dy2,
+ tx , ty)
+
+ if (dummies) {
+ ds.foreach({
+ case (x, y) => {
+ val at = AffineTransform.getTranslateInstance(x, y)
+ Dummy.paint_transformed(g, vis, None, at)
+ }
+ })
+ }
+
+ g.setStroke(stroke)
+ g.setColor(vis.Color(peer))
+ g.draw(path)
+
+ if (head) Arrow_Head.paint(g, path, vis.Drawer.shape(g, Some(peer._2)))
+ }
+ }
+ }
+
+ object Arrow_Head {
+ type Point = (Double, Double)
+
+ private def position(path: GeneralPath,
+ shape: Shape): Option[AffineTransform] = {
+ def intersecting_line(path: GeneralPath,
+ shape: Shape): Option[(Point, Point)] = {
+ import java.awt.geom.PathIterator
+
+ val i = path.getPathIterator(null, 1d)
+ var seg = Array[Double](0,0,0,0,0,0)
+ var p1 = (0d, 0d)
+ var p2 = (0d, 0d)
+ while (!i.isDone()) {
+ i.currentSegment(seg) match {
+ case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
+ case PathIterator.SEG_LINETO => {
+ p1 = p2
+ p2 = (seg(0), seg(1))
+
+ if(shape.contains(seg(0), seg(1)))
+ return Some((p1, p2))
+ }
+ case _ =>
+ }
+ i.next()
+ }
+
+ None
+ }
+
+ def binary_search(line: (Point, Point),
+ shape: Shape): Option[AffineTransform] = {
+ val ((fx, fy), (tx, ty)) = line
+ if (shape.contains(fx, fy) == shape.contains(tx, ty))
+ None
+ else {
+ val (dx, dy) = (fx - tx, fy - ty)
+ if ( (dx * dx + dy * dy) < 1d ) {
+ val at = AffineTransform.getTranslateInstance(fx, fy)
+ at.rotate(- (math.atan2(dx, dy) + math.Pi / 2))
+ Some(at)
+ } else {
+ val (mx, my) = (fx + (tx - fx) / 2d, fy + (ty - fy) / 2d)
+ if (shape.contains(fx, fy) == shape.contains(mx, my))
+ binary_search(((mx, my), (tx, ty)), shape)
+ else
+ binary_search(((fx, fy), (mx, my)), shape)
+ }
+ }
+ }
+
+ intersecting_line(path, shape) match {
+ case None => None
+ case Some(line) => binary_search(line, shape)
+ }
+ }
+
+ def paint(g: Graphics2D, path: GeneralPath, shape: Shape) {
+ position(path, shape) match {
+ case None =>
+ case Some(at) => {
+ val arrow = new GeneralPath(Path2D.WIND_EVEN_ODD, 3)
+ arrow.moveTo(0, 0)
+ arrow.lineTo(-20, 8)
+ arrow.lineTo(-13, 0)
+ arrow.lineTo(-20, -8)
+ arrow.lineTo(0, 0)
+ arrow.transform(at)
+
+ g.fill(arrow)
+ }
+ }
+ }
+ }
+}
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/Graphview/src/visualizer.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,169 @@
+/* Title: Tools/Graphview/src/visualizer.scala
+ Author: Markus Kaiser, TU Muenchen
+
+Graph visualization interface.
+*/
+
+package isabelle.graphview
+
+import isabelle._
+
+import java.awt.{RenderingHints, Graphics2D}
+
+
+class Visualizer(val model: Model) {
+ object Coordinates {
+ private var nodes = Map[String, (Double, Double)]()
+ private var dummies = Map[(String, String), List[(Double, Double)]]()
+
+ def apply(k: String): (Double, Double) = nodes.get(k) match {
+ case Some(c) => c
+ case None => (0, 0)
+ }
+
+ def apply(e: (String, String)): List[(Double, Double)] = dummies.get(e) match {
+ case Some(ds) => ds
+ case None => Nil
+ }
+
+ def translate(k: String, by: (Double, Double)) {
+ val ((x, y), (dx, dy)) = (Coordinates(k), by)
+ reposition(k, (x + dx, y + dy))
+ }
+
+ def reposition(k: String, to: (Double, Double)) {
+ nodes += (k -> to)
+ }
+
+ def translate(d: ((String, String), Int), by: (Double, Double)) {
+ val ((e, i),(dx, dy)) = (d, by)
+ val (x, y) = apply(e)(i)
+ reposition(d, (x + dx, y + dy))
+ }
+
+ def reposition(d: ((String, String), Int), to: (Double, Double)) {
+ val (e, index) = d
+ dummies.get(e) match {
+ case None =>
+ case Some(ds) =>
+ dummies += ( e ->
+ (ds.zipWithIndex :\ List[(Double, Double)]()){
+ case ((t, i), n) => if (index == i) to :: n
+ else t :: n
+ }
+ )
+ }
+ }
+
+ def layout() {
+ val (l, d) = Layout_Pendulum(model.current)
+ nodes = l
+ dummies = d
+ }
+
+ def bounds(): (Double, Double, Double, Double) =
+ model.visible_nodes().toList match {
+ case Nil => (0, 0, 0, 0)
+ case nodes => {
+ val X: (String => Double) = {n => apply(n)._1}
+ val Y: (String => Double) = {n => apply(n)._2}
+
+ (X(nodes.minBy(X)), Y(nodes.minBy(Y)),
+ X(nodes.maxBy(X)), Y(nodes.maxBy(Y)))
+ }
+ }
+ }
+
+ private val visualizer = this
+ object Drawer {
+ import Shapes._
+ import java.awt.Shape
+
+ def apply(g: Graphics2D, n: Option[String]) = n match {
+ case None =>
+ case Some(_) => Growing_Node.paint(g, visualizer, n)
+ }
+
+ def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean) = {
+ Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
+ }
+
+ def paint_all_visible(g: Graphics2D, dummies: Boolean) = {
+ g.setFont(Font())
+ g.setRenderingHints(rendering_hints)
+
+ model.visible_edges().foreach(e => {
+ apply(g, e, Parameters.arrow_heads, dummies)
+ })
+
+ model.visible_nodes().foreach(l => {
+ apply(g, Some(l))
+ })
+ }
+
+ def shape(g: Graphics2D, n: Option[String]): Shape = n match {
+ case None => Dummy.shape(g, visualizer, None)
+ case Some(_) => Growing_Node.shape(g, visualizer, n)
+ }
+ }
+
+ object Selection {
+ private var selected: List[String] = Nil
+
+ def apply() = selected
+ def apply(s: String) = selected.contains(s)
+
+ def add(s: String) { selected = s :: selected }
+ def set(ss: List[String]) { selected = ss }
+ def clear() { selected = Nil }
+ }
+
+ object Color {
+ import java.awt.{Color => awtColor}
+
+ def apply(l: Option[String]): (awtColor, awtColor, awtColor) = l match {
+ case None => (awtColor.GRAY, awtColor.WHITE, awtColor.BLACK)
+ case Some(c) => {
+ if (Selection(c))
+ (awtColor.BLUE, awtColor.GREEN, awtColor.BLACK)
+ else
+ (awtColor.BLACK,
+ model.colors.getOrElse(c, awtColor.WHITE), awtColor.BLACK)
+ }
+ }
+
+ def apply(e: (String, String)): awtColor = awtColor.BLACK
+ }
+
+ object Caption {
+ def apply(k: String) =
+ if (Parameters.long_names) k
+ else k.split('.').last
+ }
+
+ object Tooltip {
+ def content(name: String): XML.Body = model.complete.get_node(name).content
+
+ def text(name: String, fm: java.awt.FontMetrics): String = // null
+ {
+ val txt = Pretty.string_of(content(name), 76, Pretty.font_metric(fm))
+ if (txt == "") null
+ else
+ "<html><pre style=\"font-family: " + Parameters.font_family + "; font-size: " +
+ Parameters.font_size + "px; \">" + // FIXME proper scaling (!?)
+ HTML.encode(txt) + "</pre></html>"
+ }
+ }
+
+ object Font {
+ import java.awt.{Font => awtFont}
+
+ def apply() = new awtFont(Parameters.font_family,
+ awtFont.BOLD, Parameters.font_size)
+ }
+
+ val rendering_hints =
+ new RenderingHints(
+ RenderingHints.KEY_ANTIALIASING,
+ RenderingHints.VALUE_ANTIALIAS_ON)
+}
\ No newline at end of file
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Sep 26 15:04:15 2012 +0200
@@ -11,6 +11,7 @@
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
+ "src/graphview_dockable.scala"
"src/html_panel.scala"
"src/hyperlink.scala"
"src/isabelle_encoding.scala"
@@ -89,6 +90,7 @@
BUILD_ONLY=false
BUILD_JARS="jars"
+FRESH_OPTION=""
JEDIT_SESSION_DIRS=""
JEDIT_LOGIC="$ISABELLE_LOGIC"
JEDIT_PRINT_MODE=""
@@ -113,6 +115,7 @@
fi
;;
f)
+ FRESH_OPTION="-f"
BUILD_JARS="jars_fresh"
;;
j)
@@ -162,9 +165,13 @@
## dependencies
[ -e "$ISABELLE_HOME/Admin/build" ] && \
- { "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?; }
+ {
+ "$ISABELLE_HOME/Admin/build" "$BUILD_JARS" || exit $?
+ "$ISABELLE_TOOL" graphview -b $FRESH_OPTION || exit $?
+ }
PURE_JAR="$ISABELLE_HOME/lib/classes/ext/Pure.jar"
+GRAPHVIEW_JAR="$ISABELLE_HOME/lib/classes/ext/Graphview.jar"
pushd "$JEDIT_HOME" >/dev/null || failed
@@ -193,9 +200,12 @@
OUTDATED=true
else
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
- declare -a DEPS=("$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+ declare -a DEPS=(
+ "$JEDIT_JAR" "${JEDIT_JARS[@]}"
+ "$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}"
+ )
elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+ declare -a DEPS=("$PURE_JAR" "$GRAPHVIEW_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
else
declare -a DEPS=()
fi
@@ -247,7 +257,8 @@
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
(
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$SCALA_HOME/lib/scala-compiler.jar"
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR" "$GRAPHVIEW_JAR" \
+ "$SCALA_HOME/lib/scala-compiler.jar"
do
CLASSPATH="$CLASSPATH:$JAR"
done
--- a/src/Tools/jEdit/src/Isabelle.props Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Wed Sep 26 15:04:15 2012 +0200
@@ -4,20 +4,20 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
-plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=0.1.0
-plugin.isabelle.jedit.Plugin.description=Isabelle/Isar asynchronous proof document editing
+plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Fabian Immler, Markus Kaiser, Makarius Wenzel
+plugin.isabelle.jedit.Plugin.version=1.0.0
+plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
#system parameters
plugin.isabelle.jedit.Plugin.activate=startup
plugin.isabelle.jedit.Plugin.usePluginHome=false
#dependencies
-plugin.isabelle.jedit.Plugin.depend.0=jdk 1.6
-plugin.isabelle.jedit.Plugin.depend.1=jedit 04.03.99.00
-plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.4.1
-plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.8
-plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 0.8
+plugin.isabelle.jedit.Plugin.depend.0=jdk 1.7
+plugin.isabelle.jedit.Plugin.depend.1=jedit 04.05.02.00
+plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 4.5
+plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 1.9
+plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.3
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
@@ -40,9 +40,10 @@
#menu actions
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
-plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
+plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.output1-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.syslog-panel
isabelle.session-panel.label=Prover Session panel
isabelle.output-panel.label=Output panel
+isabelle.graphview-panel.label=Graphview panel
isabelle.output1-panel.label=Output1 panel
isabelle.raw-output-panel.label=Raw Output panel
isabelle.protocol-panel.label=Protocol panel
@@ -52,6 +53,7 @@
#dockables
isabelle-session.title=Prover Session
isabelle-output.title=Output
+isabelle-graphview.title=Graphview
isabelle-output1.title=Output1
isabelle-raw-output.title=Raw Output
isabelle-protocol.title=Protocol
--- a/src/Tools/jEdit/src/actions.xml Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/actions.xml Wed Sep 26 15:04:15 2012 +0200
@@ -27,6 +27,11 @@
wm.addDockableWindow("isabelle-output1");
</CODE>
</ACTION>
+ <ACTION NAME="isabelle.graphview-panel">
+ <CODE>
+ wm.addDockableWindow("isabelle-graphview");
+ </CODE>
+ </ACTION>
<ACTION NAME="isabelle.raw-output-panel">
<CODE>
wm.addDockableWindow("isabelle-raw-output");
--- a/src/Tools/jEdit/src/dockables.xml Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Wed Sep 26 15:04:15 2012 +0200
@@ -14,6 +14,9 @@
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
+ <DOCKABLE NAME="isabelle-graphview" MOVABLE="TRUE">
+ new isabelle.jedit.Graphview_Dockable(view, position);
+ </DOCKABLE>
<DOCKABLE NAME="isabelle-output1" MOVABLE="TRUE">
new isabelle.jedit.Output1_Dockable(view, position);
</DOCKABLE>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Wed Sep 26 15:04:15 2012 +0200
@@ -0,0 +1,131 @@
+/* Title: Tools/jEdit/src/graphview_dockable.scala
+ Author: Markus Kaiser, TU Muenchen
+ Author: Makarius
+
+Dockable window for graphview.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.BorderLayout
+import javax.swing.JPanel
+
+import scala.actors.Actor._
+
+import org.gjt.sp.jedit.View
+
+
+class Graphview_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ Swing_Thread.require()
+
+
+ /* component state -- owned by Swing thread */
+
+ private val do_update = true // FIXME
+
+ private var current_snapshot = Document.State.init.snapshot()
+ private var current_state = Command.empty.init_state
+ private var current_graph: XML.Body = Nil
+
+
+ /* GUI components */
+
+ private val graphview = new JPanel
+
+ // FIXME mutable GUI content
+ private def set_graphview(graph: XML.Body)
+ {
+ graphview.removeAll()
+ graphview.setLayout(new BorderLayout)
+ val panel = new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph))
+ graphview.add(panel.peer, BorderLayout.CENTER)
+ }
+
+ set_graphview(current_graph)
+ set_content(graphview)
+
+
+ private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
+ {
+ Swing_Thread.require()
+
+ val (new_snapshot, new_state) =
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val snapshot = doc_view.model.snapshot()
+ if (follow && !snapshot.is_outdated) {
+ snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
+ case Some(cmd) =>
+ (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state)
+ }
+ }
+ else (current_snapshot, current_state)
+ case None => (current_snapshot, current_state)
+ }
+
+ val new_graph =
+ if (!restriction.isDefined || restriction.get.contains(new_state.command)) {
+ new_state.markup.cumulate[Option[XML.Body]](
+ new_state.command.range, None, Some(Set(Isabelle_Markup.GRAPHVIEW)),
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.GRAPHVIEW, _), graph))) =>
+ Some(graph)
+ }).filter(_.info.isDefined) match {
+ case Text.Info(_, Some(graph)) #:: _ => graph
+ case _ => Nil
+ }
+ }
+ else current_graph
+
+ if (new_graph != current_graph) set_graphview(new_graph)
+
+ current_snapshot = new_snapshot
+ current_state = new_state
+ current_graph = new_graph
+ }
+
+
+ /* main actor */
+
+ private val main_actor = actor {
+ loop {
+ react {
+ case Session.Global_Options => // FIXME
+
+ case changed: Session.Commands_Changed =>
+ Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
+
+ case Session.Caret_Focus =>
+ Swing_Thread.later { handle_update(do_update, None) }
+
+ case bad =>
+ java.lang.System.err.println("Graphview_Dockable: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ override def init()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options += main_actor
+ Isabelle.session.commands_changed += main_actor
+ Isabelle.session.caret_focus += main_actor
+ handle_update(do_update, None)
+ }
+
+ override def exit()
+ {
+ Swing_Thread.require()
+
+ Isabelle.session.global_options -= main_actor
+ Isabelle.session.commands_changed -= main_actor
+ Isabelle.session.caret_focus -= main_actor
+ }
+}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Sep 26 15:04:15 2012 +0200
@@ -17,8 +17,7 @@
import org.gjt.sp.jedit.View
-class Raw_Output_Dockable(view: View, position: String)
- extends Dockable(view: View, position: String)
+class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val text_area = new TextArea
set_content(new ScrollPane(text_area))
--- a/src/Tools/jEdit/src/readme_dockable.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Wed Sep 26 15:04:15 2012 +0200
@@ -12,7 +12,7 @@
import org.gjt.sp.jedit.View
-class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class README_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val readme = new HTML_Panel("SansSerif", 14)
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
--- a/src/Tools/jEdit/src/session_dockable.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Wed Sep 26 15:04:15 2012 +0200
@@ -21,7 +21,7 @@
import org.gjt.sp.jedit.{View, jEdit}
-class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class Session_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* status */
--- a/src/Tools/jEdit/src/syslog_dockable.scala Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Wed Sep 26 15:04:15 2012 +0200
@@ -12,12 +12,10 @@
import scala.actors.Actor._
import scala.swing.TextArea
-import java.lang.System
-
import org.gjt.sp.jedit.View
-class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* GUI components */
@@ -42,7 +40,7 @@
case output: Isabelle_Process.Output =>
if (output.is_syslog) update_syslog()
- case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
}
}
}
--- a/src/Tools/subtyping.ML Wed Sep 26 10:41:36 2012 +0200
+++ b/src/Tools/subtyping.ML Wed Sep 26 15:04:15 2012 +0200
@@ -908,7 +908,7 @@
Syntax.string_of_typ ctxt T1 ^ "!\n\nCannot add coercion of type: " ^
Syntax.string_of_typ ctxt (T1 --> T2));
val new_edges =
- flat (Graph.dest G'' |> map (fn (x, ys) => ys |> map_filter (fn y =>
+ flat (Graph.dest G'' |> map (fn ((x, _), ys) => ys |> map_filter (fn y =>
if Graph.is_edge G' (x, y) then NONE else SOME (x, y))));
val G_and_new = Graph.add_edge (a, b) G';
@@ -950,9 +950,10 @@
if member (op aconv) ts t then (a, b) :: pairs else pairs) tab [(a, b)];
fun delete pair (G, tab) = (Graph.del_edge pair G, Symreltab.delete_safe pair tab);
val (G', tab') = fold delete pairs (G, tab);
- fun reinsert pair (G, xs) = (case (Graph.irreducible_paths G pair) of
- [] => (G, xs)
- | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
+ fun reinsert pair (G, xs) =
+ (case Graph.irreducible_paths G pair of
+ [] => (G, xs)
+ | _ => (Graph.add_edge pair G, (pair, transitive_coercion ctxt tab' G' pair) :: xs));
val (G'', ins) = fold reinsert pairs (G', []);
in
(fold Symreltab.update ins tab', G'', restrict_graph G'')