# HG changeset patch
# User wenzelm
# Date 1426243662 -3600
# Node ID 3baf9b3a24c761b2617173eae8cec8957c8785ca
# Parent  68996aa778299ac48c1ebbdc5204e4356d013126
tuned;

diff -r 68996aa77829 -r 3baf9b3a24c7 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Mar 12 22:07:26 2015 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Mar 13 11:47:42 2015 +0100
@@ -375,14 +375,14 @@
             (fn () =>
               let
                 val (tokens, _) = fold_map Token.make toks (Position.id id);
+                val pos =
+                  Token.pos_of (nth tokens blobs_index)
+                    handle General.Subscript => Position.none;
                 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 => ());
+                  if Position.is_reported pos then
+                    Position.reports
+                      ((pos, Markup.language_path) :: maps (blob_reports pos) command_blobs)
+                  else ();
               in tokens end) ());
       val commands' =
         Inttab.update_new (command_id, (name, command_blobs, span)) commands