equal
deleted
inserted
replaced
77 checksum, so that garbage can be detected. |
77 checksum, so that garbage can be detected. |
78 \<close> |
78 \<close> |
79 |
79 |
80 (*<*) |
80 (*<*) |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
81 text\<open>Concrete syntax: messages appear as \<open>\<lbrace>A,B,NA\<rbrace>\<close>, etc...\<close> |
82 nonterminal mtuple_args |
|
83 syntax |
82 syntax |
84 "" :: "'a \<Rightarrow> mtuple_args" ("_") |
83 "_MTuple" :: "['a, args] \<Rightarrow> 'a * 'b" ("(\<open>indent=2 notation=\<open>mixfix message tuple\<close>\<close>\<lbrace>_,/ _\<rbrace>)") |
85 "_MTuple_args" :: "'a \<Rightarrow> mtuple_args \<Rightarrow> mtuple_args" ("_,/ _") |
|
86 "_MTuple" :: "['a, mtuple_args] \<Rightarrow> 'a * 'b" ("(2\<lbrace>_,/ _\<rbrace>)") |
|
87 syntax_consts |
84 syntax_consts |
88 "_MTuple_args" "_MTuple" \<rightleftharpoons> MPair |
85 MPair |
89 translations |
86 translations |
90 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
87 "\<lbrace>x, y, z\<rbrace>" \<rightleftharpoons> "\<lbrace>x, \<lbrace>y, z\<rbrace>\<rbrace>" |
91 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
88 "\<lbrace>x, y\<rbrace>" \<rightleftharpoons> "CONST MPair x y" |
92 |
89 |
93 |
90 |