Opened 13 years ago
Closed 13 years ago
#387 closed defect (fixed)
Preferences lost when prover restarted
| Reported by: | Makarius | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.1 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | makarius@… |
Description
When starting the prover process, defaults are received, but current values on the PG side are not sent.
This means, users cannot work with persistent prefs at the moment.
Attachments (1)
Change History (7)
comment:1 Changed 13 years ago by
comment:3 Changed 13 years ago by
Looking at the *isabelle* buffer, there is never a setpref message as it used to be.
Getting into this situation should be trivial, e.g. start prover, change settings, save settings, stop prover, start prover.
In ProofGeneral-4.1pre101216 it works better, but might require a few rounds of change settings, save settings until it is really persistent.
comment:4 Changed 13 years ago by
| Status: | new → accepted |
|---|
Confirmed: nothing to do with the float upgrade, rather it stems from trying to smoothly support both dynamic configuration settings (potentially varying with each prover invocation) and static ones which are declared directly in the elisp.
The CVS server seems to be having problems at the moment, but a one-line workaround patch is to remove the call to makunbound on line 77 of proof-compat.el. This call has the bad effect of losing user customizations when the prover gets started for the second time in an Emacs session.
I have a more sophisticated fix for PG 4.1, for when CVS is back up, but suggest you take that simple one-line fix for Isabelle2011's PG.
The smarter fix allows for changing sets of preferences between different Isabelle invocations --- I'm not sure if that ever happens (perhaps with a change in object logic?). If it does, and the user has configured a setting which is not in the new invocation, startup may generate an error. (Workaround: new Emacs, don't change such settings...)
Changed 13 years ago by
| Attachment: | repeat-hasprefs-bug.patch added |
|---|
Simple patch to prevent loss of settings
comment:5 Changed 13 years ago by
| Summary: | Preferences not sent to prover on startup → Preferences lost when prover restarted |
|---|
comment:6 Changed 13 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | accepted → closed |
More elaborate fix in CVS now. The CVS version allows for different prover invocations to use different sets of dynamic settings (i.e., those returned from PGIP askprefs messages), but only the most recent set of settings will be saved/reset by Isabelle -> Settings -> Save Settings.
As an additional improvement, the revised code only sends setpref commands for settings which are different from the prover defaults.
This appears to be some collateral damage caused by the attempt to upgrade PGIP to support floats.
In ProofGeneral-4.1pre101216 it appears to work, i.e. that is the version we will take as a basis for Isabelle2011.