src/Pure/ML/ml_antiquotations.ML

   ML_Antiquotation.value @{binding cpat}
     (Args.context --
       Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t =>
         "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^
           ML_Syntax.atomic (ML_Syntax.print_term t))));
+
+
+(* embedded source *)
+
+val _ = Theory.setup
+ (ML_Antiquotation.value @{binding source}
+    (Scan.lift Args.text_source_position >> (fn {delimited, text, pos} =>
+      "{delimited = " ^ Bool.toString delimited ^
+      ", text = " ^ ML_Syntax.print_string text ^
+      ", pos = " ^ ML_Syntax.print_position pos ^ "}")));
 
 
 (* ML support *)
 
 val _ = Theory.setup