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