added XCONST syntax (keeps original spelling of const);
authorwenzelm
Tue Oct 23 13:29:17 2007 +0200 (2007-10-23)
changeset 251591822da5446bc
parent 25158 271e499f2d03
child 25160 72fcf0832cfe
added XCONST syntax (keeps original spelling of const);
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Oct 23 13:29:16 2007 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Oct 23 13:29:17 2007 +0200
     1.3 @@ -980,19 +980,29 @@
     1.4  
     1.5  (* authentic constants *)
     1.6  
     1.7 -fun context_const_ast_tr ctxt [Syntax.Variable c] =
     1.8 +local
     1.9 +
    1.10 +fun const_ast_tr intern ctxt [Syntax.Variable c] =
    1.11        let
    1.12          val consts = consts_of ctxt;
    1.13          val c' = Consts.intern consts c;
    1.14          val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
    1.15 -      in Syntax.Constant (const_syntax_name ctxt c') end
    1.16 -  | context_const_ast_tr _ asts = raise Syntax.AST ("const_ast_tr", asts);
    1.17 +        val d = if intern then const_syntax_name ctxt c' else c;
    1.18 +      in Syntax.Constant d end
    1.19 +  | const_ast_tr _ _ asts = raise Syntax.AST ("const_ast_tr", asts);
    1.20 +
    1.21 +in
    1.22  
    1.23  val _ = Context.add_setup
    1.24   (Sign.add_syntax
    1.25     [("_context_const", "id => 'a", Delimfix "CONST _"),
    1.26 -    ("_context_const", "longid => 'a", Delimfix "CONST _")] #>
    1.27 -  Sign.add_advanced_trfuns ([("_context_const", context_const_ast_tr)], [], [], []));
    1.28 +    ("_context_const", "longid => 'a", Delimfix "CONST _"),
    1.29 +    ("_context_xconst", "id => 'a", Delimfix "XCONST _"),
    1.30 +    ("_context_xconst", "longid => 'a", Delimfix "XCONST _")] #>
    1.31 +  Sign.add_advanced_trfuns
    1.32 +    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], []));
    1.33 +
    1.34 +end;
    1.35  
    1.36  
    1.37  (* notation *)