less bulky "_position", for improved readability of parse trees;
authorwenzelm
Tue Apr 19 22:32:49 2011 +0200 (2011-04-19 ago)
changeset 4241016bc5564535f
parent 42409 3e1e80df6a42
child 42411 ff997038e8eb
less bulky "_position", for improved readability of parse trees;
src/Pure/Syntax/syntax_phases.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 22:08:42 2011 +0200
     1.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Apr 19 22:32:49 2011 +0200
     1.3 @@ -146,7 +146,7 @@
     1.4              val c = get_type (Lexicon.str_of_token tok);
     1.5              val _ = report (Lexicon.pos_of_token tok) (markup_type ctxt) c;
     1.6            in [Ast.Constant (Lexicon.mark_type c)] end
     1.7 -      | asts_of (Parser.Node ("_constrain_position", [pt as Parser.Tip tok])) =
     1.8 +      | asts_of (Parser.Node ("_position", [pt as Parser.Tip tok])) =
     1.9            if constrain_pos then
    1.10              [Ast.Appl [Ast.Constant "_constrain", ast_of pt,
    1.11                Ast.Variable (Term_Position.encode (Lexicon.pos_of_token tok))]]
     2.1 --- a/src/Pure/pure_thy.ML	Tue Apr 19 22:08:42 2011 +0200
     2.2 +++ b/src/Pure/pure_thy.ML	Tue Apr 19 22:32:49 2011 +0200
     2.3 @@ -134,8 +134,8 @@
     2.4      ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
     2.5      ("_update_name", typ "idt",                        NoSyn),
     2.6      ("_constrainAbs", typ "'a",                        NoSyn),
     2.7 -    ("_constrain_position", typ "id => id_position",   Delimfix "_"),
     2.8 -    ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
     2.9 +    ("_position",   typ "id => id_position",           Delimfix "_"),
    2.10 +    ("_position",   typ "longid => longid_position",   Delimfix "_"),
    2.11      ("_type_constraint_", typ "'a",                    NoSyn),
    2.12      ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
    2.13      ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),