diff options
Diffstat (limited to 'isa/todo')
| -rw-r--r-- | isa/todo | 27 |
1 files changed, 13 insertions, 14 deletions
@@ -1,15 +1,14 @@ -*- mode:outline -*- -* See also ../todo for generic things to do, priority codes. - * Things to do for Isabelle -=========================== -C Investigate fix for looping rewriting in Isabelle. Continual +See also ../todo for generic things to do, priority codes. + +** C Investigate fix for looping rewriting in Isabelle. Continual and frequent messages from the prover lock out the user. Is there any easy way of fixing this? -C X-Symbol support for theory files: bugs at the moment, because +** C X-Symbol support for theory files: bugs at the moment, because of duplicate calls to proof-x-symbol-mode and mess with font-lock initialization. Problem with current version: visit a.thy, b.thy then turn on xsym. Broken in b.thy. @@ -19,22 +18,22 @@ C X-Symbol support for theory files: bugs at the moment, because [DvO reports okay]. (May need to split extra modes into two parts?) -B auto-adjust Pretty.setmargin when window is resized. Use +** B auto-adjust Pretty.setmargin when window is resized. Use generic code once it's implemented. -D Implement completion for Isabelle using tables generated by +** D Implement completion for Isabelle using tables generated by the running process. Ideally context sensitive. Would be a nice addition. (1 week) -D Add useful specific commands for Isabelle. Many could +** D Add useful specific commands for Isabelle. Many could be added. Would be better to merge in Isamode's menus. (however, probably 2 week's work to bring together Isamode and proof.el, making some of Isamode generic) -D Switching to other file with C-c C-o could be more savy +** D Switching to other file with C-c C-o could be more savy with file names and extensions (use some standard function?) -X weird bug: interrupting Isabelle process (under sml-nj) sometimes +** X weird bug: interrupting Isabelle process (under sml-nj) sometimes doesn't return, why? (see first half of interrupt error only: *** Interrupt. @@ -58,15 +57,15 @@ X weird bug: interrupting Isabelle process (under sml-nj) sometimes ProofGeneral.isa_restart(); /usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b -X Add ability to choose logic. Maybe not necessary: can use default +** X Add ability to choose logic. Maybe not necessary: can use default set in Isabelle settings nowadays, in the premise that most people stick to a particular logic? But then no support for loading user-saved databases. (ponder this) -X Write perl scripts to generate TAGS file for ML and thy files. - (6h, I've completely forgotten perl). +** X Write perl scripts to generate TAGS file for ML and thy files. + (6h, any volunteers?). -X Manage multiple proofs, perhaps by automatically inserting +** X Manage multiple proofs, perhaps by automatically inserting push_proof() and pop_proof() commands into the proof script. But would lead to unholy mess for script management! |