# HG changeset patch
# User wenzelm
# Date 1513184482 -3600
# Node ID b335e255ebcc94fd5058f44eb1ed4d0a53059116
# Parent  eb29f4868d1476b81455fe6e8d168cf872b5a768
purge more carefully (amending 26f548370e8d);
recovered 'display_drafts';

diff -r eb29f4868d14 -r b335e255ebcc src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Dec 13 17:42:17 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Wed Dec 13 18:01:22 2017 +0100
@@ -272,8 +272,7 @@
 fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
 
 fun symbol_source known name syms =
-  isabelle_body_delim name
-  |-> enclose
+  uncurry enclose (isabelle_body_delim name)
     ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
       output_known_symbols known syms);
 
diff -r eb29f4868d14 -r b335e255ebcc src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Wed Dec 13 17:42:17 2017 +0100
+++ b/src/Pure/Thy/present.ML	Wed Dec 13 18:01:22 2017 +0100
@@ -188,18 +188,16 @@
 
 (* isabelle tool wrappers *)
 
-fun isabelle_document {verbose, purge} format name tags dir =
+fun isabelle_document {verbose} format name tags dir =
   let
     val script =
       "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
         " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
-    val _ = if purge then Isabelle_System.rm_tree dir else ();
     val _ = if verbose then writeln script else ();
     val {out, err, rc, ...} = Bash.process script;
     val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
     val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
-    val _ = if purge then Isabelle_System.rm_tree dir else ();
   in doc_path end;
 
 
@@ -242,6 +240,8 @@
     fun document_job doc_prefix backdrop (doc_name, tags) =
       let
         val doc_dir = Path.append doc_prefix (Path.basic doc_name);
+        fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
+        val _ = purge ();
         val _ = Isabelle_System.mkdirs doc_dir;
         val _ =
           Isabelle_System.bash ("isabelle latex -o sty " ^
@@ -254,7 +254,7 @@
             write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
       in
         fn () =>
-          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
+          (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
             fn doc =>
               if verbose orelse not backdrop then
                 Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
@@ -359,8 +359,7 @@
       |> File.write (Path.append doc_path (tex_path name)));
     val _ = write_tex_index tex_index doc_path;
 
-    val result =
-      isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
+    val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
 
     val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
     val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"