uniform variable name for presentation graphs, to distinguish from values of type Graph.T
--- a/src/Pure/Isar/isar_cmd.ML Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Wed Dec 31 14:08:50 2014 +0100
@@ -275,7 +275,7 @@
val thy = Toplevel.theory_of state;
val thy_session = Present.session_name thy;
- val gr = rev (Theory.nodes_of thy) |> map (fn node =>
+ val graph = 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);
@@ -285,15 +285,15 @@
{name = name, ID = name, parents = parents, dir = session,
unfold = unfold, path = "", content = []}
end);
- in Graph_Display.display_graph gr end);
+ in Graph_Display.display_graph 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} =>
+ val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
{name = Locale.extern thy name, ID = name, parents = parents,
dir = "", unfold = true, path = "", content = [body]});
- in Graph_Display.display_graph gr end);
+ in Graph_Display.display_graph graph end);
(* print theorems, terms, types etc. *)
--- a/src/Pure/Tools/class_deps.ML Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML Wed Dec 31 14:08:50 2014 +0100
@@ -28,10 +28,10 @@
fun entry (c, (i, (_, cs))) =
(i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
dir = "", unfold = true, path = "", content = []});
- val gr =
+ val graph =
Graph.fold (cons o entry) classes []
|> sort (int_ord o apply2 #1) |> map #2;
- in Graph_Display.display_graph gr end;
+ in Graph_Display.display_graph graph end;
val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
val visualize_cmd = gen_visualize Syntax.read_sort;
--- a/src/Tools/Code/code_thingol.ML Wed Dec 31 14:05:06 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML Wed Dec 31 14:08:50 2014 +0100
@@ -926,10 +926,10 @@
val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
fun namify consts = map (Code.string_of_const thy) consts
|> commas;
- val prgr = map (fn (consts, constss) =>
+ val graph = map (fn (consts, constss) =>
{ name = namify consts, ID = namify consts, dir = "", unfold = true,
path = "", parents = map namify constss, content = [] }) conn;
- in Graph_Display.display_graph prgr end;
+ in Graph_Display.display_graph graph end;
local