Custom Query (361 matches)
Results (34 - 36 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#197 | fixed | Non-persistance of Unicode Tokens / Math Menu (Carbon Emacs 1.6.0) | ||
Description |
Using native Carbon Emacs 1.6.0 on Mac OS 10.4.x the Unicode Tokens and Unicode Math Menu custom settings do not really persist. For example: start Proof General (via isar/interface script), then enable both options --- works fine. Now safe safe options: resulting .emacs file only holds information for isar-maths-menu-enable and when restarting PG/Emacs only this option is enabled. After editing the .emacs file to set isar-unicode-tokens-enable as well, the corresponding menu item is ticked, but shaded, i.e. cannot be changed. Moreover, neither this mode nor the math menu are enabled. |
|||
#198 | fixed | Prover executable not found when running without interface script | ||
Description |
Using Carbon Emacs 1.6.0 without the isar/interface script, but loading .../PG/generic/proof-site.el manually, results in a non-functional environment.
When enabling PG by vising a thy file, the location of isatool is queried as expected. Nevertheless, trying to start the prover produces this error:
A brief look at the elisp sources reveals a slightly untidy situation: isatool and isabelle executable locations are not really corellated. With isatool available one could just do |
|||
#201 | fixed | X-Symbol only half enabled (Emacs: yes, prover: no) | ||
Description |
Linux (SuSE or Ubuntu) and xemacs-21.4.x Running the isabelle-interface script with option -x true (for X-Symbols) does not fully enable xsymbols mode; in the Emacs buffer symbols are rendered as expected, but the prover does not have the "xsymbols" print_mode enabled. After manual disabling and re-enabling in the PG/Options menu, xsymbols work as expected. |