blob: a6a3eec23a4751ace4cabf1782a639069b5198b2 (
plain)
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
|
-*- mode:outline -*-
* Isabelle Proof General Bugs
See also ../BUGS for generic bugs.
** set proof_timing is problematic
It will make the goals display disappear during proof. This is
because Proof General only displays goals output that appears *after*
Isabelle messages, but Isabelle prints the timing message after the
goals are displayed.
** General difficulty with proof scripts containing ML structures, etc.
Proof General does not understand full ML syntax(!), so it will be
confused by structures which contain semi-colons after declarations,
for example. Also, it cannot undo function declarations. See the
section on ML files in the manual for more details.
** Blocking when processing multiple files, beginning from a .ML file.
Proof General will block the Emacs process when it is waiting for a
theory file (and it's ancestors) to be read as scripting is turned on.
To avoid this, assert the theory file rather than the ML file.
|
