clarified quasi_consolidated state: ensure that exports are present for ok nodes;
authorwenzelm
Sun Sep 02 22:30:08 2018 +0200 (9 months ago)
changeset 688849b97d0b20d95
parent 68883 3653b3ad729e
child 68885 17486b8218e2
clarified quasi_consolidated state: ensure that exports are present for ok nodes;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Thy/thy_resources.scala
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/PIDE/command.ML	Sun Sep 02 21:22:52 2018 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Sun Sep 02 22:30:08 2018 +0200
     1.3 @@ -269,6 +269,10 @@
     1.4      | SOME st' =>
     1.5          let
     1.6            val _ = status tr Markup.finished;
     1.7 +          val _ =
     1.8 +            if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso
     1.9 +              can (Toplevel.end_theory Position.none) st'
    1.10 +            then status tr Markup.finalized else ();
    1.11          in {failed = false, command = tr, state = st'} end)
    1.12    end;
    1.13  
     2.1 --- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 21:22:52 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document_status.scala	Sun Sep 02 22:30:08 2018 +0200
     2.3 @@ -27,6 +27,7 @@
     2.4        var warned = false
     2.5        var failed = false
     2.6        var canceled = false
     2.7 +      var finalized = false
     2.8        var forks = 0
     2.9        var runs = 0
    2.10        for (markup <- markup_iterator) {
    2.11 @@ -39,10 +40,11 @@
    2.12            case Markup.WARNING | Markup.LEGACY => warned = true
    2.13            case Markup.FAILED | Markup.ERROR => failed = true
    2.14            case Markup.CANCELED => canceled = true
    2.15 +          case Markup.FINALIZED => finalized = true
    2.16            case _ =>
    2.17          }
    2.18        }
    2.19 -      Command_Status(touched, accepted, warned, failed, canceled, forks, runs)
    2.20 +      Command_Status(touched, accepted, warned, failed, canceled, finalized, forks, runs)
    2.21      }
    2.22  
    2.23      val empty = make(Iterator.empty)
    2.24 @@ -61,6 +63,7 @@
    2.25      private val warned: Boolean,
    2.26      private val failed: Boolean,
    2.27      private val canceled: Boolean,
    2.28 +    private val finalized: Boolean,
    2.29      forks: Int,
    2.30      runs: Int)
    2.31    {
    2.32 @@ -71,6 +74,7 @@
    2.33          warned || that.warned,
    2.34          failed || that.failed,
    2.35          canceled || that.canceled,
    2.36 +        finalized || that.finalized,
    2.37          forks + that.forks,
    2.38          runs + that.runs)
    2.39  
    2.40 @@ -80,6 +84,7 @@
    2.41      def is_failed: Boolean = failed
    2.42      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    2.43      def is_canceled: Boolean = canceled
    2.44 +    def is_finalized: Boolean = finalized
    2.45      def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
    2.46    }
    2.47  
    2.48 @@ -102,6 +107,7 @@
    2.49        var finished = 0
    2.50        var canceled = false
    2.51        var terminated = false
    2.52 +      var finalized = false
    2.53        for (command <- node.commands.iterator) {
    2.54          val states = state.command_states(version, command)
    2.55          val status = Command_Status.merge(states.iterator.map(_.document_status))
    2.56 @@ -114,18 +120,20 @@
    2.57  
    2.58          if (status.is_canceled) canceled = true
    2.59          if (status.is_terminated) terminated = true
    2.60 +        if (status.is_finalized) finalized = true
    2.61        }
    2.62        val initialized = state.node_initialized(version, name)
    2.63        val consolidated = state.node_consolidated(version, name)
    2.64  
    2.65        Node_Status(unprocessed, running, warned, failed, finished, canceled, terminated,
    2.66 -        initialized, consolidated)
    2.67 +        finalized, initialized, consolidated)
    2.68      }
    2.69    }
    2.70  
    2.71    sealed case class Node_Status(
    2.72      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
    2.73 -    canceled: Boolean, terminated: Boolean, initialized: Boolean, consolidated: Boolean)
    2.74 +    canceled: Boolean, terminated: Boolean, finalized: Boolean, initialized: Boolean,
    2.75 +    consolidated: Boolean)
    2.76    {
    2.77      def ok: Boolean = failed == 0
    2.78      def total: Int = unprocessed + running + warned + failed + finished
    2.79 @@ -133,8 +141,8 @@
    2.80      def json: JSON.Object.T =
    2.81        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    2.82          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    2.83 -        "canceled" -> canceled, "terminated" -> terminated, "initialized" -> initialized,
    2.84 -        "consolidated" -> consolidated)
    2.85 +        "canceled" -> canceled, "terminated" -> terminated, "finalized" -> finalized,
    2.86 +        "initialized" -> initialized, "consolidated" -> consolidated)
    2.87    }
    2.88  
    2.89  
    2.90 @@ -192,9 +200,9 @@
    2.91      def apply(name: Document.Node.Name): Node_Status = rep(name)
    2.92      def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
    2.93  
    2.94 -    def is_terminated(name: Document.Node.Name): Boolean =
    2.95 +    def quasi_consolidated(name: Document.Node.Name): Boolean =
    2.96        rep.get(name) match {
    2.97 -        case Some(st) => st.terminated
    2.98 +        case Some(st) => !st.finalized && st.terminated
    2.99          case None => false
   2.100        }
   2.101  
     3.1 --- a/src/Pure/PIDE/markup.ML	Sun Sep 02 21:22:52 2018 +0200
     3.2 +++ b/src/Pure/PIDE/markup.ML	Sun Sep 02 22:30:08 2018 +0200
     3.3 @@ -167,6 +167,7 @@
     3.4    val failedN: string val failed: T
     3.5    val canceledN: string val canceled: T
     3.6    val initializedN: string val initialized: T
     3.7 +  val finalizedN: string val finalized: T
     3.8    val consolidatedN: string val consolidated: T
     3.9    val exec_idN: string
    3.10    val initN: string
    3.11 @@ -580,6 +581,7 @@
    3.12  val (failedN, failed) = markup_elem "failed";
    3.13  val (canceledN, canceled) = markup_elem "canceled";
    3.14  val (initializedN, initialized) = markup_elem "initialized";
    3.15 +val (finalizedN, finalized) = markup_elem "finalized";
    3.16  val (consolidatedN, consolidated) = markup_elem "consolidated";
    3.17  
    3.18  
     4.1 --- a/src/Pure/PIDE/markup.scala	Sun Sep 02 21:22:52 2018 +0200
     4.2 +++ b/src/Pure/PIDE/markup.scala	Sun Sep 02 22:30:08 2018 +0200
     4.3 @@ -426,6 +426,7 @@
     4.4    val FAILED = "failed"
     4.5    val CANCELED = "canceled"
     4.6    val INITIALIZED = "initialized"
     4.7 +  val FINALIZED = "finalized"
     4.8    val CONSOLIDATED = "consolidated"
     4.9  
    4.10  
     5.1 --- a/src/Pure/Thy/thy_resources.scala	Sun Sep 02 21:22:52 2018 +0200
     5.2 +++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 02 22:30:08 2018 +0200
     5.3 @@ -123,7 +123,7 @@
     5.4              if (beyond_limit ||
     5.5                  dep_theories.forall(name =>
     5.6                    state.node_consolidated(version, name) ||
     5.7 -                  nodes_status_update.value._1.is_terminated(name)))
     5.8 +                  nodes_status_update.value._1.quasi_consolidated(name)))
     5.9              {
    5.10                val nodes =
    5.11                  for (name <- dep_theories)
     6.1 --- a/src/Pure/Tools/dump.scala	Sun Sep 02 21:22:52 2018 +0200
     6.2 +++ b/src/Pure/Tools/dump.scala	Sun Sep 02 22:30:08 2018 +0200
     6.3 @@ -136,7 +136,7 @@
     6.4      else {
     6.5        for {
     6.6          (name, status) <- theories_result.nodes if !status.ok
     6.7 -        (tree, pos) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
     6.8 +        (tree, _) <- theories_result.snapshot(name).messages if Protocol.is_error(tree)
     6.9        } progress.echo_error_message(XML.content(Pretty.formatted(List(tree))))
    6.10  
    6.11        session_result.copy(rc = session_result.rc max 1)