src/Pure/PIDE/rendering.scala
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 69320 fc221fa79741
     1.1 --- a/src/Pure/PIDE/rendering.scala	Sat Sep 01 18:39:36 2018 +0200
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Sat Sep 01 20:20:50 2018 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    object Color extends Enumeration
     1.5    {
     1.6      // background
     1.7 -    val unprocessed1, running1, bad, intensify, entity, active, active_result,
     1.8 +    val unprocessed1, running1, canceled, bad, intensify, entity, active, active_result,
     1.9        markdown_bullet1, markdown_bullet2, markdown_bullet3, markdown_bullet4 = Value
    1.10      val background_colors = values
    1.11  
    1.12 @@ -432,6 +432,7 @@
    1.13              val status = Document_Status.Command_Status.make(markups.iterator)
    1.14              if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
    1.15              else if (status.is_running) Some(Rendering.Color.running1)
    1.16 +            else if (status.is_canceled) Some(Rendering.Color.canceled)
    1.17              else opt_color
    1.18            case (_, opt_color) => opt_color
    1.19          })