--- a/src/Pure/ML/ml_lex.ML Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML Tue Sep 28 16:01:13 2021 +0200
@@ -36,6 +36,7 @@
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;
@@ -315,7 +316,7 @@
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;
@@ -389,6 +390,7 @@
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;