# HG changeset patch
# User wenzelm
# Date 1727536311 -7200
# Node ID fd3c0135bfea77cf8e7160591ad1cbc4411d3de4
# Parent  8e123493e0ccbb8bdafd53f5f4f0c3a696ca0761
tuned: more uniform;

diff -r 8e123493e0cc -r fd3c0135bfea src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 16:58:04 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sat Sep 28 17:11:51 2024 +0200
@@ -608,21 +608,22 @@
           | Nonterminal (nt, min_prec) :: sa =>
               let (*predictor operation*)
                 fun movedot_lambda (t, k) = if min_prec <= k then cons (info, sa, t @ ts) else I;
-                val (used', states') =
+                val (used', states', used_trees) =
                   (case Inttab.lookup used nt of
-                    SOME (used_prec, used_trees) => (*nonterminal has been processed*)
-                      if used_prec <= min_prec then
-                        (*wanted precedence has been processed*)
-                        (used, Parsetrees.fold movedot_lambda used_trees states)
-                      else (*wanted precedence hasn't been parsed yet*)
+                    SOME (used_prec, used_trees) =>
+                      if used_prec <= min_prec then (used, states, used_trees)
+                      else
                         let
-                          val states' = states |> add_prods nt min_prec used_prec
-                            |> Parsetrees.fold movedot_lambda used_trees;
-                        in (update_prec (nt, min_prec) used, states') end
-                  | NONE => (*nonterminal is parsed for the first time*)
-                      let val states' = states |> add_prods nt min_prec no_prec;
-                      in (update_prec (nt, min_prec) used, states') end);
-              in process used' states' (S :: Si, Sii) end
+                          val used' = update_prec (nt, min_prec) used;
+                          val states' = states |> add_prods nt min_prec used_prec;
+                        in (used', states', used_trees) end
+                  | NONE =>
+                      let
+                        val used' = update_prec (nt, min_prec) used;
+                        val states' = states |> add_prods nt min_prec no_prec;
+                      in (used', states', Parsetrees.empty) end);
+                val states'' = states' |> Parsetrees.fold movedot_lambda used_trees;
+              in process used' states'' (S :: Si, Sii) end
           | Terminal a :: sa => (*scanner operation*)
               let
                 val (_, _, id, _) = info;