diff options
| -rw-r--r-- | todo | 41 |
1 files changed, 11 insertions, 30 deletions
@@ -383,35 +383,16 @@ C Improve coqtags. I cannot handle lists e.g., with * Here are things to be done to Isabelle Mode ============================================= -A* Add annotations to prompt and output. +A* Fix bug in undo, maybe related to below? -B Intermittent problems parsing output. Seems to depend on - what has been run before. E.g. first time starting process - might not display goal. Try to find repeatable case. +A* Fix output handling routines to not display parts of messages. + Intermittent problems parsing output. Seems to depend on + what has been run before. E.g. first time starting process + might not display goal. Try to find repeatable case. -B CRUCIAL: Do something to manage .thy and .ML files coherently. - At the moment loading one into Isabelle will force the - processing of the other. We could ask that users develop - proof scripts in another kind of file entirely, or a file - with a different name. But that's an ugly hack. - But what else can we do?? - (Probably answer: Isabelle needs to support non-automatic - reading of ML file: a function "use_thy_only" ). +A* Add annotations to prompt and output using Isabelle's ml_prompts. -B (part of above): Handle proof-retract-file by querying Isabelle - about the decendants of a file. Then all the descendents can - also be unlocked. - -B (part of above): add multiple file handling for Isabelle - (4h). - Work left to do: - - test sending of "retract_file" command to Isabelle. - Handle theory files better. - - -X Write perl scripts to generate TAGS file for ML and thy files. - (6h, I've completely forgotten perl), or better: +A* Make theory files go blue. D Implement completion for Isabelle using tables generated by the running process. @@ -427,11 +408,11 @@ D Add ability to choose logic. Maybe not necessary: can use default user-saved databases. (ponder this) -X New features ideas: - 1. Manage multiple proofs (markers in possibly different buffers) - -B Set wakeup-char by using Isabelle's ml-prompts function. +X Write perl scripts to generate TAGS file for ML and thy files. + (6h, I've completely forgotten perl), or better: +X Manage multiple proofs (markers in possibly different buffers) + X Add Isabelle logo to splash screen. (30 mins) * FSF Emacs |