added ML antiquotation @{syntax_const};
authorwenzelm
Thu Feb 11 22:03:37 2010 +0100 (2010-02-11)
changeset 3511118cd034922ba
parent 35110 dc4f61a7918a
child 35112 ff6f60e6ab85
added ML antiquotation @{syntax_const};
NEWS
src/Pure/Isar/proof_context.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/NEWS	Thu Feb 11 22:03:15 2010 +0100
     1.2 +++ b/NEWS	Thu Feb 11 22:03:37 2010 +0100
     1.3 @@ -132,6 +132,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Antiquotation @{syntax_const NAME} ensures that NAME refers to a raw
     1.8 +syntax constant (cf. 'syntax' command).
     1.9 +
    1.10  * Renamed old-style Drule.standard to Drule.export_without_context, to
    1.11  emphasize that this is in no way a standard operation.
    1.12  INCOMPATIBILITY.
     2.1 --- a/src/Pure/Isar/proof_context.ML	Thu Feb 11 22:03:15 2010 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Feb 11 22:03:37 2010 +0100
     2.3 @@ -26,6 +26,7 @@
     2.4    val naming_of: Proof.context -> Name_Space.naming
     2.5    val restore_naming: Proof.context -> Proof.context -> Proof.context
     2.6    val full_name: Proof.context -> binding -> string
     2.7 +  val syn_of: Proof.context -> Syntax.syntax
     2.8    val consts_of: Proof.context -> Consts.T
     2.9    val const_syntax_name: Proof.context -> string -> string
    2.10    val the_const_constraint: Proof.context -> string -> typ
     3.1 --- a/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 22:03:15 2010 +0100
     3.2 +++ b/src/Pure/ML/ml_antiquote.ML	Thu Feb 11 22:03:37 2010 +0100
     3.3 @@ -127,5 +127,10 @@
     3.4        let val (c, _) = Term.dest_Const (ProofContext.read_const_proper ctxt c)
     3.5        in ML_Syntax.atomic (ML_Syntax.print_term (ProofContext.mk_const ctxt (c, Ts))) end));
     3.6  
     3.7 +val _ = inline "syntax_const"
     3.8 +  (Args.context -- Scan.lift Args.name >> (fn (ctxt, c) =>
     3.9 +    if Syntax.is_const (ProofContext.syn_of ctxt) c then ML_Syntax.print_string c
    3.10 +    else error ("Unknown syntax const: " ^ quote c)));
    3.11 +
    3.12  end;
    3.13  
     4.1 --- a/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:15 2010 +0100
     4.2 +++ b/src/Pure/Syntax/syntax.ML	Thu Feb 11 22:03:37 2010 +0100
     4.3 @@ -54,6 +54,7 @@
     4.4      PrintRule of 'a * 'a |
     4.5      ParsePrintRule of 'a * 'a
     4.6    val map_trrule: ('a -> 'b) -> 'a trrule -> 'b trrule
     4.7 +  val is_const: syntax -> string -> bool
     4.8    val standard_unparse_term: (string -> xstring) ->
     4.9      Proof.context -> syntax -> bool -> term -> Pretty.T
    4.10    val standard_unparse_typ: Proof.context -> syntax -> typ -> Pretty.T
    4.11 @@ -592,6 +593,8 @@
    4.12    | print_rule (ParsePrintRule pats) = SOME (swap pats);
    4.13  
    4.14  
    4.15 +fun is_const (Syntax ({consts, ...}, _)) c = member (op =) consts c;
    4.16 +
    4.17  local
    4.18  
    4.19  fun check_rule (rule as (lhs, rhs)) =
    4.20 @@ -603,11 +606,9 @@
    4.21  
    4.22  fun read_pattern ctxt is_logtype syn (root, str) =
    4.23    let
    4.24 -    val Syntax ({consts, ...}, _) = syn;
    4.25 -
    4.26      fun constify (ast as Ast.Constant _) = ast
    4.27        | constify (ast as Ast.Variable x) =
    4.28 -          if member (op =) consts x orelse Long_Name.is_qualified x then Ast.Constant x
    4.29 +          if is_const syn x orelse Long_Name.is_qualified x then Ast.Constant x
    4.30            else ast
    4.31        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
    4.32