# HG changeset patch # User wenzelm # Date 1384944952 -3600 # Node ID 92961f196d9eabdea84b41e53cc513924fb74436 # Parent de7c13e25212576f7526ab849ff90760ce0c4520 load files that are not provided by PIDE blobs; uniform resolve_files via Command.read; diff -r de7c13e25212 -r 92961f196d9e src/Pure/PIDE/command.ML --- 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; diff -r de7c13e25212 -r 92961f196d9e src/Pure/PIDE/document.ML --- 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'); diff -r de7c13e25212 -r 92961f196d9e src/Pure/PIDE/protocol.ML --- 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) diff -r de7c13e25212 -r 92961f196d9e src/Pure/PIDE/protocol.scala --- 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", diff -r de7c13e25212 -r 92961f196d9e src/Pure/Thy/thy_load.ML --- 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 () =