# HG changeset patch
# User wenzelm
# Date 1343305794 -7200
# Node ID c5d0f19ef7cba7ffee2fd7e58425ffbdfef4d0d3
# Parent  3e17f343deb580d596e152b01f050be59a195d9b
refined "document_dump_mode": "all", "tex+sty", "tex";

diff -r 3e17f343deb5 -r c5d0f19ef7cb doc-src/ROOT
--- a/doc-src/ROOT	Thu Jul 26 14:24:27 2012 +0200
+++ b/doc-src/ROOT	Thu Jul 26 14:29:54 2012 +0200
@@ -1,10 +1,12 @@
 session Classes! (doc) in "Classes/Thy" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories [document = false] Setup
   theories Classes
 
 session Codegen! (doc) in "Codegen/Thy" = "HOL-Library" +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     print_mode = "no_brackets,iff"]
   theories [document = false] Setup
   theories
@@ -17,11 +19,13 @@
     Further
 
 session Functions! (doc) in "Functions/Thy" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories Functions
 
 session IsarImplementation! (doc) in "IsarImplementation/Thy" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories
     Eq
     Integration
@@ -35,7 +39,8 @@
     Tactic
 
 session IsarRef (doc) in "IsarRef/Thy" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
   theories
     Preface
@@ -55,17 +60,20 @@
     ML_Tactic
 
 session IsarRef (doc) in "IsarRef/Thy" = HOLCF +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
   theories HOLCF_Specific
 
 session IsarRef (doc) in "IsarRef/Thy" = ZF +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     quick_and_dirty]
   theories ZF_Specific
 
 session LaTeXsugar! (doc) in "LaTeXsugar/Sugar" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     threads = 1]  (* FIXME *)
   theories [document_dump = ""]
     "~~/src/HOL/Library/LaTeXsugar"
@@ -73,18 +81,21 @@
   theories Sugar
 
 session Locales! (doc) in "Locales/Locales" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories
     Examples1
     Examples2
     Examples3
 
 session Main! (doc) in "Main/Docs" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories Main_Doc
 
 session ProgProve! (doc) in "ProgProve/Thys" = HOL +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     show_question_marks = false]
   theories
     Basics
@@ -95,7 +106,8 @@
     Isar
 
 session System! (doc) in "System/Thy" = Pure +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only]
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex"]
   theories
     Basics
     Interfaces
@@ -106,7 +118,8 @@
 (* session Tutorial (doc) in "Tutorial" = HOL + FIXME *)
 
 session examples (doc) in "ZF" = ZF +
-  options [browser_info = false, document = false, document_dump = document, document_dump_only,
+  options [browser_info = false, document = false,
+    document_dump = document, document_dump_mode = "tex",
     print_mode = "brackets"]
   theories
     IFOL_examples
diff -r 3e17f343deb5 -r c5d0f19ef7cb etc/options
--- a/etc/options	Thu Jul 26 14:24:27 2012 +0200
+++ b/etc/options	Thu Jul 26 14:29:54 2012 +0200
@@ -6,7 +6,7 @@
 declare document_variants : string = "outline=/proof,/ML"
 declare document_graph : bool = false
 declare document_dump : string = ""
-declare document_dump_only : bool = false
+declare document_dump_mode : string = "all"
 declare no_document : bool = false
 
 declare threads : int = 0
diff -r 3e17f343deb5 -r c5d0f19ef7cb src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Thu Jul 26 14:24:27 2012 +0200
+++ b/src/Pure/System/build.ML	Thu Jul 26 14:29:54 2012 +0200
@@ -65,7 +65,7 @@
         (Options.bool options "document_graph")
         (space_explode ":" (Options.string options "document_variants"))
         parent_base_name base_name
-        (not (Options.bool options "document_dump_only"), Options.string options "document_dump")
+        (Options.string options "document_dump", Options.string options "document_dump_mode")
         "" verbose;
     val _ = Session.with_timing name timing (List.app use_theories) theories;
     val _ = Session.finish ();
diff -r 3e17f343deb5 -r c5d0f19ef7cb src/Pure/System/session.ML
--- a/src/Pure/System/session.ML	Thu Jul 26 14:24:27 2012 +0200
+++ b/src/Pure/System/session.ML	Thu Jul 26 14:29:54 2012 +0200
@@ -11,7 +11,7 @@
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string list ->
-    string -> string -> bool * string -> string -> bool -> unit
+    string -> string -> string * string -> string -> bool -> unit
   val with_timing: string -> bool -> ('a -> 'b) -> 'a -> 'b
   val use_dir: string -> string -> bool -> string list -> bool -> bool -> string ->
     string -> bool -> string list -> string -> string -> bool * string ->
@@ -85,17 +85,6 @@
 
 (* use_dir *)
 
-fun get_rpath rpath =
-  (if rpath = "" then () else
-     if is_some (! remote_path) then
-       error "Path for remote theory browsing information may only be set once"
-     else
-       remote_path := SOME (Url.explode rpath);
-   (! remote_path, rpath <> ""));
-
-fun dumping (_, "") = NONE
-  | dumping (cp, path) = SOME (cp, Path.explode path);
-
 fun with_timing _ false f x = f x
   | with_timing item true f x =
       let
@@ -110,17 +99,32 @@
             Timing.message timing ^ ", factor " ^ factor ^ ")\n");
       in y end;
 
-fun init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose =
+fun get_rpath rpath =
+  (if rpath = "" then () else
+     if is_some (! remote_path) then
+       error "Path for remote theory browsing information may only be set once"
+     else
+       remote_path := SOME (Url.explode rpath);
+   (! remote_path, rpath <> ""));
+
+fun init build reset info info_path doc doc_graph doc_variants parent name doc_dump rpath verbose =
  (init_name reset parent name;
   Present.init build info info_path (if doc = "false" then "" else doc) doc_graph doc_variants
-    (path ()) name (dumping dump) (get_rpath rpath) verbose
+    (path ()) name doc_dump (get_rpath rpath) verbose
     (map Thy_Info.get_theory (Thy_Info.get_names ())));
 
+local
+
+fun doc_dump (cp, dump) = (if cp then "all" else "tex+sty", dump);
+
+in
+
 fun use_dir item root build modes reset info info_path doc doc_graph doc_variants parent
     name dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
-     (init build reset info info_path doc doc_graph doc_variants parent name dump rpath verbose;
+     (init build reset info info_path doc doc_graph doc_variants parent name
+        (doc_dump dump) rpath verbose;
       with_timing item timing use root;
       finish ()))
     |> Unsynchronized.setmp Proofterm.proofs level
@@ -134,3 +138,5 @@
   handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1);
 
 end;
+
+end;
diff -r 3e17f343deb5 -r c5d0f19ef7cb src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Jul 26 14:24:27 2012 +0200
+++ b/src/Pure/Thy/present.ML	Thu Jul 26 14:29:54 2012 +0200
@@ -18,7 +18,7 @@
   val display_graph: {name: string, ID: string, dir: string, unfold: bool,
    path: string, parents: string list} list -> unit
   val init: bool -> bool -> string -> string -> bool -> string list -> string list ->
-    string -> (bool * Path.T) option -> Url.T option * bool -> bool ->
+    string -> string * string -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
@@ -210,15 +210,15 @@
 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,
-    dump_prefix: (bool * Path.T) option, remote_path: Url.T option, verbose: bool,
+    doc_dump: (string * string), 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,
-    dump_prefix, remote_path, verbose, readme) =
+    doc_dump, 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,
-    dump_prefix = dump_prefix, remote_path = remote_path, verbose = verbose,
+    doc_dump = doc_dump, remote_path = remote_path, verbose = verbose,
     readme = readme}: session_info;
 
 
@@ -273,9 +273,9 @@
 
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
-fun init build info info_path doc doc_graph doc_variants path name dump_prefix
-    (remote_path, first_time) verbose thys =
-  if not build andalso not info andalso doc = "" andalso is_none dump_prefix then
+fun init build info info_path doc doc_graph doc_variants path name
+    (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
+  if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
@@ -309,7 +309,7 @@
     in
       session_info :=
         SOME (make_session_info (name, parent_name, session_name, path, html_prefix,
-          info, doc, doc_graph, documents, dump_prefix, remote_path, verbose, readme));
+          info, doc, doc_graph, documents, doc_dump, remote_path, verbose, readme));
       browser_info := init_browser_info remote_path path thys;
       add_html_index (0, index_text)
     end;
@@ -360,32 +360,34 @@
 
 fun finish () =
   session_default () (fn {name, info, html_prefix, doc_format,
-    doc_graph, documents, dump_prefix, path, verbose, readme, ...} =>
+    doc_graph, documents, doc_dump = (dump_prefix, dump_mode), 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_tex path (a, {tex_source, ...}: theory_info) = write_tex tex_source a path;
     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 (not (null documents) orelse is_some dump_prefix) then
+      if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then
         SOME (isabelle_browser sorted_graph)
       else NONE;
 
-    fun prepare_sources cp path =
-     (Isabelle_System.mkdirs path;
-      if cp then Isabelle_System.copy_dir document_path path else ();
-      Isabelle_System.isabelle_tool "latex"
-        ("-o sty " ^ File.shell_path (Path.append path (Path.basic "root.tex")));
+    fun prepare_sources doc_dir doc_mode =
+     (Isabelle_System.mkdirs doc_dir;
+      if doc_mode = "all" then Isabelle_System.copy_dir document_path doc_dir
+      else if doc_mode = "tex+sty" then
+        ignore (Isabelle_System.isabelle_tool "latex"
+          ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
+      else if doc_mode = "tex" then ()
+      else error ("Illegal document dump mode: " ^ quote doc_mode);
       (case opt_graphs of NONE => () | SOME (pdf, eps) =>
-        (File.write (Path.append path graph_pdf_path) pdf;
-          File.write (Path.append path graph_eps_path) eps));
-      write_tex_index tex_index path;
-      List.app (finish_tex path) thys);
+        (File.write (Path.append doc_dir graph_pdf_path) pdf;
+          File.write (Path.append doc_dir graph_eps_path) eps));
+      write_tex_index tex_index doc_dir;
+      List.app (fn (a, {tex_source, ...}) => write_tex tex_source a doc_dir) thys);
     val _ =
       if info then
        (Isabelle_System.mkdirs (Path.append html_prefix session_path);
@@ -407,16 +409,22 @@
       else ();
 
     val _ =
-      (case dump_prefix of NONE => () | SOME (cp, path) =>
-       (prepare_sources cp path;
-        if verbose then Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
-        else ()));
+      if dump_prefix = "" then ()
+      else
+        let
+          val path = Path.explode dump_prefix;
+          val _ = prepare_sources path dump_mode;
+        in
+          if verbose then
+            Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
+          else ()
+        end;
 
     val doc_paths =
       documents |> Par_List.map (fn (name, tags) =>
         let
           val path = Path.append html_prefix (Path.basic name);
-          val _ = prepare_sources true path;
+          val _ = prepare_sources path "all";
         in isabelle_document true doc_format name tags path html_prefix end);
     val _ =
       if verbose then