clarified errors: no result from forced session.stop, check pending theories;
authorwenzelm
Sat Sep 22 13:22:43 2018 +0200 (11 months ago ago)
changeset 6903290bb4cabe1e8
parent 69031 30e88eabf167
child 69033 c5db368833b1
clarified errors: no result from forced session.stop, check pending theories;
src/Pure/PIDE/headless.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/PIDE/headless.scala	Fri Sep 21 23:14:52 2018 +0100
     1.2 +++ b/src/Pure/PIDE/headless.scala	Sat Sep 22 13:22:43 2018 +0200
     1.3 @@ -71,6 +71,12 @@
     1.4      val nodes: List[(Document.Node.Name, Document_Status.Node_Status)],
     1.5      val nodes_committed: List[(Document.Node.Name, Document_Status.Node_Status)])
     1.6    {
     1.7 +    def nodes_pending: List[(Document.Node.Name, Document_Status.Node_Status)] =
     1.8 +    {
     1.9 +      val committed = nodes_committed.iterator.map(_._1).toSet
    1.10 +      nodes.filter(p => !committed(p._1))
    1.11 +    }
    1.12 +
    1.13      def snapshot(name: Document.Node.Name): Document.Snapshot =
    1.14        stable_snapshot(state, version, name)
    1.15  
     2.1 --- a/src/Pure/Tools/dump.scala	Fri Sep 21 23:14:52 2018 +0100
     2.2 +++ b/src/Pure/Tools/dump.scala	Sat Sep 22 13:22:43 2018 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4      commit_cleanup_delay: Time = Headless.default_commit_cleanup_delay,
     2.5      watchdog_timeout: Time = Headless.default_watchdog_timeout,
     2.6      system_mode: Boolean = false,
     2.7 -    selection: Sessions.Selection = Sessions.Selection.empty): Process_Result =
     2.8 +    selection: Sessions.Selection = Sessions.Selection.empty): Boolean =
     2.9    {
    2.10      if (Build.build_logic(options, logic, build_heap = true, progress = progress,
    2.11        dirs = dirs ::: select_dirs, system_mode = system_mode) != 0) error(logic + " FAILED")
    2.12 @@ -167,12 +167,16 @@
    2.13          commit_cleanup_delay = commit_cleanup_delay,
    2.14          watchdog_timeout = watchdog_timeout)
    2.15  
    2.16 -    val session_result = session.stop()
    2.17 +    session.stop()
    2.18  
    2.19      val consumer_ok = Consumer.shutdown()
    2.20  
    2.21 -    if (use_theories_result.ok && consumer_ok) session_result
    2.22 -    else session_result.error_rc
    2.23 +    use_theories_result.nodes_pending match {
    2.24 +      case Nil =>
    2.25 +      case pending => error("Pending theories " + commas_quote(pending.map(p => p._1.toString)))
    2.26 +    }
    2.27 +
    2.28 +    use_theories_result.ok && consumer_ok
    2.29    }
    2.30  
    2.31  
    2.32 @@ -245,7 +249,7 @@
    2.33  
    2.34        val progress = new Console_Progress(verbose = verbose)
    2.35  
    2.36 -      val result =
    2.37 +      val ok =
    2.38          progress.interrupt_handler {
    2.39            dump(options, logic,
    2.40              aspects = aspects,
    2.41 @@ -266,8 +270,6 @@
    2.42                sessions = sessions))
    2.43          }
    2.44  
    2.45 -      progress.echo(result.timing.message_resources)
    2.46 -
    2.47 -      sys.exit(result.rc)
    2.48 +      if (!ok) sys.exit(1)
    2.49      })
    2.50  }