diff -r 760e21900b01 -r 28e788ca2c5d src/Doc/System/Scala.thy
--- a/src/Doc/System/Scala.thy	Thu Oct 22 21:16:27 2015 +0200
+++ b/src/Doc/System/Scala.thy	Thu Oct 22 21:16:49 2015 +0200
@@ -17,18 +17,17 @@
 text \<open>The @{tool_def java} tool is a direct wrapper for the Java
   Runtime Environment, within the regular Isabelle settings
   environment (\secref{sec:settings}).  The command line arguments are
-  that of the underlying Java version.  It is run in @{verbatim
-  "-server"} mode if possible, to improve performance (at the cost of
-  extra startup time).
+  that of the underlying Java version.  It is run in \<^verbatim>\<open>-server\<close> mode
+  if possible, to improve performance (at the cost of extra startup time).
 
-  The @{verbatim java} executable is the one within @{setting
+  The \<^verbatim>\<open>java\<close> executable is the one within @{setting
   ISABELLE_JDK_HOME}, according to the standard directory layout for
   official JDK distributions.  The class loader is augmented such that
-  the name space of @{verbatim "Isabelle/Pure.jar"} is available,
+  the name space of \<^verbatim>\<open>Isabelle/Pure.jar\<close> is available,
   which is the main Isabelle/Scala module.
 
   For example, the following command-line invokes the main method of
-  class @{verbatim isabelle.GUI_Setup}, which opens a windows with
+  class \<^verbatim>\<open>isabelle.GUI_Setup\<close>, which opens a windows with
   some diagnostic information about the Isabelle environment:
   @{verbatim [display] \<open>isabelle java isabelle.GUI_Setup\<close>}
 \<close>
@@ -58,7 +57,7 @@
 
   This allows to compile further Scala modules, depending on existing
   Isabelle/Scala functionality.  The resulting class or jar files can
-  be added to the Java classpath using the @{verbatim classpath} Bash
+  be added to the Java classpath using the \<^verbatim>\<open>classpath\<close> Bash
   function that is provided by the Isabelle process environment.  Thus
   add-on components can register themselves in a modular manner, see
   also \secref{sec:components}.