# HG changeset patch # User wenzelm # Date 1005153526 -3600 # Node ID 935e29914f93d0c74d245d717b666d700fe1e236 # Parent db9a3ad6e90e05890d4f51c197419354ba90bed7 syntax for structs; diff -r db9a3ad6e90e -r 935e29914f93 src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Wed Nov 07 18:18:29 2001 +0100 +++ b/src/Pure/Syntax/mixfix.ML Wed Nov 07 18:18:46 2001 +0100 @@ -202,7 +202,7 @@ val pure_nonterms = (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes", SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop", - "asms", SynExt.any, SynExt.sprop]); + "asms", SynExt.any, SynExt.sprop, "struct", "structs"]); val pure_syntax = [("_lambda", "[pttrns, 'a] => logic", Mixfix ("(3%_./ _)", [0, 3], 3)), @@ -232,7 +232,11 @@ ("", "id => logic", Delimfix "_"), ("", "longid => logic", Delimfix "_"), ("", "var => logic", Delimfix "_"), - ("_DDDOT", "logic", Delimfix "...")]; + ("_DDDOT", "logic", Delimfix "..."), + ("_struct_app", "structs => logic => logic", Mixfix ("__", [0, 1000], 999)), + ("", "struct => structs", Delimfix "_"), + ("_structs", "struct => structs => structs", Delimfix "__"), + ("_struct", "struct", Delimfix "\\")]; val pure_appl_syntax = [("_appl", "[('b => 'a), args] => logic", Mixfix ("(1_/(1'(_')))", [SynExt.max_pri, 0], SynExt.max_pri)),