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
57
58
59
60
61
62
|
-*- mode:outline -*-
* Things to do for Isabelle
See also ../todo for generic things to do, priority codes.
See also ../isar/todo. Isar is now main instance for PG, this
instance less supported.
** X Isabelle PG: Non-blocking for .thy loading from .ML files.
** D Isabelle: I think show_sorts -> show_types, how can we reflect this ?
** D Fix mode naming for Isabelle
(might like isa-proofscript-mode -> isa-mode;
but this conflicts with entry mechanism for thy/isa mode).
** D Might be nice to unify menus a little more, e.g. add Isabelle for .thy
But several of the ops there are not relevant for theory files.
Well, favourites at least. What we have at the moment is verging
GUI-atrocity: one shouldn't have menus of the same name with
different entries, but should rather use greyed out.
** C Improvements to Isabelle that would be nice for Proof General:
-- ability to remove theorem from theorem database, issued
when undoing qed
** C X-Symbol support for theory files: bugs at the moment, because
of duplicate calls to proof-x-symbol-mode and mess with
font-lock initialization. Problem with current version:
visit a.thy, b.thy then turn on xsym. Broken in b.thy.
Seems okay visiting new buffers after that.
Must also check interaction with xsym-isa-latex stuff
may be broken by removal of mode hook settings.
[DvO reports okay].
(May need to split extra modes into two parts?)
** B auto-adjust Pretty.setmargin when window is resized. Use
generic code once it's implemented.
** D Implement completion for Isabelle using tables generated by
the running process. Ideally context sensitive.
Would be a nice addition. (1 week)
** D Add useful specific commands for Isabelle. Many could
be added. Would be better to merge in Isamode's menus.
(however, probably 2 week's work to bring together Isamode
and proof.el, making some of Isamode generic)
** D Switching to other file with C-c C-o could be more savy
with file names and extensions (use some standard function?)
** X Write perl scripts to generate TAGS file for ML and thy files.
(60h, any volunteers?) (hard);
** X Manage multiple proofs, perhaps by automatically inserting
push_proof() and pop_proof() commands into the proof script.
But would lead to unholy mess for script management! (hard!)
|
