blob: cfb5578e8ed31e98d07a3e5742a76eba083ad06c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
|
-*- 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);
|