load files that are not provided by PIDE blobs;
uniform resolve_files via Command.read;

--- a/src/Pure/PIDE/command.ML	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/PIDE/command.ML	Wed Nov 20 11:55:52 2013 +0100
@@ -6,14 +6,15 @@
 
 signature COMMAND =
 sig
-  type blob = (string * string) Exn.result
-  val read: (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition
+  type blob = (string * string option) Exn.result
+  val read_file: Path.T -> Position.T -> Path.T -> Token.file
+  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
   type eval
   val eval_eq: eval * eval -> bool
   val eval_running: eval -> bool
   val eval_finished: eval -> bool
   val eval_result_state: eval -> Toplevel.state
-  val eval: (unit -> theory) -> blob list -> Token.T list -> eval -> eval
+  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
   type print
   val print: bool -> (string * string list) list -> string ->
     eval -> print list -> print list option
@@ -83,15 +84,23 @@
 
 (* read *)
 
-type blob = (string * string) Exn.result;  (*file node name, digest or text*)
+type blob = (string * string option) Exn.result;  (*file node name, digest or text*)
 
-fun resolve_files blobs toks =
+fun read_file master_dir pos src_path =
+  let
+    val full_path = File.check_file (File.full_path master_dir src_path);
+    val _ = Position.report pos (Markup.path (Path.implode full_path));
+  in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
+
+fun resolve_files master_dir blobs toks =
   (case Thy_Syntax.parse_spans toks of
     [span] => span
       |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
         let
-          fun make_file src_path (Exn.Res (file, text)) =
-                let val _ = Position.report pos (Markup.path file);
+          fun make_file src_path (Exn.Res (_, NONE)) =
+                Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
+            | make_file src_path (Exn.Res (file, SOME text)) =
+                let val _ = Position.report pos (Markup.path file)
                 in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
             | make_file _ (Exn.Exn e) = Exn.Exn e;
 
@@ -105,7 +114,7 @@
       |> Thy_Syntax.span_content
   | _ => toks);
 
-fun read init blobs span =
+fun read init master_dir blobs span =
   let
     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
     val command_reports = Outer_Syntax.command_reports outer_syntax;
@@ -122,7 +131,7 @@
   in
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
-      (case Outer_Syntax.read_spans outer_syntax (resolve_files blobs span) of
+      (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
         [tr] =>
           if Keyword.is_control (Toplevel.name_of tr) then
             Toplevel.malformed pos "Illegal control command"
@@ -203,14 +212,14 @@
 
 in
 
-fun eval init blobs span eval0 =
+fun eval init master_dir blobs span eval0 =
   let
     val exec_id = Document_ID.make ();
     fun process () =
       let
         val tr =
           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
-            (fn () => read init blobs span |> Toplevel.exec_id exec_id) ();
+            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
       in eval_state span tr (eval_result eval0) end;
   in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
 

--- a/src/Pure/PIDE/document.ML	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Wed Nov 20 11:55:52 2013 +0100
@@ -90,9 +90,14 @@
 
 fun read_header node span =
   let
-    val (dir, {name = (name, _), imports, keywords}) = get_header node;
+    val {name = (name, _), imports, keywords} = #2 (get_header node);
     val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
-  in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end;
+  in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
+
+fun master_directory node =
+  (case try Url.explode (#1 (get_header node)) of
+    SOME (Url.File path) => path
+  | _ => Path.current);
 
 fun get_perspective (Node {perspective, ...}) = perspective;
 fun set_perspective args =
@@ -329,7 +334,7 @@
     val blobs' =
       (commands', Symtab.empty) |->
         Inttab.fold (fn (_, (_, blobs, _)) => blobs |>
-          fold (fn Exn.Res (_, digest) => Symtab.update (digest, the_blob state digest) | _ => I));
+          fold (fn Exn.Res (_, SOME b) => Symtab.update (b, the_blob state b) | _ => I));
 
   in (versions', blobs', commands', execution) end);
 
@@ -421,12 +426,8 @@
 
 fun init_theory deps node span =
   let
-    (* FIXME provide files via Isabelle/Scala, not master_dir *)
-    val (dir, header) = read_header node span;
-    val master_dir =
-      (case try Url.explode dir of
-        SOME (Url.File path) => path
-      | _ => Path.current);
+    val master_dir = master_directory node;
+    val header = read_header node span;
     val imports = #imports header;
     val parents =
       imports |> map (fn (import, _) =>
@@ -500,11 +501,12 @@
       val command_visible = visible_command node command_id';
       val command_overlays = overlays node command_id';
       val (command_name, blobs0, span0) = the_command state command_id';
-      val blobs = map (Exn.map_result (apsnd (the_blob state))) blobs0;
+      val blobs = (map o Exn.map_result o apsnd o Option.map) (the_blob state) blobs0;
       val span = Lazy.force span0;
 
       val eval' =
-        Command.eval (fn () => the_default illegal_init init span) blobs span eval;
+        Command.eval (fn () => the_default illegal_init init span)
+          (master_directory node) blobs span eval;
       val prints' = perhaps (Command.print command_visible command_overlays command_name eval') [];
       val exec' = (eval', prints');
 

--- a/src/Pure/PIDE/protocol.ML	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/PIDE/protocol.ML	Wed Nov 20 11:55:52 2013 +0100
@@ -34,8 +34,8 @@
           YXML.parse_body blobs_yxml |>
             let open XML.Decode in
               list (variant
-               [fn ([a, b], []) => Exn.Res (a, b),
-                fn ([a], []) => Exn.Exn (ERROR a)])
+               [fn ([], a) => Exn.Res (pair string (option string) a),
+                fn ([], a) => Exn.Exn (ERROR (string a))])
             end;
       in
         Document.change_state (Document.define_command (Document_ID.parse id) name blobs text)

--- a/src/Pure/PIDE/protocol.scala	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Nov 20 11:55:52 2013 +0100
@@ -322,9 +322,9 @@
     { import XML.Encode._
       val encode_blob: T[Command.Blob] =
         variant(List(
-          { case Exn.Res((a, Some(b))) => (List(a.node, b.toString), Nil) },
-          { case Exn.Res((a, None)) => (List("Missing file: " + quote(a.toString)), Nil)
-            case Exn.Exn(e) => (List(Exn.message(e)), Nil) }))
+          { case Exn.Res((a, b)) =>
+              (Nil, pair(string, option(string))((a.node, b.map(_.toString)))) },
+          { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
       YXML.string_of_body(list(encode_blob)(command.blobs))
     }
     protocol_command("Document.define_command",

--- a/src/Pure/Thy/thy_load.ML	Wed Nov 20 10:51:47 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Nov 20 11:55:52 2013 +0100
@@ -77,29 +77,19 @@
   end;
 
 
-(* inlined files *)
-
-fun read_files dir cmd (path, pos) =
-  let
-    fun make_file src_path =
-      let
-        val full_path = check_file dir src_path;
-        val _ = Position.report pos (Markup.path (Path.implode full_path));
-      in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
-  in map make_file (Keyword.command_files cmd path) end;
+(* load files *)
 
 fun parse_files cmd =
   Scan.ahead Parse.not_eof -- Parse.path >> (fn (tok, name) => fn thy =>
     (case Token.get_files tok of
-      [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
+      [] =>
+        let
+          val master_dir = master_directory thy;
+          val pos = Token.position_of tok;
+          val src_paths = Keyword.command_files cmd (Path.explode name);
+        in map (Command.read_file master_dir pos) src_paths end
     | files => map Exn.release files));
 
-fun resolve_files master_dir =
-  Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir);
-
-
-(* load files *)
-
 fun provide (src_path, id) =
   map_files (fn (master_dir, imports, provided) =>
     if AList.defined (op =) provided src_path then
@@ -140,11 +130,11 @@
   |> put_deps master_dir imports
   |> fold Thy_Header.declare_keyword keywords;
 
-fun excursion last_timing init elements =
+fun excursion master_dir last_timing init elements =
   let
     fun prepare_span span =
       Thy_Syntax.span_content span
-      |> Command.read init []
+      |> Command.read init master_dir []
       |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
 
     fun element_result span_elem (st, _) =
@@ -169,7 +159,7 @@
 
     val lexs = Keyword.get_lexicons ();
     val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
+    val spans = Thy_Syntax.parse_spans toks;
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =
@@ -178,7 +168,8 @@
           (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val (results, thy) = cond_timeit time "" (fn () => excursion last_timing init elements);
+    val (results, thy) =
+      cond_timeit time "" (fn () => excursion master_dir last_timing init elements);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
 
     fun present () =