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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
|
-*- mode:outline -*-
* Things to do for Isabelle
See also ../todo for generic things to do, priority codes.
** 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 Investigate fix for looping rewriting in Isabelle. Continual
and frequent messages from the prover lock out the user.
Is there any easy way of fixing this?
** 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 weird bug: interrupting Isabelle process (under sml-nj) sometimes
doesn't return, why? (see first half of interrupt error only:
*** Interrupt.
*** At command "time_use".
uncaught exception ERROR
raised at: library.ML:1100.35-1100.40
But not "uncaught exception" part.
What is worse: prompt disappears! But process still seems to be
there underneath. Not sure where this bug comes from.
Moreover, killing process then hangs Emacs with message
"cleaning up", and get error
(1) (error/warning) Error in process sentinel: (no-catch exited t)
To see if this is some SML/NJ or Isabelle weirdness, test in
xterm: use "ROOT.ML", interrrupt, use "ROOT.ML" again.
sig 11! (flaky hardware?)
/usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2ad09c43
Not reliably repeatable, but:
ProofGeneral.isa_restart();
/usr/lib/Isabelle_22-Sep-1999/../../share/smlnj/bin/sml: Fatal error -- unexpected fault, signal = 11, code = 0x2af9e01b
** 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!)
|
