wenzelm@6203: (*  Title:      Pure/Thy/present.ML
wenzelm@6203:     ID:         $Id$
wenzelm@7727:     Author:     Stefan Berghofer and Markus Wenzel, TU Muenchen
wenzelm@8808:     License:    GPL (GNU GENERAL PUBLIC LICENSE)
wenzelm@6203: 
wenzelm@8196: Theory presentation (HTML, graph files, (PDF)LaTeX documents).
wenzelm@6203: *)
wenzelm@6203: 
wenzelm@6203: signature BASIC_PRESENT =
wenzelm@6203: sig
wenzelm@7727:   val section: string -> unit
wenzelm@6203: end;
wenzelm@6203: 
wenzelm@6203: signature PRESENT =
wenzelm@6203: sig
wenzelm@7727:   include BASIC_PRESENT
wenzelm@8196:   val init: bool -> string -> string list -> string -> Path.T option -> Url.T option * bool -> unit
wenzelm@7727:   val finish: unit -> unit
wenzelm@7727:   val init_theory: string -> unit
wenzelm@8192:   val verbatim_source: string -> (unit -> Symbol.symbol list) -> unit
wenzelm@7757:   type token
wenzelm@7757:   val basic_token: OuterLex.token -> token
wenzelm@7757:   val markup_token: string * string -> token
wenzelm@8660:   val markup_env_token: string * string -> token
wenzelm@7789:   val verbatim_token: string -> token
wenzelm@8192:   val old_symbol_source: string -> (unit -> Symbol.symbol list) -> unit
wenzelm@7757:   val token_source: string -> (unit -> token list) -> unit
wenzelm@7727:   val begin_theory: string -> string list -> (Path.T * bool) list -> theory -> theory
wenzelm@7727:   val result: string -> string -> thm -> unit
wenzelm@7727:   val results: string -> string -> thm list -> unit
wenzelm@7727:   val theorem: string -> thm -> unit
wenzelm@7727:   val theorems: string -> thm list -> unit
wenzelm@8088:   val chapter: string -> unit
wenzelm@7727:   val subsection: string -> unit
wenzelm@7727:   val subsubsection: string -> unit
wenzelm@7727:   val setup: (theory -> theory) list
berghofe@7763:   val get_info: theory -> {session: string list, is_local: bool}
wenzelm@6203: end;
wenzelm@6203: 
wenzelm@7685: structure Present: PRESENT =
wenzelm@7685: struct
wenzelm@7685: 
wenzelm@7727: 
wenzelm@7727: (** paths **)
wenzelm@7727: 
wenzelm@7727: val output_path = Path.variable "ISABELLE_BROWSER_INFO";
wenzelm@7727: 
wenzelm@7727: fun top_path sess_path offset =
wenzelm@7727:   Path.append (Path.appends (replicate (offset + length sess_path) Path.parent));
wenzelm@7727: 
wenzelm@7727: val tex_ext = Path.ext "tex";
wenzelm@7727: val tex_path = tex_ext o Path.basic;
wenzelm@7727: val html_ext = Path.ext "html";
wenzelm@7727: val html_path = html_ext o Path.basic;
wenzelm@7727: val graph_path = Path.ext "graph" o Path.basic;
wenzelm@7727: val index_path = Path.basic "index.html";
wenzelm@7727: val doc_path = Path.basic "document";
wenzelm@8196: val doc_indexN = "session";
wenzelm@7727: 
wenzelm@7727: val session_path = Path.basic ".session";
wenzelm@7727: val session_entries_path = Path.unpack ".session/entries";
wenzelm@7727: val pre_index_path = Path.unpack ".session/pre-index";
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** additional theory data **)
wenzelm@7727: 
wenzelm@7727: structure BrowserInfoArgs =
wenzelm@7727: struct
wenzelm@7727:   val name = "Pure/browser_info";
wenzelm@7727:   type T = {session: string list, is_local: bool};
wenzelm@7727: 
wenzelm@7727:   val empty = {session = [], is_local = false};
wenzelm@7727:   val copy = I;
berghofe@7763:   fun prep_ext _ = empty;
wenzelm@7727:   fun merge _ = empty;
wenzelm@7727:   fun print _ _ = ();
wenzelm@7727: end;
wenzelm@7727: 
wenzelm@7727: structure BrowserInfoData = TheoryDataFun(BrowserInfoArgs);
wenzelm@7727: 
wenzelm@7727: fun get_info thy =
wenzelm@7727:   if Theory.eq_thy (thy, ProtoPure.thy) then BrowserInfoArgs.empty
wenzelm@7727:   else BrowserInfoData.get thy;
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** graphs **)
wenzelm@7727: 
wenzelm@7727: type graph_node =
wenzelm@7727:   {name: string, ID: string, dir: string, unfold: bool,
wenzelm@7727:    path: string, parents: string list};
wenzelm@7727: 
wenzelm@7727: fun get_graph path = map (fn (a :: b :: c :: d :: e :: r) =>
wenzelm@7727:   {name = unenclose a, ID = unenclose b,
wenzelm@7727:    dir = unenclose c, unfold = (d = "+"),
wenzelm@7727:    path = unenclose (if d = "+" then e else d),
wenzelm@7727:    parents = map unenclose (fst (split_last (if d = "+" then tl r else r)))})
wenzelm@7727:      (map (filter_out (equal "") o space_explode " ") (split_lines (File.read path)));
wenzelm@7727: 
wenzelm@7727: fun put_graph gr path =
wenzelm@7727:     File.write path (cat_lines (map (fn {name, ID, dir, unfold, path, parents} =>
wenzelm@7727:       "\"" ^ name ^ "\" \"" ^ ID ^ "\" \"" ^ dir ^ (if unfold then "\" + \"" else "\" \"") ^
wenzelm@7727:       path ^ "\" > " ^ space_implode " " (map quote parents) ^ " ;") gr));
wenzelm@7727: 
wenzelm@7727: fun dir_of sess = space_implode "/" (case sess of
wenzelm@7727:   [] => ["Pure"] | [x] => [x, "base"] | xs => xs);
wenzelm@7727: 
wenzelm@7727: fun ID_of sess s = dir_of sess ^ "/" ^ s;
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* retrieve graph data from theory loader database *)
wenzelm@7727: 
wenzelm@7727: fun make_graph remote_path unfold curr_sess = map (fn name =>
wenzelm@7727:   let
wenzelm@7727:     val {session, is_local} = get_info (ThyInfo.theory name);
wenzelm@7727:     val path' = Path.append (Path.make session) (html_path name)
wenzelm@7727:   in
wenzelm@7727:     {name = name, ID = ID_of session name, dir = dir_of session,
wenzelm@7727:      path = if null session then "" else
wenzelm@7727:             if is_some remote_path andalso not is_local then
wenzelm@7727:               Url.pack (Url.append (the remote_path) (Url.file path'))
wenzelm@7727:             else Path.pack (top_path curr_sess 2 path'),
wenzelm@7727:      unfold = unfold andalso (length session = 1),
wenzelm@7727:      parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s)
wenzelm@7727:        (ThyInfo.get_preds name)}
wenzelm@7727:   end) (ThyInfo.names ());
wenzelm@7727: 
wenzelm@7727: fun add_graph_entry' (entry as {ID, ...}) (gr : graph_node list) =
wenzelm@7727:   filter_out (fn entry' => #ID entry' = ID) gr @ [entry];
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** global browser info state **)
wenzelm@7727: 
wenzelm@7727: (* type theory_info *)
wenzelm@7727: 
wenzelm@7727: type theory_info = {tex_source: Buffer.T, html_source: Buffer.T, html: Buffer.T};
wenzelm@7727: 
wenzelm@7727: fun make_theory_info (tex_source, html_source, html) =
wenzelm@7727:   {tex_source = tex_source, html_source = html_source, html = html}: theory_info;
wenzelm@7727: 
wenzelm@7727: val empty_theory_info = make_theory_info (Buffer.empty, Buffer.empty, Buffer.empty);
wenzelm@7727: 
wenzelm@7727: fun map_theory_info f {tex_source, html_source, html} =
wenzelm@7727:   make_theory_info (f (tex_source, html_source, html));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* type browser_info *)
wenzelm@7727: 
wenzelm@7727: type browser_info = {theories: theory_info Symtab.table, tex_index: Buffer.T,
wenzelm@7727:   html_index: Buffer.T, graph: graph_node list, all_graph: graph_node list};
wenzelm@7727: 
wenzelm@7727: fun make_browser_info (theories, tex_index, html_index, graph, all_graph) =
wenzelm@7727:   {theories = theories, tex_index = tex_index, html_index = html_index,
wenzelm@7727:     graph = graph, all_graph = all_graph}: browser_info;
wenzelm@7727: 
wenzelm@7727: val empty_browser_info = make_browser_info (Symtab.empty, Buffer.empty, Buffer.empty, [], []);
wenzelm@7727: 
wenzelm@7727: fun initial_browser_info remote_path graph_path curr_sess = make_browser_info
wenzelm@7727:   (Symtab.empty, Buffer.empty, Buffer.empty, make_graph remote_path false curr_sess,
wenzelm@7727:    if_none (try get_graph graph_path) (make_graph remote_path true [""]));
wenzelm@7727: 
wenzelm@7727: fun map_browser_info f {theories, tex_index, html_index, graph, all_graph} =
wenzelm@7727:   make_browser_info (f (theories, tex_index, html_index, graph, all_graph));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* state *)
wenzelm@7727: 
wenzelm@7727: val browser_info = ref empty_browser_info;
wenzelm@7727: 
wenzelm@7727: fun change_browser_info f = browser_info := map_browser_info f (! browser_info);
wenzelm@7727: 
wenzelm@7727: fun init_theory_info name info =
wenzelm@7727:   change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
wenzelm@7727:     (Symtab.update ((name, info), theories), tex_index, html_index, graph, all_graph));
wenzelm@7727: 
wenzelm@7727: fun change_theory_info name f =
wenzelm@7727:   change_browser_info (fn (info as (theories, tex_index, html_index, graph, all_graph)) =>
wenzelm@7727:     (case Symtab.lookup (theories, name) of
wenzelm@7727:       None => (warning ("Browser info: cannot access theory document " ^ quote name); info)
wenzelm@7727:     | Some info => (Symtab.update ((name, map_theory_info f info), theories),
wenzelm@7727:         tex_index, html_index, graph, all_graph)));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: fun add_tex_index txt =
wenzelm@7727:   change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
wenzelm@7727:     (theories, Buffer.add txt tex_index, html_index, graph, all_graph));
wenzelm@7727: 
wenzelm@7727: fun add_html_index txt =
wenzelm@7727:   change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
wenzelm@7727:     (theories, tex_index, Buffer.add txt html_index, graph, all_graph));
wenzelm@7727: 
wenzelm@7727: (*add entry to graph for current session*)
wenzelm@7727: fun add_graph_entry e =
wenzelm@7727:   change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
wenzelm@7727:     (theories, tex_index, html_index, add_graph_entry' e graph, all_graph));
wenzelm@7727: 
wenzelm@7727: (*add entry to graph for all sessions*)
wenzelm@7727: fun add_all_graph_entry e =
wenzelm@7727:   change_browser_info (fn (theories, tex_index, html_index, graph, all_graph) =>
wenzelm@7727:     (theories, tex_index, html_index, graph, add_graph_entry' e all_graph));
wenzelm@7727: 
wenzelm@7727: fun add_tex_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
wenzelm@7727:   (Buffer.add txt tex_source, html_source, html));
wenzelm@7727: 
wenzelm@7727: fun add_html_source name txt = change_theory_info name (fn (tex_source, html_source, html) =>
wenzelm@7727:   (tex_source, Buffer.add txt html_source, html));
wenzelm@7727: 
wenzelm@7727: fun add_html name txt = change_theory_info name (fn (tex_source, html_source, html) =>
wenzelm@7727:   (tex_source, html_source, Buffer.add txt html));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** global session state **)
wenzelm@7727: 
wenzelm@7727: (* session_info *)
wenzelm@7727: 
wenzelm@7727: type session_info =
wenzelm@7727:   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
wenzelm@8196:     doc_format: string, doc_prefixes: (Path.T * Path.T option) option, graph_path: Path.T,
wenzelm@8196:     all_graph_path: Path.T, remote_path: Url.T option};
wenzelm@7727: 
wenzelm@8196: fun make_session_info (name, parent, session, path, html_prefix, doc_format, doc_prefixes,
wenzelm@7727:     graph_path, all_graph_path, remote_path) =
wenzelm@7802:   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
wenzelm@8196:     doc_format = doc_format, doc_prefixes = doc_prefixes, graph_path = graph_path,
wenzelm@7727:     all_graph_path = all_graph_path, remote_path = remote_path}: session_info;
wenzelm@7685: 
wenzelm@7685: 
wenzelm@7727: (* state *)
wenzelm@7727: 
wenzelm@7727: val session_info = ref (None: session_info option);
wenzelm@7727: 
wenzelm@7727: fun with_session x f = (case ! session_info of None => x | Some info => f info);
wenzelm@7727: fun with_context f = f (PureThy.get_name (Context.the_context ()));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** HTML output **)
wenzelm@7727: 
wenzelm@7727: (* maintain index *)
wenzelm@7727: 
wenzelm@7727: val session_entries =
wenzelm@7727:   HTML.session_entries o
wenzelm@7727:     map (fn name => (Url.file (Path.append (Path.basic name) index_path), name));
wenzelm@7727: 
wenzelm@7727: fun get_entries dir =
wenzelm@7727:   split_lines (File.read (Path.append dir session_entries_path));
wenzelm@7727: 
wenzelm@7727: fun put_entries entries dir =
wenzelm@7727:   File.write (Path.append dir session_entries_path) (cat_lines entries);
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: fun create_index dir =
wenzelm@7727:   File.read (Path.append dir pre_index_path) ^
wenzelm@7727:     session_entries (get_entries dir) ^ HTML.end_index
wenzelm@7727:   |> File.write (Path.append dir index_path);
wenzelm@7727: 
wenzelm@7727: fun update_index dir name =
wenzelm@7727:   (case try get_entries dir of
wenzelm@7727:     None => warning ("Browser info: cannot access session index of " ^ quote (Path.pack dir))
wenzelm@7727:   | Some es => (put_entries ((es \ name) @ [name]) dir; create_index dir));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* init session *)
wenzelm@7727: 
wenzelm@7727: fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
wenzelm@7727: 
wenzelm@7727: fun could_copy inpath outpath =
wenzelm@7727:   if File.exists inpath then (File.copy inpath outpath; true)
wenzelm@7727:   else false;
wenzelm@7727: 
wenzelm@8196: fun init false _ _ _ _ _ = (browser_info := empty_browser_info; session_info := None)
wenzelm@8196:   | init true doc path name dump_path (remote_path, first_time) =
wenzelm@7727:       let
wenzelm@7727:         val parent_name = name_of_session (take (length path - 1, path));
wenzelm@7727:         val session_name = name_of_session path;
wenzelm@7727:         val sess_prefix = Path.make path;
wenzelm@7727: 
wenzelm@7727:         val out_path = Path.expand output_path;
wenzelm@7727:         val html_prefix = Path.append out_path sess_prefix;
wenzelm@7727: 
wenzelm@8196:         val (doc_prefixes, document_path) =
wenzelm@7727:           if doc = "" then (None, None)
wenzelm@8196:           else (Some (Path.append html_prefix doc_path, dump_path), Some (Path.ext doc doc_path));
wenzelm@7727: 
wenzelm@7727:         val graph_prefix = Path.appends [out_path, Path.unpack "graph/data", sess_prefix];
wenzelm@7727:         val graph_path = Path.append graph_prefix (Path.basic "session.graph");
wenzelm@7727:         val graph_lnk = Url.file (top_path path 0 (Path.appends
wenzelm@7727:           [Path.unpack "graph/data", sess_prefix, Path.basic "medium.html"]));
wenzelm@7727:         val graph_up_lnk =
wenzelm@7727:           (Url.file (top_path path 2 (Path.append sess_prefix index_path)), session_name);
wenzelm@7727:         val codebase = Url.file (top_path path 1 Path.current);
wenzelm@7727:         val all_graph_path = Path.appends [out_path, Path.unpack "graph/data",
wenzelm@7727:           Path.basic (hd path), Path.basic "all_sessions.graph"];
wenzelm@7727: 
wenzelm@7727:         val _ = (File.mkdir html_prefix; File.mkdir graph_prefix);
wenzelm@7727: 
wenzelm@7727:         fun prep_readme readme =
wenzelm@7727:           let val readme_path = Path.basic readme in
wenzelm@7727:             if could_copy readme_path (Path.append html_prefix readme_path) then Some readme_path
wenzelm@7727:             else None
wenzelm@7727:           end;
wenzelm@7727:         val opt_readme =
wenzelm@7727:           (case prep_readme "README.html" of None => prep_readme "README" | some => some);
wenzelm@7727: 
wenzelm@7727:         val parent_index_path = Path.append Path.parent index_path;
wenzelm@7727:         val index_up_lnk = if first_time then
wenzelm@7727:             Url.append (the remote_path) (Url.file (Path.append sess_prefix parent_index_path))
wenzelm@7727:           else Url.file parent_index_path;
wenzelm@7727: 
wenzelm@7727:         val index_text = HTML.begin_index (index_up_lnk, parent_name)
wenzelm@7727:           (Url.file index_path, session_name) (apsome Url.file opt_readme)
wenzelm@7727:             (apsome Url.file document_path) graph_lnk;
wenzelm@7727:       in
wenzelm@7727:         File.mkdir (Path.append html_prefix session_path);
wenzelm@7727:         File.write (Path.append html_prefix session_entries_path) "";
wenzelm@8196:         if is_some doc_prefixes then File.copy_all doc_path html_prefix else ();
wenzelm@7727:         seq (fn (name, txt) => File.write (Path.append graph_prefix (Path.basic name)) txt)
wenzelm@7727:           (HTML.applet_pages session_name codebase graph_up_lnk (length path = 1));
wenzelm@7727:         session_info := Some (make_session_info (name, parent_name, session_name, path,
wenzelm@8196:           html_prefix, doc, doc_prefixes, graph_path, all_graph_path, remote_path));
wenzelm@7727:         browser_info := initial_browser_info remote_path all_graph_path path;
wenzelm@7727:         add_html_index index_text
wenzelm@7727:       end;
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* finish session *)
wenzelm@7685: 
wenzelm@7802: fun isatool_document doc_format doc_prefix =
wenzelm@8646:   let
wenzelm@8646:     val cmd = "$ISATOOL document -c -o '" ^ doc_format ^ "' '" ^ File.sysify_path doc_prefix ^ "'";
wenzelm@8646:   in
wenzelm@8646:     writeln cmd;
wenzelm@8646:     if system cmd <> 0 orelse not (File.exists (Path.ext doc_format doc_prefix)) then
wenzelm@8646:       error "Failed to build document"
wenzelm@8646:     else ()
wenzelm@8646:   end;
wenzelm@7802: 
wenzelm@8196: fun write_tex src name path = Buffer.write (Path.append path (tex_path name)) src;
wenzelm@8196: 
wenzelm@8196: fun write_texes src name (path, None) = write_tex src name path
wenzelm@8196:   | write_texes src name (path, Some path') = (write_tex src name path; write_tex src name path');
wenzelm@8196: 
wenzelm@8196: 
wenzelm@7727: fun finish () = with_session ()
wenzelm@8196:     (fn {name, html_prefix, doc_format, doc_prefixes, graph_path, all_graph_path, path, ...} =>
wenzelm@7727:   let
wenzelm@7727:     val {theories, tex_index, html_index, graph, all_graph} = ! browser_info;
wenzelm@7727: 
wenzelm@7727:     fun finish_node (a, {tex_source, html_source = _, html}) =
wenzelm@8196:      (doc_prefixes |> apsome (write_texes tex_source a);
wenzelm@7727:       Buffer.write (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_theory html));
wenzelm@7727:   in
wenzelm@7727:     seq finish_node (Symtab.dest theories);
wenzelm@7727:     Buffer.write (Path.append html_prefix pre_index_path) html_index;
wenzelm@8196:     doc_prefixes |> apsome (write_texes tex_index doc_indexN);
wenzelm@8196:     doc_prefixes |> apsome (isatool_document doc_format o #1);
wenzelm@7727:     put_graph graph graph_path;
wenzelm@7727:     put_graph all_graph all_graph_path;
wenzelm@7727:     create_index html_prefix;
wenzelm@7727:     update_index (Path.append html_prefix Path.parent) name;
wenzelm@7727:     browser_info := empty_browser_info;
wenzelm@7727:     session_info := None
wenzelm@7727:   end);
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (* theory elements *)
wenzelm@7727: 
wenzelm@7727: fun init_theory name = with_session () (fn _ => init_theory_info name empty_theory_info);
wenzelm@7727: 
wenzelm@7727: fun verbatim_source name mk_text =
wenzelm@7727:   with_session () (fn _ => add_html_source name (HTML.verbatim_source (mk_text ())));
wenzelm@7727: 
wenzelm@7757: 
wenzelm@7757: type token = Latex.token;
wenzelm@7757: val basic_token = Latex.Basic;
wenzelm@7757: val markup_token = Latex.Markup;
wenzelm@8660: val markup_env_token = Latex.MarkupEnv;
wenzelm@7789: val verbatim_token = Latex.Verbatim;
wenzelm@7757: 
wenzelm@8192: fun old_symbol_source name mk_text =
wenzelm@8499:   with_session () (fn _ => add_tex_source name (Latex.old_symbol_source name (mk_text ())));
wenzelm@8192: 
wenzelm@7727: fun token_source name mk_toks =
wenzelm@7727:   with_session () (fn _ => add_tex_source name (Latex.token_source (mk_toks ())));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: fun parent_link remote_path curr_session name =
wenzelm@7727:   let
wenzelm@7727:     val {session, is_local} = get_info (ThyInfo.theory name);
wenzelm@7727:     val path = Path.append (Path.make session) (html_path name)
wenzelm@7727:   in (if null session then None else
wenzelm@7727:      Some (if is_some remote_path andalso not is_local then
wenzelm@7727:        Url.append (the remote_path) (Url.file path)
wenzelm@7727:      else Url.file (top_path curr_session 0 path)), name)
wenzelm@7727:   end;
wenzelm@7727: 
wenzelm@7727: fun begin_theory name raw_parents orig_files thy =
wenzelm@7727:   with_session thy (fn {session, path, html_prefix, remote_path, ...} =>
wenzelm@7727:   let
wenzelm@7727:     val parents = map (parent_link remote_path path) raw_parents;
wenzelm@7727:     val ml_path = ThyLoad.ml_path name;
wenzelm@7727:     val files = map (apsnd Some) orig_files @
wenzelm@7727:       (if is_some (ThyLoad.check_file ml_path) then [(ml_path, None)] else []);
wenzelm@7727: 
wenzelm@7727:     fun prep_file (raw_path, loadit) =
wenzelm@7727:       (case ThyLoad.check_file raw_path of
wenzelm@7727:         Some (path, _) =>
wenzelm@7727:           let
wenzelm@7727:             val base = Path.base path;
wenzelm@7727:             val base_html = html_ext base;
wenzelm@7727:           in
wenzelm@7727:             File.write (Path.append html_prefix base_html)
wenzelm@7727:               (HTML.ml_file (Url.file base) (File.read path));
wenzelm@7727:             (Some (Url.file base_html), Url.file raw_path, loadit)
wenzelm@7727:           end
wenzelm@7727:       | None => (warning ("Browser info: expected to find ML file" ^ quote (Path.pack raw_path));
wenzelm@7727:           (None, Url.file raw_path, loadit)));
wenzelm@7727: 
wenzelm@7727:     val files_html = map prep_file files;
wenzelm@7727: 
wenzelm@7727:     fun prep_html_source (tex_source, html_source, html) =
wenzelm@7727:       let
wenzelm@7727:         val txt = HTML.begin_theory (Url.file index_path, session)
wenzelm@7727:           name parents files_html (Buffer.content html_source)
wenzelm@7727:       in (tex_source, Buffer.empty, Buffer.add txt html) end;
wenzelm@7727: 
wenzelm@7727:     fun make_entry unfold all =
wenzelm@7727:       {name = name, ID = ID_of path name, dir = dir_of path, unfold = unfold,
wenzelm@7727:        path = Path.pack (top_path (if all then [""] else path) 2
wenzelm@7727:          (Path.append (Path.make path) (html_path name))),
wenzelm@7727:        parents = map (fn s => ID_of (#session (get_info (ThyInfo.theory s))) s) raw_parents};
wenzelm@7727: 
wenzelm@7727:   in
wenzelm@7727:     change_theory_info name prep_html_source;
wenzelm@7727:     add_all_graph_entry (make_entry (length path = 1) true);
wenzelm@7727:     add_graph_entry (make_entry true false);
wenzelm@7727:     add_html_index (HTML.theory_entry (Url.file (html_path name), name));
wenzelm@7727:     add_tex_index (Latex.theory_entry name);
wenzelm@7727:     BrowserInfoData.put {session = path, is_local = is_some remote_path} thy
wenzelm@7727:   end);
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: fun result k a thm = with_session () (fn _ => with_context add_html (HTML.result k a thm));
wenzelm@7727: fun results k a thms = with_session () (fn _ => with_context add_html (HTML.results k a thms));
wenzelm@7727: fun theorem a thm = with_session () (fn _ => with_context add_html (HTML.theorem a thm));
wenzelm@7727: fun theorems a thms = with_session () (fn _ => with_context add_html (HTML.theorems a thms));
wenzelm@8088: fun chapter s = with_session () (fn _ => with_context add_html (HTML.chapter s));
wenzelm@7727: fun section s = with_session () (fn _ => with_context add_html (HTML.section s));
wenzelm@7727: fun subsection s = with_session () (fn _ => with_context add_html (HTML.subsection s));
wenzelm@7727: fun subsubsection s = with_session () (fn _ => with_context add_html (HTML.subsubsection s));
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: 
wenzelm@7727: (** theory setup **)
wenzelm@7727: 
wenzelm@7727: val setup = [BrowserInfoData.init];
wenzelm@7685: 
wenzelm@7685: 
wenzelm@7685: end;
wenzelm@7685: 
wenzelm@6203: 
wenzelm@6203: structure BasicPresent: BASIC_PRESENT = Present;
wenzelm@6203: open BasicPresent;