diff options
author | 2007-12-13 12:58:11 +0000 | |
---|---|---|
committer | 2007-12-13 12:58:11 +0000 | |
commit | d64389d34f3494b97c67b7a6094123f1a699040c (patch) | |
tree | 67c8fd95283d89a960240200970a9a2b134cb67b /isar | |
parent | 44d5bf78ff00eb2d48f111d8d8718aa3b8ad010c (diff) |
Deleted file
Diffstat (limited to 'isar')
-rw-r--r-- | isar/todo | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/isar/todo b/isar/todo deleted file mode 100644 index cfb5578e..00000000 --- a/isar/todo +++ /dev/null @@ -1,43 +0,0 @@ --*- mode:outline -*- - -* Things to do for Isabelle/Isar [maintainers' list] - -See also ../todo for generic things to do, priority codes. - -** C Improve handling of multiple files - We should recognize error messages from theory loader, in this form: - - \<^sync>ProofGeneral.inform_file_processed "/home/da/projects/proofgen/cvs/ProofGeneral/etc/isar/multiple/A.thy"; \<^sync>; -### Unknown theory "A" -### Theory loader: undefined theory entry for "A" -### Failed to register theory "A" - - (Although actually this case represents a bug elsewhere: - PG should not ask Isabelle to register some theory it doesn't know) - [Idea: maybe we need a sync-loaded-files possibility] - - NB: Multiple file handling has been repaired compared with PG 3.4, - by adding the setting `proof-cannot-reopen-processed-files'. - -** C Adjust imenu/fume to get sections/chapters usefully in tags - Need to grab a prefix of text from the markup section {* Foo *} - -** C Electric terminator for non-terminator provers would be nice. - -** B Proof nesting depth calculation not right: see debug messages - -** B Isabelle tweaks - -- theorem dependencies on spoils ordinary response buffer output - (dependency info *after* response display loses) - -** B visualise dependencies: sometimes not applicable. - Also, does not work at the moment. - -** C func-menu: - observe proof-syntactic-context (general problem of func-menu setup?); - -** C undo 'use' command: unlock corresponding ML file; - -** C provide template for empty theory (or even just for Scratch.thy); - -** C proper proof-by-pointing support (very hard); |