# HG changeset patch
# User wenzelm
# Date 1397146424 -7200
# Node ID 5c178501cf784ea478aa12dd06181dcf22fc729e
# Parent  a13c2ccc160b7622642b0e0e38dd9bc4699df0e3
removed obsolete doc_dump option (see also 892061142ba6);

diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Thu Apr 10 15:14:38 2014 +0200
+++ b/src/Pure/PIDE/session.ML	Thu Apr 10 18:13:44 2014 +0200
@@ -9,7 +9,7 @@
   val name: unit -> string
   val welcome: unit -> string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
-    string -> string * string -> bool * string -> bool -> unit
+    string -> string * string -> bool -> unit
   val finish: unit -> unit
   val protocol_handler: string -> unit
   val init_protocol_handlers: unit -> unit
@@ -34,7 +34,7 @@
 (* init *)
 
 fun init build info info_path doc doc_graph doc_output doc_variants
-    parent (chapter, name) doc_dump verbose =
+    parent (chapter, name) verbose =
   if #name (! session) <> parent orelse not (! session_finished) then
     error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
   else
@@ -44,7 +44,7 @@
     in
       Present.init build info info_path (if doc = "false" then "" else doc)
         doc_graph doc_output doc_variants (chapter, name)
-        doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
+        verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
     end;
 
 
diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Apr 10 15:14:38 2014 +0200
+++ b/src/Pure/Thy/present.ML	Thu Apr 10 18:13:44 2014 +0200
@@ -9,7 +9,7 @@
   val session_name: theory -> string
   val read_variant: string -> string * string
   val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
-    string * string -> bool * string -> bool -> theory list -> unit  (*not thread-safe!*)
+    string * string -> bool -> theory list -> unit  (*not thread-safe!*)
   val finish: unit -> unit  (*not thread-safe!*)
   val theory_output: string -> string -> unit
   val begin_theory: int -> (unit -> HTML.text) -> theory -> theory
@@ -168,17 +168,17 @@
 (* session_info *)
 
 type session_info =
-  {name: string, chapter: string, info_path: Path.T,
-    info: bool, doc_format: string, doc_graph: bool, doc_output: Path.T option,
-    documents: (string * string) list, doc_dump: (bool * string), verbose: bool,
+  {name: string, chapter: string, info_path: Path.T, info: bool,
+    doc_format: string, doc_graph: bool, doc_output: Path.T option,
+    documents: (string * string) list, verbose: bool,
     readme: Path.T option};
 
 fun make_session_info
   (name, chapter, info_path, info, doc_format, doc_graph, doc_output,
-    documents, doc_dump, verbose, readme) =
+    documents, verbose, readme) =
   {name = name, chapter = chapter, info_path = info_path, info = info,
     doc_format = doc_format, doc_graph = doc_graph, doc_output = doc_output,
-    documents = documents, doc_dump = doc_dump, verbose = verbose,
+    documents = documents, verbose = verbose,
     readme = readme}: session_info;
 
 
@@ -204,8 +204,8 @@
 (* init session *)
 
 fun init build info info_path doc doc_graph document_output doc_variants
-    (chapter, name) (doc_dump as (_, dump_prefix)) verbose thys =
-  if not build andalso not info andalso doc = "" andalso dump_prefix = "" then
+    (chapter, name) verbose thys =
+  if not build andalso not info andalso doc = "" then
     (browser_info := empty_browser_info; session_info := NONE)
   else
     let
@@ -227,7 +227,7 @@
     in
       session_info :=
         SOME (make_session_info (name, chapter, info_path, info, doc,
-          doc_graph, doc_output, documents, doc_dump, verbose, readme));
+          doc_graph, doc_output, documents, verbose, readme));
       browser_info := init_browser_info (chapter, name) thys;
       add_html_index (0, HTML.begin_session_index name docs (Url.explode "medium.html"))
     end;
@@ -278,7 +278,7 @@
 
 fun finish () =
   with_session_info () (fn {name, chapter, info, info_path, doc_format, doc_graph, doc_output,
-    documents, doc_dump = (dump_copy, dump_prefix), verbose, readme, ...} =>
+    documents, verbose, readme, ...} =>
   let
     val {theories, tex_index, html_index, graph} = ! browser_info;
     val thys = Symtab.dest theories;
@@ -291,7 +291,7 @@
 
     val sorted_graph = sorted_index graph;
     val opt_graphs =
-      if doc_graph andalso (not (null documents) orelse dump_prefix <> "") then
+      if doc_graph andalso not (null documents) then
         SOME (isabelle_browser sorted_graph)
       else NONE;
 
@@ -325,18 +325,6 @@
       List.app (fn (a, {tex_source, ...}) =>
         write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys);
 
-    val _ =
-      if dump_prefix = "" then ()
-      else
-        let
-          val path = Path.explode dump_prefix;
-          val _ = prepare_sources dump_copy path;
-        in
-          if verbose then
-            Output.physical_stderr ("Document sources at " ^ show_path path ^ "\n")
-          else ()
-        end;
-
     fun document_job doc_prefix backdrop (name, tags) =
       let
         val _ =
diff -r a13c2ccc160b -r 5c178501cf78 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Apr 10 15:14:38 2014 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 10 18:13:44 2014 +0200
@@ -157,7 +157,6 @@
           (Options.string options "document_output")
           document_variants
           parent_name (chapter, name)
-          (false, "")
           verbose;
 
       val last_timing = lookup_timings (fold update_timings command_timings empty_timings);