uniform handling of fixes;
mixfix: added Structure;

--- a/src/Pure/Isar/element.ML	Fri Jan 13 01:13:06 2006 +0100
+++ b/src/Pure/Isar/element.ML	Fri Jan 13 01:13:08 2006 +0100
@@ -8,7 +8,7 @@
 signature ELEMENT =
 sig
   datatype ('typ, 'term, 'fact) ctxt =
-    Fixes of (string * 'typ option * mixfix option) list |
+    Fixes of (string * 'typ option * mixfix) list |
     Constrains of (string * 'typ) list |
     Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
     Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
@@ -16,14 +16,13 @@
   type context (*= (string, string, thmref) ctxt*)
   type context_i (*= (typ, term, thm list) ctxt*)
   val map_ctxt: {name: string -> string,
-    var: string * mixfix option -> string * mixfix option,
+    var: string * mixfix -> string * mixfix,
     typ: 'typ -> 'a, term: 'term -> 'b, fact: 'fact -> 'c,
     attrib: Attrib.src -> Attrib.src} -> ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
   val map_ctxt_values: (typ -> typ) -> (term -> term) -> (thm -> thm) -> context_i -> context_i
   val pretty_ctxt: ProofContext.context -> context_i -> Pretty.T list
   val rename: (string * (string * mixfix option)) list -> string -> string
-  val rename_var: (string * (string * mixfix option)) list ->
-   string * mixfix option -> string * mixfix option
+  val rename_var: (string * (string * mixfix option)) list -> string * mixfix -> string * mixfix
   val rename_term: (string * (string * mixfix option)) list -> term -> term
   val rename_thm: (string * (string * mixfix option)) list -> thm -> thm
   val rename_ctxt: (string * (string * mixfix option)) list -> context_i -> context_i
@@ -44,7 +43,7 @@
 (* datatype ctxt *)
 
 datatype ('typ, 'term, 'fact) ctxt =
-  Fixes of (string * 'typ option * mixfix option) list |
+  Fixes of (string * 'typ option * mixfix) list |
   Constrains of (string * 'typ) list |
   Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
   Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
@@ -56,8 +55,7 @@
 fun map_ctxt {name, var, typ, term, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
        let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
-   | Constrains xs => Constrains (xs |> map (fn (x, T) =>
-       (#1 (var (x, SOME Syntax.NoSyn)), typ T)))
+   | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
       ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
         (term t, (map term ps, map term qs))))))
@@ -80,13 +78,13 @@
     val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
     val prt_atts = Args.pretty_attribs ctxt;
 
-    fun prt_syn syn =
-      let val s = (case syn of NONE => "(structure)" | SOME mx => Syntax.string_of_mixfix mx)
+    fun prt_mixfix mx =
+      let val s = Syntax.string_of_mixfix mx
       in if s = "" then [] else [Pretty.brk 2, Pretty.str s] end;
-    fun prt_fix (x, SOME T, syn) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
-          prt_typ T :: Pretty.brk 1 :: prt_syn syn)
-      | prt_fix (x, NONE, syn) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_syn syn);
-    fun prt_constrain (x, T) = prt_fix (x, SOME T, SOME (Syntax.NoSyn));
+    fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (x ^ " ::") :: Pretty.brk 1 ::
+          prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
+      | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str x :: Pretty.brk 1 :: prt_mixfix mx);
+    fun prt_constrain (x, T) = prt_fix (x, SOME T, NoSyn);
 
     fun prt_name name = Pretty.str (ProofContext.extern_thm ctxt name);
     fun prt_name_atts (name, atts) sep =
@@ -156,13 +154,13 @@
   | SOME (x', _) => x');
 
 fun rename_var ren (x, mx) =
-  (case (AList.lookup (op =) ren (x: string), is_some mx) of
+  (case (AList.lookup (op =) ren (x: string), mx) of
     (NONE, _) => (x, mx)
-  | (SOME (x', NONE), true) => (x', SOME Syntax.NoSyn)
-  | (SOME (x', NONE), false) => (x', mx)
-  | (SOME (x', SOME mx'), true) => (x', SOME mx')
-  | (SOME (x', SOME _), false) =>
-      error ("Attempt to change syntax of structure parameter " ^ quote x));
+  | (SOME (x', NONE), Structure) => (x', mx)
+  | (SOME (x', SOME _), Structure) =>
+      error ("Attempt to change syntax of structure parameter " ^ quote x)
+  | (SOME (x', NONE), _) => (x', NoSyn)
+  | (SOME (x', SOME mx'), _) => (x', mx'));
 
 fun rename_term ren (Free (x, T)) = Free (rename ren x, T)
   | rename_term ren (t $ u) = rename_term ren t $ rename_term ren u

--- a/src/Pure/Isar/outer_parse.ML	Fri Jan 13 01:13:06 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Jan 13 01:13:08 2006 +0100
@@ -54,13 +54,14 @@
   val arity: token list -> (string list * string) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
-  val opt_infix: token list -> Syntax.mixfix * token list
-  val opt_mixfix: token list -> Syntax.mixfix * token list
-  val opt_infix': token list -> Syntax.mixfix * token list
-  val opt_mixfix': token list -> Syntax.mixfix * token list
-  val mixfix': token list -> Syntax.mixfix * token list
-  val const: token list -> (bstring * string * Syntax.mixfix) * token list
-  val param: token list -> (bstring * string option * Syntax.mixfix) * token list
+  val mixfix: token list -> mixfix * token list
+  val opt_infix: token list -> mixfix * token list
+  val opt_mixfix: token list -> mixfix * token list
+  val opt_infix': token list -> mixfix * token list
+  val opt_mixfix': token list -> mixfix * token list
+  val const: token list -> (string * string * mixfix) * token list
+  val fixes: token list -> (string * string option * mixfix) list * token list
+  val simple_fixes: token list -> (string * string option) list * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
   val propp: token list -> (string * (string list * string list)) * token list
@@ -78,6 +79,8 @@
   val xthms1: token list -> (thmref * Attrib.src list) list * token list
   val name_facts: token list ->
     ((bstring * Attrib.src list) * (thmref * Attrib.src list) list) list * token list
+  val locale_mixfix: token list -> mixfix * token list
+  val locale_fixes: token list -> (string * string option * mixfix) list * token list
   val locale_target: token list -> xstring * token list
   val opt_locale_target: token list -> xstring option * token list
   val locale_expr: token list -> Locale.expr * token list
@@ -220,36 +223,40 @@
 
 (* mixfix annotations *)
 
-val infx = $$$ "infix" |-- !!! (nat >> Syntax.Infix || string -- nat >> Syntax.InfixName);
-val infxl = $$$ "infixl" |-- !!! (nat >> Syntax.Infixl || string -- nat >> Syntax.InfixlName);
-val infxr = $$$ "infixr" |-- !!! (nat >> Syntax.Infixr || string -- nat >> Syntax.InfixrName);
+val mfix = string --
+  !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
+    Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
+
+val infx = $$$ "infix" |-- !!! (nat >> Infix || string -- nat >> InfixName);
+val infxl = $$$ "infixl" |-- !!! (nat >> Infixl || string -- nat >> InfixlName);
+val infxr = $$$ "infixr" |-- !!! (nat >> Infixr || string -- nat >> InfixrName);
 
-val binder =
-  $$$ "binder" |--
-    !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
-  >> (Syntax.Binder o triple2);
+val binder = $$$ "binder" |--
+  !!! (string -- ($$$ "[" |-- nat --| $$$ "]" -- nat || nat >> (fn n => (n, n))))
+  >> (Binder o triple2);
+
+fun annotation guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
+fun opt_annotation guard fix = Scan.optional (annotation guard fix) NoSyn;
+
+val mixfix = annotation !!! (mfix || binder || infxl || infxr || infx);
+val opt_infix = opt_annotation !!! (infxl || infxr || infx);
+val opt_mixfix = opt_annotation !!! (mfix || binder || infxl || infxr || infx);
+val opt_infix' = opt_annotation I (infxl || infxr || infx);
+val opt_mixfix' = opt_annotation I (mfix || binder || infxl || infxr || infx);
 
 
-val opt_pris = Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [];
-
-val mixfix =
-  (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
-  >> (Syntax.Mixfix o triple2);
-
-fun fix_decl guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
-fun opt_fix guard fix = Scan.optional (fix_decl guard fix) Syntax.NoSyn;
-
-val opt_infix = opt_fix !!! (infxl || infxr || infx);
-val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
-val opt_infix' = opt_fix I (infxl || infxr || infx);
-val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
-val mixfix' = fix_decl !!! (mixfix || binder || infxl || infxr || infx);
-
-
-(* consts *)
+(* fixes *)
 
 val const = name -- ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
-val param = name -- Scan.option ($$$ "::" |-- !!! typ) -- opt_mixfix >> triple1;
+
+val params = Scan.repeat1 name -- Scan.option ($$$ "::" |-- !!! typ)
+  >> (fn (xs, T) => map (rpair T) xs);
+
+val simple_fixes = and_list1 params >> List.concat;
+
+val fixes =
+  and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- mixfix >> (single o triple1) ||
+    params >> map Syntax.no_syn) >> List.concat;
 
 
 (* terms *)
@@ -329,15 +336,19 @@
 
 (* locale and context elements *)
 
+val locale_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K Structure || mixfix;
+
+val locale_fixes =
+  and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- locale_mixfix >> (single o triple1) ||
+    params >> map Syntax.no_syn) >> List.concat;
+
 local
 
-val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K NONE || opt_mixfix >> SOME;
 val loc_keyword = $$$ "fixes" || $$$ "constrains" || $$$ "assumes" ||
    $$$ "defines" || $$$ "notes" || $$$ "includes";
 
 val loc_element =
-  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
-    >> triple1)) >> Element.Fixes ||
+  $$$ "fixes" |-- !!! locale_fixes >> Element.Fixes ||
   $$$ "constrains" |-- !!! (and_list1 (name -- ($$$ "::" |-- typ)))
     >> Element.Constrains ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
@@ -350,7 +361,7 @@
 fun plus1 scan =
   scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
 
-val rename = name -- Scan.option mixfix';
+val rename = name -- Scan.option mixfix;
 
 fun expr2 x = (xname >> Locale.Locale || $$$ "(" |-- !!! (expr0 --| $$$ ")")) x
 and expr1 x = (expr2 -- Scan.repeat1 (maybe rename) >> Locale.Rename || expr2) x