--- a/src/Pure/PIDE/document_status.scala Sun Sep 02 23:25:53 2018 +0200
+++ b/src/Pure/PIDE/document_status.scala Sun Sep 02 23:55:25 2018 +0200
@@ -141,8 +141,8 @@
finished = finished,
canceled = canceled,
terminated = terminated,
+ initialized = initialized,
finalized = finalized,
- initialized = initialized,
consolidated = consolidated)
}
}
@@ -155,8 +155,8 @@
finished: Int,
canceled: Boolean,
terminated: Boolean,
+ initialized: Boolean,
finalized: Boolean,
- initialized: Boolean,
consolidated: Boolean)
{
def ok: Boolean = failed == 0