# HG changeset patch
# User wenzelm
# Date 1659521698 -7200
# Node ID 2b448d7db0c42b93f90bd43b2ed1606924aad8df
# Parent  17b1c4fbc008b4af1c26f639c2fc2d9da4dd2127
tuned -- following hints by IntelliJ IDEA;

diff -r 17b1c4fbc008 -r 2b448d7db0c4 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Aug 03 12:10:52 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Wed Aug 03 12:14:58 2022 +0200
@@ -216,12 +216,12 @@
               (for {
                 name <- dep_graph.keys_iterator
                 if !loaded_theory(name)
-              } yield { (name -> Document_Status.Node_Status.make(state, version, name)) }).toList
+              } yield name -> Document_Status.Node_Status.make(state, version, name)).toList
             val nodes_committed =
               (for {
                 name <- dep_graph.keys_iterator
                 status <- already_committed1.get(name)
-              } yield (name -> status)).toList
+              } yield name -> status).toList
             Some(Exn.Res(new Use_Theories_Result(state, version, nodes, nodes_committed)))
           }
           else result
@@ -314,7 +314,7 @@
           }
 
         isabelle.Session.Consumer[isabelle.Session.Commands_Changed](getClass.getName) {
-          case changed =>
+          changed =>
             if (changed.nodes.exists(dep_theories_set)) {
               val snapshot = session.snapshot()
               val state = snapshot.state
@@ -339,7 +339,7 @@
                       (name, node_status) <- nodes_status1.present.iterator
                       if changed.nodes.contains(name) && !st.already_committed.isDefinedAt(name)
                       p1 = node_status.percentage
-                      if p1 > 0 && Some(p1) != st.nodes_status.get(name).map(_.percentage)
+                      if p1 > 0 && !st.nodes_status.get(name).map(_.percentage).contains(p1)
                     } yield Progress.Theory(name.theory, percentage = Some(p1))).toList
 
                   (theory_progress, st.update(nodes_status1))