src/Pure/Thy/present.ML
changeset 59208 2486d625878b
parent 59207 6b030dc97a4f
child 59209 8521841f277b
     1.1 --- a/src/Pure/Thy/present.ML	Wed Dec 31 14:13:11 2014 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Wed Dec 31 14:15:52 2014 +0100
     1.3 @@ -76,6 +76,9 @@
     1.4    end;
     1.5  
     1.6  (*retrieve graph data from initial collection of theories*)
     1.7 +type browser_node = {name: string, ident: string, parents: string list,
     1.8 +  unfold: bool, directory: string, path: string}
     1.9 +
    1.10  fun init_graph (curr_chapter, curr_session) = rev o map (fn thy =>
    1.11    let
    1.12      val {chapter, name = session_name} = Browser_Info.get thy;
    1.13 @@ -84,18 +87,17 @@
    1.14        (case theory_link (curr_chapter, curr_session) thy of
    1.15          NONE => ""
    1.16        | SOME p => Path.implode p);
    1.17 -    val entry =
    1.18 +    val graph_entry =
    1.19       {name = thy_name,
    1.20        ident = ID_of [chapter, session_name] thy_name,
    1.21        directory = session_name,
    1.22        path = path,
    1.23        unfold = false,
    1.24 -      parents = map ID_of_thy (Theory.parents_of thy),
    1.25 -      content = []};
    1.26 -  in (0, entry) end);
    1.27 +      parents = map ID_of_thy (Theory.parents_of thy)};
    1.28 +  in (0, graph_entry) end);
    1.29  
    1.30 -fun ins_graph_entry (i, entry as {ident, ...}) (gr: (int * Graph_Display.node) list) =
    1.31 -  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) gr;
    1.32 +fun ins_graph_entry (i, entry as {ident, ...}) (graph: (int * browser_node) list) =
    1.33 +  (i, entry) :: filter_out (fn (_, entry') => #ident entry' = ident) graph;
    1.34  
    1.35  
    1.36  
    1.37 @@ -118,7 +120,7 @@
    1.38   {theories: theory_info Symtab.table,
    1.39    tex_index: (int * string) list,
    1.40    html_index: (int * string) list,
    1.41 -  graph: (int * Graph_Display.node) list};
    1.42 +  graph: (int * browser_node) list};
    1.43  
    1.44  fun make_browser_info (theories, tex_index, html_index, graph) : browser_info =
    1.45    {theories = theories, tex_index = tex_index, html_index = html_index, graph = graph};
    1.46 @@ -276,6 +278,14 @@
    1.47  
    1.48  (* finish session -- output all generated text *)
    1.49  
    1.50 +fun finalize_graph (nodes : (int * browser_node) list) =
    1.51 +  nodes
    1.52 +  |> map (fn (_, {ident, parents, name, unfold, directory, path}) =>
    1.53 +      ((ident, Graph_Display.session_node
    1.54 +        {name = name, unfold = unfold, directory = directory, path = path}), parents))
    1.55 +  |> Graph.make
    1.56 +  |> pair (map (#ident o snd) (sort (int_ord o apply2 fst) (rev nodes)));
    1.57 +
    1.58  fun sorted_index index = map snd (sort (int_ord o apply2 fst) (rev index));
    1.59  fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
    1.60  
    1.61 @@ -298,10 +308,10 @@
    1.62      fun finish_html (a, {html_source, ...}: theory_info) =
    1.63        File.write (Path.append session_prefix (html_path a)) html_source;
    1.64  
    1.65 -    val sorted_graph = sorted_index graph;
    1.66 +    val graph' = finalize_graph graph;
    1.67      val opt_graphs =
    1.68        if doc_graph andalso not (null documents) then
    1.69 -        SOME (isabelle_browser sorted_graph)
    1.70 +        SOME (isabelle_browser graph')
    1.71        else NONE;
    1.72  
    1.73      val _ =
    1.74 @@ -310,7 +320,7 @@
    1.75          File.write_buffer (Path.append session_prefix index_path)
    1.76            (index_buffer html_index |> Buffer.add HTML.end_document);
    1.77          (case readme of NONE => () | SOME path => Isabelle_System.copy_file path session_prefix);
    1.78 -        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) sorted_graph;
    1.79 +        Graph_Display.write_graph_browser (Path.append session_prefix graph_path) graph';
    1.80          Isabelle_System.isabelle_tool "browser" "-b";
    1.81          Isabelle_System.copy_file (Path.explode "~~/lib/browser/GraphBrowser.jar") session_prefix;
    1.82          List.app (fn (a, txt) => File.write (Path.append session_prefix (Path.basic a)) txt)
    1.83 @@ -387,8 +397,7 @@
    1.84          directory = session_name,
    1.85          unfold = true,
    1.86          path = Path.implode (html_path name),
    1.87 -        parents = map ID_of_thy parents,
    1.88 -        content = []};
    1.89 +        parents = map ID_of_thy parents};
    1.90      in
    1.91        init_theory_info name (make_theory_info ("", html_source));
    1.92        add_graph_entry (update_time, graph_entry);