# HG changeset patch
# User wenzelm
# Date 1409135527 -7200
# Node ID 2873ca3f4b337e60e2c695fbe18477b59a920fef
# Parent  ab2483fad861f43126cbf0523759d9a82d1c7aa1
added ML antiquotation @{source} for Symbol_Pos.source;

diff -r ab2483fad861 -r 2873ca3f4b33 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