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
50
51
52
53
54
55
56

-*- 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 Isabelle support for ML and legacy files: would like to remove "isa" instance
     Could we handle theory files and even allow scripting in ML files
     at the same time as Isar?  Maybe not, if this is even beyond what
     Isar interface would allow (unless we send an ML file
     line-by-line with ML_command?)

** 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 (hard; needs major reworking of
     Isabelle's pretty-printing subsystem);