Email Gateway (Jan 11 2026 at 22:23): Email Gateway (Jan 11 2026 at 22:23):From: Makarius <makarius@sketis.net>
* Isabelle/jEdit Prover IDE *
Console/Scala: proper treatment of interrupts via "Stop" button. It
was broken since Isabelle2022: Scala interpreter thread became
inoperative afterwards.
Console/Scala: more robust Scala_Console.Progress with local output
and interrupt handling (using thread interrupt, e.g. via "Stop" button).
For example:
val progress = new Scala_Console.Progress(verbose = true)
Build.build_logic(PIDE.options, "FOL", progress = progress)
* System *
Isabelle/Scala operations Build.build(), Build.build_logic() etc.
already include progress.interrupt_handler for the main loop. It is no
longer required as a separate wrapper for command-line tools etc.
Isabelle/Scala operation Progress.interrupt_handler is now more
specific for different instances of class Progress, with mixins
Progress.Local_Interrupts (for thread interrupts) and
Progress.Global_Interrupts (for thread interrupts and process signals).
The latter is included in class Console_Progress, which is typically
used for a single command-line tool that is directly connected to the
system shell and its signals (e.g. CTRL-C). The default (new Progress)
does not change interrupt handling at all. Subtle INCOMPATIBILITY in
very rare situations.
This refers to Isabelle/174c4514438c.
It is the result of several rounds of refinements in this area. Many years
ago, class Progress was rather primitive:
https://isabelle.in.tum.de/repos/isabelle/file/8a4bd05c1735/src/Pure/System/progress.scala
Now it serves as an umbrella for many variants on message output and interrupt
handling. That required some reworking, which is hopefully sufficient for now,
although I can anticipate further refinements in the future.
Makarius
Last updated: Jan 14 2026 at 04:49 UTC