moved CONST syntax/translations to their proper place;
authorwenzelm
Fri Apr 08 20:39:09 2011 +0200 (2011-04-08)
changeset 422958fdbb3b10beb
parent 42294 0f4372a2d2e4
child 42296 dcc08f2a8671
moved CONST syntax/translations to their proper place;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 08 18:08:13 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 08 20:39:09 2011 +0200
     1.3 @@ -942,37 +942,6 @@
     1.4  end;
     1.5  
     1.6  
     1.7 -(* authentic syntax *)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun const_ast_tr intern ctxt [Ast.Variable c] =
    1.12 -      let
    1.13 -        val Const (c', _) = read_const_proper ctxt false c;
    1.14 -        val d = if intern then Lexicon.mark_const c' else c;
    1.15 -      in Ast.Constant d end
    1.16 -  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
    1.17 -
    1.18 -val typ = Simple_Syntax.read_typ;
    1.19 -
    1.20 -in
    1.21 -
    1.22 -val _ = Context.>> (Context.map_theory
    1.23 - (Sign.add_syntax_i
    1.24 -   [("_context_const", typ "id => logic", Delimfix "CONST _"),
    1.25 -    ("_context_const", typ "id => aprop", Delimfix "CONST _"),
    1.26 -    ("_context_const", typ "longid => logic", Delimfix "CONST _"),
    1.27 -    ("_context_const", typ "longid => aprop", Delimfix "CONST _"),
    1.28 -    ("_context_xconst", typ "id => logic", Delimfix "XCONST _"),
    1.29 -    ("_context_xconst", typ "id => aprop", Delimfix "XCONST _"),
    1.30 -    ("_context_xconst", typ "longid => logic", Delimfix "XCONST _"),
    1.31 -    ("_context_xconst", typ "longid => aprop", Delimfix "XCONST _")] #>
    1.32 -  Sign.add_advanced_trfuns
    1.33 -    ([("_context_const", const_ast_tr true), ("_context_xconst", const_ast_tr false)], [], [], [])));
    1.34 -
    1.35 -end;
    1.36 -
    1.37 -
    1.38  (* notation *)
    1.39  
    1.40  local
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 18:08:13 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 20:39:09 2011 +0200
     2.3 @@ -660,10 +660,23 @@
     2.4    | type_constraint_tr' _ _ _ = raise Match;
     2.5  
     2.6  
     2.7 +(* authentic syntax *)
     2.8 +
     2.9 +fun const_ast_tr intern ctxt [Ast.Variable c] =
    2.10 +      let
    2.11 +        val Const (c', _) = ProofContext.read_const_proper ctxt false c;
    2.12 +        val d = if intern then Lexicon.mark_const c' else c;
    2.13 +      in Ast.Constant d end
    2.14 +  | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
    2.15 +
    2.16 +
    2.17  (* setup translations *)
    2.18  
    2.19  val _ = Context.>> (Context.map_theory
    2.20 -  (Sign.add_advanced_trfunsT
    2.21 + (Sign.add_advanced_trfuns
    2.22 +  ([("_context_const", const_ast_tr true),
    2.23 +    ("_context_xconst", const_ast_tr false)], [], [], []) #>
    2.24 +  Sign.add_advanced_trfunsT
    2.25     [("_type_prop", type_prop_tr'),
    2.26      ("\\<^const>TYPE", type_tr'),
    2.27      ("_type_constraint_", type_constraint_tr')]));
     3.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 18:08:13 2011 +0200
     3.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 20:39:09 2011 +0200
     3.3 @@ -133,10 +133,18 @@
     3.4      ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     3.5      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     3.6      ("_update_name", typ "idt",                        NoSyn),
     3.7 -    ("_constrainAbs", typ "'a",                       NoSyn),
     3.8 +    ("_constrainAbs", typ "'a",                        NoSyn),
     3.9      ("_constrain_position", typ "id => id_position",   Delimfix "_"),
    3.10      ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
    3.11      ("_type_constraint_", typ "'a",                    NoSyn),
    3.12 +    ("_context_const", typ "id => logic",              Delimfix "CONST _"),
    3.13 +    ("_context_const", typ "id => aprop",              Delimfix "CONST _"),
    3.14 +    ("_context_const", typ "longid => logic",          Delimfix "CONST _"),
    3.15 +    ("_context_const", typ "longid => aprop",          Delimfix "CONST _"),
    3.16 +    ("_context_xconst", typ "id => logic",             Delimfix "XCONST _"),
    3.17 +    ("_context_xconst", typ "id => aprop",             Delimfix "XCONST _"),
    3.18 +    ("_context_xconst", typ "longid => logic",         Delimfix "XCONST _"),
    3.19 +    ("_context_xconst", typ "longid => aprop",         Delimfix "XCONST _"),
    3.20      (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
    3.21      (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
    3.22      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),