1.1 --- a/src/Pure/PIDE/command.ML	Wed Nov 20 10:51:47 2013 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Wed Nov 20 11:55:52 2013 +0100
     1.3 @@ -6,14 +6,15 @@
     1.4  
     1.5  signature COMMAND =
     1.6  sig
     1.7 -  type blob = (string * string) Exn.result
     1.8 -  val read: (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition
     1.9 +  type blob = (string * string option) Exn.result
    1.10 +  val read_file: Path.T -> Position.T -> Path.T -> Token.file
    1.11 +  val read: (unit -> theory) -> Path.T -> blob list -> Token.T list -> Toplevel.transition
    1.12    type eval
    1.13    val eval_eq: eval * eval -> bool
    1.14    val eval_running: eval -> bool
    1.15    val eval_finished: eval -> bool
    1.16    val eval_result_state: eval -> Toplevel.state
    1.17 -  val eval: (unit -> theory) -> blob list -> Token.T list -> eval -> eval
    1.18 +  val eval: (unit -> theory) -> Path.T -> blob list -> Token.T list -> eval -> eval
    1.19    type print
    1.20    val print: bool -> (string * string list) list -> string ->
    1.21      eval -> print list -> print list option
    1.22 @@ -83,15 +84,23 @@
    1.23  
    1.24  (* read *)
    1.25  
    1.26 -type blob = (string * string) Exn.result;  (*file node name, digest or text*)
    1.27 +type blob = (string * string option) Exn.result;  (*file node name, digest or text*)
    1.28  
    1.29 -fun resolve_files blobs toks =
    1.30 +fun read_file master_dir pos src_path =
    1.31 +  let
    1.32 +    val full_path = File.check_file (File.full_path master_dir src_path);
    1.33 +    val _ = Position.report pos (Markup.path (Path.implode full_path));
    1.34 +  in {src_path = src_path, text = File.read full_path, pos = Path.position full_path} end;
    1.35 +
    1.36 +fun resolve_files master_dir blobs toks =
    1.37    (case Thy_Syntax.parse_spans toks of
    1.38      [span] => span
    1.39        |> Thy_Syntax.resolve_files (fn cmd => fn (path, pos) =>
    1.40          let
    1.41 -          fun make_file src_path (Exn.Res (file, text)) =
    1.42 -                let val _ = Position.report pos (Markup.path file);
    1.43 +          fun make_file src_path (Exn.Res (_, NONE)) =
    1.44 +                Exn.interruptible_capture (fn () => read_file master_dir pos src_path) ()
    1.45 +            | make_file src_path (Exn.Res (file, SOME text)) =
    1.46 +                let val _ = Position.report pos (Markup.path file)
    1.47                  in Exn.Res {src_path = src_path, text = text, pos = Position.file file} end
    1.48              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.49  
    1.50 @@ -105,7 +114,7 @@
    1.51        |> Thy_Syntax.span_content
    1.52    | _ => toks);
    1.53  
    1.54 -fun read init blobs span =
    1.55 +fun read init master_dir blobs span =
    1.56    let
    1.57      val outer_syntax = #2 (Outer_Syntax.get_syntax ());
    1.58      val command_reports = Outer_Syntax.command_reports outer_syntax;
    1.59 @@ -122,7 +131,7 @@
    1.60    in
    1.61      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.62      else
    1.63 -      (case Outer_Syntax.read_spans outer_syntax (resolve_files blobs span) of
    1.64 +      (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
    1.65          [tr] =>
    1.66            if Keyword.is_control (Toplevel.name_of tr) then
    1.67              Toplevel.malformed pos "Illegal control command"
    1.68 @@ -203,14 +212,14 @@
    1.69  
    1.70  in
    1.71  
    1.72 -fun eval init blobs span eval0 =
    1.73 +fun eval init master_dir blobs span eval0 =
    1.74    let
    1.75      val exec_id = Document_ID.make ();
    1.76      fun process () =
    1.77        let
    1.78          val tr =
    1.79            Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
    1.80 -            (fn () => read init blobs span |> Toplevel.exec_id exec_id) ();
    1.81 +            (fn () => read init master_dir blobs span |> Toplevel.exec_id exec_id) ();
    1.82        in eval_state span tr (eval_result eval0) end;
    1.83    in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
    1.84