# HG changeset patch
# User wenzelm
# Date 1158599569 -7200
# Node ID a96883a6d709ece285d17c7b7e8b528d86cc3cba
# Parent  8b1591393b8d44a5400f74fc7363ae34ce16f04c
added display_graph (from thm_deps.ML);

diff -r 8b1591393b8d -r a96883a6d709 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Sep 18 19:12:48 2006 +0200
+++ b/src/Pure/Thy/present.ML	Mon Sep 18 19:12:49 2006 +0200
@@ -17,6 +17,8 @@
   val get_info: theory -> {name: string, session: string list, is_local: bool}
   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
   val init: bool -> bool -> string -> bool -> string list -> string list ->
     string -> (bool * Path.T) option -> Url.T option * bool -> bool -> unit
   val finish: unit -> unit
@@ -103,6 +105,15 @@
     "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
     path ^ "\" > " ^ space_implode " " (map Library.quote parents) ^ " ;") gr));
 
+fun display_graph gr =
+  let
+    val _ = writeln "Generating graph ...";
+    val path = File.tmp_path (Path.unpack "tmp.graph");
+    val _ = write_graph gr path;
+    val _ = File.isatool ("browser -c " ^ File.shell_path path ^ " &");
+  in () end;
+
+
 fun ID_of sess s = space_implode "/" (sess @ [s]);
 
 (*retrieve graph data from initial theory loader database*)