for graph display, prefer graph data structure over list with dependencies;
pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes

--- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/General/graph_display.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -6,10 +6,10 @@
 
 signature GRAPH_DISPLAY =
 sig
-  type node =
-   {name: string, ident: string, directory: string, unfold: bool,
-    path: string, parents: string list, content: Pretty.T list}
-  type graph = node list
+  type node
+  val content_node: string -> Pretty.T list -> node
+  val session_node: {name: string, unfold: bool, directory: string, path: string} -> node
+  type graph = string list * node Graph.T
   val write_graph_browser: Path.T -> graph -> unit
   val browserN: string
   val graphviewN: string
@@ -20,13 +20,19 @@
 structure Graph_Display: GRAPH_DISPLAY =
 struct
 
-(* external graph representation *)
+(* abstract graph representation *)
+
+type node = {name: string, content: Pretty.T list,
+  unfold: bool, directory: string, path: string};
 
-type node =
- {name: string, ident: string, directory: string, unfold: bool,
-  path: string, parents: string list, content: Pretty.T list};
+type graph = string list * node Graph.T;
+  (*partial explicit order in left argument*)
 
-type graph = node list;
+fun content_node name content =
+  {name = name, content = content, unfold = true, directory = "", path = ""};
+
+fun session_node {name: string, unfold: bool, directory: string, path: string} =
+  {name = name, content = [], unfold = unfold, directory = directory, path = path};
 
 
 (* print modes *)
@@ -43,20 +49,21 @@
 
 (* encode graph *)
 
-fun encode_browser (graph: graph) =
-  cat_lines (map (fn {name, ident, directory, unfold, path, parents, ...} =>
-    "\"" ^ name ^ "\" \"" ^ ident ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
-    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
+fun encode_browser ((keys, gr) : graph) =
+  fold_rev (update (op =)) (Graph.keys gr) keys
+  |> map (fn key => case Graph.get_node gr key of {name, unfold, content, directory, path} =>
+    "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
+    path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;")
+  |> cat_lines;
 
 fun write_graph_browser path graph = File.write path (encode_browser graph);
 
 
 val encode_content = YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks;
 
-fun encode_graphview (graph: graph) =
-  Graph.empty
-  |> fold (fn {ident, name, content, ...} => Graph.new_node (ident, (name, content))) graph
-  |> fold (fn {ident = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
+fun encode_graphview ((_, gr): graph) =
+  gr
+  |> Graph.map (fn _ => fn {name, content, ...} => (name, content))
   |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
 
 
@@ -80,4 +87,3 @@
     in () end;
 
 end;
-

--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -275,25 +275,26 @@
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
 
-    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
+    val gr_nodes = rev (Theory.nodes_of thy) |> map (fn node =>
       let
         val name = Context.theory_name node;
         val parents = map Context.theory_name (Theory.parents_of node);
         val session = Present.session_name node;
         val unfold = (session = thy_session);
       in
-       {name = name, ident = name, parents = parents, directory = session,
-        unfold = unfold, path = "", content = []}
+       ((name, Graph_Display.session_node
+         {name = name, directory = session, unfold = unfold, path = ""}), parents)
       end);
-  in Graph_Display.display_graph graph end);
+  in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end);
 
 val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
-    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
-     {name = Locale.extern thy name, ident = name, parents = parents,
-      directory = "", unfold = true, path = "", content = [body]});
-  in Graph_Display.display_graph graph end);
+    val gr = Locale.pretty_locale_deps thy
+      |> map (fn {name, parents, body} => ((name,
+          Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+      |> Graph.make;
+  in Graph_Display.display_graph ([], gr) end);
 
 
 (* print theorems, terms, types etc. *)

--- a/src/Pure/Thy/present.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -76,6 +76,9 @@
   end;
 
 (*retrieve graph data from initial collection of theories*)
+type browser_node = {name: string, ident: string, parents: string list,
+  unfold: bool, directory: string, path: string}
+
 fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
   let
     val {chapter, name = session_name} = Browser_Info.get thy;
@@ -84,18 +87,17 @@
       (case theory_link (curr_chapter, curr_session) thy of
         NONE => ""
       | SOME p => Path.implode p);
-    val entry =
+    val graph_entry =
      {name = thy_name,
       ident = ID_of [chapter, session_name] thy_name,
       directory = session_name,
       path = path,
       unfold = false,
-      parents = map ID_of_thy (Theory.parents_of thy),
-      content = []};
-  in (0, entry) end);
+      parents = map ID_of_thy (Theory.parents_of thy)};
+  in (0, graph_entry) end);
 
-fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) =
-  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr;
+fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) =
+  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph;
 
 
 
@@ -118,7 +120,7 @@
  {theories: theory_info Symtab.table,
   tex_index: (int * string) list,
   html_index: (int * string) list,
-  graph: (int * Graph_Display.node) list};
+  graph: (int * browser_node) list};
 
 fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
   {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
@@ -276,6 +278,14 @@
 
 (* finish session -- output all generated text *)
 
+fun finalize_graph (nodes : (int * browser_node) list) =
+  nodes
+  |> map (fn (_, {ident, parents, name, unfold, directory, path}) =>
+      ((ident, Graph_Display.session_node
+        {name = name, unfold = unfold, directory = directory, path = path}), parents))
+  |> Graph.make
+  |> pair (map (#ident o snd) (sort (int_ord o apply2 fst) (rev nodes)));
+
 fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
 fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
 
@@ -298,10 +308,10 @@
     fun finish_html (a, {html_source, ...}: theory_info) =
       File.write (Path.append session_prefix (html_path a)) html_source;
 
-    val sorted_graph = sorted_index graph;
+    val graph' = finalize_graph graph;
     val opt_graphs =
       if doc_graph andalso not (null documents) then
-        SOME (isabelle_browser sorted_graph)
+        SOME (isabelle_browser graph')
       else NONE;
 
     val _ =
@@ -310,7 +320,7 @@
         File.write_buffer (Path.append session_prefix index_path)
           (index_buffer html_index |> Buffer.add HTML.end_document);
         (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
-        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
+        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) graph';
         Isabelle_System.isabelle_tool "browser" "-b";
         Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
         List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
@@ -387,8 +397,7 @@
         directory = session_name,
         unfold = true,
         path = Path.implode (html_path name),
-        parents = map ID_of_thy parents,
-        content = []};
+        parents = map ID_of_thy parents};
     in
       init_theory_info name (make_theory_info ("", html_source));
       add_graph_entry (update_time, graph_entry);

--- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -24,14 +24,11 @@
       SOME sub => fn class => Sorts.sort_le original_algebra (sub, [class]);
     val (_, algebra) = Sorts.subalgebra (Context.pretty ctxt)
       (le_super andf sub_le) (K NONE) original_algebra;
-    val classes = Sorts.classes_of algebra;
-    fun entry (c, (i, (_, cs))) =
-      (i, {name = Name_Space.extern ctxt space c, ident = c, parents = Graph.Keys.dest cs,
-            directory = "", unfold = true, path = "", content = []});
-    val graph =
-      Graph.fold (cons o entry) classes []
-      |> sort (int_ord o apply2 #1) |> map #2;
-  in Graph_Display.display_graph graph end;
+    val gr =
+      Sorts.classes_of algebra
+      |> Graph.map (fn c => fn _ =>
+        Graph_Display.content_node (Name_Space.extern ctxt space c) [])
+  in Graph_Display.display_graph ([], gr) end;
 
 val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
 val visualize_cmd = gen_visualize Syntax.read_sort;

--- a/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -31,18 +31,15 @@
                       | session => [session])
                   | NONE => [])
                | _ => ["global"]);
+            val directory = space_implode "/" (session @ prefix);
             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
-            val entry =
-              {name = Long_Name.base_name name,
-               ident = name,
-               directory = space_implode "/" (session @ prefix),
-               unfold = false,
-               path = "",
-               parents = parents,
-               content = []};
-          in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
-  in Graph_Display.display_graph (sort_wrt #ident deps) end;
+          in
+            cons ((name, Graph_Display.session_node
+              {name = Long_Name.base_name name, directory = directory,
+                unfold = false, path = ""}), parents)
+          end;
+    val gr = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
+  in Graph_Display.display_graph (sort_wrt I (map (fst o fst) gr), Graph.make gr) end;
 
 val _ =
   Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"

--- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:13:11 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:15:52 2014 +0100
@@ -911,25 +911,28 @@
 
 fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
 
+fun join_strong_conn gr =
+  let
+    val xss = Graph.strong_conn gr;
+    val xss_zs = map (fn xs => (xs, commas xs)) xss;
+    val z_for = the o AList.lookup (op =) (maps (fn (xs, z) => map (fn x => (x, z)) xs) xss_zs);
+    val succs = map (fn (xs, z) => (z, (map z_for o maps (Graph.immediate_succs gr)) xs)) xss_zs;
+  in
+    Graph.empty
+    |> fold (fn (xs, z) => Graph.new_node (z, map (Graph.get_node gr) xs)) xss_zs
+    |> fold (fn (z, succs) => fold (fn w => Graph.add_edge (z, w)) succs) succs
+  end;
+
 fun code_deps ctxt consts =
   let
     val thy = Proof_Context.theory_of ctxt;
-    val eqngr = code_depgr ctxt consts;
-    val constss = Graph.strong_conn eqngr;
-    val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
-      Symtab.update (const, consts)) consts) constss;
-    fun succs consts = consts
-      |> maps (Graph.immediate_succs eqngr)
-      |> subtract (op =) consts
-      |> map (the o Symtab.lookup mapping)
-      |> distinct (op =);
-    val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
-    fun namify consts = map (Code.string_of_const thy) consts
-      |> commas;
-    val graph = map (fn (consts, constss) =>
-      { name = namify consts, ident = namify consts, directory = "", unfold = true,
-        path = "", parents = map namify constss, content = [] }) conn;
-  in Graph_Display.display_graph graph end;
+    val namify = commas o map (Code.string_of_const thy);
+    val gr =
+      code_depgr ctxt consts
+      |> Graph.map (fn c => fn _ => c)
+      |> join_strong_conn 
+      |> Graph.map (fn _ => fn cs => Graph_Display.content_node (namify cs) [])
+  in Graph_Display.display_graph ([], gr) end;
 
 local