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 () =