# 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;