# HG changeset patch
# User wenzelm
# Date 1520971482 -3600
# Node ID f701a1d5d8528166d4d557b00cf691b7fe8598bb
# Parent  5e6452a6ec896a36777f1bfb83e0d3855b921917
allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");

diff -r 5e6452a6ec89 -r f701a1d5d852 src/Pure/Thy/sessions.scala
--- 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)
diff -r 5e6452a6ec89 -r f701a1d5d852 src/Pure/Thy/thy_resources.scala
--- 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)
 
diff -r 5e6452a6ec89 -r f701a1d5d852 src/Pure/Tools/build.scala
--- 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)
diff -r 5e6452a6ec89 -r f701a1d5d852 src/Pure/Tools/server_commands.scala
--- 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,