aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa/BUGS
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.