# HG changeset patch
# User wenzelm
# Date 1301953976 -7200
# Node ID ff50c436b199c3ba455b74e1f6fc7353e72e1a6c
# Parent  b8d1fc4cc4e5b022476fbad3be666b72e937788f
accumulate parsetrees in canonical reverse order;

diff -r b8d1fc4cc4e5 -r ff50c436b199 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Mon Apr 04 23:26:32 2011 +0200
+++ b/src/Pure/Syntax/parser.ML	Mon Apr 04 23:52:56 2011 +0200
@@ -706,15 +706,15 @@
 
 
 fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) =
-  if Lexicon.valued_token c then (A, j, ts @ [Tip c], sa, id, i)
+  if Lexicon.valued_token c then (A, j, Tip c :: ts, sa, id, i)
   else (A, j, ts, sa, id, i);
 
 fun movedot_nonterm tt (A, j, ts, Nonterminal _ :: sa, id, i) =
-  (A, j, ts @ tt, sa, id, i);
+  (A, j, List.revAppend (tt, ts), sa, id, i);
 
 fun movedot_lambda [] _ = []
   | movedot_lambda ((t, ki) :: ts) (state as (B, j, tss, Nonterminal (A, k) :: sa, id, i)) =
-      if k <= ki then (B, j, tss @ t, sa, id, i) :: movedot_lambda ts state
+      if k <= ki then (B, j, List.revAppend (t, tss), sa, id, i) :: movedot_lambda ts state
       else movedot_lambda ts state;
 
 
@@ -784,7 +784,7 @@
                 (S :: Si,
                   if Lexicon.matching_tokens (a, c) then movedot_term c S :: Sii else Sii)
           | (A, prec, ts, [], id, j) => (*completer operation*)
-              let val tt = if id = "" then ts else [Node (id, ts)] in
+              let val tt = if id = "" then ts else [Node (id, rev ts)] in
                 if j = i then (*lambda production?*)
                   let
                     val (used', prec') = update_trees used (A, (tt, prec));