mixfix: added Structure;
authorwenzelm
Fri Jan 13 01:13:17 2006 +0100 (2006-01-13)
changeset 18673fad60fe1565c
parent 18672 ac1a048ca7dd
child 18674 98d380757893
mixfix: added Structure;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Jan 13 01:13:16 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Jan 13 01:13:17 2006 +0100
     1.3 @@ -17,7 +17,8 @@
     1.4      Infix of int |    (*obsolete*)
     1.5      Infixl of int |   (*obsolete*)
     1.6      Infixr of int |   (*obsolete*)
     1.7 -    Binder of string * int * int
     1.8 +    Binder of string * int * int |
     1.9 +    Structure
    1.10  end;
    1.11  
    1.12  signature MIXFIX1 =
    1.13 @@ -62,7 +63,8 @@
    1.14    Infix of int |      (*obsolete*)
    1.15    Infixl of int |     (*obsolete*)
    1.16    Infixr of int |     (*obsolete*)
    1.17 -  Binder of string * int * int;
    1.18 +  Binder of string * int * int |
    1.19 +  Structure;
    1.20  
    1.21  val literal = Delimfix o SynExt.escape_mfix;
    1.22  
    1.23 @@ -86,7 +88,8 @@
    1.24    | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
    1.25    | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
    1.26    | string_of_mixfix (Binder (sy, p1, p2)) =
    1.27 -      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2]);
    1.28 +      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2])
    1.29 +  | string_of_mixfix Structure = "(structure)";
    1.30  
    1.31  
    1.32  (* syntax specifications *)
    1.33 @@ -128,6 +131,7 @@
    1.34    | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
    1.35    | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
    1.36    | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
    1.37 +  | map_mixfix _ Structure = Structure
    1.38    | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
    1.39  
    1.40  val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
    1.41 @@ -141,7 +145,8 @@
    1.42    | mixfix_args (Infix _) = 2
    1.43    | mixfix_args (Infixl _) = 2
    1.44    | mixfix_args (Infixr _) = 2
    1.45 -  | mixfix_args (Binder _) = 1;
    1.46 +  | mixfix_args (Binder _) = 1
    1.47 +  | mixfix_args Structure = 0;
    1.48  
    1.49  
    1.50  (* syn_ext_types *)
    1.51 @@ -201,7 +206,8 @@
    1.52          | (sy, ty, Infixl p) => mk_infix sy ty c p (p + 1) p
    1.53          | (sy, ty, Infixr p) => mk_infix sy ty c (p + 1) p p
    1.54          | (_, ty, Binder (sy, p, q)) =>
    1.55 -            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)])
    1.56 +            [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, sy, [0, p], q)]
    1.57 +        | _ => error ("Bad mixfix declaration for const: " ^ quote c))
    1.58      end;
    1.59  
    1.60      fun binder (c, _, Binder (sy, _, _)) = SOME (sy, c)