# HG changeset patch
# User wenzelm
# Date 1348580441 -7200
# Node ID 26fc70e983c2ff961a7cd93a5cbd5cd2f9ff8005
# Parent  11430dd89e358adc8c6bf6099a0ce3382bb4af33
separate module Graph_Display;
tuned signature;

diff -r 11430dd89e35 -r 26fc70e983c2 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Sep 25 15:40:41 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;
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/General/graph_display.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/graph_display.ML	Tue Sep 25 15:40:41 2012 +0200
@@ -0,0 +1,45 @@
+(*  Title:      Pure/General/graph_display.ML
+    Author:     Makarius
+
+Graph display.
+*)
+
+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: Path.T -> graph -> unit
+  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;
+
+fun write_graph 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));
+
+
+(* display graph *)
+
+fun display_graph graph =
+  let
+    val path = Isabelle_System.create_tmp_path "graph" "";
+    val _ = write_graph path graph;
+    val _ = writeln "Displaying graph ...";
+    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
+  in () end;
+
+end;
+
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 15:40:41 2012 +0200
@@ -403,8 +403,11 @@
         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 class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
@@ -413,11 +416,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)
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Pure/ROOT	Tue Sep 25 15:40:41 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"
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Pure/ROOT.ML	Tue Sep 25 15:40:41 2012 +0200
@@ -250,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";
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Pure/Thy/present.ML	Tue Sep 25 15:40:41 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 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 (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);
diff -r 11430dd89e35 -r 26fc70e983c2 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Tue Sep 25 15:40:41 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 *)
diff -r 11430dd89e35 -r 26fc70e983c2 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Tue Sep 25 14:32:41 2012 +0200
+++ b/src/Tools/Code/code_thingol.ML	Tue Sep 25 15:40:41 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