purge more thoroughly;
authorwenzelm
Tue Dec 12 17:53:59 2017 +0100 (17 months ago)
changeset 6719226f548370e8d
parent 67191 9ab34bb83a84
child 67193 4ade0d387429
purge more thoroughly;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Tue Dec 12 17:46:22 2017 +0100
     1.2 +++ b/src/Pure/Thy/present.ML	Tue Dec 12 17:53:59 2017 +0100
     1.3 @@ -194,11 +194,12 @@
     1.4        "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
     1.5          " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
     1.6      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
     1.7 +    val _ = if purge then Isabelle_System.rm_tree dir else ();
     1.8      val _ = if verbose then writeln script else ();
     1.9      val {out, err, rc, ...} = Bash.process script;
    1.10      val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
    1.11      val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
    1.12 -    val _ = if purge andalso rc = 0 then Isabelle_System.rm_tree dir else ();
    1.13 +    val _ = if purge then Isabelle_System.rm_tree dir else ();
    1.14    in doc_path end;
    1.15  
    1.16