# HG changeset patch
# User wenzelm
# Date 1384945446 -3600
# Node ID bfeb0ea6c2c0c0657119d3837f39f2fff091016a
# Parent  92961f196d9eabdea84b41e53cc513924fb74436
proper static resolution of files via Thy_Load.load_thy, instead of TTY fall-back;

diff -r 92961f196d9e -r bfeb0ea6c2c0 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Wed Nov 20 11:55:52 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 20 12:04:06 2013 +0100
@@ -106,10 +106,11 @@
 
           val src_paths = Keyword.command_files cmd path;
         in
-          if null blobs then []
-          else if length src_paths <> length blobs then
-            error ("Misalignment of inlined files" ^ Position.here pos)
-          else map2 make_file src_paths blobs
+          if null blobs then
+            map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
+          else if length src_paths = length blobs then
+            map2 make_file src_paths blobs
+          else error ("Misalignment of inlined files" ^ Position.here pos)
         end)
       |> Thy_Syntax.span_content
   | _ => toks);