src/Pure/PIDE/document_status.scala
author wenzelm
Fri, 06 Sep 2019 11:32:38 +0200
changeset 70658 4655897b8287
parent 70653 f7c5b30fc432
child 71601 97ccf48c2f0c
permissions -rw-r--r--
unused;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/PIDE/document_status.scala
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     3
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     4
Document status based on markup information.
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     6
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     8
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
     9
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    10
object Document_Status
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    11
{
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    12
  /* command status */
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    13
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    14
  object Command_Status
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    15
  {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    16
    val proper_elements: Markup.Elements =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    17
      Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
    18
        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    19
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    20
    val liberal_elements: Markup.Elements =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    21
      proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    22
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    23
    def make(markup_iterator: Iterator[Markup]): Command_Status =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    24
    {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    25
      var touched = false
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    26
      var accepted = false
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    27
      var warned = false
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    28
      var failed = false
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
    29
      var canceled = false
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
    30
      var finalized = false
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    31
      var forks = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    32
      var runs = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    33
      for (markup <- markup_iterator) {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    34
        markup.name match {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    35
          case Markup.ACCEPTED => accepted = true
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    36
          case Markup.FORKED => touched = true; forks += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    37
          case Markup.JOINED => forks -= 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    38
          case Markup.RUNNING => touched = true; runs += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    39
          case Markup.FINISHED => runs -= 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    40
          case Markup.WARNING | Markup.LEGACY => warned = true
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    41
          case Markup.FAILED | Markup.ERROR => failed = true
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
    42
          case Markup.CANCELED => canceled = true
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
    43
          case Markup.FINALIZED => finalized = true
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    44
          case _ =>
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    45
        }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    46
      }
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    47
      Command_Status(
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    48
        touched = touched,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    49
        accepted = accepted,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    50
        warned = warned,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    51
        failed = failed,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    52
        canceled = canceled,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    53
        finalized = finalized,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    54
        forks = forks,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    55
        runs = runs)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    56
    }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    57
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    58
    val empty = make(Iterator.empty)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    59
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    60
    def merge(status_iterator: Iterator[Command_Status]): Command_Status =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    61
      if (status_iterator.hasNext) {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    62
        val status0 = status_iterator.next
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    63
        (status0 /: status_iterator)(_ + _)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    64
      }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    65
      else empty
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    66
  }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    67
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    68
  sealed case class Command_Status(
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    69
    private val touched: Boolean,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    70
    private val accepted: Boolean,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    71
    private val warned: Boolean,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    72
    private val failed: Boolean,
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
    73
    private val canceled: Boolean,
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
    74
    private val finalized: Boolean,
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    75
    forks: Int,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    76
    runs: Int)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    77
  {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    78
    def + (that: Command_Status): Command_Status =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    79
      Command_Status(
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    80
        touched = touched || that.touched,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    81
        accepted = accepted || that.accepted,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    82
        warned = warned || that.warned,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    83
        failed = failed || that.failed,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    84
        canceled = canceled || that.canceled,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    85
        finalized = finalized || that.finalized,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    86
        forks = forks + that.forks,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
    87
        runs = runs + that.runs)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    88
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    89
    def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    90
    def is_running: Boolean = runs != 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    91
    def is_warned: Boolean = warned
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    92
    def is_failed: Boolean = failed
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    93
    def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
    94
    def is_canceled: Boolean = canceled
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
    95
    def is_finalized: Boolean = finalized
68881
d975449b266e more detailed node_status;
wenzelm
parents: 68873
diff changeset
    96
    def is_terminated: Boolean = canceled || touched && forks == 0 && runs == 0
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    97
  }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    98
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
    99
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   100
  /* node status */
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   101
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   102
  object Node_Status
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   103
  {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   104
    def make(
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   105
      state: Document.State,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   106
      version: Document.Version,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   107
      name: Document.Node.Name): Node_Status =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   108
    {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   109
      val node = version.nodes(name)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   110
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   111
      var unprocessed = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   112
      var running = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   113
      var warned = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   114
      var failed = 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   115
      var finished = 0
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
   116
      var canceled = false
68892
dce6cbd3cafc proper polarity of terminated status;
wenzelm
parents: 68889
diff changeset
   117
      var terminated = true
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
   118
      var finalized = false
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   119
      for (command <- node.commands.iterator) {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   120
        val states = state.command_states(version, command)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   121
        val status = Command_Status.merge(states.iterator.map(_.document_status))
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   122
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   123
        if (status.is_running) running += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   124
        else if (status.is_failed) failed += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   125
        else if (status.is_warned) warned += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   126
        else if (status.is_finished) finished += 1
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   127
        else unprocessed += 1
68871
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
   128
f5c76072db55 more explicit status for "canceled" command within theory node;
wenzelm
parents: 68770
diff changeset
   129
        if (status.is_canceled) canceled = true
68892
dce6cbd3cafc proper polarity of terminated status;
wenzelm
parents: 68889
diff changeset
   130
        if (!status.is_terminated) terminated = false
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
   131
        if (status.is_finalized) finalized = true
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   132
      }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   133
      val initialized = state.node_initialized(version, name)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   134
      val consolidated = state.node_consolidated(version, name)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   135
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   136
      Node_Status(
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   137
        is_suppressed = version.nodes.is_suppressed(name),
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   138
        unprocessed = unprocessed,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   139
        running = running,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   140
        warned = warned,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   141
        failed = failed,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   142
        finished = finished,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   143
        canceled = canceled,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   144
        terminated = terminated,
68889
d9c051e9da2b tuned signature;
wenzelm
parents: 68887
diff changeset
   145
        initialized = initialized,
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   146
        finalized = finalized,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   147
        consolidated = consolidated)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   148
    }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   149
  }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   150
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   151
  sealed case class Node_Status(
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   152
    is_suppressed: Boolean,
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   153
    unprocessed: Int,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   154
    running: Int,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   155
    warned: Int,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   156
    failed: Int,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   157
    finished: Int,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   158
    canceled: Boolean,
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   159
    terminated: Boolean,
68889
d9c051e9da2b tuned signature;
wenzelm
parents: 68887
diff changeset
   160
    initialized: Boolean,
68887
b07735ce02b3 tuned -- more robust against changes;
wenzelm
parents: 68885
diff changeset
   161
    finalized: Boolean,
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
   162
    consolidated: Boolean)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   163
  {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   164
    def ok: Boolean = failed == 0
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   165
    def total: Int = unprocessed + running + warned + failed + finished
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   166
69844
b21ddfa7042b clarified quasi_consolidated status after 5f160df596c1 -- relevant for headless PIDE session (e.g. "isabelle dump");
wenzelm
parents: 69818
diff changeset
   167
    def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
68897
bdc38f0fd68c tuned signature;
wenzelm
parents: 68892
diff changeset
   168
68898
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   169
    def percentage: Int =
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   170
      if (consolidated) 100
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   171
      else if (total == 0) 0
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   172
      else (((total - unprocessed).toDouble / total) * 100).toInt min 99
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   173
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   174
    def json: JSON.Object.T =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   175
      JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   176
        "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
68898
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   177
        "canceled" -> canceled, "consolidated" -> consolidated,
241d08beaf5c more informative node_status;
wenzelm
parents: 68897
diff changeset
   178
        "percentage" -> percentage)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   179
  }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   180
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   181
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   182
  /* overall timing */
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   183
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   184
  object Overall_Timing
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   185
  {
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   186
    val empty: Overall_Timing = Overall_Timing(0.0, Map.empty)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   187
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   188
    def make(
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   189
      state: Document.State,
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   190
      version: Document.Version,
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   191
      commands: Iterable[Command],
69864
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   192
      threshold: Double = 0.0): Overall_Timing =
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   193
    {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   194
      var total = 0.0
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   195
      var command_timings = Map.empty[Command, Double]
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   196
      for {
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   197
        command <- commands.iterator
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   198
        st <- state.command_states(version, command)
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   199
      } {
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   200
        val command_timing =
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   201
          (0.0 /: st.status)({
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   202
            case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   203
            case (timing, _) => timing
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   204
          })
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   205
        total += command_timing
69864
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   206
        if (command_timing > 0.0 && command_timing >= threshold) {
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   207
          command_timings += (command -> command_timing)
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   208
        }
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   209
      }
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   210
      Overall_Timing(total, command_timings)
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   211
    }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   212
  }
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   213
69863
9532d5b2e932 clarified signature: more general types;
wenzelm
parents: 69844
diff changeset
   214
  sealed case class Overall_Timing(total: Double, command_timings: Map[Command, Double])
69864
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   215
  {
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   216
    def command_timing(command: Command): Double =
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   217
      command_timings.getOrElse(command, 0.0)
d594997cdcf4 clarified signature;
wenzelm
parents: 69863
diff changeset
   218
  }
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   219
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   220
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   221
  /* nodes status */
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   222
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   223
  object Overall_Node_Status extends Enumeration
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   224
  {
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   225
    val ok, failed, pending = Value
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   226
  }
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   227
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   228
  object Nodes_Status
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   229
  {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   230
    val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   231
  }
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   232
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   233
  final class Nodes_Status private(
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   234
    private val rep: Map[Document.Node.Name, Node_Status],
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   235
    nodes: Document.Nodes)
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   236
  {
68770
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68769
diff changeset
   237
    def is_empty: Boolean = rep.isEmpty
add44e2b8cb0 optional notification of nodes_status (via progress);
wenzelm
parents: 68769
diff changeset
   238
    def apply(name: Document.Node.Name): Node_Status = rep(name)
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   239
    def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   240
69818
60d0ee8f2ddb more robust: avoid potentially unrelated snapshot for the sake of is_suppressed;
wenzelm
parents: 69817
diff changeset
   241
    def present: List[(Document.Node.Name, Node_Status)] =
69817
5f160df596c1 clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
wenzelm
parents: 69255
diff changeset
   242
      (for {
5f160df596c1 clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
wenzelm
parents: 69255
diff changeset
   243
        name <- nodes.topological_order.iterator
5f160df596c1 clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
wenzelm
parents: 69255
diff changeset
   244
        node_status <- get(name)
5f160df596c1 clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
wenzelm
parents: 69255
diff changeset
   245
      } yield (name, node_status)).toList
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   246
68884
9b97d0b20d95 clarified quasi_consolidated state: ensure that exports are present for ok nodes;
wenzelm
parents: 68883
diff changeset
   247
    def quasi_consolidated(name: Document.Node.Name): Boolean =
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68881
diff changeset
   248
      rep.get(name) match {
68897
bdc38f0fd68c tuned signature;
wenzelm
parents: 68892
diff changeset
   249
        case Some(st) => st.quasi_consolidated
68883
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68881
diff changeset
   250
        case None => false
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68881
diff changeset
   251
      }
3653b3ad729e clarified Thy_Resources.Session.use_theories: "terminated" node status is sufficient;
wenzelm
parents: 68881
diff changeset
   252
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   253
    def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   254
      rep.get(name) match {
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   255
        case Some(st) if st.consolidated =>
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   256
          if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   257
        case _ => Overall_Node_Status.pending
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   258
      }
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   259
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   260
    def update(
69255
800b1ce96fce more general support for Isabelle/PIDE file formats -- less hardwired Bibtex operations;
wenzelm
parents: 68904
diff changeset
   261
      resources: Resources,
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   262
      state: Document.State,
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   263
      version: Document.Version,
68769
59fcff4f8b73 tuned signature;
wenzelm
parents: 68766
diff changeset
   264
      domain: Option[Set[Document.Node.Name]] = None,
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   265
      trim: Boolean = false): (Boolean, Nodes_Status) =
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   266
    {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   267
      val nodes1 = version.nodes
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   268
      val update_iterator =
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   269
        for {
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   270
          name <- domain.getOrElse(nodes1.domain).iterator
69817
5f160df596c1 clarified Node_Status vs. is_suppressed, e.g. relevant for purged nodes in Theories_Dockable after 0626cae56b6f;
wenzelm
parents: 69255
diff changeset
   271
          if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   272
          st = Document_Status.Node_Status.make(state, version, name)
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   273
          if !rep.isDefinedAt(name) || rep(name) != st
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   274
        } yield (name -> st)
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   275
      val rep1 = rep ++ update_iterator
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   276
      val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
68764
b523e903d6e4 clarified signature;
wenzelm
parents: 68763
diff changeset
   277
68903
58525b08eed1 clarified Nodes_Status;
wenzelm
parents: 68898
diff changeset
   278
      (rep != rep2, new Nodes_Status(rep2, nodes1))
68763
3c5857c6bc5b clarified signature;
wenzelm
parents: 68761
diff changeset
   279
    }
68761
8bb51b3de39f trim nodes_status: avoid potential memory leak;
wenzelm
parents: 68760
diff changeset
   280
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   281
    override def hashCode: Int = rep.hashCode
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   282
    override def equals(that: Any): Boolean =
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   283
      that match {
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   284
        case other: Nodes_Status => rep == other.rep
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   285
        case _ => false
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   286
      }
68765
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   287
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   288
    override def toString: String =
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   289
    {
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   290
      var ok = 0
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   291
      var failed = 0
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   292
      var pending = 0
68873
13a984eba612 clarified message;
wenzelm
parents: 68871
diff changeset
   293
      var canceled = 0
68765
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   294
      for (name <- rep.keysIterator) {
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   295
        overall_node_status(name) match {
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   296
          case Overall_Node_Status.ok => ok += 1
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   297
          case Overall_Node_Status.failed => failed += 1
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   298
          case Overall_Node_Status.pending => pending += 1
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   299
        }
68873
13a984eba612 clarified message;
wenzelm
parents: 68871
diff changeset
   300
        if (apply(name).canceled) canceled += 1
68765
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   301
      }
68873
13a984eba612 clarified message;
wenzelm
parents: 68871
diff changeset
   302
      "Nodes_Status(ok = " + ok + ", failed = " + failed + ", pending = " + pending +
13a984eba612 clarified message;
wenzelm
parents: 68871
diff changeset
   303
        ", canceled = " + canceled + ")"
68765
be5f255a9943 tuned output;
wenzelm
parents: 68764
diff changeset
   304
    }
68759
4247e91fa21d clarified modules;
wenzelm
parents: 68758
diff changeset
   305
  }
68758
a110e7e24e55 clarified modules;
wenzelm
parents:
diff changeset
   306
}