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

-*- mode:outline -*-

* Things to do for Isabelle/Isar

See also ../todo for generic things to do, priority codes.

** B switch to ProofGeneral.undo (after Isabelle99-1 is out!);

** C fix '{{' and '}}' keywords (e.g. proper font-lock, indentation);
unfortunately the present word boundary regexp does not work since { }
are already part of comment syntax;

** C undo 'use' command: unlock corresponding ML file;

** C interactive support for diagnostic commands: easy way to run
thm/prop/term/typ on region in an ad-hoc fashion;

** 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);

** C speedup indentation (rather do this at generic level?); would be
nice if current indentation stack would be somehow stored within the
extend(s) processed last;

** C eliminate explicit ";" terminator; rather refer to regexp (note:
requires {{ }} to be fixed; ideally, current set of keywords would be
retrieved from the running process, in order to gain robustness);

** C tune behaviour of goals/response buffers (e.g. hide empty
response buffers when using 2 buffer model);

** D Combine with isa/ to get single Isabelle PG instance, somehow?

Then users could use both proof languages.