--- a/src/Pure/Syntax/syntax_ext.ML Sun Sep 16 20:33:37 2018 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Sun Sep 16 22:45:34 2018 +0200
@@ -20,6 +20,8 @@
datatype xprod = XProd of string * xsymb list * string * int
val chain_pri: int
val delims_of: xprod list -> string list list
+ datatype assoc = No_Assoc | Left_Assoc | Right_Assoc
+ val get_infix: xprod list -> string -> {assoc: assoc, delim: string, pri: int} option
datatype syn_ext =
Syn_Ext of {
xprods: xprod list,
@@ -111,6 +113,23 @@
|> map Symbol.explode;
+(* plain infix syntax *)
+
+datatype assoc = No_Assoc | Left_Assoc | Right_Assoc;
+
+fun get_infix xprods c =
+ xprods |> get_first (fn XProd (_, xsymbs, const, p) =>
+ if c = const then
+ (case xsymbs of
+ [Bg _, Argument (_, p1), Space _, Delim s, Brk _, Argument (_, p2), En] =>
+ if p1 = p + 1 andalso p2 = p + 1 then SOME {assoc = No_Assoc, delim = s, pri = p}
+ else if p1 = p andalso p2 = p + 1 then SOME {assoc = Left_Assoc, delim = s, pri = p}
+ else if p1 = p + 1 andalso p2 = p then SOME {assoc = Right_Assoc, delim = s, pri = p}
+ else NONE
+ | _ => NONE)
+ else NONE);
+
+
(** datatype mfix **)