--- 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
})