# HG changeset patch
# User wenzelm
# Date 1429176156 -7200
# Node ID 8bd5999133d4776926ddd71d4556fca06b2530dd
# Parent  bc57cb0c5001513be743cf6ca8a7a0b5bca9da60
let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);

diff -r bc57cb0c5001 -r 8bd5999133d4 NEWS
--- a/NEWS	Wed Apr 15 22:27:31 2015 +0200
+++ b/NEWS	Thu Apr 16 11:22:36 2015 +0200
@@ -74,10 +74,8 @@
 * Less waste of vertical space via negative line spacing (see Global
 Options / Text Area).
 
-* Improved graphview panel (with optional output of PNG or PDF)
-supersedes the old graph browser from 1996, but the latter remains
-available for some time as a fall-back. The old browser is still
-required for the massive graphs produced by 'thm_deps', for example.
+* Improved graphview panel with optional output of PNG or PDF, for
+display of 'thy_deps', 'locale_deps', 'class_deps' etc.
 
 * Improved scheduling for asynchronous print commands (e.g. provers
 managed by the Sledgehammer panel) wrt. ongoing document processing.
diff -r bc57cb0c5001 -r 8bd5999133d4 src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Wed Apr 15 22:27:31 2015 +0200
+++ b/src/Pure/General/graph_display.ML	Thu Apr 16 11:22:36 2015 +0200
@@ -11,6 +11,7 @@
   val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
   type entry = (string * node) * string list
   val display_graph: entry list -> unit
+  val display_graph_old: entry list -> unit
 end;
 
 structure Graph_Display: GRAPH_DISPLAY =
@@ -30,7 +31,9 @@
 type entry = (string * node) * string list;
 
 
-(* encode graph *)
+(* display graph *)
+
+local
 
 fun encode_node (Node {name, content, ...}) =
   (name, content) |>
@@ -40,9 +43,22 @@
 val encode_graph =
   let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
 
+in
+
+fun display_graph entries =
+  let
+    val ((bg1, bg2), en) =
+      YXML.output_markup_elem
+        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
+  in writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en) end;
+
+end;
+
 
 (* support for old browser *)
 
+local
+
 structure Graph =
   Graph(type key = string * string val ord = prod_ord string_ord string_ord);
 
@@ -71,23 +87,15 @@
     path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
   #> cat_lines;
 
+in
 
-(* display graph *)
-
-fun display_graph entries =
+fun display_graph_old entries =
   let
     val ((bg1, bg2), en) =
       YXML.output_markup_elem
-        (Active.make_markup Markup.graphviewN {implicit = false, properties = []});
-    val _ =
-      writeln ("See " ^ bg1 ^ YXML.string_of_body (encode_graph entries) ^ bg2 ^ "graph" ^ en);
-
-    (*old browser*)
-    val ((bg1, bg2), en) =
-      YXML.output_markup_elem
         (Active.make_markup Markup.browserN {implicit = false, properties = []});
-    val _ =
-      writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "old graph" ^ en);
-  in () end;
+  in writeln ("See " ^ bg1 ^ encode_browser entries ^ bg2 ^ "graph" ^ en) end;
 
 end;
+
+end;
diff -r bc57cb0c5001 -r 8bd5999133d4 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Wed Apr 15 22:27:31 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 11:22:36 2015 +0200
@@ -44,7 +44,7 @@
         else Symtab.update (d, (make_node d "", [])) tab)) entries0 entries0;
   in
     Symtab.fold (fn (name, (node, deps)) => cons ((name, node), deps)) entries1 []
-    |> Graph_Display.display_graph
+    |> Graph_Display.display_graph_old
   end;
 
 val _ =
diff -r bc57cb0c5001 -r 8bd5999133d4 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Apr 15 22:27:31 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Apr 16 11:22:36 2015 +0200
@@ -946,7 +946,7 @@
     |> join_strong_conn
     |> Graph.dest
     |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
-    |> Graph_Display.display_graph
+    |> Graph_Display.display_graph_old
   end;
 
 local