added ML antiquotation @{source} for Symbol_Pos.source;
authorwenzelm
Wed, 27 Aug 2014 12:32:07 +0200
changeset 58046 2873ca3f4b33
parent 58045 ab2483fad861
child 58047 9f3826352b52
added ML antiquotation @{source} for Symbol_Pos.source;
src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Mon Aug 25 12:58:20 2014 +0200
+++ b/src/Pure/ML/ml_antiquotations.ML	Wed Aug 27 12:32:07 2014 +0200
@@ -52,6 +52,16 @@
           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