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_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
