removed obsolete option (see 74a1b722507e);
authorwenzelm
Sun Dec 10 18:43:08 2017 +0100 (17 months ago)
changeset 67177af5b89bc065c
parent 67176 13b5c3ff1954
child 67178 70576478bda9
removed obsolete option (see 74a1b722507e);
src/Pure/Thy/present.scala
     1.1 --- a/src/Pure/Thy/present.scala	Sun Dec 10 18:31:41 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.scala	Sun Dec 10 18:43:08 2017 +0100
     1.3 @@ -157,9 +157,10 @@
     1.4      document_name: String = default_document_name,
     1.5      document_format: String = default_document_format,
     1.6      document_dir: Option[Path] = None,
     1.7 -    clean: Boolean = false,
     1.8      tags: List[String] = Nil)
     1.9    {
    1.10 +    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
    1.11 +
    1.12      if (!document_formats.contains(document_format))
    1.13        error("Bad document output format: " + quote(document_format))
    1.14  
    1.15 @@ -187,16 +188,6 @@
    1.16      }
    1.17  
    1.18  
    1.19 -    /* clean target */
    1.20 -
    1.21 -    val document_target = Path.parent + Path.explode(document_name).ext(document_format)
    1.22 -
    1.23 -    if (clean) {
    1.24 -      bash("rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log " +
    1.25 -        File.bash_path(document_target)).check
    1.26 -    }
    1.27 -
    1.28 -
    1.29      /* prepare document */
    1.30  
    1.31      File.write(dir + Path.explode("isabelletags.sty"), document_tags(tags))
    1.32 @@ -226,9 +217,6 @@
    1.33  
    1.34      bash("[ -f " + root_bash(document_format) + " ] && cp -f " +
    1.35        root_bash(document_format) + " " + File.bash_path(document_target)).check
    1.36 -
    1.37 -    // beware!
    1.38 -    if (clean) Isabelle_System.rm_tree(dir)
    1.39    }
    1.40  
    1.41  
    1.42 @@ -237,7 +225,6 @@
    1.43    val isabelle_tool =
    1.44      Isabelle_Tool("document", "prepare theory session document", args =>
    1.45    {
    1.46 -    var clean = false
    1.47      var document_dir: Option[Path] = None
    1.48      var document_name = default_document_name
    1.49      var document_format = default_document_format
    1.50 @@ -247,7 +234,6 @@
    1.51  Usage: isabelle document [OPTIONS]
    1.52  
    1.53    Options are:
    1.54 -    -c           aggressive cleanup of -d DIR content
    1.55      -d DIR       document output directory (default """ +
    1.56        default_document_dir(default_document_name) + """)
    1.57      -n NAME      document name (default """ + quote(default_document_name) + """)
    1.58 @@ -259,7 +245,6 @@
    1.59    Prepare the theory session document in document directory, producing the
    1.60    specified output format.
    1.61  """,
    1.62 -      "c" -> (_ => clean = true),
    1.63        "d:" -> (arg => document_dir = Some(Path.explode(arg))),
    1.64        "n:" -> (arg => document_name = arg),
    1.65        "o:" -> (arg => document_format = arg),
    1.66 @@ -269,6 +254,6 @@
    1.67      if (more_args.nonEmpty) getopts.usage()
    1.68  
    1.69      build_document(document_dir = document_dir, document_name = document_name,
    1.70 -      document_format = document_format, clean = clean, tags = tags)
    1.71 +      document_format = document_format, tags = tags)
    1.72    })
    1.73  }