src/Pure/PIDE/markup.ML
changeset 68871 f5c76072db55
parent 68822 253f04c1e814
child 68884 9b97d0b20d95
--- 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";