# HG changeset patch
# User wenzelm
# Date 1420031591 -3600
# Node ID 6b030dc97a4f493492932bf5d2216bb7f60a4c8f
# Parent  36808125e00f38f6e793dc7010e3730900d996ac
more explict and generic field names

diff -r 36808125e00f -r 6b030dc97a4f src/Pure/General/graph_display.ML
--- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Pure/General/graph_display.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -7,7 +7,7 @@
 signature GRAPH_DISPLAY =
 sig
   type node =
-   {name: string, ID: string, dir: string, unfold: bool,
+   {name: string, ident: string, directory: string, unfold: bool,
     path: string, parents: string list, content: Pretty.T list}
   type graph = node list
   val write_graph_browser: Path.T -> graph -> unit
@@ -23,7 +23,7 @@
 (* external graph representation *)
 
 type node =
- {name: string, ID: string, dir: string, unfold: bool,
+ {name: string, ident: string, directory: string, unfold: bool,
   path: string, parents: string list, content: Pretty.T list};
 
 type graph = node list;
@@ -44,8 +44,8 @@
 (* encode graph *)
 
 fun encode_browser (graph: graph) =
-  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
-    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
+  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 write_graph_browser path graph = File.write path (encode_browser graph);
@@ -55,8 +55,8 @@
 
 fun encode_graphview (graph: graph) =
   Graph.empty
-  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
-  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
+  |> 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
   |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
 
 
diff -r 36808125e00f -r 6b030dc97a4f src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -282,7 +282,7 @@
         val session = Present.session_name node;
         val unfold = (session = thy_session);
       in
-       {name = name, ID = name, parents = parents, dir = session,
+       {name = name, ident = name, parents = parents, directory = session,
         unfold = unfold, path = "", content = []}
       end);
   in Graph_Display.display_graph graph end);
@@ -291,8 +291,8 @@
   let
     val thy = Toplevel.theory_of state;
     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]});
+     {name = Locale.extern thy name, ident = name, parents = parents,
+      directory = "", unfold = true, path = "", content = [body]});
   in Graph_Display.display_graph graph end);
 
 
diff -r 36808125e00f -r 6b030dc97a4f src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -86,16 +86,16 @@
       | SOME p => Path.implode p);
     val entry =
      {name = thy_name,
-      ID = ID_of [chapter, session_name] thy_name,
-      dir = session_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);
 
-fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
-  (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
+fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) =
+  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr;
 
 
 
@@ -383,8 +383,8 @@
 
       val graph_entry =
        {name = name,
-        ID = ID_of [chapter, session_name] name,
-        dir = session_name,
+        ident = ID_of [chapter, session_name] name,
+        directory = session_name,
         unfold = true,
         path = Path.implode (html_path name),
         parents = map ID_of_thy parents,
diff -r 36808125e00f -r 6b030dc97a4f src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -26,8 +26,8 @@
       (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, ID = c, parents = Graph.Keys.dest cs,
-            dir = "", unfold = true, path = "", content = []});
+      (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;
diff -r 36808125e00f -r 6b030dc97a4f src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -34,15 +34,15 @@
             val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
             val entry =
               {name = Long_Name.base_name name,
-               ID = name,
-               dir = space_implode "/" (session @ prefix),
+               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 #ID deps) end;
+  in Graph_Display.display_graph (sort_wrt #ident deps) end;
 
 val _ =
   Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
diff -r 36808125e00f -r 6b030dc97a4f src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:08:50 2014 +0100
+++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:13:11 2014 +0100
@@ -927,7 +927,7 @@
     fun namify consts = map (Code.string_of_const thy) consts
       |> commas;
     val graph = map (fn (consts, constss) =>
-      { name = namify consts, ID = namify consts, dir = "", unfold = true,
+      { name = namify consts, ident = namify consts, directory = "", unfold = true,
         path = "", parents = map namify constss, content = [] }) conn;
   in Graph_Display.display_graph graph end;