--- a/NEWS Mon Apr 06 22:46:55 2020 +0100
+++ b/NEWS Tue Apr 07 09:35:59 2020 +0100
@@ -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)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/delay.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 =>
+ }
+ }
+}
--- a/src/Pure/Concurrent/isabelle_thread.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/Concurrent/isabelle_thread.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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
+ }
}
- }
}
--- a/src/Pure/GUI/gui_thread.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/GUI/gui_thread.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 } }
}
--- a/src/Pure/General/exn.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/General/exn.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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
}
--- a/src/Pure/General/file_watcher.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/General/file_watcher.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
--- a/src/Pure/ML/ml_console.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/ML/ml_console.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
}
}
}
--- a/src/Pure/PIDE/headless.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/PIDE/headless.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 ...")
--- a/src/Pure/PIDE/session.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/PIDE/session.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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] =
{
--- a/src/Pure/System/bash.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/System/bash.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 => }
--- a/src/Pure/System/isabelle_process.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/System/isabelle_process.scala Tue Apr 07 09:35:59 2020 +0100
@@ -76,4 +76,6 @@
session.stop()
result
}
+
+ def terminate { process.terminate }
}
--- a/src/Pure/System/isabelle_system.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Apr 07 09:35:59 2020 +0100
@@ -287,7 +287,7 @@
proc.getInputStream.close
proc.getErrorStream.close
proc.destroy
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
(output, rc)
}
--- a/src/Pure/System/tty_loop.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/System/tty_loop.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 }
--- a/src/Pure/Tools/build.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/Tools/build.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
+ }
}
}
--- a/src/Pure/Tools/debugger.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/Tools/debugger.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
}
--- a/src/Pure/Tools/server.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/Tools/server.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
}
--- a/src/Pure/build-jars Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Pure/build-jars Tue Apr 07 09:35:59 2020 +0100
@@ -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
--- a/src/Tools/Graphview/tree_panel.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
--- a/src/Tools/VSCode/src/server.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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()
}
--- a/src/Tools/jEdit/src/completion_popup.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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()
}
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/document_view.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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)
}
--- a/src/Tools/jEdit/src/font_info.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/font_info.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 =>
{
--- a/src/Tools/jEdit/src/info_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/jedit_editor.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/monitor_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/monitor_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 */
--- a/src/Tools/jEdit/src/output_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/plugin.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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()
--- a/src/Tools/jEdit/src/pretty_text_area.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 {
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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()
}
--- a/src/Tools/jEdit/src/query_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/scala_console.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Tue Apr 07 09:35:59 2020 +0100
@@ -152,7 +152,7 @@
}
finally {
running.change(_ => None)
- Thread.interrupted
+ Exn.Interrupt.dispose()
}
GUI_Thread.later {
if (err != null) err.commandDone()
--- a/src/Tools/jEdit/src/session_build.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/session_build.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 {
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/state_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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() }
--- a/src/Tools/jEdit/src/symbols_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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 =
--- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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
--- a/src/Tools/jEdit/src/text_overview.scala Mon Apr 06 22:46:55 2020 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Tue Apr 07 09:35:59 2020 +0100
@@ -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) {