src/Pure/PIDE/document.ML
changeset 59687 3baf9b3a24c7
parent 59685 c043306d2598
child 59689 7968c57ea240
     1.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 12 22:07:26 2015 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Mar 13 11:47:42 2015 +0100
     1.3 @@ -375,14 +375,14 @@
     1.4              (fn () =>
     1.5                let
     1.6                  val (tokens, _) = fold_map Token.make toks (Position.id id);
     1.7 +                val pos =
     1.8 +                  Token.pos_of (nth tokens blobs_index)
     1.9 +                    handle General.Subscript => Position.none;
    1.10                  val _ =
    1.11 -                  (case try (Token.pos_of o nth tokens) blobs_index of
    1.12 -                    SOME pos =>
    1.13 -                      if Position.is_reported pos then
    1.14 -                        Position.reports
    1.15 -                          ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
    1.16 -                      else ()
    1.17 -                  | NONE => ());
    1.18 +                  if Position.is_reported pos then
    1.19 +                    Position.reports
    1.20 +                      ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
    1.21 +                  else ();
    1.22                in tokens end) ());
    1.23        val commands' =
    1.24          Inttab.update_new (command_id, (name, command_blobs, span)) commands