more explict and generic field names
authorwenzelm
Wed Dec 31 14:13:11 2014 +0100 (2014-12-31)
changeset 592076b030dc97a4f
parent 59206 36808125e00f
child 59208 2486d625878b
more explict and generic field names
src/Pure/General/graph_display.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Thy/present.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/thm_deps.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Pure/General/graph_display.ML	Wed Dec 31 14:08:50 2014 +0100
     1.2 +++ b/src/Pure/General/graph_display.ML	Wed Dec 31 14:13:11 2014 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature GRAPH_DISPLAY =
     1.5  sig
     1.6    type node =
     1.7 -   {name: string, ID: string, dir: string, unfold: bool,
     1.8 +   {name: string, ident: string, directory: string, unfold: bool,
     1.9      path: string, parents: string list, content: Pretty.T list}
    1.10    type graph = node list
    1.11    val write_graph_browser: Path.T -> graph -> unit
    1.12 @@ -23,7 +23,7 @@
    1.13  (* external graph representation *)
    1.14  
    1.15  type node =
    1.16 - {name: string, ID: string, dir: string, unfold: bool,
    1.17 + {name: string, ident: string, directory: string, unfold: bool,
    1.18    path: string, parents: string list, content: Pretty.T list};
    1.19  
    1.20  type graph = node list;
    1.21 @@ -44,8 +44,8 @@
    1.22  (* encode graph *)
    1.23  
    1.24  fun encode_browser (graph: graph) =
    1.25 -  cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    1.26 -    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.27 +  cat_lines (map (fn {name, ident, directory, unfold, path, parents, ...} =>
    1.28 +    "\"" ^ name ^ "\" \"" ^ ident ^ "\" \"" ^ directory ^ (if unfold then "\" + \"" else "\" \"") ^
    1.29      path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph);
    1.30  
    1.31  fun write_graph_browser path graph = File.write path (encode_browser graph);
    1.32 @@ -55,8 +55,8 @@
    1.33  
    1.34  fun encode_graphview (graph: graph) =
    1.35    Graph.empty
    1.36 -  |> fold (fn {ID, name, content, ...} => Graph.new_node (ID, (name, content))) graph
    1.37 -  |> fold (fn {ID = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.38 +  |> fold (fn {ident, name, content, ...} => Graph.new_node (ident, (name, content))) graph
    1.39 +  |> fold (fn {ident = a, parents = bs, ...} => fold (fn b => Graph.add_edge (b, a)) bs) graph
    1.40    |> let open XML.Encode in Graph.encode string (pair string encode_content) end;
    1.41  
    1.42  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:08:50 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Dec 31 14:13:11 2014 +0100
     2.3 @@ -282,7 +282,7 @@
     2.4          val session = Present.session_name node;
     2.5          val unfold = (session = thy_session);
     2.6        in
     2.7 -       {name = name, ID = name, parents = parents, dir = session,
     2.8 +       {name = name, ident = name, parents = parents, directory = session,
     2.9          unfold = unfold, path = "", content = []}
    2.10        end);
    2.11    in Graph_Display.display_graph graph end);
    2.12 @@ -291,8 +291,8 @@
    2.13    let
    2.14      val thy = Toplevel.theory_of state;
    2.15      val graph = Locale.pretty_locale_deps thy |> map (fn {name, parents, body} =>
    2.16 -     {name = Locale.extern thy name, ID = name, parents = parents,
    2.17 -      dir = "", unfold = true, path = "", content = [body]});
    2.18 +     {name = Locale.extern thy name, ident = name, parents = parents,
    2.19 +      directory = "", unfold = true, path = "", content = [body]});
    2.20    in Graph_Display.display_graph graph end);
    2.21  
    2.22  
     3.1 --- a/src/Pure/Thy/present.ML	Wed Dec 31 14:08:50 2014 +0100
     3.2 +++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:13:11 2014 +0100
     3.3 @@ -86,16 +86,16 @@
     3.4        | SOME p => Path.implode p);
     3.5      val entry =
     3.6       {name = thy_name,
     3.7 -      ID = ID_of [chapter, session_name] thy_name,
     3.8 -      dir = session_name,
     3.9 +      ident = ID_of [chapter, session_name] thy_name,
    3.10 +      directory = session_name,
    3.11        path = path,
    3.12        unfold = false,
    3.13        parents = map ID_of_thy (Theory.parents_of thy),
    3.14        content = []};
    3.15    in (0, entry) end);
    3.16  
    3.17 -fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
    3.18 -  (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
    3.19 +fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) =
    3.20 +  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr;
    3.21  
    3.22  
    3.23  
    3.24 @@ -383,8 +383,8 @@
    3.25  
    3.26        val graph_entry =
    3.27         {name = name,
    3.28 -        ID = ID_of [chapter, session_name] name,
    3.29 -        dir = session_name,
    3.30 +        ident = ID_of [chapter, session_name] name,
    3.31 +        directory = session_name,
    3.32          unfold = true,
    3.33          path = Path.implode (html_path name),
    3.34          parents = map ID_of_thy parents,
     4.1 --- a/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:08:50 2014 +0100
     4.2 +++ b/src/Pure/Tools/class_deps.ML	Wed Dec 31 14:13:11 2014 +0100
     4.3 @@ -26,8 +26,8 @@
     4.4        (le_super andf sub_le) (K NONE) original_algebra;
     4.5      val classes = Sorts.classes_of algebra;
     4.6      fun entry (c, (i, (_, cs))) =
     4.7 -      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
     4.8 -            dir = "", unfold = true, path = "", content = []});
     4.9 +      (i, {name = Name_Space.extern ctxt space c, ident = c, parents = Graph.Keys.dest cs,
    4.10 +            directory = "", unfold = true, path = "", content = []});
    4.11      val graph =
    4.12        Graph.fold (cons o entry) classes []
    4.13        |> sort (int_ord o apply2 #1) |> map #2;
     5.1 --- a/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:08:50 2014 +0100
     5.2 +++ b/src/Pure/Tools/thm_deps.ML	Wed Dec 31 14:13:11 2014 +0100
     5.3 @@ -34,15 +34,15 @@
     5.4              val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
     5.5              val entry =
     5.6                {name = Long_Name.base_name name,
     5.7 -               ID = name,
     5.8 -               dir = space_implode "/" (session @ prefix),
     5.9 +               ident = name,
    5.10 +               directory = space_implode "/" (session @ prefix),
    5.11                 unfold = false,
    5.12                 path = "",
    5.13                 parents = parents,
    5.14                 content = []};
    5.15            in cons entry end;
    5.16      val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    5.17 -  in Graph_Display.display_graph (sort_wrt #ID deps) end;
    5.18 +  in Graph_Display.display_graph (sort_wrt #ident deps) end;
    5.19  
    5.20  val _ =
    5.21    Outer_Syntax.command @{command_spec "thm_deps"} "visualize theorem dependencies"
     6.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:08:50 2014 +0100
     6.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 31 14:13:11 2014 +0100
     6.3 @@ -927,7 +927,7 @@
     6.4      fun namify consts = map (Code.string_of_const thy) consts
     6.5        |> commas;
     6.6      val graph = map (fn (consts, constss) =>
     6.7 -      { name = namify consts, ID = namify consts, dir = "", unfold = true,
     6.8 +      { name = namify consts, ident = namify consts, directory = "", unfold = true,
     6.9          path = "", parents = map namify constss, content = [] }) conn;
    6.10    in Graph_Display.display_graph graph end;
    6.11