src/Pure/PIDE/rendering.scala
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 69320 fc221fa79741
--- 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
         })