tuned;
authorwenzelm
Thu Apr 10 18:29:32 2014 +0200 (2014-04-10)
changeset 56531ec4cd116844b
parent 56530 5c178501cf78
child 56532 3da244bc02bd
tuned;
src/Pure/Thy/present.ML
     1.1 --- a/src/Pure/Thy/present.ML	Thu Apr 10 18:13:44 2014 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Thu Apr 10 18:29:32 2014 +0200
     1.3 @@ -313,33 +313,36 @@
     1.4          else ())
     1.5        else ();
     1.6  
     1.7 -    fun prepare_sources doc_copy doc_dir =
     1.8 -     (Isabelle_System.mkdirs doc_dir;
     1.9 -      if doc_copy then Isabelle_System.copy_dir document_path doc_dir else ();
    1.10 -      Isabelle_System.isabelle_tool "latex"
    1.11 -        ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
    1.12 -      (case opt_graphs of NONE => () | SOME (pdf, eps) =>
    1.13 -        (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.14 -          File.write (Path.append doc_dir graph_eps_path) eps));
    1.15 -      write_tex_index tex_index doc_dir;
    1.16 -      List.app (fn (a, {tex_source, ...}) =>
    1.17 -        write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys);
    1.18 -
    1.19      fun document_job doc_prefix backdrop (name, tags) =
    1.20        let
    1.21          val _ =
    1.22            File.eq (document_path, doc_prefix) andalso
    1.23              error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    1.24 -        val dir = Path.append doc_prefix (Path.basic name);
    1.25 -        val copy = not (File.eq (document_path, dir));
    1.26 -        val _ = prepare_sources copy dir;
    1.27 -        fun inform doc =
    1.28 -          if verbose orelse not backdrop then
    1.29 -            Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
    1.30 -          else ();
    1.31 +        val doc_dir = Path.append doc_prefix (Path.basic name);
    1.32 +        val _ = Isabelle_System.mkdirs doc_dir;
    1.33 +        val _ =
    1.34 +          if File.eq (document_path, doc_dir) then ()
    1.35 +          else Isabelle_System.copy_dir document_path doc_dir;
    1.36 +        val _ =
    1.37 +          Isabelle_System.isabelle_tool "latex"
    1.38 +            ("-o sty " ^ File.shell_path (Path.append doc_dir (Path.basic "root.tex")));
    1.39 +        val _ =
    1.40 +          (case opt_graphs of
    1.41 +            NONE => ()
    1.42 +          | SOME (pdf, eps) =>
    1.43 +              (File.write (Path.append doc_dir graph_pdf_path) pdf;
    1.44 +                File.write (Path.append doc_dir graph_eps_path) eps));
    1.45 +        val _ = write_tex_index tex_index doc_dir;
    1.46 +        val _ =
    1.47 +          List.app (fn (a, {tex_source, ...}) =>
    1.48 +            write_tex (Buffer.add tex_source Buffer.empty) a doc_dir) thys;
    1.49        in
    1.50          fn () =>
    1.51 -          (isabelle_document {verbose = true, purge = backdrop} doc_format name tags dir, inform)
    1.52 +          (isabelle_document {verbose = true, purge = backdrop} doc_format name tags doc_dir,
    1.53 +            fn doc =>
    1.54 +              if verbose orelse not backdrop then
    1.55 +                Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
    1.56 +              else ())
    1.57        end;
    1.58  
    1.59      val jobs =