# HG changeset patch
# User wenzelm
# Date 1727600923 -7200
# Node ID 720bc21720205d14c3c160886b9aff6effb6e999
# Parent  addebc07f06e7a676a9ed43c751e227241553985
tuned signature;

diff -r addebc07f06e -r 720bc2172020 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Sat Sep 28 23:23:30 2024 +0200
+++ b/src/Pure/Syntax/parser.ML	Sun Sep 29 11:08:43 2024 +0200
@@ -551,9 +551,9 @@
 
 val empty_output = Output (0, []);
 
-fun init_output t = Output (1, [t]);
+fun token_output tok (Output (n, ts)) = Output (n + 1, Tip tok :: ts);
 
-fun add_output t (Output (n, ts)) = Output (n + 1, t :: ts);
+fun node_output id (Output (_, ts)) = Output (1, [Node (id, rev ts)]);
 
 fun append_output (Output (m, ss)) (Output (n, ts)) = Output (m + n, ss @ ts);
 
@@ -562,8 +562,6 @@
     EQUAL => dict_ord tree_ord (ss, tt)
   | ord => ord));
 
-fun output_content (Output (_, ts)) = rev ts;
-
 fun output_result (Output (_, [t])) = SOME t
   | output_result _ = NONE;
 
@@ -659,14 +657,14 @@
                   else (*move dot*)
                     let
                       val out' =
-                        if Lexicon.valued_token c orelse id <> "" then add_output (Tip c) out
+                        if Lexicon.valued_token c orelse id <> "" then token_output c out
                         else out;
                     in (info, sa, out') :: Sii end;
               in process used states (S :: Si, Sii') end
           | [] => (*completer operation*)
               let
                 val (A, p, id, j) = info;
-                val out' = if id = "" then out else init_output (Node (id, output_content out));
+                val out' = if id = "" then out else node_output id out;
                 val (used', Slist) =
                   if j = i then (*lambda production?*)
                     let val (q, used') = update_output (A, (out', p)) used