merged
authornipkow
Sun, 09 Sep 2018 17:56:13 +0200
changeset 68964 ff6b594e4230
parent 68962 50676b0ab970 (diff)
parent 68963 ed6511997d2b (current diff)
child 68965 1254f3e57fed
merged
--- a/src/Pure/Thy/thy_resources.scala	Sun Sep 09 17:56:00 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Sun Sep 09 17:56:13 2018 +0200
@@ -270,9 +270,9 @@
                       (for {
                         (name, node_status) <- nodes_status1.present.iterator
                         if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
-                        percentage = Some(node_status.percentage)
-                        if percentage != st.nodes_status.get(name).map(_.percentage)
-                      } yield Progress.Theory(name.theory, percentage = percentage)).toList
+                        p1 = node_status.percentage
+                        if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
+                      } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
 
                     (theory_progress, st.update(nodes_status1))
                   })