src/Pure/Thy/present.ML
changeset 48935 4c92a2f310b6
parent 48933 d25e47e32bc0
child 49561 26fc70e983c2
     1.1 --- a/src/Pure/Thy/present.ML	Mon Aug 27 16:00:42 2012 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Mon Aug 27 16:07:48 2012 +0200
     1.3 @@ -429,25 +429,32 @@
     1.4            else ()
     1.5          end;
     1.6  
     1.7 -    val doc_paths =
     1.8 -      documents |> Par_List.map (fn (name, tags) =>
     1.9 -        let
    1.10 -          val (doc_prefix, purge) =
    1.11 -            (case doc_output of
    1.12 -              SOME path => (path, false)
    1.13 -            | NONE => (html_prefix, true));
    1.14 -          val _ =
    1.15 -            File.eq (document_path, doc_prefix) andalso
    1.16 -              error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    1.17 -          val dir = Path.append doc_prefix (Path.basic name);
    1.18 -          val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
    1.19 -          val _ = prepare_sources dir mode;
    1.20 -        in isabelle_document {verbose = true, purge = purge} doc_format name tags dir end);
    1.21 -    val _ =
    1.22 -      if verbose orelse is_some doc_output then
    1.23 -        doc_paths
    1.24 -        |> List.app (fn doc => Output.physical_stderr ("Document at " ^ show_path doc ^ "\n"))
    1.25 -      else ();
    1.26 +    fun document_job doc_prefix backdrop (name, tags) =
    1.27 +      let
    1.28 +        val _ =
    1.29 +          File.eq (document_path, doc_prefix) andalso
    1.30 +            error ("Overlap of document input and output directory " ^ Path.print doc_prefix);
    1.31 +        val dir = Path.append doc_prefix (Path.basic name);
    1.32 +        val mode = if File.eq (document_path, dir) then Dump_tex_sty else Dump_all;
    1.33 +        val _ = prepare_sources dir mode;
    1.34 +        fun inform doc =
    1.35 +          if verbose orelse not backdrop then
    1.36 +            Output.physical_stderr ("Document at " ^ show_path doc ^ "\n")
    1.37 +          else ();
    1.38 +      in
    1.39 +        fn () =>
    1.40 +          (isabelle_document {verbose = true, purge = backdrop} doc_format name tags dir, inform)
    1.41 +      end;
    1.42 +
    1.43 +    val jobs =
    1.44 +      (if info orelse is_none doc_output then
    1.45 +        map (document_job html_prefix true) documents
    1.46 +       else []) @
    1.47 +      (case doc_output of
    1.48 +        NONE => []
    1.49 +      | SOME path => map (document_job path false) documents);
    1.50 +
    1.51 +    val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>);
    1.52    in
    1.53      browser_info := empty_browser_info;
    1.54      session_info := NONE