added CONST syntax;
authorwenzelm
Wed May 17 22:34:52 2006 +0200 (2006-05-17)
changeset 19681871167b2c70e
parent 19680 6a34b1b1f540
child 19682 c8c301eb965a
added CONST syntax;
tuned interfaces;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed May 17 22:34:50 2006 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed May 17 22:34:52 2006 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4    val get_case: context -> string -> string option list -> RuleCases.T
     1.5    val expand_abbrevs: bool -> context -> context
     1.6    val add_const_syntax: string * bool -> (string * mixfix) list -> context -> context
     1.7 -  val add_abbrevs: string * bool -> (bstring * term * mixfix) list -> context -> context
     1.8 +  val add_abbrevs: string * bool -> ((bstring * mixfix) * term) list -> context -> context
     1.9    val verbose: bool ref
    1.10    val setmp_verbose: ('a -> 'b) -> 'a -> 'b
    1.11    val print_syntax: context -> unit
    1.12 @@ -1109,19 +1109,33 @@
    1.13  end;
    1.14  
    1.15  
    1.16 -(* const syntax *)
    1.17 +(* authentic constants *)
    1.18  
    1.19  fun add_const_syntax prmode args ctxt =
    1.20    ctxt |> map_syntax
    1.21      (LocalSyntax.add_modesyntax (theory_of ctxt) prmode
    1.22        (map (pair false o Consts.syntax (consts_of ctxt)) args));
    1.23  
    1.24 +fun context_const_ast_tr context [Syntax.Variable c] =
    1.25 +      let
    1.26 +        val consts = Context.cases Sign.consts_of consts_of context;
    1.27 +        val c' = Consts.intern consts c;
    1.28 +        val _ = Consts.constraint consts c' handle TYPE (msg, _, _) => error msg;
    1.29 +      in Syntax.Constant (Syntax.constN ^ c') end
    1.30 +  | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);
    1.31 +
    1.32 +val _ = Context.add_setup
    1.33 + (Sign.add_syntax
    1.34 +   [("_context_const", "id => 'a", Delimfix "CONST _"),
    1.35 +    ("_context_const", "longid => 'a", Delimfix "CONST _")] #>
    1.36 +  Sign.add_advanced_trfuns ([("_context_const", context_const_ast_tr)], [], [], []));
    1.37 +
    1.38  
    1.39  (* abbreviations *)
    1.40  
    1.41  val expand_abbrevs = map_consts o apsnd o Consts.expand_abbrevs;
    1.42  
    1.43 -fun add_abbrevs prmode = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt =>
    1.44 +fun add_abbrevs prmode = fold (fn ((raw_c, raw_mx), raw_t) => fn ctxt =>
    1.45    let
    1.46      val ([(c, _, mx)], _) = cert_vars [(raw_c, NONE, raw_mx)] ctxt;
    1.47      val c' = Syntax.constN ^ full_name ctxt c;
    1.48 @@ -1134,7 +1148,7 @@
    1.49      ctxt
    1.50      |> declare_term t
    1.51      |> map_consts (apsnd
    1.52 -      (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), false)))
    1.53 +      (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) (#1 prmode) ((c, t), true)))
    1.54      |> map_syntax (LocalSyntax.add_modesyntax (theory_of ctxt) prmode [(false, (c', T, mx))])
    1.55    end);
    1.56