--- a/src/Doc/IsarImplementation/ML.thy Sat Jan 26 16:10:50 2013 +0100
+++ b/src/Doc/IsarImplementation/ML.thy Sat Jan 26 16:30:47 2013 +0100
@@ -1050,7 +1050,7 @@
\begin{warn}
The actual error channel is accessed via @{ML Output.error_msg}, but
- the interaction protocol of Proof~General \emph{crashes} if that
+ the old interaction protocol of Proof~General \emph{crashes} if that
function is used in regular ML code: error output and toplevel
command failure always need to coincide.
\end{warn}
--- a/src/Doc/IsarRef/Outer_Syntax.thy Sat Jan 26 16:10:50 2013 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy Sat Jan 26 16:30:47 2013 +0100
@@ -41,11 +41,12 @@
clearly recognized from the input syntax, e.g.\ encounter of the
next command keyword.
- More advanced interfaces such as Proof~General \cite{proofgeneral}
- do not require explicit semicolons, the amount of input text is
- determined automatically by inspecting the present content of the
- Emacs text buffer. In the printed presentation of Isabelle/Isar
- documents semicolons are omitted altogether for readability.
+ More advanced interfaces such as Isabelle/jEdit \cite{Wenzel:2012}
+ and Proof~General \cite{proofgeneral} do not require explicit
+ semicolons, the amount of input text is determined automatically by
+ inspecting the present content of the Emacs text buffer. In the
+ printed presentation of Isabelle/Isar documents semicolons are
+ omitted altogether for readability.
\begin{warn}
Proof~General requires certain syntax classification tables in
--- a/src/Doc/IsarRef/Preface.thy Sat Jan 26 16:10:50 2013 +0100
+++ b/src/Doc/IsarRef/Preface.thy Sat Jan 26 16:30:47 2013 +0100
@@ -17,12 +17,16 @@
theory and proof development. Compared to raw ML, the Isabelle/Isar
top-level provides a more robust and comfortable development
platform, with proper support for theory development graphs, managed
- transactions with unlimited undo etc. The Isabelle/Isar version of
- the \emph{Proof~General} user interface
- \cite{proofgeneral,Aspinall:TACAS:2000} provides a decent front-end
- for interactive theory and proof development in this advanced
- theorem proving environment, even though it is somewhat biased
- towards old-style proof scripts.
+ transactions with unlimited undo etc.
+
+ In its pioneering times, the Isabelle/Isar version of the
+ \emph{Proof~General} user interface
+ \cite{proofgeneral,Aspinall:TACAS:2000} has contributed to the
+ success of for interactive theory and proof development in this
+ advanced theorem proving environment, even though it was somewhat
+ biased towards old-style proof scripts. The more recent
+ Isabelle/jEdit Prover IDE \cite{Wenzel:2012} emphasizes the
+ document-oriented approach of Isabelle/Isar again more explicitly.
\medskip Apart from the technical advances over bare-bones ML
programming, the main purpose of the Isar language is to provide a
--- a/src/Doc/manual.bib Sat Jan 26 16:10:50 2013 +0100
+++ b/src/Doc/manual.bib Sat Jan 26 16:30:47 2013 +0100
@@ -1792,6 +1792,16 @@
editor = {Dos Reis, G. and L. Th\'ery},
publisher = {ACM Digital Library}}
+@InProceedings{Wenzel:2012,
+ author = {Makarius Wenzel},
+ title = {{Isabelle/jEdit} --- a {Prover IDE} within the {PIDE} framework},
+ booktitle = {Conference on Intelligent Computer Mathematics (CICM 2012)},
+ year = 2012,
+ editor = {J. Jeuring and others},
+ volume = 7362,
+ series = {LNAI},
+ publisher = {Springer}}
+
@book{principia,
author = {A. N. Whitehead and B. Russell},
title = {Principia Mathematica},