src/Pure/Syntax/mixfix.ML
changeset 19003 64ad6c520464
parent 18719 dca3ae4f6dd6
child 19020 e1867198df48
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Feb 10 02:22:50 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 10 02:22:52 2006 +0100
     1.3 @@ -32,6 +32,7 @@
     1.4    val fix_mixfix: string -> mixfix -> mixfix
     1.5    val unlocalize_mixfix: mixfix -> mixfix
     1.6    val mixfix_args: mixfix -> int
     1.7 +  val mixfix_conflict: mixfix * mixfix -> bool
     1.8  end;
     1.9  
    1.10  signature MIXFIX =
    1.11 @@ -142,6 +143,23 @@
    1.12    | mixfix_args (Binder _) = 1
    1.13    | mixfix_args Structure = 0;
    1.14  
    1.15 +fun mixfix_conflict (mx1, mx2) =
    1.16 +  let
    1.17 +    fun content kind sy = SOME (kind, SynExt.mfix_delims sy);
    1.18 +    fun content_of (Mixfix (sy, _, _)) = content 0 sy
    1.19 +      | content_of (Delimfix sy) = content 0 sy
    1.20 +      | content_of (InfixName (sy, _)) = content 1 sy
    1.21 +      | content_of (InfixlName (sy, _)) = content 1 sy
    1.22 +      | content_of (InfixrName (sy, _)) = content 1 sy
    1.23 +      | content_of (Binder (sy, _, _)) = content 2 sy
    1.24 +      | content_of _ = NONE;
    1.25 +  in
    1.26 +    (case (content_of mx1, content_of mx2) of
    1.27 +      (SOME (kind1, delims1), SOME (kind2, delims2)) =>
    1.28 +        (kind1 = 0 orelse kind2 = 0 orelse kind1 = kind2) andalso delims1 = delims2
    1.29 +    | _ => false)
    1.30 +  end;
    1.31 +
    1.32  
    1.33  (* syn_ext_types *)
    1.34