--- a/src/Pure/Isar/parse.ML Wed Oct 20 18:13:17 2021 +0200
+++ b/src/Pure/Isar/parse.ML Wed Oct 20 20:04:28 2021 +0200
@@ -118,6 +118,8 @@
val thm: (Facts.ref * Token.src list) parser
val thms1: (Facts.ref * Token.src list) list parser
val options: ((string * Position.T) * (string * Position.T)) list parser
+ val embedded_ml: ML_Lex.token Antiquote.antiquote list parser
+ val embedded_ml_underscore: ML_Lex.token Antiquote.antiquote list parser
end;
structure Parse: PARSE =
@@ -494,4 +496,14 @@
val options = $$$ "[" |-- list1 option --| $$$ "]";
+
+(* embedded ML *)
+
+val embedded_ml =
+ embedded_input >> ML_Lex.read_source ||
+ control >> (ML_Lex.read_symbols o Antiquote.control_symbols);
+
+val embedded_ml_underscore =
+ input underscore >> ML_Lex.read_source || embedded_ml;
+
end;