Opened 17 years ago
Last modified 11 years ago
#27 new defect
Efficiency problems with larger files and larger outputs
Reported by: | Owned by: | David Aspinall | |
---|---|---|---|
Priority: | major | Milestone: | |
Component: | 1:pg-eclipse | Keywords: | |
Cc: |
Description
Try processing BigTheory?.thy and compare time taken in Eclipse with Emacs PG. TraceSimp?.thy tends to crash the system (also a challenge for Emacs). We should do *much* better here.
A likely culprit is processing so many events on every message that gets sent, and trying to display output at every step. So things get worse the more editors/views that are open, even though most of them are completely uninterested in the events passed in.
Ahsan's branch has improvements for events which we should port back (SessionManager? has single filter, listeners register for events they're interested in rather than every kind of PGIP message). Anyway, the event model should be investigated, documented, justified (seems possible many events are spurious/avoidable).
PGIP supports <startquiet>
and <stopquiet>
which should be used.
Test cases AThousandXXX.thy
also show up problems pretty easily.
Change History (2)
comment:1 Changed 17 years ago by
Milestone: | PG-Eclipse-1.0.6 → PG-Eclipse-1.0.7 |
---|
comment:2 Changed 11 years ago by
Milestone: | PG-Eclipse-1.0.7 |
---|
Milestone PG-Eclipse-1.0.7 deleted