# HG changeset patch
# User wenzelm
# Date 1512927788 -3600
# Node ID af5b89bc065c504985fcd59c1f901da0506da5ad
# Parent  13b5c3ff195489593c108d7e09ba47a4ef44084d
removed obsolete option (see 74a1b722507e);

diff -r 13b5c3ff1954 -r af5b89bc065c src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Sun Dec 10 18:31:41 2017 +0100
+++ b/src/Pure/Thy/present.scala	Sun Dec 10 18:43:08 2017 +0100
@@ -157,9 +157,10 @@
     document_name: String = default_document_name,
     document_format: String = default_document_format,
     document_dir: Option[Path] = None,
-    clean: Boolean = false,
     tags: List[String] = Nil)
   {
+    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
+
     if (!document_formats.contains(document_format))
       error("Bad document output format: " + quote(document_format))
 
@@ -187,16 +188,6 @@
     }
 
 
-    /* clean target */
-
-    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
-
-    if (clean) {
-      bash("rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log " +
-        File.bash_path(document_target)).check
-    }
-
-
     /* prepare document */
 
     File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
@@ -226,9 +217,6 @@
 
     bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
       root_bash(document_format) + " " + File.bash_path(document_target)).check
-
-    // beware!
-    if (clean) Isabelle_System.rm_tree(dir)
   }
 
 
@@ -237,7 +225,6 @@
   val isabelle_tool =
     Isabelle_Tool("document", "prepare theory session document", args =>
   {
-    var clean = false
     var document_dir: Option[Path] = None
     var document_name = default_document_name
     var document_format = default_document_format
@@ -247,7 +234,6 @@
 Usage: isabelle document [OPTIONS]
 
   Options are:
-    -c           aggressive cleanup of -d DIR content
     -d DIR       document output directory (default """ +
       default_document_dir(default_document_name) + """)
     -n NAME      document name (default """ + quote(default_document_name) + """)
@@ -259,7 +245,6 @@
   Prepare the theory session document in document directory, producing the
   specified output format.
 """,
-      "c" -> (_ => clean = true),
       "d:" -> (arg => document_dir = Some(Path.explode(arg))),
       "n:" -> (arg => document_name = arg),
       "o:" -> (arg => document_format = arg),
@@ -269,6 +254,6 @@
     if (more_args.nonEmpty) getopts.usage()
 
     build_document(document_dir = document_dir, document_name = document_name,
-      document_format = document_format, clean = clean, tags = tags)
+      document_format = document_format, tags = tags)
   })
 }