more explicit status for "canceled" command within theory node;
authorwenzelm
Sat Sep 01 20:20:50 2018 +0200 (9 months ago)
changeset 68871f5c76072db55
parent 68870 53a75627aab7
child 68872 cd7ab35aa40c
more explicit status for "canceled" command within theory node;
src/Doc/System/Server.thy
src/Pure/PIDE/command.ML
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/PIDE/rendering.scala
src/Tools/VSCode/extension/package.json
src/Tools/VSCode/extension/src/decorations.ts
src/Tools/jEdit/etc/options
     1.1 --- a/src/Doc/System/Server.thy	Sat Sep 01 18:39:36 2018 +0200
     1.2 +++ b/src/Doc/System/Server.thy	Sat Sep 01 20:20:50 2018 +0200
     1.3 @@ -516,14 +516,16 @@
     1.4    session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
     1.5  
     1.6    \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
     1.7 -  int, warned: int, failed: int, finished: int, initialized: bool,
     1.8 -  consolidated: bool}\<close> represents a formal theory node status of the PIDE
     1.9 -  document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
    1.10 +  int, warned: int, failed: int, finished: int, canceled: bool, initialized:
    1.11 +  bool, consolidated: bool}\<close> represents a formal theory node status of the
    1.12 +  PIDE document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
    1.13    \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
    1.14 -  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
    1.15 -  that the initial \<^theory_text>\<open>theory\<close> command has been processed. The \<open>consolidated\<close>
    1.16 -  flag indicates whether the outermost theory command structure has finished
    1.17 -  (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
    1.18 +  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>canceled\<close> flag tells if some
    1.19 +  command in the theory has been spontaneously canceled (by an Interrupt
    1.20 +  exception that could also indicate resource problems). The \<open>initialized\<close>
    1.21 +  flag indicates that the initial \<^theory_text>\<open>theory\<close> command has been processed. The
    1.22 +  \<open>consolidated\<close> flag indicates whether the outermost theory command structure
    1.23 +  has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
    1.24  \<close>
    1.25  
    1.26  
     2.1 --- a/src/Pure/PIDE/command.ML	Sat Sep 01 18:39:36 2018 +0200
     2.2 +++ b/src/Pure/PIDE/command.ML	Sat Sep 01 20:20:50 2018 +0200
     2.3 @@ -260,7 +260,7 @@
     2.4          let
     2.5            val _ = status tr Markup.failed;
     2.6            val _ = status tr Markup.finished;
     2.7 -          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
     2.8 +          val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
     2.9          in {failed = true, command = tr, state = st} end
    2.10      | SOME st' =>
    2.11          let
     3.1 --- a/src/Pure/PIDE/document_status.scala	Sat Sep 01 18:39:36 2018 +0200
     3.2 +++ b/src/Pure/PIDE/document_status.scala	Sat Sep 01 20:20:50 2018 +0200
     3.3 @@ -15,7 +15,7 @@
     3.4    {
     3.5      val proper_elements: Markup.Elements =
     3.6        Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
     3.7 -        Markup.FINISHED, Markup.FAILED)
     3.8 +        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
     3.9  
    3.10      val liberal_elements: Markup.Elements =
    3.11        proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
    3.12 @@ -26,6 +26,7 @@
    3.13        var accepted = false
    3.14        var warned = false
    3.15        var failed = false
    3.16 +      var canceled = false
    3.17        var forks = 0
    3.18        var runs = 0
    3.19        for (markup <- markup_iterator) {
    3.20 @@ -37,10 +38,11 @@
    3.21            case Markup.FINISHED => runs -= 1
    3.22            case Markup.WARNING | Markup.LEGACY => warned = true
    3.23            case Markup.FAILED | Markup.ERROR => failed = true
    3.24 +          case Markup.CANCELED => canceled = true
    3.25            case _ =>
    3.26          }
    3.27        }
    3.28 -      Command_Status(touched, accepted, warned, failed, forks, runs)
    3.29 +      Command_Status(touched, accepted, warned, failed, canceled, forks, runs)
    3.30      }
    3.31  
    3.32      val empty = make(Iterator.empty)
    3.33 @@ -58,6 +60,7 @@
    3.34      private val accepted: Boolean,
    3.35      private val warned: Boolean,
    3.36      private val failed: Boolean,
    3.37 +    private val canceled: Boolean,
    3.38      forks: Int,
    3.39      runs: Int)
    3.40    {
    3.41 @@ -67,6 +70,7 @@
    3.42          accepted || that.accepted,
    3.43          warned || that.warned,
    3.44          failed || that.failed,
    3.45 +        canceled || that.canceled,
    3.46          forks + that.forks,
    3.47          runs + that.runs)
    3.48  
    3.49 @@ -75,6 +79,7 @@
    3.50      def is_warned: Boolean = warned
    3.51      def is_failed: Boolean = failed
    3.52      def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
    3.53 +    def is_canceled: Boolean = canceled
    3.54    }
    3.55  
    3.56  
    3.57 @@ -94,6 +99,7 @@
    3.58        var warned = 0
    3.59        var failed = 0
    3.60        var finished = 0
    3.61 +      var canceled = false
    3.62        for (command <- node.commands.iterator) {
    3.63          val states = state.command_states(version, command)
    3.64          val status = Command_Status.merge(states.iterator.map(_.document_status))
    3.65 @@ -103,17 +109,20 @@
    3.66          else if (status.is_warned) warned += 1
    3.67          else if (status.is_finished) finished += 1
    3.68          else unprocessed += 1
    3.69 +
    3.70 +        if (status.is_canceled) canceled = true
    3.71        }
    3.72        val initialized = state.node_initialized(version, name)
    3.73        val consolidated = state.node_consolidated(version, name)
    3.74  
    3.75 -      Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
    3.76 +      Node_Status(
    3.77 +        unprocessed, running, warned, failed, finished, canceled, initialized, consolidated)
    3.78      }
    3.79    }
    3.80  
    3.81    sealed case class Node_Status(
    3.82      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
    3.83 -    initialized: Boolean, consolidated: Boolean)
    3.84 +    canceled: Boolean, initialized: Boolean, consolidated: Boolean)
    3.85    {
    3.86      def ok: Boolean = failed == 0
    3.87      def total: Int = unprocessed + running + warned + failed + finished
    3.88 @@ -121,7 +130,7 @@
    3.89      def json: JSON.Object.T =
    3.90        JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
    3.91          "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
    3.92 -        "initialized" -> initialized, "consolidated" -> consolidated)
    3.93 +        "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated)
    3.94    }
    3.95  
    3.96  
     4.1 --- a/src/Pure/PIDE/markup.ML	Sat Sep 01 18:39:36 2018 +0200
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sat Sep 01 20:20:50 2018 +0200
     4.3 @@ -165,6 +165,7 @@
     4.4    val runningN: string val running: T
     4.5    val finishedN: string val finished: T
     4.6    val failedN: string val failed: T
     4.7 +  val canceledN: string val canceled: T
     4.8    val initializedN: string val initialized: T
     4.9    val consolidatedN: string val consolidated: T
    4.10    val exec_idN: string
    4.11 @@ -577,7 +578,7 @@
    4.12  val (runningN, running) = markup_elem "running";
    4.13  val (finishedN, finished) = markup_elem "finished";
    4.14  val (failedN, failed) = markup_elem "failed";
    4.15 -
    4.16 +val (canceledN, canceled) = markup_elem "canceled";
    4.17  val (initializedN, initialized) = markup_elem "initialized";
    4.18  val (consolidatedN, consolidated) = markup_elem "consolidated";
    4.19  
     5.1 --- a/src/Pure/PIDE/markup.scala	Sat Sep 01 18:39:36 2018 +0200
     5.2 +++ b/src/Pure/PIDE/markup.scala	Sat Sep 01 20:20:50 2018 +0200
     5.3 @@ -424,7 +424,7 @@
     5.4    val RUNNING = "running"
     5.5    val FINISHED = "finished"
     5.6    val FAILED = "failed"
     5.7 -
     5.8 +  val CANCELED = "canceled"
     5.9    val INITIALIZED = "initialized"
    5.10    val CONSOLIDATED = "consolidated"
    5.11  
     6.1 --- a/src/Pure/PIDE/rendering.scala	Sat Sep 01 18:39:36 2018 +0200
     6.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Sep 01 20:20:50 2018 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4    object Color extends Enumeration
     6.5    {
     6.6      // background
     6.7 -    val unprocessed1, running1, bad, intensify, entity, active, active_result,
     6.8 +    val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
     6.9        markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
    6.10      val background_colors = values
    6.11  
    6.12 @@ -432,6 +432,7 @@
    6.13              val status = Document_Status.Command_Status.make(markups.iterator)
    6.14              if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
    6.15              else if (status.is_running) Some(Rendering.Color.running1)
    6.16 +            else if (status.is_canceled) Some(Rendering.Color.canceled)
    6.17              else opt_color
    6.18            case (_, opt_color) => opt_color
    6.19          })
     7.1 --- a/src/Tools/VSCode/extension/package.json	Sat Sep 01 18:39:36 2018 +0200
     7.2 +++ b/src/Tools/VSCode/extension/package.json	Sat Sep 01 20:20:50 2018 +0200
     7.3 @@ -250,6 +250,14 @@
     7.4                      "type": "string",
     7.5                      "default": "rgba(255, 160, 160, 0.40)"
     7.6                  },
     7.7 +                "isabelle.canceled_light_color": {
     7.8 +                    "type": "string",
     7.9 +                    "default": "rgba(255, 106, 106, 0.40)"
    7.10 +                },
    7.11 +                "isabelle.canceled_dark_color": {
    7.12 +                    "type": "string",
    7.13 +                    "default": "rgba(255, 106, 106, 0.40)"
    7.14 +                },
    7.15                  "isabelle.bad_light_color": {
    7.16                      "type": "string",
    7.17                      "default": "rgba(255, 106, 106, 0.40)"
     8.1 --- a/src/Tools/VSCode/extension/src/decorations.ts	Sat Sep 01 18:39:36 2018 +0200
     8.2 +++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Sep 01 20:20:50 2018 +0200
     8.3 @@ -13,6 +13,7 @@
     8.4  const background_colors = [
     8.5    "unprocessed1",
     8.6    "running1",
     8.7 +  "canceled",
     8.8    "bad",
     8.9    "intensify",
    8.10    "quoted",
     9.1 --- a/src/Tools/jEdit/etc/options	Sat Sep 01 18:39:36 2018 +0200
     9.2 +++ b/src/Tools/jEdit/etc/options	Sat Sep 01 20:20:50 2018 +0200
     9.3 @@ -95,6 +95,7 @@
     9.4  option error_message_color : string = "FFC1C1FF"
     9.5  option spell_checker_color : string = "0000FFFF"
     9.6  option bad_color : string = "FF6A6A64"
     9.7 +option canceled_color : string = "FF6A6A64"
     9.8  option intensify_color : string = "FFCC6664"
     9.9  option entity_color : string = "CCD9FF80"
    9.10  option entity_ref_color : string = "800080FF"