src/Pure/PIDE/document.ML
changeset 59702 58dfaa369c11
parent 59689 7968c57ea240
child 59715 4f0d0e4ad68d
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Mar 15 14:46:01 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Mar 15 19:21:15 2015 +0100
     1.3 @@ -365,7 +365,7 @@
     1.4  
     1.5  (* commands *)
     1.6  
     1.7 -fun define_command command_id name command_blobs blobs_index toks =
     1.8 +fun define_command command_id name blobs_digests blobs_index toks =
     1.9    map_state (fn (versions, blobs, commands, execution) =>
    1.10      let
    1.11        val id = Document_ID.print command_id;
    1.12 @@ -375,17 +375,19 @@
    1.13              (fn () =>
    1.14                let
    1.15                  val (tokens, _) = fold_map Token.make toks (Position.id id);
    1.16 -                val pos =
    1.17 -                  Token.pos_of (nth tokens blobs_index)
    1.18 -                    handle General.Subscript => Position.none;
    1.19                  val _ =
    1.20 -                  if Position.is_reported pos then
    1.21 -                    Position.reports
    1.22 -                      ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
    1.23 -                  else ();
    1.24 +                  if blobs_index < 0
    1.25 +                  then (*inlined errors*)
    1.26 +                    map_filter Exn.get_exn blobs_digests
    1.27 +                    |> List.app (Output.error_message o Runtime.exn_message)
    1.28 +                  else (*auxiliary files*)
    1.29 +                    let val pos = Token.pos_of (nth tokens blobs_index) in
    1.30 +                      Position.reports
    1.31 +                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
    1.32 +                    end;
    1.33                in tokens end) ());
    1.34        val commands' =
    1.35 -        Inttab.update_new (command_id, (name, command_blobs, blobs_index, span)) commands
    1.36 +        Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands
    1.37            handle Inttab.DUP dup => err_dup "command" dup;
    1.38        val _ =
    1.39          Position.setmp_thread_data (Position.id_only id)