1.1 --- a/src/Pure/Thy/present.ML	Sun Jun 13 15:30:08 2004 +0200
     1.2 +++ b/src/Pure/Thy/present.ML	Sun Jun 13 15:30:58 2004 +0200
     1.3 @@ -495,6 +495,17 @@
     1.4  
     1.5  fun drafts doc_format src_paths =
     1.6    let
     1.7 +    fun prep_draft (tex_index, path) =
     1.8 +      let
     1.9 +        val base = Path.base path;
    1.10 +        val name = Path.pack (#1 (Path.split_ext base));
    1.11 +      in
    1.12 +        if File.exists path then
    1.13 +          (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
    1.14 +        else error ("Bad file: " ^ quote (Path.pack path))
    1.15 +      end;
    1.16 +    val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
    1.17 +
    1.18      val doc_path = File.tmp_path (Path.basic "document");
    1.19      val _ = File.mkdir doc_path;
    1.20      val root_path = Path.append doc_path (Path.basic "root.tex");
    1.21 @@ -510,18 +521,10 @@
    1.22      val known_syms = known "syms.lst";
    1.23      val known_ctrls = known "ctrls.lst";
    1.24  
    1.25 -    fun write_draft (tex_index, path) =
    1.26 -      let
    1.27 -        val base = Path.base path;
    1.28 -        val name = Path.pack (#1 (Path.split_ext base));
    1.29 -      in
    1.30 -        Symbol.explode (File.read path)
    1.31 -        |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
    1.32 -        |> File.write (Path.append doc_path (tex_path name));
    1.33 -        Buffer.add (Latex.theory_entry name) tex_index
    1.34 -      end;
    1.35 -
    1.36 -    val tex_index = foldl write_draft (Buffer.empty, src_paths);
    1.37 +    val _ = srcs |> seq (fn (name, base, txt) =>
    1.38 +      Symbol.explode txt
    1.39 +      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
    1.40 +      |> File.write (Path.append doc_path (tex_path name)));
    1.41      val _ = write_tex_index tex_index doc_path;
    1.42      val _ = isatool_document doc_format doc_path;
    1.43    in Path.ext doc_format doc_path end;