uniform variable name for presentation graphs, to distinguish from values of type Graph.T
authorwenzelm
Wed Dec 31 14:08:50 2014 +0100 (2014-12-31 ago)
changeset 5920636808125e00f
parent 59205 663794ab87e6
child 59207 6b030dc97a4f
uniform variable name for presentation graphs, to distinguish from values of type Graph.T
src/Pure/Isar/isar_cmd.ML
src/Pure/Tools/class_deps.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:05:06 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:08:50 2014 +0100
     1.3 @@ -275,7 +275,7 @@
     1.4      val thy = Toplevel.theory_of state;
     1.5      val thy_session = Present.session_name thy;
     1.6  
     1.7 -    val gr = rev (Theory.nodes_of thy) |> map (fn node =>
     1.8 +    val graph = rev (Theory.nodes_of thy) |> map (fn node =>
     1.9        let
    1.10          val name = Context.theory_name node;
    1.11          val parents = map Context.theory_name (Theory.parents_of node);
    1.12 @@ -285,15 +285,15 @@
    1.13         {name = name, ID = name, parents = parents, dir = session,
    1.14          unfold = unfold, path = "", content = []}
    1.15        end);
    1.16 -  in Graph_Display.display_graph gr end);
    1.17 +  in Graph_Display.display_graph graph end);
    1.18  
    1.19  val locale_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    1.20    let
    1.21      val thy = Toplevel.theory_of state;
    1.22 -    val gr = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    1.23 +    val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    1.24       {name = Locale.extern thy name, ID = name, parents = parents,
    1.25        dir = "", unfold = true, path = "", content = [body]});
    1.26 -  in Graph_Display.display_graph gr end);
    1.27 +  in Graph_Display.display_graph graph end);
    1.28  
    1.29  
    1.30  (* print theorems, terms, types etc. *)
     2.1 --- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:05:06 2014 +0100
     2.2 +++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:08:50 2014 +0100
     2.3 @@ -28,10 +28,10 @@
     2.4      fun entry (c, (i, (_, cs))) =
     2.5        (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
     2.6              dir = "", unfold = true, path = "", content = []});
     2.7 -    val gr =
     2.8 +    val graph =
     2.9        Graph.fold (cons o entry) classes []
    2.10        |> sort (int_ord o apply2 #1) |> map #2;
    2.11 -  in Graph_Display.display_graph gr end;
    2.12 +  in Graph_Display.display_graph graph end;
    2.13  
    2.14  val visualize = gen_visualize (Type.cert_sort o Proof_Context.tsig_of);
    2.15  val visualize_cmd = gen_visualize Syntax.read_sort;
     3.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:05:06 2014 +0100
     3.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:08:50 2014 +0100
     3.3 @@ -926,10 +926,10 @@
     3.4      val conn = [] |> fold (fn consts => cons (consts, succs consts)) constss;
     3.5      fun namify consts = map (Code.string_of_const thy) consts
     3.6        |> commas;
     3.7 -    val prgr = map (fn (consts, constss) =>
     3.8 +    val graph = map (fn (consts, constss) =>
     3.9        { name = namify consts, ID = namify consts, dir = "", unfold = true,
    3.10          path = "", parents = map namify constss, content = [] }) conn;
    3.11 -  in Graph_Display.display_graph prgr end;
    3.12 +  in Graph_Display.display_graph graph end;
    3.13  
    3.14  local
    3.15