clarified Progress.stopped: rising edge only;
also cancel jobs that have not been considered yet;

--- a/src/Pure/Tools/build.scala	Sat Feb 23 12:55:59 2013 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 23 14:16:07 2013 +0100
@@ -38,7 +38,7 @@
 
     @volatile private var is_stopped = false
     def interrupt_handler[A](e: => A): A = Interrupt.handler { is_stopped = true } { e }
-    override def stopped: Boolean = { val b = is_stopped; is_stopped = false; b  }
+    override def stopped: Boolean = is_stopped
   }
 
 
@@ -745,11 +745,10 @@
       results: Map[String, Result]): Map[String, Result] =
     {
       if (pending.is_empty) results
-      else if (progress.stopped) {
-        for ((_, (_, job)) <- running) job.terminate
-        sleep(); loop(pending, running, results)
-      }
-      else
+      else {
+        if (progress.stopped)
+          for ((_, (_, job)) <- running) job.terminate
+
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((name, (parent_heap, job))) =>
             //{{{ finish job
@@ -826,7 +825,7 @@
                   if (verbose) progress.echo("Skipping " + name + " ...")
                   loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
                 }
-                else if (parent_result.rc == 0) {
+                else if (parent_result.rc == 0 && !progress.stopped) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
                     new Job(progress, name, info, output, do_output, verbose, browser_info,
@@ -842,6 +841,7 @@
             ///}}}
           case None => sleep(); loop(pending, running, results)
         }
+      }
     }
 
 

--- a/src/Pure/Tools/build_dialog.scala	Sat Feb 23 12:55:59 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Sat Feb 23 14:16:07 2013 +0100
@@ -69,7 +69,7 @@
 
     /* GUI state */
 
-    private var is_stopped = false
+    @volatile private var is_stopped = false
     private var return_code = 2
 
     override def closeOperation { sys.exit(return_code) }
@@ -96,8 +96,7 @@
         }
       override def theory(session: String, theory: String): Unit =
         echo(session + ": theory " + theory)
-      override def stopped: Boolean =
-        Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }
+      override def stopped: Boolean = is_stopped
     }