# HG changeset patch # User wenzelm # Date 1535920208 -7200 # Node ID 9b97d0b20d95d42a6211196b0eef63c014f5b829 # Parent 3653b3ad729efc380c70b69e5d21b618e0ac7dd9 clarified quasi_consolidated state: ensure that exports are present for ok nodes; diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/PIDE/command.ML --- a/src/Pure/PIDE/command.ML Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/PIDE/command.ML Sun Sep 02 22:30:08 2018 +0200 @@ -269,6 +269,10 @@ | SOME st' => let val _ = status tr Markup.finished; + val _ = + if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso + can (Toplevel.end_theory Position.none) st' + then status tr Markup.finalized else (); in {failed = false, command = tr, state = st'} end) end; diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/PIDE/document_status.scala --- a/src/Pure/PIDE/document_status.scala Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/PIDE/document_status.scala Sun Sep 02 22:30:08 2018 +0200 @@ -27,6 +27,7 @@ var warned = false var failed = false var canceled = false + var finalized = false var forks = 0 var runs = 0 for (markup <- markup_iterator) { @@ -39,10 +40,11 @@ case Markup.WARNING | Markup.LEGACY => warned = true case Markup.FAILED | Markup.ERROR => failed = true case Markup.CANCELED => canceled = true + case Markup.FINALIZED => finalized = true case _ => } } - Command_Status(touched, accepted, warned, failed, canceled, forks, runs) + Command_Status(touched, accepted, warned, failed, canceled, finalized, forks, runs) } val empty = make(Iterator.empty) @@ -61,6 +63,7 @@ private val warned: Boolean, private val failed: Boolean, private val canceled: Boolean, + private val finalized: Boolean, forks: Int, runs: Int) { @@ -71,6 +74,7 @@ warned || that.warned, failed || that.failed, canceled || that.canceled, + finalized || that.finalized, forks + that.forks, runs + that.runs) @@ -80,6 +84,7 @@ def is_failed: Boolean = failed def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0 def is_canceled: Boolean = canceled + def is_finalized: Boolean = finalized def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0 } @@ -102,6 +107,7 @@ var finished = 0 var canceled = false var terminated = false + var finalized = false for (command <- node.commands.iterator) { val states = state.command_states(version, command) val status = Command_Status.merge(states.iterator.map(_.document_status)) @@ -114,18 +120,20 @@ if (status.is_canceled) canceled = true if (status.is_terminated) terminated = true + if (status.is_finalized) finalized = true } val initialized = state.node_initialized(version, name) val consolidated = state.node_consolidated(version, name) Node_Status(unprocessed, running, warned, failed, finished, canceled, terminated, - initialized, consolidated) + finalized, initialized, consolidated) } } sealed case class Node_Status( unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, - canceled: Boolean, terminated: Boolean, initialized: Boolean, consolidated: Boolean) + canceled: Boolean, terminated: Boolean, finalized: Boolean, initialized: Boolean, + consolidated: Boolean) { def ok: Boolean = failed == 0 def total: Int = unprocessed + running + warned + failed + finished @@ -133,8 +141,8 @@ def json: JSON.Object.T = JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed, "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished, - "canceled" -> canceled, "terminated" -> terminated, "initialized" -> initialized, - "consolidated" -> consolidated) + "canceled" -> canceled, "terminated" -> terminated, "finalized" -> finalized, + "initialized" -> initialized, "consolidated" -> consolidated) } @@ -192,9 +200,9 @@ def apply(name: Document.Node.Name): Node_Status = rep(name) def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name) - def is_terminated(name: Document.Node.Name): Boolean = + def quasi_consolidated(name: Document.Node.Name): Boolean = rep.get(name) match { - case Some(st) => st.terminated + case Some(st) => !st.finalized && st.terminated case None => false } diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/PIDE/markup.ML --- a/src/Pure/PIDE/markup.ML Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/PIDE/markup.ML Sun Sep 02 22:30:08 2018 +0200 @@ -167,6 +167,7 @@ val failedN: string val failed: T val canceledN: string val canceled: T val initializedN: string val initialized: T + val finalizedN: string val finalized: T val consolidatedN: string val consolidated: T val exec_idN: string val initN: string @@ -580,6 +581,7 @@ val (failedN, failed) = markup_elem "failed"; val (canceledN, canceled) = markup_elem "canceled"; val (initializedN, initialized) = markup_elem "initialized"; +val (finalizedN, finalized) = markup_elem "finalized"; val (consolidatedN, consolidated) = markup_elem "consolidated"; diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/PIDE/markup.scala Sun Sep 02 22:30:08 2018 +0200 @@ -426,6 +426,7 @@ val FAILED = "failed" val CANCELED = "canceled" val INITIALIZED = "initialized" + val FINALIZED = "finalized" val CONSOLIDATED = "consolidated" diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/Thy/thy_resources.scala --- a/src/Pure/Thy/thy_resources.scala Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/Thy/thy_resources.scala Sun Sep 02 22:30:08 2018 +0200 @@ -123,7 +123,7 @@ if (beyond_limit || dep_theories.forall(name => state.node_consolidated(version, name) || - nodes_status_update.value._1.is_terminated(name))) + nodes_status_update.value._1.quasi_consolidated(name))) { val nodes = for (name <- dep_theories) diff -r 3653b3ad729e -r 9b97d0b20d95 src/Pure/Tools/dump.scala --- a/src/Pure/Tools/dump.scala Sun Sep 02 21:22:52 2018 +0200 +++ b/src/Pure/Tools/dump.scala Sun Sep 02 22:30:08 2018 +0200 @@ -136,7 +136,7 @@ else { for { (name, status) <- theories_result.nodes if !status.ok - (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree) + (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree) } progress.echo_error_message(XML.content(Pretty.formatted(List(tree)))) session_result.copy(rc = session_result.rc max 1)