allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
authorwenzelm
Tue Mar 13 21:04:42 2018 +0100 (14 months ago)
changeset 67852f701a1d5d852
parent 67851 5e6452a6ec89
child 67853 74e2a4b62826
allow cancellation of Sessions.deps/base_info via progress.stopped (progress.echo only happens for options like "verbose");
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/build.scala
src/Pure/Tools/server_commands.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Mar 13 20:04:58 2018 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Mar 13 21:04:42 2018 +0100
     1.3 @@ -369,6 +369,7 @@
     1.4  
     1.5    def base_info(options: Options,
     1.6      session: String,
     1.7 +    progress: Progress = No_Progress,
     1.8      dirs: List[Path] = Nil,
     1.9      ancestor_session: Option[String] = None,
    1.10      all_known: Boolean = false,
    1.11 @@ -385,7 +386,7 @@
    1.12  
    1.13      val (session1, infos1) =
    1.14        if (required_session && ancestor.isDefined) {
    1.15 -        val deps = Sessions.deps(selected_sessions, global_theories)
    1.16 +        val deps = Sessions.deps(selected_sessions, global_theories, progress = progress)
    1.17          val base = deps(session)
    1.18  
    1.19          val ancestor_loaded =
    1.20 @@ -439,7 +440,7 @@
    1.21        full_sessions1.selection(Selection(sessions = select_sessions1))
    1.22  
    1.23      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    1.24 -    val deps1 = Sessions.deps(sessions1, global_theories)
    1.25 +    val deps1 = Sessions.deps(sessions1, global_theories, progress = progress)
    1.26      val base1 = if (all_known) deps1(session1).copy(known = deps1.all_known) else deps1(session1)
    1.27  
    1.28      Base_Info(session1, sessions1, deps1.errors, base1, infos1)
     2.1 --- a/src/Pure/Thy/thy_resources.scala	Tue Mar 13 20:04:58 2018 +0100
     2.2 +++ b/src/Pure/Thy/thy_resources.scala	Tue Mar 13 21:04:42 2018 +0100
     2.3 @@ -13,6 +13,7 @@
     2.4  
     2.5    def start_session(
     2.6      options: Options,
     2.7 +    progress: Progress = No_Progress,
     2.8      session_name: String,
     2.9      session_dirs: List[Path] = Nil,
    2.10      session_base: Option[Sessions.Base] = None,
    2.11 @@ -21,7 +22,7 @@
    2.12    {
    2.13      val base =
    2.14        session_base getOrElse
    2.15 -        Sessions.base_info(options, session_name, dirs = session_dirs).check_base
    2.16 +      Sessions.base_info(options, session_name, progress = progress, dirs = session_dirs).check_base
    2.17      val resources = new Thy_Resources(base, log = log)
    2.18      val session = new Session(options, resources)
    2.19  
     3.1 --- a/src/Pure/Tools/build.scala	Tue Mar 13 20:04:58 2018 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 13 21:04:42 2018 +0100
     3.3 @@ -415,8 +415,8 @@
     3.4          val selected_sessions =
     3.5            full_sessions.selection(Sessions.Selection(sessions = outdated))
     3.6          val deps =
     3.7 -          Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
     3.8 -            .check_errors
     3.9 +          Sessions.deps(selected_sessions, full_sessions.global_theories,
    3.10 +            progress = progress, inlined_files = true).check_errors
    3.11          (selected_sessions, deps)
    3.12        }
    3.13        else (selected_sessions0, deps0)
     4.1 --- a/src/Pure/Tools/server_commands.scala	Tue Mar 13 20:04:58 2018 +0100
     4.2 +++ b/src/Pure/Tools/server_commands.scala	Tue Mar 13 21:04:42 2018 +0100
     4.3 @@ -48,6 +48,7 @@
     4.4        val base_info =
     4.5          Sessions.base_info(options,
     4.6            args.session,
     4.7 +          progress = progress,
     4.8            dirs = dirs,
     4.9            ancestor_session = proper_string(args.ancestor_session),
    4.10            all_known = args.all_known,