# HG changeset patch
# User wenzelm
# Date 1727089150 -7200
# Node ID f6e595e4f6089250fa372b5d94b09ad57f3ded2b
# Parent  a9e2f4e845a092c8b9a0962988dd314b3fdf46f2
tuned;

diff -r a9e2f4e845a0 -r f6e595e4f608 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Sep 23 11:36:03 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Sep 23 12:59:10 2024 +0200
@@ -660,19 +660,17 @@
                     Pretty.breaks (map (Pretty.str o Lexicon.str_of_token) (#1 (split_last toks))) @
                     [Pretty.str "\""])])))
       end
-  | s =>
+  | states =>
       (case indata of
-        [] => s
+        [] => states
       | c :: cs =>
           let
-            val (si, sii) = PROCESSS gram stateset i c s;
-            val _ = Array.upd stateset i si;
-            val _ = Array.upd stateset (i + 1) sii;
+            val (Si, Sii) = PROCESSS gram stateset i c states;
+            val _ = Array.upd stateset i Si;
+            val _ = Array.upd stateset (i + 1) Sii;
           in produce gram stateset (i + 1) cs c end));
 
 
-fun get_trees states = map_filter (fn (_, [pt], _) => SOME pt | _ => NONE) states;
-
 fun earley (gram as Gram {tags, ...}) startsymbol indata =
   let
     val start_tag =
@@ -683,9 +681,8 @@
     val s = length indata + 1;
     val Estate = Array.array (s, []);
     val _ = Array.upd Estate 0 [S0];
-  in
-    get_trees (produce gram Estate 0 indata Lexicon.eof)
-  end;
+    val states = produce gram Estate 0 indata Lexicon.eof;
+  in map_filter (fn (_, [pt], _) => SOME pt | _ => NONE) states end;
 
 
 fun parse gram start toks =