src/Pure/ML/ml_lex.ML

   val read_range: Position.range -> Symbol_Pos.text -> token Antiquote.antiquote list
   val read_source': {language: bool -> Markup.T, opaque_warning: bool, symbols: bool} ->
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
   val read_source_sml: Input.source -> token Antiquote.antiquote list
+  val read_symbols: Symbol_Pos.T list -> token Antiquote.antiquote list
   val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
 end;
 
 structure ML_Lex: ML_LEX =
 struct

 
 val scan_sml_antiq = scan_sml >> Antiquote.Text;
 
 val scan_ml_antiq =
   Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
-  Antiquote.scan_control >> Antiquote.Control ||
+  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
   scan_rat_antiq >> Antiquote.Antiq ||
   scan_sml_antiq;
 
 fun recover msg =

 
 val read_source_sml =
   read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
     scan_sml_antiq;
 
+val read_symbols = reader {opaque_warning = true} scan_ml_antiq;
 val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
 
 end;
 
 end;