src/Doc/antiquote_setup.ML
changeset 59064 a8bcb5a446c8
parent 58978 e42da880c61e
child 59066 45ab32a542fe
     1.1 --- a/src/Doc/antiquote_setup.ML	Sat Nov 29 14:43:10 2014 +0100
     1.2 +++ b/src/Doc/antiquote_setup.ML	Sun Nov 30 12:24:56 2014 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4    | _ => error ("Single ML name expected in input: " ^ quote txt));
     1.5  
     1.6  fun prep_ml source =
     1.7 -  (#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source);
     1.8 +  (#1 (Input.source_content source), ML_Lex.read_source false source);
     1.9  
    1.10  fun index_ml name kind ml = Thy_Output.antiquotation name
    1.11    (Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position)))
    1.12 @@ -90,7 +90,7 @@
    1.13          else txt1 ^ " : " ^ txt2;
    1.14        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.15  
    1.16 -      val (pos, _) = #range source1;
    1.17 +      val pos = Input.pos_of source1;
    1.18        val _ =
    1.19          ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2))
    1.20            handle ERROR msg => error (msg ^ Position.here pos);