src/Pure/PIDE/document.ML
changeset 59685 c043306d2598
parent 59347 2183c731f0a7
child 59687 3baf9b3a24c7
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 12 20:34:08 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 12 22:00:51 2015 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4    val init_state: state
     1.5    val define_blob: string -> string -> state -> state
     1.6    type blob_digest = (string * string option) Exn.result
     1.7 -  val define_command: Document_ID.command -> string -> blob_digest list ->
     1.8 +  val define_command: Document_ID.command -> string -> blob_digest list -> int ->
     1.9      ((int * int) * string) list -> state -> state
    1.10    val remove_versions: Document_ID.version list -> state -> state
    1.11    val start_execution: state -> state
    1.12 @@ -359,23 +359,37 @@
    1.13    blob_digest |> Exn.map_result (fn (file_node, raw_digest) =>
    1.14      (file_node, Option.map (the_blob state) raw_digest));
    1.15  
    1.16 +fun blob_reports pos (blob_digest: blob_digest) =
    1.17 +  (case blob_digest of Exn.Res (file_node, _) => [(pos, Markup.path file_node)] | _ => []);
    1.18 +
    1.19  
    1.20  (* commands *)
    1.21  
    1.22 -fun define_command command_id name command_blobs toks =
    1.23 +fun define_command command_id name command_blobs blobs_index toks =
    1.24    map_state (fn (versions, blobs, commands, execution) =>
    1.25      let
    1.26        val id = Document_ID.print command_id;
    1.27        val span =
    1.28          Lazy.lazy (fn () =>
    1.29            Position.setmp_thread_data (Position.id_only id)
    1.30 -            (fn () => #1 (fold_map Token.make toks (Position.id id))) ());
    1.31 +            (fn () =>
    1.32 +              let
    1.33 +                val (tokens, _) = fold_map Token.make toks (Position.id id);
    1.34 +                val _ =
    1.35 +                  (case try (Token.pos_of o nth tokens) blobs_index of
    1.36 +                    SOME pos =>
    1.37 +                      if Position.is_reported pos then
    1.38 +                        Position.reports
    1.39 +                          ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
    1.40 +                      else ()
    1.41 +                  | NONE => ());
    1.42 +              in tokens end) ());
    1.43 +      val commands' =
    1.44 +        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    1.45 +          handle Inttab.DUP dup => err_dup "command" dup;
    1.46        val _ =
    1.47          Position.setmp_thread_data (Position.id_only id)
    1.48            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    1.49 -      val commands' =
    1.50 -        Inttab.update_new (command_id, (name, command_blobs, span)) commands
    1.51 -          handle Inttab.DUP dup => err_dup "command" dup;
    1.52      in (versions, blobs, commands', execution) end);
    1.53  
    1.54  fun the_command (State {commands, ...}) command_id =