isar/todo


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
44
45
46
47
48
49

-*- 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 theorem dependencies: using Isar's "thm" command does not
   work at top level.  This is annoying for browsing the fully
   qualified dependency names.  (Even the ML_command "thm"
   returns unknown theory context error).  Can we use something
   else?

** 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 (vary hard);