# HG changeset patch
# User wenzelm
# Date 1535826050 -7200
# Node ID f5c76072db557d66ed6d5af807dc82b03679dfa4
# Parent  53a75627aab737c26a1ea974064f92658ef1ca89
more explicit status for "canceled" command within theory node;

diff -r 53a75627aab7 -r f5c76072db55 src/Doc/System/Server.thy
--- a/src/Doc/System/Server.thy	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Doc/System/Server.thy	Sat Sep 01 20:20:50 2018 +0200
@@ -516,14 +516,16 @@
   session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>).
 
   \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running:
-  int, warned: int, failed: int, finished: int, initialized: bool,
-  consolidated: bool}\<close> represents a formal theory node status of the PIDE
-  document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
+  int, warned: int, failed: int, finished: int, canceled: bool, initialized:
+  bool, consolidated: bool}\<close> represents a formal theory node status of the
+  PIDE document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>,
   \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node;
-  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>initialized\<close> flag indicates
-  that the initial \<^theory_text>\<open>theory\<close> command has been processed. The \<open>consolidated\<close>
-  flag indicates whether the outermost theory command structure has finished
-  (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
+  \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>canceled\<close> flag tells if some
+  command in the theory has been spontaneously canceled (by an Interrupt
+  exception that could also indicate resource problems). The \<open>initialized\<close>
+  flag indicates that the initial \<^theory_text>\<open>theory\<close> command has been processed. The
+  \<open>consolidated\<close> flag indicates whether the outermost theory command structure
+  has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked.
 \<close>
 
 
diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Pure/PIDE/command.ML	Sat Sep 01 20:20:50 2018 +0200
@@ -260,7 +260,7 @@
         let
           val _ = status tr Markup.failed;
           val _ = status tr Markup.finished;
-          val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
+          val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else ();
         in {failed = true, command = tr, state = st} end
     | SOME st' =>
         let
diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/document_status.scala
--- a/src/Pure/PIDE/document_status.scala	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala	Sat Sep 01 20:20:50 2018 +0200
@@ -15,7 +15,7 @@
   {
     val proper_elements: Markup.Elements =
       Markup.Elements(Markup.ACCEPTED, Markup.FORKED, Markup.JOINED, Markup.RUNNING,
-        Markup.FINISHED, Markup.FAILED)
+        Markup.FINISHED, Markup.FAILED, Markup.CANCELED)
 
     val liberal_elements: Markup.Elements =
       proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
@@ -26,6 +26,7 @@
       var accepted = false
       var warned = false
       var failed = false
+      var canceled = false
       var forks = 0
       var runs = 0
       for (markup <- markup_iterator) {
@@ -37,10 +38,11 @@
           case Markup.FINISHED => runs -= 1
           case Markup.WARNING | Markup.LEGACY => warned = true
           case Markup.FAILED | Markup.ERROR => failed = true
+          case Markup.CANCELED => canceled = true
           case _ =>
         }
       }
-      Command_Status(touched, accepted, warned, failed, forks, runs)
+      Command_Status(touched, accepted, warned, failed, canceled, forks, runs)
     }
 
     val empty = make(Iterator.empty)
@@ -58,6 +60,7 @@
     private val accepted: Boolean,
     private val warned: Boolean,
     private val failed: Boolean,
+    private val canceled: Boolean,
     forks: Int,
     runs: Int)
   {
@@ -67,6 +70,7 @@
         accepted || that.accepted,
         warned || that.warned,
         failed || that.failed,
+        canceled || that.canceled,
         forks + that.forks,
         runs + that.runs)
 
@@ -75,6 +79,7 @@
     def is_warned: Boolean = warned
     def is_failed: Boolean = failed
     def is_finished: Boolean = !failed && touched && forks == 0 && runs == 0
+    def is_canceled: Boolean = canceled
   }
 
 
@@ -94,6 +99,7 @@
       var warned = 0
       var failed = 0
       var finished = 0
+      var canceled = false
       for (command <- node.commands.iterator) {
         val states = state.command_states(version, command)
         val status = Command_Status.merge(states.iterator.map(_.document_status))
@@ -103,17 +109,20 @@
         else if (status.is_warned) warned += 1
         else if (status.is_finished) finished += 1
         else unprocessed += 1
+
+        if (status.is_canceled) canceled = true
       }
       val initialized = state.node_initialized(version, name)
       val consolidated = state.node_consolidated(version, name)
 
-      Node_Status(unprocessed, running, warned, failed, finished, initialized, consolidated)
+      Node_Status(
+        unprocessed, running, warned, failed, finished, canceled, initialized, consolidated)
     }
   }
 
   sealed case class Node_Status(
     unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int,
-    initialized: Boolean, consolidated: Boolean)
+    canceled: Boolean, initialized: Boolean, consolidated: Boolean)
   {
     def ok: Boolean = failed == 0
     def total: Int = unprocessed + running + warned + failed + finished
@@ -121,7 +130,7 @@
     def json: JSON.Object.T =
       JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
         "running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
-        "initialized" -> initialized, "consolidated" -> consolidated)
+        "canceled" -> canceled, "initialized" -> initialized, "consolidated" -> consolidated)
   }
 
 
diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Pure/PIDE/markup.ML	Sat Sep 01 20:20:50 2018 +0200
@@ -165,6 +165,7 @@
   val runningN: string val running: T
   val finishedN: string val finished: T
   val failedN: string val failed: T
+  val canceledN: string val canceled: T
   val initializedN: string val initialized: T
   val consolidatedN: string val consolidated: T
   val exec_idN: string
@@ -577,7 +578,7 @@
 val (runningN, running) = markup_elem "running";
 val (finishedN, finished) = markup_elem "finished";
 val (failedN, failed) = markup_elem "failed";
-
+val (canceledN, canceled) = markup_elem "canceled";
 val (initializedN, initialized) = markup_elem "initialized";
 val (consolidatedN, consolidated) = markup_elem "consolidated";
 
diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Pure/PIDE/markup.scala	Sat Sep 01 20:20:50 2018 +0200
@@ -424,7 +424,7 @@
   val RUNNING = "running"
   val FINISHED = "finished"
   val FAILED = "failed"
-
+  val CANCELED = "canceled"
   val INITIALIZED = "initialized"
   val CONSOLIDATED = "consolidated"
 
diff -r 53a75627aab7 -r f5c76072db55 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sat Sep 01 20:20:50 2018 +0200
@@ -19,7 +19,7 @@
   object Color extends Enumeration
   {
     // background
-    val unprocessed1, running1, bad, intensify, entity, active, active_result,
+    val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
       markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
     val background_colors = values
 
@@ -432,6 +432,7 @@
             val status = Document_Status.Command_Status.make(markups.iterator)
             if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
             else if (status.is_running) Some(Rendering.Color.running1)
+            else if (status.is_canceled) Some(Rendering.Color.canceled)
             else opt_color
           case (_, opt_color) => opt_color
         })
diff -r 53a75627aab7 -r f5c76072db55 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Tools/VSCode/extension/package.json	Sat Sep 01 20:20:50 2018 +0200
@@ -250,6 +250,14 @@
                     "type": "string",
                     "default": "rgba(255, 160, 160, 0.40)"
                 },
+                "isabelle.canceled_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 106, 106, 0.40)"
+                },
+                "isabelle.canceled_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 106, 106, 0.40)"
+                },
                 "isabelle.bad_light_color": {
                     "type": "string",
                     "default": "rgba(255, 106, 106, 0.40)"
diff -r 53a75627aab7 -r f5c76072db55 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Sep 01 20:20:50 2018 +0200
@@ -13,6 +13,7 @@
 const background_colors = [
   "unprocessed1",
   "running1",
+  "canceled",
   "bad",
   "intensify",
   "quoted",
diff -r 53a75627aab7 -r f5c76072db55 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Sep 01 18:39:36 2018 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Sep 01 20:20:50 2018 +0200
@@ -95,6 +95,7 @@
 option error_message_color : string = "FFC1C1FF"
 option spell_checker_color : string = "0000FFFF"
 option bad_color : string = "FF6A6A64"
+option canceled_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option entity_color : string = "CCD9FF80"
 option entity_ref_color : string = "800080FF"