tuned signature;
authorwenzelm
Sun Sep 02 23:55:25 2018 +0200 (10 months ago)
changeset 68889d9c051e9da2b
parent 68888 4fe165254e20
child 68891 3cdde2ea2667
child 68892 dce6cbd3cafc
tuned signature;
src/Pure/PIDE/document_status.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 23:25:53 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Sun Sep 02 23:55:25 2018 +0200
     1.3 @@ -141,8 +141,8 @@
     1.4          finished = finished,
     1.5          canceled = canceled,
     1.6          terminated = terminated,
     1.7 +        initialized = initialized,
     1.8          finalized = finalized,
     1.9 -        initialized = initialized,
    1.10          consolidated = consolidated)
    1.11      }
    1.12    }
    1.13 @@ -155,8 +155,8 @@
    1.14      finished: Int,
    1.15      canceled: Boolean,
    1.16      terminated: Boolean,
    1.17 +    initialized: Boolean,
    1.18      finalized: Boolean,
    1.19 -    initialized: Boolean,
    1.20      consolidated: Boolean)
    1.21    {
    1.22      def ok: Boolean = failed == 0