--- 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