[isabelle-dev] Unresponsive Isabelle/jEdit

[Makarius]

On Tue, 1 Apr 2014, Johannes Hölzl wrote:

> Currently I have the problem that when opening a file in
> Multivariate_Analysis it can take quite some time until the theories it
> depends on are loaded. In this time I/jEdit does not respond to mouse or
> keyboard input.
>
> I tried to bisect the recent changes, and the problem seams to be appear
> with the changeset
>
>  0fc032898b05: back to cumulative treatment of command status, which is
>                important for total accounting (amending
> 8201790fdeb9);).

Thanks for keeping an eye on it, and doing the bisection already.

At first I did not believe the result, because 0fc032898b05 looks quite
innocent.  Some hours later, I realized that the use of local value
definition within a 'for' comprehension always entails a 'yield', which
means there is a potentially expensive map of the whole structure involved
("The Scala Language Specification Version 2.9", section 6.19).

The following changeset adddresses that:

# HG changeset patch
# User wenzelm
# Date 1396383901 -7200
#      Tue Apr 01 22:25:01 2014 +0200
# Node ID 1a9f569b5b7e16760fc419df8f17e7216be795c7
# Parent  a6f8c3566560fd9e8955c7240f4ac19cdc9e037d
some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);

diff -r a6f8c3566560 -r 1a9f569b5b7e src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 01 20:22:25 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Apr 01 22:25:01 2014 +0200
@@ -114,11 +114,11 @@
      var finished = 0
      var warned = 0
      var failed = 0
-    for {
-      command <- node.commands
-      states = state.command_states(version, command)
-      status = command_status(states.iterator.flatMap(st => st.status.iterator))
-    } {
+    for { command <- node.commands }
+    {
+      val states = state.command_states(version, command)
+      val status = command_status(states.iterator.flatMap(st => st.status.iterator))
+
        if (status.is_running) running += 1
        else if (status.is_finished) {
          val warning = states.exists(st => st.results.entries.exists(p => is_warning(p._2)))

The node.commands structure contains all command spans of the theory, 
which can be quite substantial especially in Multivariate_Analysis.  The 
plain iteration over the structure is already a bit slow, but a few 
redundant maps of it can be deadly to real-time performance.


 	Makarius