fixed parser ignoring tokens and flipped associativity the right way round

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/FormulaParser.sml

@@ -24,10 +24,10 @@ struct
   open Scanner
 
   val prec =
-    fn AND => (6, 7)
-     | OR => (4, 5)
-     | RARROW => (3, 2)
-     | LRARROW => (1, 2)
+    fn AND => (7, 6)
+     | OR => (5, 4)
+     | RARROW => (2, 3)
+     | LRARROW => (1, 1)
      | _ => (~1, ~1)
 
   exception NotOperator
@@ -122,8 +122,13 @@ struct
                   val (lprec, rprec) = prec t
                   val comb = comb_func t
                 in
-                  if lprec < mprec then OK (v, r1, ts)
-                  else ((comb_p rprec) oo (fn res => comb (v, res))) rest
+                  if lprec < mprec then
+                    if connective t then
+                      ((comb_p 0) oo (fn res => comb (v, res))) rest
+                    else
+                      OK (v, r1, ts)
+                  else
+                    ((comb_p rprec) oo (fn res => comb (v, res))) rest
                 end
     in
       comb_p 0

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/SCANNER.sig

@@ -18,4 +18,6 @@ sig
 
   val scan: {srcname: string, input: string} -> (token * Region.reg) list
   val pp_token: token -> string
+
+  val connective: token -> bool
 end

lib/forgejo.ballcloud.cc/wball/proof-checker/parser/Scanner.sml

@@ -61,4 +61,7 @@ struct
      | ERR => "unk"
      | HASH => "#"
      | IDENT s => s
+
+  val connective =
+    fn AND => true | OR => true | RARROW => true | LRARROW => true | _ => false
 end