proper polarity of terminated status;
authorwenzelm
Mon Sep 03 15:04:04 2018 +0200 (9 months ago)
changeset 68892dce6cbd3cafc
parent 68889 d9c051e9da2b
child 68893 58bf801d679a
proper polarity of terminated status;
src/Pure/PIDE/document_status.scala
     1.1 --- a/src/Pure/PIDE/document_status.scala	Sun Sep 02 23:55:25 2018 +0200
     1.2 +++ b/src/Pure/PIDE/document_status.scala	Mon Sep 03 15:04:04 2018 +0200
     1.3 @@ -114,7 +114,7 @@
     1.4        var failed = 0
     1.5        var finished = 0
     1.6        var canceled = false
     1.7 -      var terminated = false
     1.8 +      var terminated = true
     1.9        var finalized = false
    1.10        for (command <- node.commands.iterator) {
    1.11          val states = state.command_states(version, command)
    1.12 @@ -127,7 +127,7 @@
    1.13          else unprocessed += 1
    1.14  
    1.15          if (status.is_canceled) canceled = true
    1.16 -        if (status.is_terminated) terminated = true
    1.17 +        if (!status.is_terminated) terminated = false
    1.18          if (status.is_finalized) finalized = true
    1.19        }
    1.20        val initialized = state.node_initialized(version, name)