added @{binding} ML antiquotations;
authorwenzelm
Tue, 03 Mar 2009 21:49:05 +0100
changeset 30231 b3f3ad327d4d
parent 30230 a2094a8c1672
child 30232 8f551a13ee99
added @{binding} ML antiquotations;
src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Tue Mar 03 21:48:40 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Tue Mar 03 21:49:05 2009 +0100
@@ -59,12 +59,13 @@
 
 
 
-(** concrete antiquotations **)
+(** misc antiquotations **)
 
 structure P = OuterParse;
 
-
-(* misc *)
+val _ = inline "binding" (Scan.lift (P.position Args.name) >> (fn b =>
+  ML_Syntax.atomic ("Binding.make " ^
+    ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_position b)));
 
 val _ = value "theory"
   (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)