# HG changeset patch # User wenzelm # Date 1586204980 -7200 # Node ID 23abd7f9f054a55e9690ce3ec298ed1774dc2b5f # Parent 54ac957c53ec171362ec0eb2ccb17d9e93d547b3# Parent 8e5c20e4e11a35c4dbe0f256c659823e3d16e434 merged; diff -r 8e5c20e4e11a -r 23abd7f9f054 NEWS --- a/NEWS Mon Apr 06 19:46:38 2020 +0100 +++ b/NEWS Mon Apr 06 22:29:40 2020 +0200 @@ -7,6 +7,11 @@ New in this Isabelle version ---------------------------- +*** System *** + +* The command-line tool "isabelle console" now supports interrupts +properly (on Linux and macOS). + New in Isabelle2020 (April 2020) diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/Concurrent/delay.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/delay.scala Mon Apr 06 22:29:40 2020 +0200 @@ -0,0 +1,66 @@ +/* Title: Pure/Concurrent/delay.scala + Author: Makarius + +Delayed events. +*/ + +package isabelle + + +object Delay +{ + // delayed event after first invocation + def first(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay = + new Delay(true, delay, log, if (gui) GUI_Thread.later { event } else event ) + + // delayed event after last invocation + def last(delay: => Time, log: Logger = No_Logger, gui: Boolean = false)(event: => Unit): Delay = + new Delay(false, delay, log, if (gui) GUI_Thread.later { event } else event ) +} + +final class Delay private(first: Boolean, delay: => Time, log: Logger, event: => Unit) +{ + private var running: Option[Event_Timer.Request] = None + + private def run: Unit = + { + val do_run = synchronized { + if (running.isDefined) { running = None; true } else false + } + if (do_run) { + try { event } + catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn } + } + } + + def invoke(): Unit = synchronized + { + val new_run = + running match { + case Some(request) => if (first) false else { request.cancel; true } + case None => true + } + if (new_run) + running = Some(Event_Timer.request(Time.now() + delay)(run)) + } + + def revoke(): Unit = synchronized + { + running match { + case Some(request) => request.cancel; running = None + case None => + } + } + + def postpone(alt_delay: Time): Unit = synchronized + { + running match { + case Some(request) => + val alt_time = Time.now() + alt_delay + if (request.time < alt_time && request.cancel) { + running = Some(Event_Timer.request(alt_time)(run)) + } + case None => + } + } +} diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/Concurrent/isabelle_thread.scala --- a/src/Pure/Concurrent/isabelle_thread.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/Concurrent/isabelle_thread.scala Mon Apr 06 22:29:40 2020 +0200 @@ -12,7 +12,19 @@ object Isabelle_Thread { - /* fork */ + /* self-thread */ + + def self: Isabelle_Thread = + Thread.currentThread match { + case thread: Isabelle_Thread => thread + case thread => error("Isabelle-specific thread required: " + thread) + } + + def check_self: Boolean = + Thread.currentThread.isInstanceOf[Isabelle_Thread] + + + /* create threads */ private val counter = Counter.make() @@ -21,6 +33,18 @@ def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup + def create( + main: Runnable, + name: String = "", + group: ThreadGroup = current_thread_group, + pri: Int = Thread.NORM_PRIORITY, + daemon: Boolean = false, + inherit_locals: Boolean = false): Isabelle_Thread = + { + new Isabelle_Thread(main, name = make_name(name = name), group = group, + pri = pri, daemon = daemon, inherit_locals = inherit_locals) + } + def fork( name: String = "", group: ThreadGroup = current_thread_group, @@ -29,108 +53,71 @@ inherit_locals: Boolean = false, uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread = { - val main = - if (uninterruptible) new Runnable { override def run { Isabelle_Thread.uninterruptible { body } } } - else new Runnable { override def run { body } } + val main: Runnable = + if (uninterruptible) { () => Isabelle_Thread.uninterruptible { body } } + else { () => body } val thread = - new Isabelle_Thread(main, name = make_name(name = name), group = group, - pri = pri, daemon = daemon, inherit_locals = inherit_locals) + create(main, name = name, group = group, pri = pri, + daemon = daemon, inherit_locals = inherit_locals) thread.start thread } - /* self */ - - def self: Isabelle_Thread = - Thread.currentThread match { - case thread: Isabelle_Thread => thread - case _ => error("Isabelle-specific thread required") - } - - def uninterruptible[A](body: => A): A = self.uninterruptible(body) - - - /* pool */ + /* thread pool */ lazy val pool: ThreadPoolExecutor = - { - val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 - val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 - val executor = - new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) - executor.setThreadFactory( - new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group)) - executor - } + { + val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 + val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 + val executor = + new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) + executor.setThreadFactory(create(_, name = make_name(base = "worker"), group = current_thread_group)) + executor + } - /* delayed events */ - - final class Delay private[Isabelle_Thread]( - first: Boolean, delay: => Time, log: Logger, event: => Unit) - { - private var running: Option[Event_Timer.Request] = None + /* interrupt handlers */ - private def run: Unit = - { - val do_run = synchronized { - if (running.isDefined) { running = None; true } else false - } - if (do_run) { - try { event } - catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn } - } - } + object Interrupt_Handler + { + def apply(handle: Isabelle_Thread => Unit, name: String = "handler"): Interrupt_Handler = + new Interrupt_Handler(handle, name) + + val interruptible: Interrupt_Handler = + Interrupt_Handler(_.raise_interrupt, name = "interruptible") - def invoke(): Unit = synchronized - { - val new_run = - running match { - case Some(request) => if (first) false else { request.cancel; true } - case None => true - } - if (new_run) - running = Some(Event_Timer.request(Time.now() + delay)(run)) - } + val uninterruptible: Interrupt_Handler = + Interrupt_Handler(_.postpone_interrupt, name = "uninterruptible") + } - def revoke(): Unit = synchronized - { - running match { - case Some(request) => request.cancel; running = None - case None => - } - } - - def postpone(alt_delay: Time): Unit = synchronized - { - running match { - case Some(request) => - val alt_time = Time.now() + alt_delay - if (request.time < alt_time && request.cancel) { - running = Some(Event_Timer.request(alt_time)(run)) - } - case None => - } - } + class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String) + extends Function[Isabelle_Thread, Unit] + { + def apply(thread: Isabelle_Thread) { handle(thread) } + override def toString: String = name } - // delayed event after first invocation - def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = - new Delay(true, delay, log, event) + def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A = + if (handler == null) body + else self.interrupt_handler(handler)(body) + + def interrupt_handler[A](handle: Isabelle_Thread => Unit)(body: => A): A = + self.interrupt_handler(Interrupt_Handler(handle))(body) - // delayed event after last invocation - def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = - new Delay(false, delay, log, event) + def interruptible[A](body: => A): A = + interrupt_handler(Interrupt_Handler.interruptible)(body) + + def uninterruptible[A](body: => A): A = + interrupt_handler(Interrupt_Handler.uninterruptible)(body) + + def try_uninterruptible[A](body: => A): A = + if (check_self) interrupt_handler(Interrupt_Handler.uninterruptible)(body) + else body } -class Isabelle_Thread private( - main: Runnable, - name: String = "", - group: ThreadGroup = null, - pri: Int = Thread.NORM_PRIORITY, - daemon: Boolean = false, - inherit_locals: Boolean = false) +class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup, + pri: Int, daemon: Boolean, inherit_locals: Boolean) extends Thread(group, null, name, 0L, inherit_locals) { thread => @@ -140,30 +127,56 @@ override def run { main.run() } - private var interruptible: Boolean = true - private var interrupt_pending: Boolean = false + def is_self: Boolean = Thread.currentThread == thread + + + /* interrupt state */ + + // synchronized, with concurrent changes + private var interrupt_postponed: Boolean = false - override def interrupt: Unit = synchronized + def clear_interrupt: Boolean = synchronized { - if (interruptible) super.interrupt() - else { interrupt_pending = true } + val was_interrupted = isInterrupted || interrupt_postponed + Exn.Interrupt.dispose() + interrupt_postponed = false + was_interrupted + } + + def raise_interrupt: Unit = synchronized + { + interrupt_postponed = false + super.interrupt() } - def uninterruptible[A](body: => A): A = + def postpone_interrupt: Unit = synchronized { - require(Thread.currentThread == thread) + interrupt_postponed = true + Exn.Interrupt.dispose() + } + + + /* interrupt handler */ + + // non-synchronized, only changed on self-thread + @volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible + + override def interrupt: Unit = handler(thread) - val interruptible0 = synchronized { val b = interruptible; interruptible = false; b } - try { body } - finally { - synchronized { - interruptible = interruptible0 - if (interruptible && interrupt_pending) { - interrupt_pending = false - super.interrupt() - } + def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A = + if (new_handler == null) body + else { + require(is_self) + + val old_handler = handler + handler = new_handler + try { + if (clear_interrupt) interrupt + body } - Exn.Interrupt.expose() + finally { + handler = old_handler + if (clear_interrupt) interrupt + } } - } } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/GUI/gui_thread.scala --- a/src/Pure/GUI/gui_thread.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/GUI/gui_thread.scala Mon Apr 06 22:29:40 2020 +0200 @@ -16,13 +16,13 @@ def assert[A](body: => A): A = { - Predef.assert(SwingUtilities.isEventDispatchThread()) + Predef.assert(SwingUtilities.isEventDispatchThread) body } def require[A](body: => A): A = { - Predef.require(SwingUtilities.isEventDispatchThread()) + Predef.require(SwingUtilities.isEventDispatchThread) body } @@ -31,36 +31,27 @@ def now[A](body: => A): A = { - if (SwingUtilities.isEventDispatchThread()) body + if (SwingUtilities.isEventDispatchThread) body else { - lazy val result = { assert { Exn.capture(body) } } - SwingUtilities.invokeAndWait(new Runnable { def run = result }) + lazy val result = assert { Exn.capture(body) } + SwingUtilities.invokeAndWait(() => result) Exn.release(result) } } def later(body: => Unit) { - if (SwingUtilities.isEventDispatchThread()) body - else SwingUtilities.invokeLater(new Runnable { def run = body }) + if (SwingUtilities.isEventDispatchThread) body + else SwingUtilities.invokeLater(() => body) } def future[A](body: => A): Future[A] = { - if (SwingUtilities.isEventDispatchThread()) Future.value(body) + if (SwingUtilities.isEventDispatchThread) Future.value(body) else { val promise = Future.promise[A] later { promise.fulfill_result(Exn.capture(body)) } promise } } - - - /* delayed events */ - - def delay_first(delay: => Time)(event: => Unit): Isabelle_Thread.Delay = - Isabelle_Thread.delay_first(delay) { later { event } } - - def delay_last(delay: => Time)(event: => Unit): Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(delay) { later { event } } } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/General/exn.scala --- a/src/Pure/General/exn.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/General/exn.scala Mon Apr 06 22:29:40 2020 +0200 @@ -96,22 +96,10 @@ def apply(): Throwable = new InterruptedException def unapply(exn: Throwable): Boolean = is_interrupt(exn) + def dispose() { Thread.interrupted } def expose() { if (Thread.interrupted) throw apply() } def impose() { Thread.currentThread.interrupt } - def postpone[A](body: => A): Option[A] = - { - val interrupted = Thread.interrupted - val result = capture { body } - if (interrupted) impose() - result match { - case Res(x) => Some(x) - case Exn(e) => - if (is_interrupt(e)) { impose(); None } - else throw e - } - } - val return_code = 130 } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/General/file_watcher.scala --- a/src/Pure/General/file_watcher.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/General/file_watcher.scala Mon Apr 06 22:29:40 2020 +0200 @@ -84,7 +84,7 @@ /* changed directory entries */ - private val delay_changed = Isabelle_Thread.delay_last(delay) + private val delay_changed = Delay.last(delay) { val changed = state.change_result(st => (st.changed, st.copy(changed = Set.empty))) handle(changed) diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/ML/ml_console.scala --- a/src/Pure/ML/ml_console.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/ML/ml_console.scala Mon Apr 06 22:29:40 2020 +0200 @@ -74,16 +74,11 @@ else Some(Sessions.base_info( options, logic, dirs = dirs, include_sessions = include_sessions).check_base)) - val tty_loop = new TTY_Loop(process.stdin, process.stdout, Some(process.interrupt _)) - val process_result = Future.thread[Int]("process_result") { + POSIX_Interrupt.handler { process.interrupt } { + new TTY_Loop(process.stdin, process.stdout).join val rc = process.join - tty_loop.cancel // FIXME does not quite work, cannot interrupt blocking read on System.in - rc + if (rc != 0) sys.exit(rc) } - tty_loop.join - - val rc = process_result.join - if (rc != 0) sys.exit(rc) } } } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/PIDE/headless.scala --- a/src/Pure/PIDE/headless.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/PIDE/headless.scala Mon Apr 06 22:29:40 2020 +0200 @@ -304,12 +304,12 @@ val consumer = { val delay_nodes_status = - Isabelle_Thread.delay_first(nodes_status_delay max Time.zero) { + Delay.first(nodes_status_delay max Time.zero) { progress.nodes_status(use_theories_state.value.nodes_status) } val delay_commit_clean = - Isabelle_Thread.delay_first(commit_cleanup_delay max Time.zero) { + Delay.first(commit_cleanup_delay max Time.zero) { val clean_theories = use_theories_state.change_result(_.clean_theories) if (clean_theories.nonEmpty) { progress.echo("Removing " + clean_theories.length + " theories ...") diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/PIDE/session.scala Mon Apr 06 22:29:40 2020 +0200 @@ -268,7 +268,7 @@ nodes = Set.empty commands = Set.empty } - private val delay_flush = Isabelle_Thread.delay_first(output_delay) { flush() } + private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { @@ -313,7 +313,7 @@ private object consolidation { private val delay = - Isabelle_Thread.delay_first(consolidate_delay) { manager.send(Consolidate_Execution) } + Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) @@ -382,7 +382,7 @@ /* manager thread */ private val delay_prune = - Isabelle_Thread.delay_first(prune_delay) { manager.send(Prune_History) } + Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/System/bash.scala Mon Apr 06 22:29:40 2020 +0200 @@ -10,6 +10,8 @@ import java.io.{File => JFile, BufferedReader, InputStreamReader, BufferedWriter, OutputStreamWriter} +import scala.annotation.tailrec + object Bash { @@ -100,41 +102,36 @@ private val pid = stdout.readLine - def interrupt() - { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } } - - private def kill(signal: String): Boolean = - Exn.Interrupt.postpone { - Isabelle_System.kill(signal, pid) - Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true - - private def multi_kill(signal: String): Boolean = + @tailrec private def kill(signal: String, count: Int = 1): Boolean = { - var running = true - var count = 10 - while (running && count > 0) { - if (kill(signal)) { - Exn.Interrupt.postpone { - Time.seconds(0.1).sleep - count -= 1 - } + count <= 0 || + { + Isabelle_System.kill(signal, pid) + val running = Isabelle_System.kill("0", pid)._2 == 0 + if (running) { + Time.seconds(0.1).sleep + kill(signal, count - 1) } - else running = false + else false } - running } - def terminate() + def terminate(): Unit = Isabelle_Thread.try_uninterruptible { - multi_kill("INT") && multi_kill("TERM") && kill("KILL") + kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") proc.destroy do_cleanup() } + def interrupt(): Unit = Isabelle_Thread.try_uninterruptible + { + Isabelle_System.kill("INT", pid) + } + // JVM shutdown hook - private val shutdown_hook = new Thread { override def run = terminate() } + private val shutdown_hook = Isabelle_Thread.create(() => terminate()) try { Runtime.getRuntime.addShutdownHook(shutdown_hook) } catch { case _: IllegalStateException => } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/System/isabelle_process.scala Mon Apr 06 22:29:40 2020 +0200 @@ -76,4 +76,6 @@ session.stop() result } + + def terminate { process.terminate } } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/System/isabelle_system.scala Mon Apr 06 22:29:40 2020 +0200 @@ -287,7 +287,7 @@ proc.getInputStream.close proc.getErrorStream.close proc.destroy - Thread.interrupted + Exn.Interrupt.dispose() } (output, rc) } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/System/tty_loop.scala --- a/src/Pure/System/tty_loop.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/System/tty_loop.scala Mon Apr 06 22:29:40 2020 +0200 @@ -10,13 +10,14 @@ import java.io.{IOException, Writer, Reader, InputStreamReader, BufferedReader} -class TTY_Loop(writer: Writer, reader: Reader, - writer_lock: AnyRef = new Object, - interrupt: Option[() => Unit] = None) +class TTY_Loop( + writer: Writer, + reader: Reader, + writer_lock: AnyRef = new Object) { - private val console_output = Future.thread[Unit]("console_output") { + private val console_output = Future.thread[Unit]("console_output", uninterruptible = true) { try { - var result = new StringBuilder(100) + val result = new StringBuilder(100) var finished = false while (!finished) { var c = -1 @@ -40,32 +41,25 @@ catch { case e: IOException => case Exn.Interrupt() => } } - private val console_input = Future.thread[Unit]("console_input") { + private val console_input = Future.thread[Unit]("console_input", uninterruptible = true) { val console_reader = new BufferedReader(new InputStreamReader(System.in)) - def body - { - try { - var finished = false - while (!finished) { - console_reader.readLine() match { - case null => - writer.close() - finished = true - case line => - writer_lock.synchronized { - writer.write(line) - writer.write("\n") - writer.flush() - } - } + try { + var finished = false + while (!finished) { + console_reader.readLine() match { + case null => + writer.close() + finished = true + case line => + writer_lock.synchronized { + writer.write(line) + writer.write("\n") + writer.flush() + } } } - catch { case e: IOException => case Exn.Interrupt() => } } - interrupt match { - case None => body - case Some(int) => POSIX_Interrupt.handler { int() } { body } - } + catch { case e: IOException => case Exn.Interrupt() => } } def join { console_output.join; console_input.join } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/Tools/build.scala Mon Apr 06 22:29:40 2020 +0200 @@ -174,7 +174,7 @@ Export.consumer(store.open_database(session_name, output = true), cache = store.xz_cache) private val future_result: Future[Process_Result] = - Future.thread("build") { + Future.thread("build", uninterruptible = true) { val parent = info.parent.getOrElse("") val base = deps(parent) val args_yxml = @@ -321,14 +321,17 @@ cwd = info.dir.file, env = env) val errors = - Exn.capture { process.await_startup } match { - case Exn.Res(_) => - session.protocol_command("build_session", args_yxml) - build_session_errors.join - case Exn.Exn(exn) => List(Exn.message(exn)) + Isabelle_Thread.interrupt_handler(_ => process.terminate) { + Exn.capture { process.await_startup } match { + case Exn.Res(_) => + session.protocol_command("build_session", args_yxml) + build_session_errors.join_result + case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) + } } - val process_result = process.await_shutdown + val process_result = + Isabelle_Thread.interrupt_handler(_ => process.terminate) { process.await_shutdown } val process_output = stdout.toString :: messages.toList ::: command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: @@ -337,11 +340,16 @@ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) val result = process_result.output(process_output) - if (errors.isEmpty) result - else { - result.error_rc.output( - errors.flatMap(s => split_lines(Output.error_message_text(s))) ::: - errors.map(Protocol.Error_Message_Marker.apply)) + + errors match { + case Exn.Res(Nil) => result + case Exn.Res(errs) => + result.error_rc.output( + errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: + errs.map(Protocol.Error_Message_Marker.apply)) + case Exn.Exn(Exn.Interrupt()) => + if (result.ok) result.copy(rc = Exn.Interrupt.return_code) else result + case Exn.Exn(exn) => throw exn } } else { @@ -358,28 +366,30 @@ use_prelude = use_prelude, eval_main = eval_main, cwd = info.dir.file, env = env, cleanup = () => args_file.delete) - process.result( - progress_stdout = - { - case Protocol.Loading_Theory_Marker(theory) => - progress.theory(Progress.Theory(theory, session = session_name)) - case Protocol.Export.Marker((args, path)) => - val body = - try { Bytes.read(path) } - catch { - case ERROR(msg) => - error("Failed to read export " + quote(args.compound_name) + "\n" + msg) - } - path.file.delete - export_consumer(session_name, args, body) - case _ => - }, - progress_limit = - options.int("process_output_limit") match { - case 0 => None - case m => Some(m * 1000000L) - }, - strict = false) + Isabelle_Thread.interrupt_handler(_ => process.terminate) { + process.result( + progress_stdout = + { + case Protocol.Loading_Theory_Marker(theory) => + progress.theory(Progress.Theory(theory, session = session_name)) + case Protocol.Export.Marker((args, path)) => + val body = + try { Bytes.read(path) } + catch { + case ERROR(msg) => + error("Failed to read export " + quote(args.compound_name) + "\n" + msg) + } + path.file.delete + export_consumer(session_name, args, body) + case _ => + }, + progress_limit = + options.int("process_output_limit") match { + case 0 => None + case m => Some(m * 1000000L) + }, + strict = false) + } } } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/Tools/debugger.scala --- a/src/Pure/Tools/debugger.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/Tools/debugger.scala Mon Apr 06 22:29:40 2020 +0200 @@ -155,7 +155,7 @@ private val state = Synchronized(Debugger.State()) private val delay_update = - Isabelle_Thread.delay_first(session.output_delay) { + Delay.first(session.output_delay) { session.debugger_updates.post(Debugger.Update) } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/Tools/server.scala Mon Apr 06 22:29:40 2020 +0200 @@ -173,12 +173,11 @@ private val out = new BufferedOutputStream(socket.getOutputStream) private val out_lock: AnyRef = new Object - def tty_loop(interrupt: Option[() => Unit] = None): TTY_Loop = + def tty_loop(): TTY_Loop = new TTY_Loop( new OutputStreamWriter(out), new InputStreamReader(in), - writer_lock = out_lock, - interrupt = interrupt) + writer_lock = out_lock) def read_password(password: String): Boolean = try { Byte_Message.read_line(in).map(_.text) == Some(password) } @@ -491,7 +490,7 @@ if (operation_list) { for { - server_info <- using(SQLite.open_database(Data.database))(list(_)) + server_info <- using(SQLite.open_database(Data.database))(list) if server_info.active } Output.writeln(server_info.toString, stdout = true) } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Pure/build-jars --- a/src/Pure/build-jars Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Pure/build-jars Mon Apr 06 22:29:40 2020 +0200 @@ -28,6 +28,7 @@ src/Pure/Admin/other_isabelle.scala src/Pure/Concurrent/consumer_thread.scala src/Pure/Concurrent/counter.scala + src/Pure/Concurrent/delay.scala src/Pure/Concurrent/event_timer.scala src/Pure/Concurrent/future.scala src/Pure/Concurrent/isabelle_thread.scala diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/Graphview/tree_panel.scala Mon Apr 06 22:29:40 2020 +0200 @@ -112,7 +112,7 @@ private val selection_field_foreground = selection_field.foreground private val selection_delay = - GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) { + Delay.last(graphview.options.seconds("editor_input_delay"), gui = true) { val (pattern, ok) = selection_field.text match { case null | "" => (None, true) diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/VSCode/src/server.scala Mon Apr 06 22:29:40 2020 +0200 @@ -127,12 +127,12 @@ /* input from client or file-system */ - private val delay_input: Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger) + private val delay_input: Delay = + Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { resources.flush_input(session, channel) } - private val delay_load: Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) { + private val delay_load: Delay = + Delay.last(options.seconds("vscode_load_delay"), channel.Error_Logger) { val (invoke_input, invoke_load) = resources.resolve_dependencies(session, editor, file_watcher) if (invoke_input) delay_input.invoke() @@ -183,8 +183,8 @@ /* caret handling */ - private val delay_caret_update: Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger) + private val delay_caret_update: Delay = + Delay.last(options.seconds("vscode_input_delay"), channel.Error_Logger) { session.caret_focus.post(Session.Caret_Focus) } private def update_caret(caret: Option[(JFile, Line.Position)]) @@ -199,8 +199,8 @@ private lazy val preview_panel = new Preview_Panel(resources) - private lazy val delay_preview: Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger) + private lazy val delay_preview: Delay = + Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (preview_panel.flush(channel)) delay_preview.invoke() } @@ -214,8 +214,8 @@ /* output to client */ - private val delay_output: Isabelle_Thread.Delay = - Isabelle_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger) + private val delay_output: Delay = + Delay.last(options.seconds("vscode_output_delay"), channel.Error_Logger) { if (resources.flush_output(channel)) delay_output.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/completion_popup.scala Mon Apr 06 22:29:40 2020 +0200 @@ -373,7 +373,7 @@ } private val input_delay = - GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } @@ -530,7 +530,7 @@ } private val process_delay = - GUI_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { + Delay.last(PIDE.options.seconds("jedit_completion_delay"), gui = true) { action() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -362,7 +362,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Mon Apr 06 22:29:40 2020 +0200 @@ -184,7 +184,7 @@ /* caret handling */ private val delay_caret_update = - GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { session.caret_focus.post(Session.Caret_Focus) JEdit_Lib.invalidate(text_area) } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/font_info.scala --- a/src/Tools/jEdit/src/font_info.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/font_info.scala Mon Apr 06 22:29:40 2020 +0200 @@ -56,7 +56,7 @@ // owned by GUI thread private var steps = 0 - private val delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) + private val delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { change_size(size => { diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/info_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -80,7 +80,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Mon Apr 06 22:29:40 2020 +0200 @@ -32,10 +32,10 @@ def purge() { flush_edits(purge = true) } private val delay1_flush = - GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } + Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() } private val delay2_flush = - GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() } + Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() } def invoke(): Unit = delay1_flush.invoke() def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -59,10 +59,10 @@ } private val input_delay = - GUI_Thread.delay_first(PIDE.options.seconds("editor_input_delay")) { update_chart } + Delay.first(PIDE.options.seconds("editor_input_delay"), gui = true) { update_chart } private val update_delay = - GUI_Thread.delay_first(PIDE.options.seconds("editor_chart_delay")) { update_chart } + Delay.first(PIDE.options.seconds("editor_chart_delay"), gui = true) { update_chart } /* controls */ diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/output_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -151,7 +151,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Mon Apr 06 22:29:40 2020 +0200 @@ -107,7 +107,7 @@ /* theory files */ lazy val delay_init = - GUI_Thread.delay_last(options.seconds("editor_load_delay")) + Delay.last(options.seconds("editor_load_delay"), gui = true) { init_models() } @@ -178,7 +178,7 @@ } private lazy val delay_load = - GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() } + Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() } private def file_watcher_action(changed: Set[JFile]): Unit = if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated() diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Mon Apr 06 22:29:40 2020 +0200 @@ -191,7 +191,7 @@ Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") { private val input_delay = - GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { search_action(this) } getDocument.addDocumentListener(new DocumentListener { diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/pretty_tooltip.scala --- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala Mon Apr 06 22:29:40 2020 +0200 @@ -77,7 +77,7 @@ private var active = true private val pending_delay = - GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { + Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { pending match { case Some(body) => pending = None; body() case None => @@ -99,7 +99,7 @@ } private lazy val reactivate_delay = - GUI_Thread.delay_last(PIDE.options.seconds("jedit_tooltip_delay")) { + Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) { active = true } @@ -113,7 +113,7 @@ /* dismiss */ - private lazy val focus_delay = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) + private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { dismiss_unfocused() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/query_dockable.scala --- a/src/Tools/jEdit/src/query_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/query_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -320,7 +320,7 @@ } private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/scala_console.scala Mon Apr 06 22:29:40 2020 +0200 @@ -152,7 +152,7 @@ } finally { running.change(_ => None) - Thread.interrupted + Exn.Interrupt.dispose() } GUI_Thread.later { if (err != null) err.commandDone() diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/session_build.scala --- a/src/Tools/jEdit/src/session_build.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/session_build.scala Mon Apr 06 22:29:40 2020 +0200 @@ -102,7 +102,7 @@ } private val delay_exit = - GUI_Thread.delay_first(Time.seconds(1.0)) + Delay.first(Time.seconds(1.0), gui = true) { if (can_auto_close) conclude() else { diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -144,7 +144,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/simplifier_trace_window.scala --- a/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Apr 06 22:29:40 2020 +0200 @@ -182,7 +182,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } peer.addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -58,7 +58,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -40,7 +40,7 @@ /* resize */ private val delay_resize = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent) { delay_resize.invoke() } diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -28,7 +28,7 @@ private val abbrevs_panel = new Abbrevs_Panel private val abbrevs_refresh_delay = - GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh } + Delay.last(PIDE.options.seconds("editor_update_delay"), gui = true) { abbrevs_panel.refresh } private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button { @@ -129,7 +129,7 @@ val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym)) val search_delay = - GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { + Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { val search_words = Word.explode(Word.lowercase(search_field.text)) val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0 val results = diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/syslog_dockable.scala --- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 06 22:29:40 2020 +0200 @@ -21,7 +21,7 @@ private val syslog = new TextArea() - private def syslog_delay = GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) + private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { val text = PIDE.session.syslog_content() if (text != syslog.text) syslog.text = text diff -r 8e5c20e4e11a -r 23abd7f9f054 src/Tools/jEdit/src/text_overview.scala --- a/src/Tools/jEdit/src/text_overview.scala Mon Apr 06 19:46:38 2020 +0100 +++ b/src/Tools/jEdit/src/text_overview.scala Mon Apr 06 22:29:40 2020 +0200 @@ -75,7 +75,7 @@ private var current_overview = Overview() private val delay_repaint = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { repaint() } + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { repaint() } override def paintComponent(gfx: Graphics) { @@ -116,7 +116,7 @@ def revoke(): Unit = { delay_refresh.revoke(); future_refresh.change(x => { x.cancel; x }) } private val delay_refresh = - GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { + Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { if (!doc_view.rich_text_area.check_robust_body) invoke() else { JEdit_Lib.buffer_lock(buffer) {