# HG changeset patch
# User wenzelm
# Date 1535925325 -7200
# Node ID d9c051e9da2ba5fae849b5c37d60331b4ac7020a
# Parent  4fe165254e20f07c19588b9a0e155f6497779804
tuned signature;

diff -r 4fe165254e20 -r d9c051e9da2b src/Pure/PIDE/document_status.scala
--- 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