NEWS: Build progress and interrupts in Isabelle/Scala

Makarius makarius at sketis.net
Sun Jan 11 23:22:22 CET 2026


*** 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



More information about the isabelle-dev mailing list