# HG changeset patch
# User wenzelm
# Date 1221578917 -7200
# Node ID 04fc1ba19f93405e1d9d6886927479e2811c3277
# Parent  79b8efed66bf4f8a594b6b1928512ad59223ddcc
tuned;

diff -r 79b8efed66bf -r 04fc1ba19f93 doc-src/System/Thy/Misc.thy
--- a/doc-src/System/Thy/Misc.thy	Tue Sep 16 17:21:14 2008 +0200
+++ b/doc-src/System/Thy/Misc.thy	Tue Sep 16 17:28:37 2008 +0200
@@ -15,7 +15,7 @@
 section {* The Proof General / Emacs interface *}
 
 text {*
-  The @{tool_def emacs} tool invokes a version of Emacs with Proof
+  The @{tool_def emacs} tool invokes a version of Emacs and Proof
   General within the regular Isabelle settings environment
   (\secref{sec:settings}).  This is more robust than starting Emacs
   separately, loading the Proof General lisp files, and then
@@ -26,10 +26,8 @@
   distribution~\cite{proofgeneral}; its usage depends on the
   particular version.  There are some options available, such as
   @{verbatim "-l"} for passing the logic image to be used by default,
-  or @{verbatim "-m"} to tune the standard print mode.
-
-  The following Isabelle settings are particularly important for Proof
-  General:
+  or @{verbatim "-m"} to tune the standard print mode.  The following
+  Isabelle settings are particularly important for Proof General:
 
   \begin{description}
 
@@ -44,7 +42,7 @@
 
   \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell
   script to install the X11 fonts required for the X-Symbols mode of
-  Proof General.  This is only required if the X11 display server runs
+  Proof General.  This is only relevant if the X11 display server runs
   on a different machine than the Emacs application, with a different
   file-system view on the Proof General installation.  Under most
   circumstances Proof General is able to refer to the font files that
diff -r 79b8efed66bf -r 04fc1ba19f93 doc-src/System/Thy/document/Misc.tex
--- a/doc-src/System/Thy/document/Misc.tex	Tue Sep 16 17:21:14 2008 +0200
+++ b/doc-src/System/Thy/document/Misc.tex	Tue Sep 16 17:28:37 2008 +0200
@@ -35,7 +35,7 @@
 \isamarkuptrue%
 %
 \begin{isamarkuptext}%
-The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs with Proof
+The \indexdef{}{tool}{emacs}\hypertarget{tool.emacs}{\hyperlink{tool.emacs}{\mbox{\isa{\isatt{emacs}}}}} tool invokes a version of Emacs and Proof
   General within the regular Isabelle settings environment
   (\secref{sec:settings}).  This is more robust than starting Emacs
   separately, loading the Proof General lisp files, and then
@@ -46,10 +46,8 @@
   distribution~\cite{proofgeneral}; its usage depends on the
   particular version.  There are some options available, such as
   \verb|-l| for passing the logic image to be used by default,
-  or \verb|-m| to tune the standard print mode.
-
-  The following Isabelle settings are particularly important for Proof
-  General:
+  or \verb|-m| to tune the standard print mode.  The following
+  Isabelle settings are particularly important for Proof General:
 
   \begin{description}
 
@@ -63,7 +61,7 @@
 
   \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isacharunderscore}INSTALLFONTS}}}}}] may contain a small shell
   script to install the X11 fonts required for the X-Symbols mode of
-  Proof General.  This is only required if the X11 display server runs
+  Proof General.  This is only relevant if the X11 display server runs
   on a different machine than the Emacs application, with a different
   file-system view on the Proof General installation.  Under most
   circumstances Proof General is able to refer to the font files that