redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
1.1 --- a/src/Doc/antiquote_setup.ML Tue Jul 01 17:16:11 2014 +0200
1.2 +++ b/src/Doc/antiquote_setup.ML Tue Jul 01 17:59:56 2014 +0200
1.3 @@ -99,8 +99,10 @@
1.4 else txt1 ^ " : " ^ txt2;
1.5 val txt' = if kind = "" then txt else kind ^ " " ^ txt;
1.6
1.7 + val pos = #pos source1;
1.8 val _ =
1.9 - ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2));
1.10 + ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
1.11 + handle ERROR msg => error (msg ^ Position.here pos);
1.12 val kind' = if kind = "" then "ML" else "ML " ^ kind;
1.13 in
1.14 "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^