# HG changeset patch
# User wenzelm
# Date 1359214247 -3600
# Node ID 98c48d023136f5b22e95ea652219ffe995da563f
# Parent  a22b134f862e794a1f6b975f31fcfd899151f10e
some updates concerning Proof General;

diff -r a22b134f862e -r 98c48d023136 src/Doc/IsarImplementation/ML.thy
--- 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}
diff -r a22b134f862e -r 98c48d023136 src/Doc/IsarRef/Outer_Syntax.thy
--- 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
diff -r a22b134f862e -r 98c48d023136 src/Doc/IsarRef/Preface.thy
--- 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
diff -r a22b134f862e -r 98c48d023136 src/Doc/manual.bib
--- 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},