purge more carefully (amending 26f548370e8d);
authorwenzelm
Wed Dec 13 18:01:22 2017 +0100 (17 months ago)
changeset 67197b335e255ebcc
parent 67196 eb29f4868d14
child 67198 694f29a5433b
purge more carefully (amending 26f548370e8d);
recovered 'display_drafts';
src/Pure/Thy/latex.ML
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Dec 13 17:42:17 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Dec 13 18:01:22 2017 +0100
     1.3 @@ -272,8 +272,7 @@
     1.4  fun isabelle_body name = isabelle_body_delim name |-> enclose_body;
     1.5  
     1.6  fun symbol_source known name syms =
     1.7 -  isabelle_body_delim name
     1.8 -  |-> enclose
     1.9 +  uncurry enclose (isabelle_body_delim name)
    1.10      ("\\isamarkupfile{" ^ output_known_symbols known (Symbol.explode name) ^ "}%\n" ^
    1.11        output_known_symbols known syms);
    1.12  
     2.1 --- a/src/Pure/Thy/present.ML	Wed Dec 13 17:42:17 2017 +0100
     2.2 +++ b/src/Pure/Thy/present.ML	Wed Dec 13 18:01:22 2017 +0100
     2.3 @@ -188,18 +188,16 @@
     2.4  
     2.5  (* isabelle tool wrappers *)
     2.6  
     2.7 -fun isabelle_document {verbose, purge} format name tags dir =
     2.8 +fun isabelle_document {verbose} format name tags dir =
     2.9    let
    2.10      val script =
    2.11        "isabelle document -d " ^ File.bash_path dir ^ " -o " ^ Bash.string format ^
    2.12          " -n " ^ Bash.string name ^ " -t " ^ Bash.string tags;
    2.13      val doc_path = Path.appends [dir, Path.parent, Path.basic name |> Path.ext format];
    2.14 -    val _ = if purge then Isabelle_System.rm_tree dir else ();
    2.15      val _ = if verbose then writeln script else ();
    2.16      val {out, err, rc, ...} = Bash.process script;
    2.17      val _ = if verbose then writeln (trim_line (normalize_lines out)) else ();
    2.18      val _ = if not (File.exists doc_path) orelse rc <> 0 then error (trim_line err) else ();
    2.19 -    val _ = if purge then Isabelle_System.rm_tree dir else ();
    2.20    in doc_path end;
    2.21  
    2.22  
    2.23 @@ -242,6 +240,8 @@
    2.24      fun document_job doc_prefix backdrop (doc_name, tags) =
    2.25        let
    2.26          val doc_dir = Path.append doc_prefix (Path.basic doc_name);
    2.27 +        fun purge () = if backdrop then Isabelle_System.rm_tree doc_dir else ();
    2.28 +        val _ = purge ();
    2.29          val _ = Isabelle_System.mkdirs doc_dir;
    2.30          val _ =
    2.31            Isabelle_System.bash ("isabelle latex -o sty " ^
    2.32 @@ -254,7 +254,7 @@
    2.33              write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
    2.34        in
    2.35          fn () =>
    2.36 -          (isabelle_document {verbose = true, purge = backdrop} doc_format doc_name tags doc_dir,
    2.37 +          (isabelle_document {verbose = true} doc_format doc_name tags doc_dir before purge (),
    2.38              fn doc =>
    2.39                if verbose orelse not backdrop then
    2.40                  Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
    2.41 @@ -359,8 +359,7 @@
    2.42        |> File.write (Path.append doc_path (tex_path name)));
    2.43      val _ = write_tex_index tex_index doc_path;
    2.44  
    2.45 -    val result =
    2.46 -      isabelle_document {verbose = false, purge = true} "pdf" documentN "" doc_path;
    2.47 +    val result = isabelle_document {verbose = false} "pdf" documentN "" doc_path;
    2.48  
    2.49      val target_dir = Path.explode "$ISABELLE_HOME_USER/tmp";
    2.50      val target = Path.explode "$ISABELLE_HOME_USER/tmp/drafts.pdf"