# HG changeset patch
# User wenzelm
# Date 1265922217 -3600
# Node ID 18cd034922baae15cc4d536e06d36d0812b82709
# Parent  dc4f61a7918abf17cd40cdcd6f8a032b58e2dc26
added ML antiquotation @{syntax_const};

diff -r dc4f61a7918a -r 18cd034922ba NEWS
--- a/NEWS	Thu Feb 11 22:03:15 2010 +0100
+++ b/NEWS	Thu Feb 11 22:03:37 2010 +0100
@@ -132,6 +132,9 @@
 
 *** ML ***
 
+* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
+syntax constant (cf. 'syntax' command).
+
 * Renamed old-style Drule.standard to Drule.export_without_context, to
 emphasize that this is in no way a standard operation.
 INCOMPATIBILITY.
diff -r dc4f61a7918a -r 18cd034922ba src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Feb 11 22:03:15 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Feb 11 22:03:37 2010 +0100
@@ -26,6 +26,7 @@
   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
+  val syn_of: Proof.context -> Syntax.syntax
   val consts_of: Proof.context -> Consts.T
   val const_syntax_name: Proof.context -> string -> string
   val the_const_constraint: Proof.context -> string -> typ
diff -r dc4f61a7918a -r 18cd034922ba src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 22:03:15 2010 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 22:03:37 2010 +0100
@@ -127,5 +127,10 @@
       let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
       in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
 
+val _ = inline "syntax_const"
+  (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
+    if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
+    else error ("Unknown syntax const: " ^ quote c)));
+
 end;
 
diff -r dc4f61a7918a -r 18cd034922ba src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:15 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:37 2010 +0100
@@ -54,6 +54,7 @@
     PrintRule of 'a * 'a |
     ParsePrintRule of 'a * 'a
   val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
+  val is_const: syntax -> string -> bool
   val standard_unparse_term: (string -> xstring) ->
     Proof.context -> syntax -> bool -> term -> Pretty.T
   val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
@@ -592,6 +593,8 @@
   | print_rule (ParsePrintRule pats) = SOME (swap pats);
 
 
+fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
+
 local
 
 fun check_rule (rule as (lhs, rhs)) =
@@ -603,11 +606,9 @@
 
 fun read_pattern ctxt is_logtype syn (root, str) =
   let
-    val Syntax ({consts, ...}, _) = syn;
-
     fun constify (ast as Ast.Constant _) = ast
       | constify (ast as Ast.Variable x) =
-          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
+          if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);