# HG changeset patch
# User wenzelm
# Date 1237818815 -3600
# Node ID df8a3c2fd5a214c25b5943f57910a326c059d134
# Parent  53fbf7c679b0adca8e9902b35c43a7a87d590e6c
maintain parse trees cumulatively;

diff -r 53fbf7c679b0 -r df8a3c2fd5a2 src/Pure/ML/ml_test.ML
--- a/src/Pure/ML/ml_test.ML	Mon Mar 23 15:23:06 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Mon Mar 23 15:33:35 2009 +0100
@@ -6,7 +6,7 @@
 
 signature ML_TEST =
 sig
-  val get_result: Proof.context -> PolyML.parseTree option
+  val get_result: Proof.context -> PolyML.parseTree list
   val eval: bool -> bool -> Position.T -> ML_Lex.token list -> unit
 end
 
@@ -17,10 +17,10 @@
 
 structure Result = GenericDataFun
 (
-  type T = PolyML.parseTree option;
-  val empty = NONE;
-  fun extend _ = NONE;
-  fun merge _ _ = NONE;
+  type T = PolyML.parseTree list;
+  val empty = [];
+  fun extend _ = [];
+  fun merge _ _ = [];
 );
 
 val get_result = Result.get o Context.Proof;
@@ -61,7 +61,8 @@
       put (Position.str_of (pos_of location) ^ "\n"));
 
     fun result_fun (parse_tree, code) () =
-      (Context.>> (Result.put parse_tree); (if is_none code then warning "Static Errors" else ()));
+     (Context.>> (Result.map (append (the_list parse_tree)));
+      if is_none code then warning "Static Errors" else ());
 
     val parameters =
      [PolyML.Compiler.CPOutStream put,