Opened 16 years ago
Last modified 11 years ago
#240 assigned defect
Bad behaviour in startup when proof executables (isabelle, isatool) not found — at Version 2
| Reported by: | David Aspinall | Owned by: | Graham Dutton |
|---|---|---|---|
| Priority: | minor | Milestone: | |
| Component: | 1:pg-eclipse | Keywords: | |
| Cc: |
Description (last modified by )
If the workbench is started when an editor on a script file is open, the user is shown the dialog for entering a path, but the system repeatedly tries the broken path. If the workbench is started without an open editor, it hangs when the first editor is opened.
Change History (3)
comment:1 Changed 16 years ago by
| Owner: | changed from David Aspinall to Graham Dutton |
|---|---|
| Status: | new → assigned |
comment:2 Changed 16 years ago by
| Description: | modified (diff) |
|---|
Seems this change is not good enough: fetching a session manager is the main path for starting the prover now! What we can try to do is to keep a flag indicating whether the prover path is invalid, and not attempt to start the prover if this flag suggests it shouldn't be started. Probably also need a method to explicitly check/start prover before main actions, then popping up dialog is OK.
Note: See
TracTickets for help on using
tickets.
Fixed repeated attempts to startup prover by using additional flag to SessionManager? constructor when displaying dialog. However, there is still a deadlock when the wizard is used to create a new theory file without finding the "isabelle" executable.