Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
mixfix_args: 1 for binders;
authorwenzelm
Fri, 02 Dec 2005 22:54:51 +0100
changeset 18341 d99396e96632
parent 18340 3fdff270aa04
child 18342 1b7109c10b7b
mixfix_args: 1 for binders; string_of_mixfix: proper output of binders;
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:50 2005 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Dec 02 22:54:51 2005 +0100
@@ -85,7 +85,7 @@
   | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
   | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
   | string_of_mixfix (Binder (sy, p1, p2)) =
-      parens (spaces ["binder", brackets (string_of_int p1), string_of_int p2]);
+      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2]);
 
 
 (* syntax specifications *)
@@ -126,7 +126,10 @@
   | mixfix_args (InfixName (sy, _)) = 2 + SynExt.mfix_args sy
   | mixfix_args (InfixlName (sy, _)) = 2 + SynExt.mfix_args sy
   | mixfix_args (InfixrName (sy, _)) = 2 + SynExt.mfix_args sy
-  | mixfix_args (*old infix or binder*) _ = 2;
+  | mixfix_args (Infix _) = 2
+  | mixfix_args (Infixl _) = 2
+  | mixfix_args (Infixr _) = 2
+  | mixfix_args (Binder _) = 1;
 
 
 (* syn_ext_types *)
isabelle