isabelle build no longer supports document_dump/document_dump_mode (no INCOMPATIBILITY, since it was never in official release);
always generate sty files, as before c5d0f19ef7cb;

--- a/etc/options	Sun Nov 18 16:31:41 2012 +0100
+++ b/etc/options	Sun Nov 18 19:01:30 2012 +0100
@@ -13,10 +13,6 @@
   -- "option alternative document variants (separated by colons)"
 option document_graph : bool = false
   -- "generate session graph image for document"
-option document_dump : string = ""
-  -- "dump generated document sources into given directory"
-option document_dump_mode : string = "all"
-  -- "specific document dump mode: all, tex, tex+sty"
 
 option show_question_marks : bool = true
   -- "show leading question mark of schematic variables"

--- a/src/Pure/System/build.ML	Sun Nov 18 16:31:41 2012 +0100
+++ b/src/Pure/System/build.ML	Sun Nov 18 19:01:30 2012 +0100
@@ -15,8 +15,7 @@
 local
 
 fun no_document options =
-  (case Options.string options "document" of "" => true | "false" => true | _ => false) andalso
-  (Options.string options "document_dump" = "");
+  (case Options.string options "document" of "" => true | "false" => true | _ => false);
 
 fun use_thys options =
   Thy_Info.use_thys
@@ -73,11 +72,6 @@
         | dups => error ("Duplicate document variants: " ^ commas_quote dups));
 
       val _ =
-        if Options.string options "document_dump" = "" then ()
-        else
-          Output.physical_stderr
-            "### Legacy feature: old option \"document_dump\" -- use \"document_output\" instead\n";
-      val _ =
         Session.init do_output false
           (Options.bool options "browser_info") browser_info
           (Options.string options "document")
@@ -85,9 +79,8 @@
           (Options.string options "document_output")
           document_variants
           parent_name name
-          (Options.string options "document_dump",
-            Present.dump_mode (Options.string options "document_dump_mode"))
-          "" verbose;
+          (false, "") ""
+          verbose;
 
       val res1 =
         theories |>

--- a/src/Pure/System/session.ML	Sun Nov 18 16:31:41 2012 +0100
+++ b/src/Pure/System/session.ML	Sun Nov 18 19:01:30 2012 +0100
@@ -11,7 +11,7 @@
   val welcome: unit -> string
   val finish: unit -> unit
   val init: bool -> bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string -> string -> string * Present.dump_mode -> string -> bool -> unit
+    string -> string -> bool * 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 ->
@@ -115,8 +115,6 @@
 
 local
 
-fun doc_dump (cp, dump) = (dump, if cp then Present.Dump_all else Present.Dump_tex_sty);
-
 fun read_variants strs =
   rev (distinct (eq_fst (op =)) (rev (("document", "") :: map Present.read_variant strs)))
   |> filter_out (fn (_, s) => s = "-");
@@ -124,7 +122,7 @@
 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
+    name doc_dump rpath level timing verbose max_threads trace_threads
     parallel_proofs parallel_proofs_threshold =
   ((fn () =>
     let
@@ -133,7 +131,7 @@
           "### Legacy feature: old \"isabelle usedir\" -- use \"isabelle build\" instead!\n";
       val _ =
         init build reset info info_path doc doc_graph "" (read_variants doc_variants) parent name
-          (doc_dump dump) rpath verbose;
+          doc_dump rpath verbose;
       val res1 = (use |> with_timing item timing |> Exn.capture) root;
       val res2 = Exn.capture finish ();
     in ignore (Par_Exn.release_all [res1, res2]) end)

--- a/src/Pure/Thy/present.ML	Sun Nov 18 16:31:41 2012 +0100
+++ b/src/Pure/Thy/present.ML	Sun Nov 18 19:01:30 2012 +0100
@@ -13,11 +13,9 @@
 sig
   include BASIC_PRESENT
   val session_name: theory -> string
-  datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty
-  val dump_mode: string -> dump_mode
   val read_variant: string -> string * string
   val init: bool -> bool -> string -> string -> bool -> string -> (string * string) list ->
-    string list -> string -> string * dump_mode -> Url.T option * bool -> bool ->
+    string list -> string -> bool * string -> Url.T option * bool -> bool ->
     theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val init_theory: string -> unit
@@ -190,18 +188,10 @@
 
 (* session_info *)
 
-datatype dump_mode = Dump_all | Dump_tex | Dump_tex_sty;
-
-fun dump_mode "all" = Dump_all
-  | dump_mode "tex" = Dump_tex
-  | dump_mode "tex+sty" = Dump_tex_sty
-  | dump_mode s =
-      error ("Illegal document dump mode: " ^ quote s ^ " (expected \"all\", \"tex\", \"tex+sty\")");
-
 type session_info =
   {name: string, parent: string, session: string, path: string list, html_prefix: Path.T,
     info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
-    documents: (string * string) list, doc_dump: (string * dump_mode), remote_path: Url.T option,
+    documents: (string * string) list, doc_dump: (bool * string), remote_path: Url.T option,
     verbose: bool, readme: Path.T option};
 
 fun make_session_info
@@ -261,7 +251,7 @@
 fun name_of_session elems = space_implode "/" ("Isabelle" :: elems);
 
 fun init build info info_path doc doc_graph document_output doc_variants path name
-    (doc_dump as (dump_prefix, _)) (remote_path, first_time) verbose thys =
+    (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
@@ -348,7 +338,7 @@
 
 fun finish () =
   session_default () (fn {name, info, html_prefix, doc_format, doc_graph, doc_output,
-    documents, doc_dump = (dump_prefix, dump_mode), path, verbose, readme, ...} =>
+    documents, doc_dump = (dump_copy, dump_prefix), path, verbose, readme, ...} =>
   let
     val {theories, files, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
@@ -383,14 +373,11 @@
         else ())
       else ();
 
-    fun prepare_sources doc_dir doc_mode =
+    fun prepare_sources doc_copy doc_dir =
      (Isabelle_System.mkdirs doc_dir;
-      (case doc_mode of
-        Dump_all => Isabelle_System.copy_dir document_path doc_dir
-      | Dump_tex_sty =>
-          ignore (Isabelle_System.isabelle_tool "latex"
-            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex"))))
-      | Dump_tex => ());
+      if doc_copy then Isabelle_System.copy_dir document_path doc_dir else ();
+      Isabelle_System.isabelle_tool "latex"
+        ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
       (case opt_graphs of NONE => () | SOME (pdf, eps) =>
         (File.write (Path.append doc_dir graph_pdf_path) pdf;
           File.write (Path.append doc_dir graph_eps_path) eps));
@@ -402,7 +389,7 @@
       else
         let
           val path = Path.explode dump_prefix;
-          val _ = prepare_sources path dump_mode;
+          val _ = prepare_sources dump_copy path;
         in
           if verbose then
             Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
@@ -415,8 +402,8 @@
           File.eq (document_path, doc_prefix) andalso
             error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
         val dir = Path.append doc_prefix (Path.basic name);
-        val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
-        val _ = prepare_sources dir mode;
+        val copy = not (File.eq (document_path, dir));
+        val _ = prepare_sources copy dir;
         fun inform doc =
           if verbose orelse not backdrop then
             Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")