# HG changeset patch
# User wenzelm
# Date 1404230396 -7200
# Node ID c3b5cb53ea794caaec6b316c6e31b1935bb54a51
# Parent  dc542b78ef0f25333e406ab1db65d907f46f968a
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;

diff -r dc542b78ef0f -r c3b5cb53ea79 src/Doc/antiquote_setup.ML
--- 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) ^ "}" ^