merged

--- a/src/Pure/Concurrent/future.ML	Mon Mar 23 19:01:17 2009 +0100
+++ b/src/Pure/Concurrent/future.ML	Mon Mar 23 19:01:34 2009 +0100
@@ -212,7 +212,8 @@
     val _ = if continue then () else scheduler := NONE;
 
     val _ = notify_all ();
-    val _ = interruptible (fn () => wait_timeout (Time.fromSeconds 1)) ()
+    val _ = interruptible (fn () =>
+        wait_timeout (Time.fromMilliseconds (if null (! canceled) then 1000 else 50))) ()
       handle Exn.Interrupt => List.app do_cancel (Task_Queue.cancel_all (! queue));
   in continue end;
 

--- a/src/Pure/General/pretty.ML	Mon Mar 23 19:01:17 2009 +0100
+++ b/src/Pure/General/pretty.ML	Mon Mar 23 19:01:34 2009 +0100
@@ -104,9 +104,9 @@
 (** printing items: compound phrases, strings, and breaks **)
 
 datatype T =
-  Block of Markup.T * T list * int * int |  (*markup, body, indentation, length*)
-  String of output * int |                  (*text, length*)
-  Break of bool * int;                      (*mandatory flag, width if not taken*)
+  Block of (output * output) * T list * int * int |  (*markup output, body, indentation, length*)
+  String of output * int |                           (*text, length*)
+  Break of bool * int;                               (*mandatory flag, width if not taken*)
 
 fun length (Block (_, _, _, len)) = len
   | length (String (_, len)) = len
@@ -124,12 +124,14 @@
 fun breaks prts = Library.separate (brk 1) prts;
 fun fbreaks prts = Library.separate fbrk prts;
 
-fun markup_block m (indent, es) =
+fun block_markup m (indent, es) =
   let
     fun sum [] k = k
       | sum (e :: es) k = sum es (length e + k);
   in Block (m, es, indent, sum es 0) end;
 
+fun markup_block m arg = block_markup (Markup.output m) arg;
+
 val blk = markup_block Markup.none;
 fun block prts = blk (2, prts);
 val strs = block o breaks o map str;
@@ -197,7 +199,7 @@
 local
   fun pruning dp (Block (m, bes, indent, wd)) =
         if dp > 0
-        then markup_block m (indent, map (pruning (dp - 1)) bes)
+        then block_markup m (indent, map (pruning (dp - 1)) bes)
         else str "..."
     | pruning dp e = e
 in
@@ -263,7 +265,7 @@
 fun format ([], _, _) text = text
   | format (e :: es, block as (blockind, blockin), after) (text as {ind, pos, nl, ...}) =
       (case e of
-        Block (markup, bes, indent, wd) =>
+        Block ((bg, en), bes, indent, wd) =>
           let
             val {emergencypos, ...} = ! margin_info;
             val pos' = pos + indent;
@@ -271,7 +273,6 @@
             val block' =
               if pos' < emergencypos then (ind |> add_indent indent, pos')
               else (add_indent pos'' Buffer.empty, pos'');
-            val (bg, en) = Markup.output markup;
             val btext: text = text
               |> control bg
               |> format (bes, block', breakdist (es, after))
@@ -303,9 +304,9 @@
 (*symbolic markup -- no formatting*)
 fun symbolic prt =
   let
-    fun out (Block (m, [], _, _)) = Buffer.markup m I
-      | out (Block (m, prts, indent, _)) =
-          Buffer.markup m (Buffer.markup (Markup.block indent) (fold out prts))
+    fun out (Block ((bg, en), [], _, _)) = Buffer.add bg #> Buffer.add en
+      | out (Block ((bg, en), prts, indent, _)) =
+          Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
       | out (String (s, _)) = Buffer.add s
       | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
       | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
@@ -314,7 +315,7 @@
 (*unformatted output*)
 fun unformatted prt =
   let
-    fun fmt (Block (m, prts, _, _)) = Buffer.markup m (fold fmt prts)
+    fun fmt (Block ((bg, en), prts, _, _)) = Buffer.add bg #> fold fmt prts #> Buffer.add en
       | fmt (String (s, _)) = Buffer.add s
       | fmt (Break (false, wd)) = Buffer.add (output_spaces wd)
       | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
@@ -323,11 +324,11 @@
 
 (* ML toplevel pretty printing *)
 
-fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (m, map to_ML prts, ind)
   | to_ML (String s) = ML_Pretty.String s
   | to_ML (Break b) = ML_Pretty.Break b;
 
-fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+fun from_ML (ML_Pretty.Block (m, prts, ind)) = block_markup m (ind, map from_ML prts)
   | from_ML (ML_Pretty.String s) = String s
   | from_ML (ML_Pretty.Break b) = Break b;
 

--- a/src/Pure/ML/ml_test.ML	Mon Mar 23 19:01:17 2009 +0100
+++ b/src/Pure/ML/ml_test.ML	Mon Mar 23 19:01:34 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,