src/Doc/antiquote_setup.ML
changeset 55828 42ac3cfb89f6
parent 55743 225a060e7445
child 55831 3a9386b32211
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Mar 01 19:55:01 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sat Mar 01 22:46:31 2014 +0100
     1.3 @@ -86,7 +86,9 @@
     1.4          then txt1 ^ ": " ^ txt2
     1.5          else txt1 ^ " : " ^ txt2;
     1.6        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
     1.7 -      val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
     1.8 +      val _ =  (* ML_Lex.read (!?) *)
     1.9 +        ML_Context.eval_source_in (SOME ctxt) false
    1.10 +          {delimited = false, text = ml (txt1, txt2), pos = Position.none};
    1.11        val kind' = if kind = "" then "ML" else "ML " ^ kind;
    1.12      in
    1.13        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^