# HG changeset patch
# User wenzelm
# Date 1402689492 -7200
# Node ID ffa4be8277348c7598bcc76bccb347e640ef1eef
# Parent  5e7488f4309eb7334c7eb1d47d77355415615e36
tuned;

diff -r 5e7488f4309e -r ffa4be827734 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Jun 13 20:01:39 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Fri Jun 13 21:58:12 2014 +0200
@@ -613,11 +613,11 @@
   Isabelle/jEdit via its standard application wrapper (in contrast to
   @{verbatim "isabelle jedit"} run from the command line).
 
-  For convenience, Isabelle/jEdit imitates at least @{verbatim
-  "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the Java
-  process environment, in order to allow easy access to these important places
-  from the editor. The file browser of jEdit also includes \emph{Favorites}
-  for these two important locations.
+  For convenience, Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and
+  @{verbatim "$ISABELLE_HOME_USER"} within the Java process environment, in
+  order to allow easy access to these important places from the editor. The
+  file browser of jEdit also includes \emph{Favorites} for these two important
+  locations.
 
   \medskip Path specifications in prover input or output usually include
   formal markup that turns it into a hyperlink (see also
@@ -1117,10 +1117,10 @@
   may be completed to @{verbatim "foo"} or @{verbatim "foobar"}, if these are
   both known in the context.
 
-  The special identifier @{verbatim "__"} serves as a wild-card for arbitrary
-  completion: it exposes the name-space content to the completion mechanism
-  (truncated according to @{system_option completion_limit}). This is
-  occasionally useful to explore an unknown name-space, e.g.\ in some
+  The special identifier ``@{verbatim "__"}'' serves as a wild-card for
+  arbitrary completion: it exposes the name-space content to the completion
+  mechanism (truncated according to @{system_option completion_limit}). This
+  is occasionally useful to explore an unknown name-space, e.g.\ in some
   template.
 *}
 
@@ -1167,8 +1167,8 @@
 
   In exceptional situations, the prover may produce \emph{no completion}
   markup, to tell that some language keywords should be excluded from further
-  completion attempts. For example, @{verbatim ":"} within accepted Isar
-  syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
+  completion attempts. For example, ``@{verbatim ":"}'' within accepted Isar
+  syntax looses its meaning as abbreviation for symbol ``@{text "\<in>"}''.
 *}