clarified quasi_consolidated state: ensure that exports are present for ok nodes;

--- 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;
 

--- 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
       }
 

--- 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";
 
 

--- 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"
 
 

--- 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)

--- 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)