redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
authorwenzelm
Tue Jul 01 17:59:56 2014 +0200 (2014-07-01)
changeset 57477c3b5cb53ea79
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
     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) ^ "}" ^