--- 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 =
--- 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)))
--- 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 = "",
--- 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")
--- 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)
--- 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,
--- 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)
{
--- 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)
--- 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")
--- 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")
--- 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)
}
--- 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 */
--- 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)
--- 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))
--- 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 =
--- 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
--- 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)
--- 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 =
--- 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 =
--- 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,
--- 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,
--- 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)
--- 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()
--- 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
}
--- 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,
--- 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,
--- 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)
--- 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,
--- 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 ..."))
}