Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
authorwenzelm
Tue, 01 Jul 2014 17:59:56 +0200
changeset 57477 c3b5cb53ea79
parent 57476 dc542b78ef0f
child 57478 fa14d60a8cca
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
src/Doc/antiquote_setup.ML file | annotate | diff | comparison | revisions 
--- a/src/Doc/antiquote_setup.ML	Tue Jul 01 17:16:11 2014 +0200
+++ b/src/Doc/antiquote_setup.ML	Tue Jul 01 17:59:56 2014 +0200
@@ -99,8 +99,10 @@
         else txt1 ^ " : " ^ txt2;
       val txt' = if kind = "" then txt else kind ^ " " ^ txt;
 
+      val pos = #pos source1;
       val _ =
-        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2));
+        ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
+          handle ERROR msg => error (msg ^ Position.here pos);
       val kind' = if kind = "" then "ML" else "ML " ^ kind;
     in
       "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^
isabelle