1.1 --- a/src/Pure/Thy/present.ML Fri Aug 03 22:33:07 2007 +0200
1.2 +++ b/src/Pure/Thy/present.ML Fri Aug 03 22:33:09 2007 +0200
1.3 @@ -25,7 +25,7 @@
1.4 val init_theory: string -> unit
1.5 val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
1.6 val theory_output: string -> string -> unit
1.7 - val begin_theory: Path.T -> (Path.T * bool) list -> theory -> theory
1.8 + val begin_theory: int -> Path.T -> (Path.T * bool) list -> theory -> theory
1.9 val add_hook: (string -> (string * thm list) list -> unit) -> unit
1.10 val results: string -> (string * thm list) list -> unit
1.11 val theorem: string -> thm -> unit
1.12 @@ -114,25 +114,25 @@
1.13
1.14
1.15 (*retrieve graph data from initial collection of theories*)
1.16 -fun init_graph remote_path curr_sess = map (fn thy =>
1.17 +fun init_graph remote_path curr_sess = rev o map (fn thy =>
1.18 let
1.19 val name = Context.theory_name thy;
1.20 val {name = sess_name, session, is_local} = get_info thy;
1.21 val path' = Path.append (Path.make session) (html_path name);
1.22 - in
1.23 - {name = name, ID = ID_of session name, dir = sess_name,
1.24 - path =
1.25 - if null session then "" else
1.26 - if is_some remote_path andalso not is_local then
1.27 - Url.implode (Url.append (the remote_path) (Url.File
1.28 - (Path.append (Path.make session) (html_path name))))
1.29 - else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
1.30 - unfold = false,
1.31 - parents = map ID_of_thy (Theory.parents_of thy)}
1.32 - end);
1.33 + val entry =
1.34 + {name = name, ID = ID_of session name, dir = sess_name,
1.35 + path =
1.36 + if null session then "" else
1.37 + if is_some remote_path andalso not is_local then
1.38 + Url.implode (Url.append (the remote_path) (Url.File
1.39 + (Path.append (Path.make session) (html_path name))))
1.40 + else Path.implode (Path.append (mk_rel_path curr_sess session) (html_path name)),
1.41 + unfold = false,
1.42 + parents = map ID_of_thy (Theory.parents_of thy)};
1.43 + in (0, entry) end);
1.44
1.45 -fun ins_graph_entry (entry as {ID, ...}) (gr: graph_node list) =
1.46 - filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
1.47 +fun ins_graph_entry (i, entry as {ID, ...}) (gr: (int * graph_node) list) =
1.48 + (i, entry) :: filter_out (fn (_, entry') => #ID entry' = ID) gr;
1.49
1.50
1.51
1.52 @@ -154,16 +154,16 @@
1.53 (* type browser_info *)
1.54
1.55 type browser_info = {theories: theory_info Symtab.table, files: (Path.T * string) list,
1.56 - tex_index: Buffer.T, html_index: Buffer.T, graph: graph_node list};
1.57 + tex_index: (int * string) list, html_index: (int * string) list, graph: (int * graph_node) list};
1.58
1.59 fun make_browser_info (theories, files, tex_index, html_index, graph) =
1.60 {theories = theories, files = files, tex_index = tex_index, html_index = html_index,
1.61 graph = graph}: browser_info;
1.62
1.63 -val empty_browser_info = make_browser_info (Symtab.empty, [], Buffer.empty, Buffer.empty, []);
1.64 +val empty_browser_info = make_browser_info (Symtab.empty, [], [], [], []);
1.65
1.66 fun init_browser_info remote_path curr_sess thys = make_browser_info
1.67 - (Symtab.empty, [], Buffer.empty, Buffer.empty, init_graph remote_path curr_sess thys);
1.68 + (Symtab.empty, [], [], [], init_graph remote_path curr_sess thys);
1.69
1.70 fun map_browser_info f {theories, files, tex_index, html_index, graph} =
1.71 make_browser_info (f (theories, files, tex_index, html_index, graph));
1.72 @@ -195,15 +195,15 @@
1.73
1.74 fun add_tex_index txt =
1.75 change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
1.76 - (theories, files, Buffer.add txt tex_index, html_index, graph));
1.77 + (theories, files, txt :: tex_index, html_index, graph));
1.78
1.79 fun add_html_index txt =
1.80 change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
1.81 - (theories, files, tex_index, Buffer.add txt html_index, graph));
1.82 + (theories, files, tex_index, txt :: html_index, graph));
1.83
1.84 -fun add_graph_entry e =
1.85 +fun add_graph_entry entry =
1.86 change_browser_info (fn (theories, files, tex_index, html_index, graph) =>
1.87 - (theories, files, tex_index, html_index, ins_graph_entry e graph));
1.88 + (theories, files, tex_index, html_index, ins_graph_entry entry graph));
1.89
1.90 fun add_tex_source name txt =
1.91 if ! suppress_tex_source then ()
1.92 @@ -266,10 +266,10 @@
1.93 session_entries (get_entries dir) ^ HTML.end_index
1.94 |> File.write (Path.append dir index_path);
1.95
1.96 -fun update_index dir name =
1.97 +fun update_index dir name = CRITICAL (fn () =>
1.98 (case try get_entries dir of
1.99 NONE => warning ("Browser info: cannot access session index of " ^ quote (Path.implode dir))
1.100 - | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir));
1.101 + | SOME es => (put_entries ((remove (op =) name es) @ [name]) dir; create_index dir)));
1.102
1.103
1.104 (* document versions *)
1.105 @@ -326,7 +326,7 @@
1.106 session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
1.107 info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
1.108 browser_info := init_browser_info remote_path path thys;
1.109 - add_html_index index_text
1.110 + add_html_index (0, index_text)
1.111 end);
1.112
1.113
1.114 @@ -364,11 +364,14 @@
1.115
1.116 (* finish session -- output all generated text *)
1.117
1.118 +fun sorted_index index = map snd (sort (int_ord o pairself fst) (rev index));
1.119 +fun index_buffer index = Buffer.add (implode (sorted_index index)) Buffer.empty;
1.120 +
1.121 fun write_tex src name path =
1.122 Buffer.write (Path.append path (tex_path name)) src;
1.123
1.124 fun write_tex_index tex_index path =
1.125 - write_tex (Buffer.add Latex.tex_trailer tex_index) doc_indexN path;
1.126 + write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
1.127
1.128
1.129 fun finish () = CRITICAL (fn () =>
1.130 @@ -383,9 +386,10 @@
1.131 fun finish_html (a, {html, ...}: theory_info) =
1.132 Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html);
1.133
1.134 + val sorted_graph = sorted_index graph;
1.135 val opt_graphs =
1.136 if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
1.137 - SOME (isatool_browser graph)
1.138 + SOME (isatool_browser sorted_graph)
1.139 else NONE;
1.140
1.141 fun prepare_sources cp path =
1.142 @@ -400,12 +404,12 @@
1.143 in
1.144 if info then
1.145 (File.mkdir (Path.append html_prefix session_path);
1.146 - Buffer.write (Path.append html_prefix pre_index_path) html_index;
1.147 + Buffer.write (Path.append html_prefix pre_index_path) (index_buffer html_index);
1.148 File.write (Path.append html_prefix session_entries_path) "";
1.149 create_index html_prefix;
1.150 if length path > 1 then update_index parent_html_prefix name else ();
1.151 (case readme of NONE => () | SOME path => File.copy path html_prefix);
1.152 - write_graph graph (Path.append html_prefix graph_path);
1.153 + write_graph sorted_graph (Path.append html_prefix graph_path);
1.154 File.copy (Path.explode "~~/lib/browser/GraphBrowser.jar") html_prefix;
1.155 List.app (fn (a, txt) => File.write (Path.append html_prefix (Path.basic a)) txt)
1.156 (HTML.applet_pages name (Url.File index_path, name));
1.157 @@ -456,7 +460,7 @@
1.158 else Url.File (Path.append (mk_rel_path curr_session session) (html_path name)));
1.159 in (link, name) end;
1.160
1.161 -fun begin_theory dir orig_files thy =
1.162 +fun begin_theory update_time dir orig_files thy =
1.163 with_session thy (fn {name = sess_name, session, path, html_prefix, remote_path, ...} =>
1.164 let
1.165 val name = Context.theory_name thy;
1.166 @@ -493,12 +497,11 @@
1.167 {name = name, ID = ID_of path name, dir = sess_name, unfold = true,
1.168 path = Path.implode (html_path name),
1.169 parents = map ID_of_thy parents};
1.170 -
1.171 in
1.172 change_theory_info name prep_html_source;
1.173 - add_graph_entry entry;
1.174 - add_html_index (HTML.theory_entry (Url.File (html_path name), name));
1.175 - add_tex_index (Latex.theory_entry name);
1.176 + add_graph_entry (update_time, entry);
1.177 + add_html_index (update_time, HTML.theory_entry (Url.File (html_path name), name));
1.178 + add_tex_index (update_time, Latex.theory_entry name);
1.179 BrowserInfoData.put {name = sess_name, session = path, is_local = is_some remote_path} thy
1.180 end);
1.181
1.182 @@ -524,17 +527,17 @@
1.183
1.184 fun drafts doc_format src_paths =
1.185 let
1.186 - fun prep_draft (tex_index, path) =
1.187 + fun prep_draft path i =
1.188 let
1.189 val base = Path.base path;
1.190 val name =
1.191 (case Path.implode (#1 (Path.split_ext base)) of "" => gensym "DUMMY" | s => s);
1.192 in
1.193 if File.exists path then
1.194 - (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
1.195 + (((name, base, File.read path), (i, Latex.theory_entry name)), i + 1)
1.196 else error ("Bad file: " ^ quote (Path.implode path))
1.197 end;
1.198 - val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
1.199 + val (srcs, tex_index) = split_list (fst (fold_map prep_draft src_paths 0));
1.200
1.201 val doc_path = File.tmp_path document_path;
1.202 val result_path = Path.append doc_path Path.parent;