src/Pure/Thy/present.ML
changeset 49561 26fc70e983c2
parent 48935 4c92a2f310b6
child 49565 ea4308b7ef0f
     1.1 --- a/src/Pure/Thy/present.ML	Tue Sep 25 14:32:41 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Sep 25 15:40:41 2012 +0200
     1.3 @@ -13,10 +13,6 @@
     1.4  sig
     1.5    include BASIC_PRESENT
     1.6    val session_name: theory -> string
     1.7 -  val write_graph: {name: string, ID: string, dir: string, unfold: bool,
     1.8 -   path: string, parents: string list} list -> Path.T -> unit
     1.9 -  val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    1.10 -   path: string, parents: string list} list -> unit
    1.11    datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
    1.12    val dump_mode: string -> dump_mode
    1.13    val read_variant: string -> string * string
    1.14 @@ -82,24 +78,6 @@
    1.15  
    1.16  (** graphs **)
    1.17  
    1.18 -type graph_node =
    1.19 -  {name: string, ID: string, dir: string, unfold: bool,
    1.20 -   path: string, parents: string list};
    1.21 -
    1.22 -fun write_graph gr path =
    1.23 -  File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
    1.24 -    "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
    1.25 -    path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
    1.26 -
    1.27 -fun display_graph gr =
    1.28 -  let
    1.29 -    val path = Isabelle_System.create_tmp_path "graph" "";
    1.30 -    val _ = write_graph gr path;
    1.31 -    val _ = writeln "Displaying graph ...";
    1.32 -    val _ = Isabelle_System.isabelle_tool "browser" ("-c " ^ File.shell_path path ^ " &");
    1.33 -  in () end;
    1.34 -
    1.35 -
    1.36  fun ID_of sess s = space_implode "/" (sess @ [s]);
    1.37  fun ID_of_thy thy = ID_of (#session (get_info thy)) (Context.theory_name thy);
    1.38  
    1.39 @@ -118,10 +96,11 @@
    1.40              (Path.append (Path.make session) (html_path name))))
    1.41          else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
    1.42        unfold = false,
    1.43 -      parents = map ID_of_thy (Theory.parents_of thy)};
    1.44 +      parents = map ID_of_thy (Theory.parents_of thy),
    1.45 +      content = []};
    1.46    in (0, entry) end);
    1.47  
    1.48 -fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
    1.49 +fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * Graph_Display.node) list) =
    1.50    (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
    1.51  
    1.52  
    1.53 @@ -144,7 +123,8 @@
    1.54  (* type browser_info *)
    1.55  
    1.56  type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
    1.57 -  tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
    1.58 +  tex_index: (int * string) list, html_index: (int * string) list,
    1.59 +  graph: (int * Graph_Display.node) list};
    1.60  
    1.61  fun make_browser_info (theories, files, tex_index, html_index, graph) =
    1.62    {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
    1.63 @@ -344,7 +324,7 @@
    1.64      val pdf_path = Path.append dir graph_pdf_path;
    1.65      val eps_path = Path.append dir graph_eps_path;
    1.66      val graph_path = Path.append dir graph_path;
    1.67 -    val _ = write_graph graph graph_path;
    1.68 +    val _ = Graph_Display.write_graph graph_path graph;
    1.69      val args = "-o " ^ File.shell_path pdf_path ^ " " ^ File.shell_path graph_path;
    1.70    in
    1.71      if Isabelle_System.isabelle_tool "browser" args = 0 andalso
    1.72 @@ -391,7 +371,7 @@
    1.73          create_index html_prefix;
    1.74          if length path > 1 then update_index parent_html_prefix name else ();
    1.75          (case readme of NONE => () | SOME path => File.copy path html_prefix);
    1.76 -        write_graph sorted_graph (Path.append html_prefix graph_path);
    1.77 +        Graph_Display.write_graph (Path.append html_prefix graph_path) sorted_graph;
    1.78          Isabelle_System.isabelle_tool "browser" "-b";
    1.79          File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
    1.80          List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
    1.81 @@ -509,7 +489,8 @@
    1.82      val entry =
    1.83       {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
    1.84        path = Path.implode (html_path name),
    1.85 -      parents = map ID_of_thy parents};
    1.86 +      parents = map ID_of_thy parents,
    1.87 +      content = []};
    1.88    in
    1.89      change_theory_info name prep_html_source;
    1.90      add_graph_entry (update_time, entry);