clarified markup for embedded files, early before execution;
authorwenzelm
Thu Mar 12 22:00:51 2015 +0100 (2015-03-12)
changeset 59685c043306d2598
parent 59684 86a76300137e
child 59686 68996aa77829
clarified markup for embedded files, early before execution;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
src/Pure/PIDE/protocol.ML
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Mar 12 20:34:08 2015 +0100
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Mar 12 22:00:51 2015 +0100
     1.3 @@ -51,21 +51,19 @@
     1.4  
     1.5  fun read_file_node file_node master_dir pos src_path =
     1.6    let
     1.7 -    val _ = Position.report pos Markup.language_path;
     1.8      val _ =
     1.9        (case try Url.explode file_node of
    1.10          NONE => ()
    1.11        | SOME (Url.File _) => ()
    1.12        | _ =>
    1.13 -         (Position.report pos (Markup.path file_node);
    1.14            error ("Prover cannot load remote file " ^
    1.15 -            Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
    1.16 +            Markup.markup (Markup.path file_node) (quote file_node)));
    1.17      val full_path = File.check_file (File.full_path master_dir src_path);
    1.18 -    val _ = Position.report pos (Markup.path (Path.implode full_path));
    1.19      val text = File.read full_path;
    1.20      val lines = split_lines text;
    1.21      val digest = SHA1.digest text;
    1.22 -  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
    1.23 +  in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end
    1.24 +  handle ERROR msg => error (msg ^ Position.here pos);
    1.25  
    1.26  val read_file = read_file_node "";
    1.27  
    1.28 @@ -89,8 +87,7 @@
    1.29                  Exn.interruptible_capture (fn () =>
    1.30                    read_file_node file_node master_dir pos src_path) ()
    1.31              | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
    1.32 -               (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
    1.33 -                Exn.Res (blob_file src_path lines digest file_node))
    1.34 +                Exn.Res (blob_file src_path lines digest file_node)
    1.35              | make_file _ (Exn.Exn e) = Exn.Exn e;
    1.36            val src_paths = Keyword.command_files keywords cmd path;
    1.37          in
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 12 20:34:08 2015 +0100
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 12 22:00:51 2015 +0100
     2.3 @@ -19,7 +19,7 @@
     2.4    val init_state: state
     2.5    val define_blob: string -> string -> state -> state
     2.6    type blob_digest = (string * string option) Exn.result
     2.7 -  val define_command: Document_ID.command -> string -> blob_digest list ->
     2.8 +  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     2.9      ((int * int) * string) list -> state -> state
    2.10    val remove_versions: Document_ID.version list -> state -> state
    2.11    val start_execution: state -> state
    2.12 @@ -359,23 +359,37 @@
    2.13    blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
    2.14      (file_node, Option.map (the_blob state) raw_digest));
    2.15  
    2.16 +fun blob_reports pos (blob_digest: blob_digest) =
    2.17 +  (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
    2.18 +
    2.19  
    2.20  (* commands *)
    2.21  
    2.22 -fun define_command command_id name command_blobs toks =
    2.23 +fun define_command command_id name command_blobs blobs_index toks =
    2.24    map_state (fn (versions, blobs, commands, execution) =>
    2.25      let
    2.26        val id = Document_ID.print command_id;
    2.27        val span =
    2.28          Lazy.lazy (fn () =>
    2.29            Position.setmp_thread_data (Position.id_only id)
    2.30 -            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
    2.31 +            (fn () =>
    2.32 +              let
    2.33 +                val (tokens, _) = fold_map Token.make toks (Position.id id);
    2.34 +                val _ =
    2.35 +                  (case try (Token.pos_of o nth tokens) blobs_index of
    2.36 +                    SOME pos =>
    2.37 +                      if Position.is_reported pos then
    2.38 +                        Position.reports
    2.39 +                          ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
    2.40 +                      else ()
    2.41 +                  | NONE => ());
    2.42 +              in tokens end) ());
    2.43 +      val commands' =
    2.44 +        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    2.45 +          handle Inttab.DUP dup => err_dup "command" dup;
    2.46        val _ =
    2.47          Position.setmp_thread_data (Position.id_only id)
    2.48            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    2.49 -      val commands' =
    2.50 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    2.51 -          handle Inttab.DUP dup => err_dup "command" dup;
    2.52      in (versions, blobs, commands', execution) end);
    2.53  
    2.54  fun the_command (State {commands, ...}) command_id =
     3.1 --- a/src/Pure/PIDE/protocol.ML	Thu Mar 12 20:34:08 2015 +0100
     3.2 +++ b/src/Pure/PIDE/protocol.ML	Thu Mar 12 22:00:51 2015 +0100
     3.3 @@ -30,17 +30,20 @@
     3.4    Isabelle_Process.protocol_command "Document.define_command"
     3.5      (fn id :: name :: blobs_yxml :: toks_yxml :: sources =>
     3.6        let
     3.7 -        val blobs =
     3.8 +        val (blobs, blobs_index) =
     3.9            YXML.parse_body blobs_yxml |>
    3.10              let open XML.Decode in
    3.11 -              list (variant
    3.12 -               [fn ([], a) => Exn.Res (pair string (option string) a),
    3.13 -                fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))])
    3.14 +              pair
    3.15 +                (list (variant
    3.16 +                 [fn ([], a) => Exn.Res (pair string (option string) a),
    3.17 +                  fn ([], a) => Exn.Exn (ERROR (YXML.string_of_body a))]))
    3.18 +                int
    3.19              end;
    3.20          val toks =
    3.21            (YXML.parse_body toks_yxml |> let open XML.Decode in list (pair int int) end) ~~ sources;
    3.22        in
    3.23 -        Document.change_state (Document.define_command (Document_ID.parse id) name blobs toks)
    3.24 +        Document.change_state
    3.25 +          (Document.define_command (Document_ID.parse id) name blobs blobs_index toks)
    3.26        end);
    3.27  
    3.28  val _ =
     4.1 --- a/src/Pure/PIDE/protocol.scala	Thu Mar 12 20:34:08 2015 +0100
     4.2 +++ b/src/Pure/PIDE/protocol.scala	Thu Mar 12 22:00:51 2015 +0100
     4.3 @@ -392,7 +392,7 @@
     4.4                (Nil, pair(string, option(string))((a.node, b.map(p => p._1.toString)))) },
     4.5            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
     4.6  
     4.7 -      YXML.string_of_body(list(encode_blob)(command.blobs))
     4.8 +      YXML.string_of_body(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     4.9      }
    4.10  
    4.11      val toks = command.span.content