1.1 --- a/src/Pure/Isar/local_syntax.ML	Sun Apr 09 18:51:20 2006 +0200
     1.2 +++ b/src/Pure/Isar/local_syntax.ML	Sun Apr 09 18:51:21 2006 +0200
     1.3 @@ -21,12 +21,17 @@
     1.4  structure LocalSyntax: LOCAL_SYNTAX =
     1.5  struct
     1.6  
     1.7 +
     1.8  (* datatype T *)
     1.9  
    1.10 +type local_mixfix =
    1.11 +  ((string * bool) * string list list) *          (*name, fixed?, mixfix content*)
    1.12 +  ((string * bool) * (string * typ * mixfix));    (*mode, inout?, mixfix syntax*)
    1.13 +
    1.14  datatype T = Syntax of
    1.15   {thy_syntax: Syntax.syntax,
    1.16    local_syntax: Syntax.syntax,
    1.17 -  mixfixes: (((string * bool) * string list list) * (string * typ * mixfix)) list,
    1.18 +  mixfixes: local_mixfix list,
    1.19    idents: string list * string list};
    1.20  
    1.21  fun make_syntax (thy_syntax, local_syntax, mixfixes, idents) =
    1.22 @@ -53,9 +58,10 @@
    1.23      val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
    1.24      val local_syntax = thy_syntax
    1.25        |> Syntax.extend_trfuns
    1.26 -         (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    1.27 -          map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    1.28 -      |> Syntax.extend_const_gram is_logtype Syntax.default_mode (map snd mixfixes)
    1.29 +          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
    1.30 +           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
    1.31 +      |> fold (uncurry (Syntax.extend_const_gram is_logtype))
    1.32 +          (coalesce (op =) (rev (map snd mixfixes)));
    1.33    in make_syntax (thy_syntax, local_syntax, mixfixes, idents) end;
    1.34  
    1.35  fun init thy = build_syntax thy ([], ([], []));
    1.36 @@ -72,14 +78,17 @@
    1.37  fun mixfix_nosyn (_, (_, _, mx)) = mx = NoSyn;
    1.38  fun mixfix_struct (_, (_, _, mx)) = mx = Structure;
    1.39  
    1.40 -fun mixfix_conflict (content1: string list list, ((_, content2), _)) =
    1.41 -  exists (fn x => exists (fn y => x = y) content2) content1;
    1.42 +fun mixfix_conflict ((content1: string list list, inout1), ((_, content2), ((_, inout2), _))) =
    1.43 +  inout1 andalso inout2 andalso exists (fn x => exists (fn y => x = y) content2) content1;
    1.44  
    1.45 -fun add_mixfix (fixed, (x, T, mx)) =
    1.46 +fun add_mixfix (mode, inout) (fixed, (x, T, mx)) =
    1.47    let
    1.48      val content = Syntax.mixfix_content mx;
    1.49      val c = if fixed then Syntax.fixedN ^ x else x;
    1.50 -  in remove mixfix_conflict content #> cons (((x, fixed), content), (c, T, mx)) end;
    1.51 +  in
    1.52 +    remove mixfix_conflict (content, inout) #>
    1.53 +    cons (((x, fixed), content), ((mode, inout), (c, T, mx)))
    1.54 +  end;
    1.55  
    1.56  fun prep_struct (fixed, (c, _, Structure)) =
    1.57        if fixed then SOME c
    1.58 @@ -93,7 +102,7 @@
    1.59      [] => syntax
    1.60    | decls =>
    1.61        let
    1.62 -        val mixfixes' = mixfixes |> fold add_mixfix (filter_out mixfix_struct decls);
    1.63 +        val mixfixes' = mixfixes |> fold (add_mixfix prmode) (filter_out mixfix_struct decls);
    1.64          val fixes' = fold (fn (((x, true), _), _) => cons x | _ => I) mixfixes' [];
    1.65          val structs' = structs @ List.mapPartial prep_struct decls;
    1.66        in build_syntax thy (mixfixes', (structs', fixes')) end);