allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
--- a/src/Pure/Thy/sessions.scala Tue Mar 13 20:04:58 2018 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Mar 13 21:04:42 2018 +0100
@@ -369,6 +369,7 @@
def base_info(options: Options,
session: String,
+ progress: Progress = No_Progress,
dirs: List[Path] = Nil,
ancestor_session: Option[String] = None,
all_known: Boolean = false,
@@ -385,7 +386,7 @@
val (session1, infos1) =
if (required_session && ancestor.isDefined) {
- val deps = Sessions.deps(selected_sessions, global_theories)
+ val deps = Sessions.deps(selected_sessions, global_theories, progress = progress)
val base = deps(session)
val ancestor_loaded =
@@ -439,7 +440,7 @@
full_sessions1.selection(Selection(sessions = select_sessions1))
val sessions1 = if (all_known) full_sessions1 else selected_sessions1
- val deps1 = Sessions.deps(sessions1, global_theories)
+ val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
Base_Info(session1, sessions1, deps1.errors, base1, infos1)
--- a/src/Pure/Thy/thy_resources.scala Tue Mar 13 20:04:58 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala Tue Mar 13 21:04:42 2018 +0100
@@ -13,6 +13,7 @@
def start_session(
options: Options,
+ progress: Progress = No_Progress,
session_name: String,
session_dirs: List[Path] = Nil,
session_base: Option[Sessions.Base] = None,
@@ -21,7 +22,7 @@
{
val base =
session_base getOrElse
- Sessions.base_info(options, session_name, dirs = session_dirs).check_base
+ Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base
val resources = new Thy_Resources(base, log = log)
val session = new Session(options, resources)
--- a/src/Pure/Tools/build.scala Tue Mar 13 20:04:58 2018 +0100
+++ b/src/Pure/Tools/build.scala Tue Mar 13 21:04:42 2018 +0100
@@ -415,8 +415,8 @@
val selected_sessions =
full_sessions.selection(Sessions.Selection(sessions = outdated))
val deps =
- Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
- .check_errors
+ Sessions.deps(selected_sessions, full_sessions.global_theories,
+ progress = progress, inlined_files = true).check_errors
(selected_sessions, deps)
}
else (selected_sessions0, deps0)
--- a/src/Pure/Tools/server_commands.scala Tue Mar 13 20:04:58 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Tue Mar 13 21:04:42 2018 +0100
@@ -48,6 +48,7 @@
val base_info =
Sessions.base_info(options,
args.session,
+ progress = progress,
dirs = dirs,
ancestor_session = proper_string(args.ancestor_session),
all_known = args.all_known,