src/Doc/antiquote_setup.ML
changeset 58978 e42da880c61e
parent 58931 3097ec653547
child 59064 a8bcb5a446c8
     1.1 --- a/src/Doc/antiquote_setup.ML	Tue Nov 11 15:55:31 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Tue Nov 11 18:16:25 2014 +0100
     1.3 @@ -90,7 +90,7 @@
     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 (pos, _) = #range source1;
     1.9        val _ =
    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);