# HG changeset patch
# User wenzelm
# Date 1586288976 -7200
# Node ID a5fda30edae2b7d9e91d18ac4e0200e96b0c4d33
# Parent  c255ed5820959c0de5cf382f8a4279428b38f40c
clarified signature: more uniform treatment of stopped/interrupted state;

diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_doc.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -16,7 +16,7 @@
 
   def build_doc(
     options: Options,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     all_docs: Boolean = false,
     max_jobs: Int = 1,
     docs: List[String] = Nil): Int =
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_fonts.scala
--- a/src/Pure/Admin/build_fonts.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_fonts.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -216,7 +216,7 @@
     target_prefix: String = "Isabelle",
     target_version: String = "",
     target_dir: Path = default_target_dir,
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     progress.echo("Directory " + target_dir)
     hinting.foreach(hinted => Isabelle_System.mkdirs(target_dir + hinted_path(hinted)))
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_history.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -106,7 +106,7 @@
     options: Options,
     root: Path,
     user_home: Path = default_user_home,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     rev: String = default_rev,
     afp_rev: Option[String] = None,
     afp_partition: Int = 0,
@@ -519,7 +519,7 @@
     afp_repos_source: String = AFP.repos_source,
     isabelle_identifier: String = "remote_build_history",
     self_update: Boolean = false,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     rev: String = "",
     afp_rev: Option[String] = None,
     options: String = "",
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_jdk.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -133,7 +133,7 @@
 
   def build_jdk(
     archives: List[Path],
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     target_dir: Path = Path.current)
   {
     if (Platform.is_windows) error("Cannot build jdk on Windows")
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_polyml.scala
--- a/src/Pure/Admin/build_polyml.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_polyml.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -49,7 +49,7 @@
   def build_polyml(
     root: Path,
     sha1_root: Option[Path] = None,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     arch_64: Boolean = false,
     options: List[String] = Nil,
     msys_root: Option[Path] = None)
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -265,7 +265,7 @@
   def build_release(base_dir: Path,
     options: Options,
     components_base: Path = Components.default_components_base,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     rev: String = "",
     afp_rev: String = "",
     official_release: Boolean = false,
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -49,7 +49,7 @@
   /* build status */
 
   def build_status(options: Options,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     verbose: Boolean = false,
@@ -200,7 +200,7 @@
   }
 
   def read_data(options: Options,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     profiles: List[Profile] = default_profiles,
     only_sessions: Set[String] = Set.empty,
     ml_statistics: Boolean = false,
@@ -362,7 +362,7 @@
   /* present data */
 
   def present_data(data: Data,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     target_dir: Path = default_target_dir,
     image_size: (Int, Int) = default_image_size)
   {
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/components.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -45,7 +45,7 @@
   def contrib(dir: Path = Path.current, name: String = ""): Path =
     dir + Path.explode("contrib") + Path.explode(name)
 
-  def unpack(dir: Path, archive: Path, progress: Progress = No_Progress): String =
+  def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String =
   {
     val name = Archive.get_name(archive.file_name)
     progress.echo("Unpacking " + name)
@@ -56,7 +56,7 @@
   def resolve(base_dir: Path, names: List[String],
     target_dir: Option[Path] = None,
     copy_dir: Option[Path] = None,
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     Isabelle_System.mkdirs(base_dir)
     for (name <- names) {
@@ -135,7 +135,7 @@
   def build_components(
     options: Options,
     components: List[Path],
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     publish: Boolean = false,
     force: Boolean = false,
     update_components_sha1: Boolean = false)
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -394,7 +394,7 @@
 
   object Log_Service
   {
-    def apply(options: Options, progress: Progress = No_Progress): Log_Service =
+    def apply(options: Options, progress: Progress = new Progress): Log_Service =
       new Log_Service(SSH.init_context(options), progress)
   }
 
@@ -599,7 +599,7 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      val progress = if (verbose) new Console_Progress() else No_Progress
+      val progress = if (verbose) new Console_Progress() else new Progress
 
       if (force) cronjob(progress, exclude_task)
       else error("Need to apply force to do anything")
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/jenkins.scala
--- a/src/Pure/Admin/jenkins.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/jenkins.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -40,7 +40,7 @@
 
 
   def download_logs(
-    options: Options, job_names: List[String], dir: Path, progress: Progress = No_Progress)
+    options: Options, job_names: List[String], dir: Path, progress: Progress = new Progress)
   {
     val store = Sessions.store(options)
     val infos = job_names.flatMap(build_job_infos)
@@ -96,7 +96,7 @@
       }
     }
 
-    def download_log(store: Sessions.Store, dir: Path, progress: Progress = No_Progress)
+    def download_log(store: Sessions.Store, dir: Path, progress: Progress = new Progress)
     {
       val log_dir = dir + Build_Log.log_subdir(date)
       val log_path = log_dir + log_filename.ext("xz")
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Admin/other_isabelle.scala
--- a/src/Pure/Admin/other_isabelle.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Admin/other_isabelle.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -12,7 +12,7 @@
   def apply(isabelle_home: Path,
       isabelle_identifier: String = "",
       user_home: Path = Path.explode("$USER_HOME"),
-      progress: Progress = No_Progress): Other_Isabelle =
+      progress: Progress = new Progress): Other_Isabelle =
     new Other_Isabelle(isabelle_home.canonical, isabelle_identifier, user_home, progress)
 }
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -230,7 +230,7 @@
     remote_name: String = "",
     path_name: String = default_path_name,
     remote_exists: Boolean = false,
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     /* local repository */
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/PIDE/headless.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -244,7 +244,7 @@
       // commit: must not block, must not fail
       commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
       commit_cleanup_delay: Time = default_commit_cleanup_delay,
-      progress: Progress = No_Progress): Use_Theories_Result =
+      progress: Progress = new Progress): Use_Theories_Result =
     {
       val dependencies =
       {
@@ -404,7 +404,7 @@
       session_name: String,
       session_dirs: List[Path] = Nil,
       include_sessions: List[String] = Nil,
-      progress: Progress = No_Progress,
+      progress: Progress = new Progress,
       log: Logger = No_Logger): Resources =
     {
       val base_info =
@@ -567,7 +567,7 @@
 
     /* session */
 
-    def start_session(print_mode: List[String] = Nil, progress: Progress = No_Progress): Session =
+    def start_session(print_mode: List[String] = Nil, progress: Progress = new Progress): Session =
     {
       val session = new Session(session_base_info.session, options, resources)
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -265,10 +265,10 @@
 
   def dependencies(
       thys: List[(Document.Node.Name, Position.T)],
-      progress: Progress = No_Progress): Dependencies[Unit] =
+      progress: Progress = new Progress): Dependencies[Unit] =
     Dependencies.empty[Unit].require_thys((), thys, progress = progress)
 
-  def session_dependencies(info: Sessions.Info, progress: Progress = No_Progress)
+  def session_dependencies(info: Sessions.Info, progress: Progress = new Progress)
     : Dependencies[Options] =
   {
     (Dependencies.empty[Options] /: info.theories)({ case (dependencies, (options, thys)) =>
@@ -303,7 +303,7 @@
     def require_thy(adjunct: A,
       thy: (Document.Node.Name, Position.T),
       initiators: List[Document.Node.Name] = Nil,
-      progress: Progress = No_Progress): Dependencies[A] =
+      progress: Progress = new Progress): Dependencies[A] =
     {
       val (name, pos) = thy
 
@@ -337,7 +337,7 @@
 
     def require_thys(adjunct: A,
         thys: List[(Document.Node.Name, Position.T)],
-        progress: Progress = No_Progress,
+        progress: Progress = new Progress,
         initiators: List[Document.Node.Name] = Nil): Dependencies[A] =
       (this /: thys)(_.require_thy(adjunct, _, progress = progress, initiators = initiators))
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/System/linux.scala
--- a/src/Pure/System/linux.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/System/linux.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -62,12 +62,12 @@
   def check_reboot_required(): Unit =
     if (reboot_required()) error("Reboot required")
 
-  def package_update(progress: Progress = No_Progress): Unit =
+  def package_update(progress: Progress = new Progress): Unit =
     progress.bash(
       """apt-get update -y && apt-get upgrade -y && apt autoremove -y""",
       echo = true).check
 
-  def package_install(packages: List[String], progress: Progress = No_Progress): Unit =
+  def package_install(packages: List[String], progress: Progress = new Progress): Unit =
     progress.bash("apt-get install -y -- " + Bash.strings(packages), echo = true).check
 
   def package_installed(name: String): Boolean =
diff -r c255ed582095 -r a5fda30edae2 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/System/progress.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -36,8 +36,15 @@
   def timeit[A](message: String = "", enabled: Boolean = true)(e: => A): A =
     Timing.timeit(message, enabled, echo)(e)
 
-  def stopped: Boolean = false
-  def interrupt_handler[A](e: => A): A = e
+  @volatile protected var is_stopped = false
+  def stop { is_stopped = true }
+  def stopped: Boolean =
+  {
+    if (Thread.interrupted) is_stopped = true
+    is_stopped
+  }
+
+  def interrupt_handler[A](e: => A): A = POSIX_Interrupt.handler { stop } { e }
   def expose_interrupt() { if (stopped) throw Exn.Interrupt() }
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
 
@@ -55,8 +62,6 @@
   }
 }
 
-object No_Progress extends Progress
-
 class Console_Progress(verbose: Boolean = false, stderr: Boolean = false) extends Progress
 {
   override def echo(msg: String): Unit =
@@ -64,15 +69,6 @@
 
   override def theory(theory: Progress.Theory): Unit =
     if (verbose) echo(theory.message)
-
-  @volatile private var is_stopped = false
-  override def interrupt_handler[A](e: => A): A =
-    POSIX_Interrupt.handler { is_stopped = true } { e }
-  override def stopped: Boolean =
-  {
-    if (Thread.interrupted) is_stopped = true
-    is_stopped
-  }
 }
 
 class File_Progress(path: Path, verbose: Boolean = false) extends Progress
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Thy/export.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -299,7 +299,7 @@
     store: Sessions.Store,
     session_name: String,
     export_dir: Path,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     export_prune: Int = 0,
     export_list: Boolean = false,
     export_patterns: List[String] = Nil)
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Thy/export_theory.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -30,7 +30,7 @@
     store: Sessions.Store,
     sessions_structure: Sessions.Structure,
     session_name: String,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     cache: Term.Cache = Term.make_cache()): Session =
   {
     val thys =
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -116,7 +116,7 @@
   }
 
   def deps(sessions_structure: Structure,
-      progress: Progress = No_Progress,
+      progress: Progress = new Progress,
       inlined_files: Boolean = false,
       verbose: Boolean = false,
       list_files: Boolean = false,
@@ -345,7 +345,7 @@
 
   def base_info(options: Options,
     session: String,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     dirs: List[Path] = Nil,
     include_sessions: List[String] = Nil,
     session_ancestor: Option[String] = None,
@@ -708,7 +708,7 @@
     def selection_deps(
       options: Options,
       selection: Selection,
-      progress: Progress = No_Progress,
+      progress: Progress = new Progress,
       loading_sessions: Boolean = false,
       inlined_files: Boolean = false,
       verbose: Boolean = false): Deps =
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -461,7 +461,7 @@
 
   def build(
     options: Options,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     check_unknown_files: Boolean = false,
     build_heap: Boolean = false,
     clean_build: Boolean = false,
@@ -611,8 +611,9 @@
 
       if (pending.is_empty) results
       else {
-        if (progress.stopped)
+        if (progress.stopped) {
           for ((_, (_, job)) <- running) job.terminate
+        }
 
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((session_name, (input_heaps, job))) =>
@@ -763,7 +764,7 @@
           progress.echo("Exporting " + info.name + " ...")
           for ((dir, prune, pats) <- info.export_files) {
             Export.export_files(store, name, info.dir + dir,
-              progress = if (verbose) progress else No_Progress,
+              progress = if (verbose) progress else new Progress,
               export_prune = prune,
               export_patterns = pats)
           }
@@ -937,7 +938,7 @@
   /* build logic image */
 
   def build_logic(options: Options, logic: String,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     build_heap: Boolean = false,
     dirs: List[Path] = Nil,
     fresh: Boolean = false,
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/dump.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -94,7 +94,7 @@
     def apply(
       options: Options,
       aspects: List[Aspect] = Nil,
-      progress: Progress = No_Progress,
+      progress: Progress = new Progress,
       dirs: List[Path] = Nil,
       select_dirs: List[Path] = Nil,
       selection: Sessions.Selection = Sessions.Selection.empty,
@@ -395,7 +395,7 @@
     options: Options,
     logic: String,
     aspects: List[Aspect] = Nil,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/mkroot.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -25,7 +25,7 @@
     init_repos: Boolean = false,
     title: String = "",
     author: String = "",
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     Isabelle_System.mkdirs(session_dir)
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/phabricator.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -193,7 +193,7 @@
     command
   }
 
-  def mercurial_setup(mercurial_source: String, progress: Progress = No_Progress)
+  def mercurial_setup(mercurial_source: String, progress: Progress = new Progress)
   {
     progress.echo("\nMercurial installation from source " + quote(mercurial_source) + " ...")
     Isabelle_System.with_tmp_dir("mercurial")(tmp_dir =>
@@ -226,7 +226,7 @@
     repo: String = "",
     package_update: Boolean = false,
     mercurial_source: String = "",
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     /* system environment */
 
@@ -599,7 +599,7 @@
     name: String = default_name,
     config_file: Option[Path] = None,
     test_user: String = "",
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     Linux.check_system_root()
 
@@ -717,7 +717,7 @@
   def phabricator_setup_ssh(
     server_port: Int = default_server_port,
     system_port: Int = default_system_port,
-    progress: Progress = No_Progress)
+    progress: Progress = new Progress)
   {
     Linux.check_system_root()
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/server.scala
--- a/src/Pure/Tools/server.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/server.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -274,10 +274,6 @@
       context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
     }
 
-    @volatile private var is_stopped = false
-    override def stopped: Boolean = is_stopped
-    def stop { is_stopped = true }
-
     override def toString: String = context.toString
   }
 
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/server_commands.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -45,7 +45,7 @@
           include_sessions = include_sessions, verbose = verbose)
       }
 
-    def command(args: Args, progress: Progress = No_Progress)
+    def command(args: Args, progress: Progress = new Progress)
       : (JSON.Object.T, Build.Results, Options, Sessions.Base_Info) =
     {
       val options = Options.init(prefs = args.preferences, opts = args.options)
@@ -103,7 +103,7 @@
       }
       yield Args(build = build, print_mode = print_mode)
 
-    def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
+    def command(args: Args, progress: Progress = new Progress, log: Logger = No_Logger)
       : (JSON.Object.T, (UUID.T, Headless.Session)) =
     {
       val (_, _, options, base_info) =
@@ -179,7 +179,7 @@
     def command(args: Args,
       session: Headless.Session,
       id: UUID.T = UUID.random(),
-      progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
+      progress: Progress = new Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
     {
       val result =
         session.use_theories(args.theories, master_dir = args.master_dir,
diff -r c255ed582095 -r a5fda30edae2 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Pure/Tools/update.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -10,7 +10,7 @@
 object Update
 {
   def update(options: Options, logic: String,
-    progress: Progress = No_Progress,
+    progress: Progress = new Progress,
     log: Logger = No_Logger,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
diff -r c255ed582095 -r a5fda30edae2 src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -17,7 +17,7 @@
 
   /* grammar */
 
-  def build_grammar(options: Options, progress: Progress = No_Progress)
+  def build_grammar(options: Options, progress: Progress = new Progress)
   {
     val logic = Grammar.default_logic
     val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
@@ -30,7 +30,7 @@
 
   /* extension */
 
-  def build_extension(progress: Progress = No_Progress, publish: Boolean = false)
+  def build_extension(progress: Progress = new Progress, publish: Boolean = false)
   {
     val output_path = extension_dir + Path.explode("out")
     progress.echo(output_path.implode)
diff -r c255ed582095 -r a5fda30edae2 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -126,7 +126,7 @@
       session_requirements = logic_requirements)
 
   def session_build(
-    options: Options, progress: Progress = No_Progress, no_build: Boolean = false): Int =
+    options: Options, progress: Progress = new Progress, no_build: Boolean = false): Int =
   {
     Build.build(session_options(options), progress = progress, build_heap = true,
       no_build = no_build, dirs = session_dirs(), infos = PIDE.resources.session_base_info.infos,
diff -r c255ed582095 -r a5fda30edae2 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Tue Apr 07 21:07:28 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Tue Apr 07 21:49:36 2020 +0200
@@ -57,8 +57,6 @@
 
     /* progress */
 
-    @volatile private var is_stopped = false
-
     private val progress = new Progress {
       override def echo(txt: String): Unit =
         GUI_Thread.later {
@@ -68,8 +66,6 @@
         }
 
       override def theory(theory: Progress.Theory): Unit = echo(theory.message)
-
-      override def stopped: Boolean = is_stopped
     }
 
 
@@ -132,7 +128,7 @@
 
     private def stopping()
     {
-      is_stopped = true
+      progress.stop
       set_actions(new Label("Stopping ..."))
     }