# HG changeset patch # User wenzelm # Date 1426194051 -3600 # Node ID c043306d2598710f43984dcb4e84a9f4ddfc4e30 # Parent 86a76300137e5c3bfc4d7e8d4e02ae5d7704d3aa clarified markup for embedded files, early before execution; diff -r 86a76300137e -r c043306d2598 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Thu Mar 12 20:34:08 2015 +0100 +++ b/src/Pure/PIDE/command.ML Thu Mar 12 22:00:51 2015 +0100 @@ -51,21 +51,19 @@ fun read_file_node file_node master_dir pos src_path = let - val _ = Position.report pos Markup.language_path; val _ = (case try Url.explode file_node of NONE => () | SOME (Url.File _) => () | _ => - (Position.report pos (Markup.path file_node); error ("Prover cannot load remote file " ^ - Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos))); + Markup.markup (Markup.path file_node) (quote file_node))); val full_path = File.check_file (File.full_path master_dir src_path); - val _ = Position.report pos (Markup.path (Path.implode full_path)); val text = File.read full_path; val lines = split_lines text; val digest = SHA1.digest text; - in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end; + in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end + handle ERROR msg => error (msg ^ Position.here pos); val read_file = read_file_node ""; @@ -89,8 +87,7 @@ Exn.interruptible_capture (fn () => read_file_node file_node master_dir pos src_path) () | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = - (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)]; - Exn.Res (blob_file src_path lines digest file_node)) + Exn.Res (blob_file src_path lines digest file_node) | make_file _ (Exn.Exn e) = Exn.Exn e; val src_paths = Keyword.command_files keywords cmd path; in diff -r 86a76300137e -r c043306d2598 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu Mar 12 20:34:08 2015 +0100 +++ b/src/Pure/PIDE/document.ML Thu Mar 12 22:00:51 2015 +0100 @@ -19,7 +19,7 @@ val init_state: state val define_blob: string -> string -> state -> state type blob_digest = (string * string option) Exn.result - val define_command: Document_ID.command -> string -> blob_digest list -> + val define_command: Document_ID.command -> string -> blob_digest list -> int -> ((int * int) * string) list -> state -> state val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state @@ -359,23 +359,37 @@ blob_digest |> Exn.map_result (fn (file_node, raw_digest) => (file_node, Option.map (the_blob state) raw_digest)); +fun blob_reports pos (blob_digest: blob_digest) = + (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []); + (* commands *) -fun define_command command_id name command_blobs toks = +fun define_command command_id name command_blobs blobs_index toks = map_state (fn (versions, blobs, commands, execution) => let val id = Document_ID.print command_id; val span = Lazy.lazy (fn () => Position.setmp_thread_data (Position.id_only id) - (fn () => #1 (fold_map Token.make toks (Position.id id))) ()); + (fn () => + let + val (tokens, _) = fold_map Token.make toks (Position.id id); + val _ = + (case try (Token.pos_of o nth tokens) blobs_index of + SOME pos => + if Position.is_reported pos then + Position.reports + ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs) + else () + | NONE => ()); + in tokens end) ()); + val commands' = + Inttab.update_new (command_id, (name, command_blobs, span)) commands + handle Inttab.DUP dup => err_dup "command" dup; val _ = Position.setmp_thread_data (Position.id_only id) (fn () => Output.status (Markup.markup_only Markup.accepted)) (); - val commands' = - Inttab.update_new (command_id, (name, command_blobs, span)) commands - handle Inttab.DUP dup => err_dup "command" dup; in (versions, blobs, commands', execution) end); fun the_command (State {commands, ...}) command_id = diff -r 86a76300137e -r c043306d2598 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu Mar 12 20:34:08 2015 +0100 +++ b/src/Pure/PIDE/protocol.ML Thu Mar 12 22:00:51 2015 +0100 @@ -30,17 +30,20 @@ Isabelle_Process.protocol_command "Document.define_command" (fn id :: name :: blobs_yxml :: toks_yxml :: sources => let - val blobs = + val (blobs, blobs_index) = YXML.parse_body blobs_yxml |> let open XML.Decode in - list (variant - [fn ([], a) => Exn.Res (pair string (option string) a), - fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]) + pair + (list (variant + [fn ([], a) => Exn.Res (pair string (option string) a), + fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])) + int end; val toks = (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources; in - Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks) + Document.change_state + (Document.define_command (Document_ID.parse id) name blobs blobs_index toks) end); val _ = diff -r 86a76300137e -r c043306d2598 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu Mar 12 20:34:08 2015 +0100 +++ b/src/Pure/PIDE/protocol.scala Thu Mar 12 22:00:51 2015 +0100 @@ -392,7 +392,7 @@ (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) }, { case Exn.Exn(e) => (Nil, string(Exn.message(e))) })) - YXML.string_of_body(list(encode_blob)(command.blobs)) + YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index)) } val toks = command.span.content