# HG changeset patch
# User wenzelm
# Date 1505823985 -7200
# Node ID 74a1b722507e6c356fe27770893e9138d441d68c
# Parent  ed8d359d92e46ecdab311e7d493cbafd1469f769
clarified "purge": retain .aux files etc. before "isabelle document", to allow 'document_files' providing such generated files (see also c3ea910b3581, 38ce936acb99);

diff -r ed8d359d92e4 -r 74a1b722507e src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Sep 19 14:22:51 2017 +0200
+++ b/src/Pure/Thy/present.ML	Tue Sep 19 14:26:25 2017 +0200
@@ -196,7 +196,7 @@
 
 fun isabelle_document {verbose, purge} format name tags dir =
   let
-    val s = "isabelle document" ^ (if purge then " -c" else "") ^ " -o '" ^ format ^ "' \
+    val s = "isabelle document -o '" ^ format ^ "' \
       \-n '" ^ name ^ "' -t '" ^ tags ^ "' " ^ File.bash_path dir ^ " 2>&1";
     val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     val _ = if verbose then writeln s else ();
@@ -206,6 +206,7 @@
         cat_error out ("Failed to build document " ^ quote (show_path doc_path))
       else if verbose then writeln out
       else ();
+    val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
   in doc_path end;