equal
deleted
inserted
replaced
10 |
10 |
11 text {* |
11 text {* |
12 Isabelle/jEdit is a Prover IDE that integrates \emph{parallel proof |
12 Isabelle/jEdit is a Prover IDE that integrates \emph{parallel proof |
13 checking} @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with |
13 checking} @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with |
14 \emph{asynchronous user interaction} @{cite "Wenzel:2010" and |
14 \emph{asynchronous user interaction} @{cite "Wenzel:2010" and |
15 "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE"}, based on a |
15 "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, |
16 document-oriented approach to \emph{continuous proof processing} @{cite |
16 based on a document-oriented approach to \emph{continuous proof processing} |
17 "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system components |
17 @{cite "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system |
18 are fit together in order to make this work. The main building blocks are as |
18 components are fit together in order to make this work. The main building |
19 follows. |
19 blocks are as follows. |
20 |
20 |
21 \begin{description} |
21 \begin{description} |
22 |
22 |
23 \item [PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. |
23 \item [PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. |
24 It is built around a concept of parallel and asynchronous document |
24 It is built around a concept of parallel and asynchronous document |