equal
deleted
inserted
replaced
13 <body> |
13 <body> |
14 |
14 |
15 <center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center> |
15 <center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center> |
16 |
16 |
17 <p> |
17 <p> |
18 <b>PIDE</b> is a novel framework for sophisticated Prover IDEs, |
18 <b>PIDE</b> is a framework for sophisticated Prover IDEs, |
19 based on Isabelle/Scala technology that is integrated with Isabelle. |
19 based on Isabelle/Scala technology that is integrated with Isabelle. |
20 It is built around a concept of |
20 It is built around a concept of |
21 <em>asynchronous document processing</em>, which is supported |
21 <em>asynchronous document processing</em>, which is supported |
22 natively by the <em>parallel proof engine</em> implemented in Isabelle/ML. |
22 natively by the <em>parallel proof engine</em> implemented in Isabelle/ML. |
23 </p> |
23 </p> |
24 |
24 |
25 <p> |
25 <p> |
26 <b>Isabelle/jEdit</b> is an example application within the PIDE |
26 <b>Isabelle/jEdit</b> is the main example application within the PIDE |
27 framework — it illustrates many of the ideas in a realistic |
27 framework — it illustrates many of the ideas in a realistic |
28 manner, ready to be used right now in Isabelle applications. |
28 manner, ready to be used right now in Isabelle applications. |
29 </p> |
29 </p> |
30 |
30 |
31 <p> |
31 <p> |
158 |
158 |
159 |
159 |
160 <h2>Limitations and workarounds</h2> |
160 <h2>Limitations and workarounds</h2> |
161 |
161 |
162 <ul> |
162 <ul> |
163 <li>No way to start/stop prover or switch to a different logic.<br/> |
|
164 <em>Workaround:</em> Change options and restart editor.</li> |
|
165 |
|
166 <li>Odd behavior of some diagnostic commands, notably those starting |
163 <li>Odd behavior of some diagnostic commands, notably those starting |
167 external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/> |
164 external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/> |
168 <em>Workaround:</em> Avoid such commands.</li> |
165 <em>Workaround:</em> Avoid such commands.</li> |
169 |
166 |
170 <li>Lack of dependency managed for auxiliary files that contribute |
167 <li>Lack of dependency managed for auxiliary files that contribute |
177 worst-case situation.</li> |
174 worst-case situation.</li> |
178 |
175 |
179 <li>No support for non-local markup, e.g. commands reporting on |
176 <li>No support for non-local markup, e.g. commands reporting on |
180 previous commands (proof end on proof head), or markup produced by |
177 previous commands (proof end on proof head), or markup produced by |
181 loading external files.</li> |
178 loading external files.</li> |
182 |
|
183 <li>Lack of a few conveniences known from Proof General.</li> |
|
184 </ul> |
179 </ul> |
185 |
180 |
186 |
181 |
187 <h2>Known problems with Mac OS X</h2> |
182 <h2>Known problems with Mac OS X</h2> |
188 |
183 |