diff options
| -rw-r--r-- | todo | 14 |
1 files changed, 14 insertions, 0 deletions
@@ -40,6 +40,14 @@ A* multiple files bug fix: --> One case now fixed by allowing current scripting buffer to be retracted. Are there other cases? (da to investigate) +C Strange behaviour when killing and re-visiting files that + haven't been completely processed. Since they stay on + the proof-included-files-list, on re-visiting, they are + marked atomic as completely processed! + Possible fix: if file hasn't been completely processed, + maybe retract (and hence remove from proof-included-files-list), + or query the user? + C The semantics of `proof-script-buffer-list' is ambigous. The first element is the current script buffer, we are not quite sure what role the other elements ought to have. We propose to abandon @@ -443,6 +451,12 @@ A Fixup multiple file handling with theory loader hacks to Isabelle. C derive an isa-response-mode from proof-response-mode; see lego.el (10min) +C Obscure process-handling problem which prevents goal appearing + when Isabelle HOL is started. Visit example.ML, do "next command". + Suggested process: debug proof-shell-filter. Has something to + do with annotated prompts. + (4h) + D Implement completion for Isabelle using tables generated by the running process. |