src/Pure/ML/ml_lex.ML

   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
       Source.source) Source.source
   val tokenize: string -> token list
   val read: Position.T -> Symbol_Pos.text -> token Antiquote.antiquote list
+  val read_source: Symbol_Pos.source -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
 struct
 

   Symbol_Pos.source (Position.line 1) src
   |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_ml)) (SOME (false, recover));
 
 val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust;
 
-fun read pos txt =
+fun read pos text =
   let
-    val _ = Position.report pos Markup.language_ML;
-    val syms = Symbol_Pos.explode (txt, pos);
+    val syms = Symbol_Pos.explode (text, pos);
     val termination =
       if null syms then []
       else
         let
           val pos1 = List.last syms |-> Position.advance;

         |> Source.exhaust
         |> tap (Position.reports_text o Antiquote.antiquote_reports (single o report_of_token))
         |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())));
   in input @ termination end;
 
-end;
-
-end;
-
+fun read_source {delimited, text, pos} =
+  (Position.report pos (Markup.language_ML delimited); read pos text);
+
+end;
+
+end;
+