--- a/src/Pure/PIDE/document_status.scala Sun Sep 02 22:30:08 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sun Sep 02 22:34:50 2018 +0200
@@ -141,8 +141,7 @@
def json: JSON.Object.T =
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
- "canceled" -> canceled, "terminated" -> terminated, "finalized" -> finalized,
- "initialized" -> initialized, "consolidated" -> consolidated)
+ "canceled" -> canceled, "consolidated" -> consolidated)
}