# 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,