32 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent |
32 <li>Dockable panels (e.g. <em>Output</em>) are managed as independent |
33 windows by jEdit, which also allows multiple instances.</li> |
33 windows by jEdit, which also allows multiple instances.</li> |
34 |
34 |
35 </ul> |
35 </ul> |
36 |
36 |
|
37 <h2>Limitations and workrounds (January 2011)</h2> |
|
38 |
|
39 <ul> |
|
40 <li>No way to start/stop prover or switch to a different logic.<br/> |
|
41 <em>Workaround:</em> Change options and restart editor.</li> |
|
42 |
|
43 <li>Multiple theory buffers cannot depend on each other, imports are |
|
44 resolved via the file-system.<br/> |
|
45 <em>Workaround:</em> Save/reload files manually.</li> |
|
46 |
|
47 <li>No reclaiming of old/unused document versions in prover or |
|
48 editor.<br/> |
|
49 <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li> |
|
50 |
|
51 <li>Incremental reparsing sometimes produces unexpected command |
|
52 spans.<br/> |
|
53 <em>Workaround:</em> Cut/paste larger parts or reload buffer.</li> |
|
54 |
|
55 <li>Command execution sometimes gets stuck (purple background).<br/> |
|
56 <em>Workaround:</em> Force reparsing as above.</li> |
|
57 |
|
58 <li>Odd behavior of some diagnostic commands, notably those |
|
59 starting external processes asynchronously |
|
60 (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/> |
|
61 <em>Workaround:</em> Avoid such commands.</li> |
|
62 |
|
63 <li>No support for non-local markup, e.g. commands reporting on |
|
64 previous commands (proof end on proof head), or markup produced by |
|
65 loading external files.</li> |
|
66 |
|
67 <li>General lack of various conveniences known from Proof |
|
68 General.</li> |
|
69 </ul> |
|
70 |
37 </body> |
71 </body> |
38 </html> |
72 </html> |
39 |
73 |