src/Pure/PIDE/markup.ML
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 68884 9b97d0b20d95
     1.1 --- a/src/Pure/PIDE/markup.ML	Sat Sep 01 18:39:36 2018 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sat Sep 01 20:20:50 2018 +0200
     1.3 @@ -165,6 +165,7 @@
     1.4    val runningN: string val running: T
     1.5    val finishedN: string val finished: T
     1.6    val failedN: string val failed: T
     1.7 +  val canceledN: string val canceled: T
     1.8    val initializedN: string val initialized: T
     1.9    val consolidatedN: string val consolidated: T
    1.10    val exec_idN: string
    1.11 @@ -577,7 +578,7 @@
    1.12  val (runningN, running) = markup_elem "running";
    1.13  val (finishedN, finished) = markup_elem "finished";
    1.14  val (failedN, failed) = markup_elem "failed";
    1.15 -
    1.16 +val (canceledN, canceled) = markup_elem "canceled";
    1.17  val (initializedN, initialized) = markup_elem "initialized";
    1.18  val (consolidatedN, consolidated) = markup_elem "consolidated";
    1.19