separate module Graph_Display;
authorwenzelm
Tue Sep 25 15:40:41 2012 +0200 (2012-09-25)
changeset 4956126fc70e983c2
parent 49560 11430dd89e35
child 49562 ba9dcdbf45f1
separate module Graph_Display;
tuned signature;
src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
src/Pure/General/graph_display.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_deps.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Sep 25 14:32:41 2012 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Sep 25 15:40:41 2012 +0200
     1.3 @@ -315,8 +315,8 @@
     1.4        |> commas;
     1.5      val prgr = map (fn (consts, constss) =>
     1.6        { name = namify consts, ID = namify consts, dir = "", unfold = true,
     1.7 -        path = "", parents = map namify constss }) conn;
     1.8 -  in Present.display_graph prgr end;
     1.9 +        path = "", parents = map namify constss, content = [] }) conn;
    1.10 +  in Graph_Display.display_graph prgr end;
    1.11  
    1.12  
    1.13  end;
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/graph_display.ML	Tue Sep 25 15:40:41 2012 +0200
     2.3 @@ -0,0 +1,45 @@
     2.4 +(*  Title:      Pure/General/graph_display.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Graph display.
     2.8 +*)
     2.9 +
    2.10 +signature GRAPH_DISPLAY =
    2.11 +sig
    2.12 +  type node =
    2.13 +   {name: string, ID: string, dir: string, unfold: bool,
    2.14 +    path: string, parents: string list, content: Pretty.T list}
    2.15 +  type graph = node list
    2.16 +  val write_graph: Path.T -> graph -> unit
    2.17 +  val display_graph: graph -> unit
    2.18 +end;
    2.19 +
    2.20 +structure Graph_Display: GRAPH_DISPLAY =
    2.21 +struct
    2.22 +
    2.23 +(* external graph representation *)
    2.24 +
    2.25 +type node =
    2.26 + {name: string, ID: string, dir: string, unfold: bool,
    2.27 +  path: string, parents: string list, content: Pretty.T list};
    2.28 +
    2.29 +type graph = node list;
    2.30 +
    2.31 +fun write_graph path (graph: graph) =
    2.32 +  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents, ...} =>
    2.33 +    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    2.34 +    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") graph));
    2.35 +
    2.36 +
    2.37 +(* display graph *)
    2.38 +
    2.39 +fun display_graph graph =
    2.40 +  let
    2.41 +    val path = Isabelle_System.create_tmp_path "graph" "";
    2.42 +    val _ = write_graph path graph;
    2.43 +    val _ = writeln "Displaying graph ...";
    2.44 +    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    2.45 +  in () end;
    2.46 +
    2.47 +end;
    2.48 +
     3.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 14:32:41 2012 +0200
     3.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Sep 25 15:40:41 2012 +0200
     3.3 @@ -403,8 +403,11 @@
     3.4          val parents = map Context.theory_name (Theory.parents_of node);
     3.5          val session = Present.session_name node;
     3.6          val unfold = (session = thy_session);
     3.7 -      in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
     3.8 -  in Present.display_graph gr end);
     3.9 +      in
    3.10 +       {name = name, ID = name, parents = parents, dir = session,
    3.11 +        unfold = unfold, path = "", content = []}
    3.12 +      end);
    3.13 +  in Graph_Display.display_graph gr end);
    3.14  
    3.15  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.16    let
    3.17 @@ -413,11 +416,11 @@
    3.18      val classes = Sorts.classes_of algebra;
    3.19      fun entry (c, (i, (_, cs))) =
    3.20        (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
    3.21 -            dir = "", unfold = true, path = ""});
    3.22 +            dir = "", unfold = true, path = "", content = []});
    3.23      val gr =
    3.24        Graph.fold (cons o entry) classes []
    3.25        |> sort (int_ord o pairself #1) |> map #2;
    3.26 -  in Present.display_graph gr end);
    3.27 +  in Graph_Display.display_graph gr end);
    3.28  
    3.29  fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    3.30    Thm_Deps.thm_deps (Toplevel.theory_of state)
     4.1 --- a/src/Pure/ROOT	Tue Sep 25 14:32:41 2012 +0200
     4.2 +++ b/src/Pure/ROOT	Tue Sep 25 15:40:41 2012 +0200
     4.3 @@ -67,6 +67,7 @@
     4.4      "General/buffer.ML"
     4.5      "General/file.ML"
     4.6      "General/graph.ML"
     4.7 +    "General/graph_display.ML"
     4.8      "General/heap.ML"
     4.9      "General/integer.ML"
    4.10      "General/linear_set.ML"
     5.1 --- a/src/Pure/ROOT.ML	Tue Sep 25 14:32:41 2012 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Tue Sep 25 15:40:41 2012 +0200
     5.3 @@ -250,6 +250,7 @@
     5.4  use "Thy/thy_syntax.ML";
     5.5  use "PIDE/command.ML";
     5.6  use "Isar/outer_syntax.ML";
     5.7 +use "General/graph_display.ML";
     5.8  use "Thy/present.ML";
     5.9  use "Thy/thy_load.ML";
    5.10  use "Thy/thy_info.ML";
     6.1 --- a/src/Pure/Thy/present.ML	Tue Sep 25 14:32:41 2012 +0200
     6.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 25 15:40:41 2012 +0200
     6.3 @@ -13,10 +13,6 @@
     6.4  sig
     6.5    include BASIC_PRESENT
     6.6    val session_name: theory -> string
     6.7 -  val write_graph: {name: string, ID: string, dir: string, unfold: bool,
     6.8 -   path: string, parents: string list} list -> Path.T -> unit
     6.9 -  val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    6.10 -   path: string, parents: string list} list -> unit
    6.11    datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
    6.12    val dump_mode: string -> dump_mode
    6.13    val read_variant: string -> string * string
    6.14 @@ -82,24 +78,6 @@
    6.15  
    6.16  (** graphs **)
    6.17  
    6.18 -type graph_node =
    6.19 -  {name: string, ID: string, dir: string, unfold: bool,
    6.20 -   path: string, parents: string list};
    6.21 -
    6.22 -fun write_graph gr path =
    6.23 -  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    6.24 -    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    6.25 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    6.26 -
    6.27 -fun display_graph gr =
    6.28 -  let
    6.29 -    val path = Isabelle_System.create_tmp_path "graph" "";
    6.30 -    val _ = write_graph gr path;
    6.31 -    val _ = writeln "Displaying graph ...";
    6.32 -    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    6.33 -  in () end;
    6.34 -
    6.35 -
    6.36  fun ID_of sess s = space_implode "/" (sess @ [s]);
    6.37  fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
    6.38  
    6.39 @@ -118,10 +96,11 @@
    6.40              (Path.append (Path.make session) (html_path name))))
    6.41          else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
    6.42        unfold = false,
    6.43 -      parents = map ID_of_thy (Theory.parents_of thy)};
    6.44 +      parents = map ID_of_thy (Theory.parents_of thy),
    6.45 +      content = []};
    6.46    in (0, entry) end);
    6.47  
    6.48 -fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
    6.49 +fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
    6.50    (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
    6.51  
    6.52  
    6.53 @@ -144,7 +123,8 @@
    6.54  (* type browser_info *)
    6.55  
    6.56  type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
    6.57 -  tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
    6.58 +  tex_index: (int * string) list, html_index: (int * string) list,
    6.59 +  graph: (int * Graph_Display.node) list};
    6.60  
    6.61  fun make_browser_info (theories, files, tex_index, html_index, graph) =
    6.62    {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
    6.63 @@ -344,7 +324,7 @@
    6.64      val pdf_path = Path.append dir graph_pdf_path;
    6.65      val eps_path = Path.append dir graph_eps_path;
    6.66      val graph_path = Path.append dir graph_path;
    6.67 -    val _ = write_graph graph graph_path;
    6.68 +    val _ = Graph_Display.write_graph graph_path graph;
    6.69      val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    6.70    in
    6.71      if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    6.72 @@ -391,7 +371,7 @@
    6.73          create_index html_prefix;
    6.74          if length path > 1 then update_index parent_html_prefix name else ();
    6.75          (case readme of NONE => () | SOME path => File.copy path html_prefix);
    6.76 -        write_graph sorted_graph (Path.append html_prefix graph_path);
    6.77 +        Graph_Display.write_graph (Path.append html_prefix graph_path) sorted_graph;
    6.78          Isabelle_System.isabelle_tool "browser" "-b";
    6.79          File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
    6.80          List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
    6.81 @@ -509,7 +489,8 @@
    6.82      val entry =
    6.83       {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
    6.84        path = Path.implode (html_path name),
    6.85 -      parents = map ID_of_thy parents};
    6.86 +      parents = map ID_of_thy parents,
    6.87 +      content = []};
    6.88    in
    6.89      change_theory_info name prep_html_source;
    6.90      add_graph_entry (update_time, entry);
     7.1 --- a/src/Pure/Thy/thm_deps.ML	Tue Sep 25 14:32:41 2012 +0200
     7.2 +++ b/src/Pure/Thy/thm_deps.ML	Tue Sep 25 15:40:41 2012 +0200
     7.3 @@ -38,10 +38,11 @@
     7.4                 dir = space_implode "/" (session @ prefix),
     7.5                 unfold = false,
     7.6                 path = "",
     7.7 -               parents = parents};
     7.8 +               parents = parents,
     7.9 +               content = []};
    7.10            in cons entry end;
    7.11      val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
    7.12 -  in Present.display_graph (sort_wrt #ID deps) end;
    7.13 +  in Graph_Display.display_graph (sort_wrt #ID deps) end;
    7.14  
    7.15  
    7.16  (* unused_thms *)
     8.1 --- a/src/Tools/Code/code_thingol.ML	Tue Sep 25 14:32:41 2012 +0200
     8.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Sep 25 15:40:41 2012 +0200
     8.3 @@ -1045,8 +1045,8 @@
     8.4        |> commas;
     8.5      val prgr = map (fn (consts, constss) =>
     8.6        { name = namify consts, ID = namify consts, dir = "", unfold = true,
     8.7 -        path = "", parents = map namify constss }) conn;
     8.8 -  in Present.display_graph prgr end;
     8.9 +        path = "", parents = map namify constss, content = [] }) conn;
    8.10 +  in Graph_Display.display_graph prgr end;
    8.11  
    8.12  local
    8.13