clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names);
tuned;

--- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Pure/General/graph_display.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -9,7 +9,10 @@
   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
+  type entry = (string * node) * string list
+  val eq_entry: entry * entry -> bool
+  type graph = entry list
+  val sort_graph: graph -> graph
   val write_graph_browser: Path.T -> graph -> unit
   val browserN: string
   val graphviewN: string
@@ -20,19 +23,44 @@
 structure Graph_Display: GRAPH_DISPLAY =
 struct
 
-(* abstract graph representation *)
+(* type node *)
 
-type node = {name: string, content: Pretty.T list,
-  unfold: bool, directory: string, path: string};
-
-type graph = string list * node Graph.T;
-  (*partial explicit order in left argument*)
+datatype node =
+  Node of {name: string, content: Pretty.T list, unfold: bool, directory: string, path: string};
 
 fun content_node name content =
-  {name = name, content = content, unfold = true, directory = "", path = ""};
+  Node {name = name, content = content, unfold = true, directory = "", path = ""};
+
+fun session_node {name, unfold, directory, path} =
+  Node {name = name, content = [], unfold = unfold, directory = directory, path = path};
+
+
+(* type graph *)
+
+type entry = (string * node) * string list;
+val eq_entry: entry * entry -> bool = op = o apply2 (#1 o #1);
+
+type graph = entry list;
+
+structure Aux_Graph =
+  Graph(type key = string * string val ord = prod_ord string_ord string_ord);
 
-fun session_node {name: string, unfold: bool, directory: string, path: string} =
-  {name = name, content = [], unfold = unfold, directory = directory, path = path};
+fun sort_graph (graph: graph) =
+  let
+    val ident_names =
+      fold (fn ((ident, Node {name, ...}), _) => Symtab.update_new (ident, (name, ident)))
+        graph Symtab.empty;
+    val the_key = the o Symtab.lookup ident_names;
+    val G =
+      Aux_Graph.empty
+      |> fold (fn ((ident, node), _) => Aux_Graph.new_node (the_key ident, node)) graph
+      |> fold (fn ((ident, _), parents) =>
+          fold (fn parent => Aux_Graph.add_edge (the_key parent, the_key ident)) parents) graph
+  in
+    Aux_Graph.topological_order G |> map (fn key =>
+      let val (_, (node, (preds, _))) = Aux_Graph.get_entry G key
+      in ((#2 key, node), map #2 (Aux_Graph.Keys.dest preds)) end)
+  end;
 
 
 (* print modes *)
@@ -49,41 +77,43 @@
 
 (* encode 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} =>
+val encode_browser =
+  map (fn ((key, Node {name, unfold, content, directory, path}), parents) =>
     "\"" ^ name ^ "\" \"" ^ key ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
-    path ^ "\" > " ^ space_implode " " (map quote (Graph.immediate_succs gr key)) ^ " ;")
-  |> cat_lines;
+    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;")
+  #> cat_lines;
 
-fun write_graph_browser path graph = File.write path (encode_browser graph);
+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_node (Node {name, content, ...}) =
+  (name, content) |>
+    let open XML.Encode
+    in pair string (YXML.parse_body o Pretty.symbolic_string_of o Pretty.chunks) end;
 
-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;
+val encode_graph =
+  let open XML.Encode in list (pair (pair string encode_node) (list string)) end;
 
 
 (* display graph *)
 
-fun display_graph graph =
-  if print_mode_active active_graphN then
-    let
-      val (markup, body) =
-        if is_browser () then (Markup.browserN, encode_browser graph)
-        else (Markup.graphviewN, YXML.string_of_body (encode_graphview graph));
-      val ((bg1, bg2), en) =
-        YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
-    in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
-  else
-    let
-      val _ = writeln "Displaying graph ...";
-      val path = Isabelle_System.create_tmp_path "graph" "";
-      val _ = write_graph_browser path graph;
-      val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
-    in () end;
+val display_graph =
+  sort_graph #> (fn graph =>
+    if print_mode_active active_graphN then
+      let
+        val (markup, body) =
+          if is_browser () then (Markup.browserN, encode_browser graph)
+          else (Markup.graphviewN, YXML.string_of_body (encode_graph graph));
+        val ((bg1, bg2), en) =
+          YXML.output_markup_elem (Active.make_markup markup {implicit = false, properties = []});
+      in writeln ("See " ^ bg1 ^ body ^ bg2 ^ "graph" ^ en) end
+    else
+      let
+        val _ = writeln "Displaying graph ...";
+        val path = Isabelle_System.create_tmp_path "graph" "";
+        val _ = write_graph_browser path graph;
+        val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
+      in () end);
 
 end;

--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -274,27 +274,29 @@
   let
     val thy = Toplevel.theory_of state;
     val thy_session = Present.session_name thy;
-
-    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, Graph_Display.session_node
-         {name = name, directory = session, unfold = unfold, path = ""}), parents)
-      end);
-  in Graph_Display.display_graph (map (fst o fst) gr_nodes, Graph.make gr_nodes) end);
+  in
+    Theory.nodes_of thy
+    |> map (fn thy_node =>
+        let
+          val name = Context.theory_name thy_node;
+          val parents = map Context.theory_name (Theory.parents_of thy_node);
+          val session = Present.session_name thy_node;
+          val node =
+            Graph_Display.session_node
+              {name = name, directory = session, unfold = session = thy_session, path = ""};
+        in ((name, node), parents) end)
+    |> Graph_Display.display_graph
+  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,
-          Graph_Display.content_node (Locale.extern thy name) [body]), parents))
-      |> Graph.make;
-  in Graph_Display.display_graph ([], gr) end);
+  in
+    Locale.pretty_locale_deps thy
+    |> map (fn {name, parents, body} =>
+      ((name, Graph_Display.content_node (Locale.extern thy name) [body]), parents))
+    |> Graph_Display.display_graph
+  end);
 
 
 (* print theorems, terms, types etc. *)

--- a/src/Pure/Thy/present.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Pure/Thy/present.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -75,29 +75,20 @@
     else SOME (Path.appends [Path.parent, Path.parent, Path.basic chapter, Path.basic session, link])
   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 =>
+fun init_graph_entry session thy =
   let
-    val {chapter, name = session_name} = Browser_Info.get thy;
-    val thy_name = Context.theory_name thy;
-    val path =
-      (case theory_link (curr_chapter, curr_session) thy of
-        NONE => ""
-      | SOME p => Path.implode p);
-    val graph_entry =
-     {name = thy_name,
-      ident = ident_of [chapter, session_name] thy_name,
-      directory = session_name,
-      path = path,
-      unfold = false,
-      parents = map ident_of_thy (Theory.parents_of thy)};
-  in (0, graph_entry) end);
-
-fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) =
-  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph;
+    val ident = ident_of_thy thy;
+    val parents = map ident_of_thy (Theory.parents_of thy);
+    val node =
+      Graph_Display.session_node
+       {name = Context.theory_name thy,
+        unfold = false,
+        directory = session_name thy,
+        path =
+          (case theory_link session thy of
+            NONE => ""
+          | SOME p => Path.implode p)};
+  in ((ident, node), parents) end;
 
 
 
@@ -120,7 +111,7 @@
  {theories: theory_info Symtab.table,
   tex_index: (int * string) list,
   html_index: (int * string) list,
-  graph: (int * browser_node) list};
+  graph: Graph_Display.graph};
 
 fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
   {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
@@ -128,7 +119,7 @@
 val empty_browser_info = make_browser_info (Symtab.empty, [], [], []);
 
 fun init_browser_info session thys =
-  make_browser_info (Symtab.empty, [], [], init_graph session thys);
+  make_browser_info (Symtab.empty, [], [], map (init_graph_entry session) thys);
 
 fun map_browser_info f {theories, tex_index, html_index, graph} =
   make_browser_info (f (theories, tex_index, html_index, graph));
@@ -161,7 +152,7 @@
 
 fun add_graph_entry entry =
   change_browser_info (fn (theories, tex_index, html_index, graph) =>
-    (theories, tex_index, html_index, ins_graph_entry entry graph));
+    (theories, tex_index, html_index, update Graph_Display.eq_entry entry graph));
 
 
 
@@ -278,14 +269,6 @@
 
 (* 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;
 
@@ -308,10 +291,10 @@
     fun finish_html (a, {html_source, ...}: theory_info) =
       File.write (Path.append session_prefix (html_path a)) html_source;
 
-    val graph' = finalize_graph graph;
+    val sorted_graph = Graph_Display.sort_graph graph;
     val opt_graphs =
       if doc_graph andalso not (null documents) then
-        SOME (isabelle_browser graph')
+        SOME (isabelle_browser sorted_graph)
       else NONE;
 
     val _ =
@@ -320,7 +303,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) graph';
+        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_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)
@@ -392,15 +375,16 @@
       val html_source = HTML.theory name parent_specs (mk_text ());
 
       val graph_entry =
-       {name = name,
-        ident = ident_of [chapter, session_name] name,
-        directory = session_name,
-        unfold = true,
-        path = Path.implode (html_path name),
-        parents = map ident_of_thy parents};
+        ((ident_of [chapter, session_name] name,
+          Graph_Display.session_node
+           {name = name,
+            directory = session_name,
+            unfold = true,
+            path = Path.implode (html_path name)}),
+          map ident_of_thy parents);
     in
       init_theory_info name (make_theory_info ("", html_source));
-      add_graph_entry (update_time, graph_entry);
+      add_graph_entry graph_entry;
       add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
       add_tex_index (update_time, Latex.theory_entry name);
       Browser_Info.put {chapter = chapter, name = session_name} thy

--- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -6,11 +6,11 @@
 
 signature CLASS_DEPS =
 sig
-  val visualize: Proof.context -> sort -> sort option -> unit
-  val visualize_cmd: Proof.context -> string -> string option -> unit
+  val class_deps: Proof.context -> sort -> sort option -> unit
+  val class_deps_cmd: Proof.context -> string -> string option -> unit
 end;
 
-structure Class_deps: CLASS_DEPS =
+structure Class_Deps: CLASS_DEPS =
 struct
 
 fun gen_visualize prep_sort ctxt raw_super raw_sub =
@@ -19,23 +19,28 @@
     val sub = Option.map (prep_sort ctxt) raw_sub;
     val {classes = (space, original_algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
     fun le_super class = Sorts.sort_le original_algebra ([class], super);
-    val sub_le = case sub of
-      NONE => K true |
-      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 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 sub_le =
+      (case sub of
+        NONE => K true
+      | 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;
+  in
+    Sorts.classes_of algebra
+    |> Graph.dest
+    |> map (fn ((c, _), ds) =>
+        ((c, Graph_Display.content_node (Name_Space.extern ctxt space c) []), ds))
+    |> Graph_Display.display_graph
+  end;
 
-val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
-val visualize_cmd = gen_visualize Syntax.read_sort;
+val class_deps = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
+val class_deps_cmd = gen_visualize Syntax.read_sort;
 
 val _ =
   Outer_Syntax.command @{command_spec "class_deps"} "visualize class dependencies"
-    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (raw_super, raw_sub) =>
-      ((Toplevel.unknown_theory oo Toplevel.keep) (fn st => visualize_cmd (Toplevel.context_of st) raw_super raw_sub))));
+    ((Scan.optional Parse.sort "{}" -- Scan.option Parse.sort) >> (fn (super, sub) =>
+      (Toplevel.unknown_theory o
+       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) super sub))));
 
 end;

--- a/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -38,8 +38,10 @@
               {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;
+  in
+    Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []
+    |> Graph_Display.display_graph
+  end;
 
 val _ =
   Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"

--- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:28:04 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 20:42:45 2014 +0100
@@ -927,12 +927,14 @@
   let
     val thy = Proof_Context.theory_of ctxt;
     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;
+  in
+    code_depgr ctxt consts
+    |> Graph.map (fn c => fn _ => c)
+    |> join_strong_conn
+    |> Graph.dest
+    |> map (fn ((c, cs), ds) => ((c, Graph_Display.content_node (namify cs) []), ds))
+    |> Graph_Display.display_graph
+  end;
 
 local
 
@@ -953,7 +955,7 @@
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.unknown_context o
-      Toplevel.keep (fn state => code_deps_cmd (Toplevel.context_of state) cs)));
+      Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
 
 end;