--- a/src/Pure/ML/ml_antiquotations.ML Fri Nov 06 23:31:50 2015 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Sat Nov 07 00:28:42 2015 +0100
@@ -10,7 +10,13 @@
(* ML support *)
val _ = Theory.setup
- (ML_Antiquotation.inline @{binding assert}
+ (ML_Antiquotation.value @{binding cartouche}
+ (Args.context -- Scan.lift (Parse.position Args.cartouche_input) >> (fn (ctxt, (source, pos)) =>
+ (Context_Position.report ctxt pos Markup.ML_cartouche;
+ "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
+ ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source))))) #>
+
+ ML_Antiquotation.inline @{binding assert}
(Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
ML_Antiquotation.inline @{binding make_string}