src/Pure/Thy/present.ML

 (* session_info *)
 
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
     info: bool, doc_format: string, doc_graph: bool, documents: (string * string) list,
-    doc_prefix1: (Path.T * Path.T) option, doc_prefix2: (bool * Path.T) option,
+    doc_prefix1: (Path.T * Path.T) option, dump_prefix: (bool * Path.T) option,
     remote_path: Url.T option, verbose: bool, readme: Path.T option};
 
 fun make_session_info
   (name, parent, session, path, html_prefix, info, doc_format, doc_graph, documents,
-    doc_prefix1, doc_prefix2, remote_path, verbose, readme) =
+    doc_prefix1, dump_prefix, remote_path, verbose, readme) =
   {name = name, parent = parent, session = session, path = path, html_prefix = html_prefix,
     info = info, doc_format = doc_format, doc_graph = doc_graph, documents = documents,
-    doc_prefix1 = doc_prefix1, doc_prefix2 = doc_prefix2, remote_path = remote_path,
+    doc_prefix1 = doc_prefix1, dump_prefix = dump_prefix, remote_path = remote_path,
     verbose = verbose, readme = readme}: session_info;
 
 
 (* state *)
 

 
 (* init session *)
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info doc doc_graph doc_variants path name doc_prefix2
+fun init build info doc doc_graph doc_variants path name dump_prefix
     (remote_path, first_time) verbose thys = CRITICAL (fn () =>
-  if not build andalso not info andalso doc = "" andalso is_none doc_prefix2 then
+  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
       val parent_name = name_of_session (take (length path - 1) path);
       val session_name = name_of_session path;

         map (fn (name, _) => (Url.File (Path.ext doc (Path.basic name)), name)) documents;
       val index_text = HTML.begin_index (index_up_lnk, parent_name)
         (Url.File index_path, session_name) docs (Url.explode "medium.html");
     in
       session_info := SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
-        info, doc, doc_graph, documents, doc_prefix1, doc_prefix2, remote_path, verbose, readme));
+        info, doc, doc_graph, documents, doc_prefix1, dump_prefix, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index (0, index_text)
     end);
 
 

   write_tex (index_buffer tex_index |> Buffer.add Latex.tex_trailer) doc_indexN path;
 
 
 fun finish () = CRITICAL (fn () =>
     with_session () (fn {name, info, html_prefix, doc_format, doc_graph,
-      documents, doc_prefix1, doc_prefix2, path, verbose, readme, ...} =>
+      documents, doc_prefix1, dump_prefix, path, verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
     val parent_html_prefix = Path.append html_prefix Path.parent;
 

     fun finish_html (a, {html, ...}: theory_info) =
       File.write_buffer (Path.append html_prefix (html_path a)) (Buffer.add HTML.end_document html);
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
-      if doc_graph andalso (is_some doc_prefix1 orelse is_some doc_prefix2) then
+      if doc_graph andalso (is_some doc_prefix1 orelse is_some dump_prefix) then
         SOME (isabelle_browser sorted_graph)
       else NONE;
 
     fun prepare_sources cp path =
      (Isabelle_System.mkdirs path;

       List.app finish_html thys;
       List.app (uncurry File.write) files;
       if verbose then Output.raw_stderr ("Browser info at " ^ show_path html_prefix ^ "\n") else ())
     else ();
 
-    (case doc_prefix2 of NONE => () | SOME (cp, path) =>
+    (case dump_prefix of NONE => () | SOME (cp, path) =>
      (prepare_sources cp path;
       if verbose then Output.raw_stderr ("Document sources at " ^ show_path path ^ "\n") else ()));
 
     (case doc_prefix1 of NONE => () | SOME (path, result_path) =>
       documents |> List.app (fn (name, tags) =>