1.1 --- a/src/Pure/PIDE/command.ML Tue Nov 19 13:54:02 2013 +0100
1.2 +++ b/src/Pure/PIDE/command.ML Tue Nov 19 19:33:27 2013 +0100
1.3 @@ -6,13 +6,14 @@
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) Exn.result
1.9 + val read: (unit -> theory) -> blob list -> Token.T list -> Toplevel.transition
1.10 type eval
1.11 val eval_eq: eval * eval -> bool
1.12 val eval_running: eval -> bool
1.13 val eval_finished: eval -> bool
1.14 val eval_result_state: eval -> Toplevel.state
1.15 - val eval: (unit -> theory) -> Token.T list -> eval -> eval
1.16 + val eval: (unit -> theory) -> blob list -> Token.T list -> eval -> eval
1.17 type print
1.18 val print: bool -> (string * string list) list -> string ->
1.19 eval -> print list -> print list option
1.20 @@ -82,7 +83,19 @@
1.21
1.22 (* read *)
1.23
1.24 -fun read init span =
1.25 +type blob = (string * string) Exn.result; (*file node name, digest or text*)
1.26 +
1.27 +fun resolve_files blobs toks =
1.28 + (case Thy_Syntax.parse_spans toks of
1.29 + [span] => span
1.30 + |> Thy_Syntax.resolve_files (fn _ => fn (path, pos) =>
1.31 + blobs |> map (Exn.release #> (fn (file, text) =>
1.32 + let val _ = Position.report pos (Markup.path file);
1.33 + in {src_path = path (* FIXME *), text = text, pos = Position.file file} end)))
1.34 + |> Thy_Syntax.span_content
1.35 + | _ => toks);
1.36 +
1.37 +fun read init blobs span =
1.38 let
1.39 val outer_syntax = #2 (Outer_Syntax.get_syntax ());
1.40 val command_reports = Outer_Syntax.command_reports outer_syntax;
1.41 @@ -99,7 +112,7 @@
1.42 in
1.43 if is_malformed then Toplevel.malformed pos "Malformed command syntax"
1.44 else
1.45 - (case Outer_Syntax.read_spans outer_syntax span of
1.46 + (case Outer_Syntax.read_spans outer_syntax (resolve_files blobs span) of
1.47 [tr] =>
1.48 if Keyword.is_control (Toplevel.name_of tr) then
1.49 Toplevel.malformed pos "Illegal control command"
1.50 @@ -180,14 +193,14 @@
1.51
1.52 in
1.53
1.54 -fun eval init span eval0 =
1.55 +fun eval init blobs span eval0 =
1.56 let
1.57 val exec_id = Document_ID.make ();
1.58 fun process () =
1.59 let
1.60 val tr =
1.61 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
1.62 - (fn () => read init span |> Toplevel.exec_id exec_id) ();
1.63 + (fn () => read init blobs span |> Toplevel.exec_id exec_id) ();
1.64 in eval_state span tr (eval_result eval0) end;
1.65 in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
1.66