# HG changeset patch
# User wenzelm
# Date 1087133458 -7200
# Node ID c2441592be1416e5196860fb922867a3f7b13eb9
# Parent  bf9f525d4821a25b9ce86058caa3007aef98b7d1
tuned Present.drafts;

diff -r bf9f525d4821 -r c2441592be14 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sun Jun 13 15:30:08 2004 +0200
+++ b/src/Pure/Thy/present.ML	Sun Jun 13 15:30:58 2004 +0200
@@ -495,6 +495,17 @@
 
 fun drafts doc_format src_paths =
   let
+    fun prep_draft (tex_index, path) =
+      let
+        val base = Path.base path;
+        val name = Path.pack (#1 (Path.split_ext base));
+      in
+        if File.exists path then
+          (Buffer.add (Latex.theory_entry name) tex_index, (name, base, File.read path))
+        else error ("Bad file: " ^ quote (Path.pack path))
+      end;
+    val (tex_index, srcs) = foldl_map prep_draft (Buffer.empty, src_paths);
+
     val doc_path = File.tmp_path (Path.basic "document");
     val _ = File.mkdir doc_path;
     val root_path = Path.append doc_path (Path.basic "root.tex");
@@ -510,18 +521,10 @@
     val known_syms = known "syms.lst";
     val known_ctrls = known "ctrls.lst";
 
-    fun write_draft (tex_index, path) =
-      let
-        val base = Path.base path;
-        val name = Path.pack (#1 (Path.split_ext base));
-      in
-        Symbol.explode (File.read path)
-        |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
-        |> File.write (Path.append doc_path (tex_path name));
-        Buffer.add (Latex.theory_entry name) tex_index
-      end;
-
-    val tex_index = foldl write_draft (Buffer.empty, src_paths);
+    val _ = srcs |> seq (fn (name, base, txt) =>
+      Symbol.explode txt
+      |> Latex.symbol_source (known_syms, known_ctrls) (Path.pack base)
+      |> File.write (Path.append doc_path (tex_path name)));
     val _ = write_tex_index tex_index doc_path;
     val _ = isatool_document doc_format doc_path;
   in Path.ext doc_format doc_path end;