# HG changeset patch
# User wenzelm
# Date 1444671145 -7200
# Node ID 9020a3ba6c9adb086912b429547cb90bb40cd09d
# Parent  7ba7b81035653e4051c72316318f496b257fc55f
@{verbatim [display]} supersedes old alltt/ttbox;

diff -r 7ba7b8103565 -r 9020a3ba6c9a src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Mon Oct 12 19:32:25 2015 +0200
@@ -1036,12 +1036,11 @@
 text \<open>The ML datatype @{ML_type Ast.ast} explicitly represents the
   intermediate AST format that is used for syntax rewriting
   (\secref{sec:syn-trans}).  It is defined in ML as follows:
-  \begin{ttbox}
-  datatype ast =
-    Constant of string |
-    Variable of string |
-    Appl of ast list
-  \end{ttbox}
+  @{verbatim [display]
+\<open>datatype ast =
+  Constant of string |
+  Variable of string |
+  Appl of ast list\<close>}
 
   An AST is either an atom (constant or variable) or a list of (at
   least two) subtrees.  Occasional diagnostic output of ASTs uses
diff -r 7ba7b8103565 -r 9020a3ba6c9a src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Mon Oct 12 19:32:25 2015 +0200
@@ -484,11 +484,7 @@
   of @{command "show"} predicts potential failure and displays the
   resulting error as a warning beforehand.  Watch out for the
   following message:
-
-  %FIXME proper antiquotation
-  \begin{ttbox}
-  Problem! Local statement will fail to solve any pending goal
-  \end{ttbox}
+  @{verbatim [display] \<open>Local statement fails to refine any pending goal\<close>}
 
   \item @{command "hence"} abbreviates ``@{command "then"}~@{command
   "have"}'', i.e.\ claims a local goal to be proven by forward
diff -r 7ba7b8103565 -r 9020a3ba6c9a src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon Oct 12 19:32:25 2015 +0200
@@ -222,8 +222,8 @@
   Nonetheless it is occasionally useful to invoke the Prover IDE on the
   command-line, with some extra options and environment settings as explained
   below. The command-line usage of @{tool_def jedit} is as follows:
-\begin{ttbox}
-  Usage: isabelle jedit [OPTIONS] [FILES ...]
+  @{verbatim [display]
+\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
 
   Options are:
     -J OPTION    add JVM runtime option
@@ -237,8 +237,7 @@
     -s           system build mode for session image
 
   Start jEdit with Isabelle plugin setup and open theory FILES
-  (default "\$USER_HOME/Scratch.thy").
-\end{ttbox}
+  (default "$USER_HOME/Scratch.thy").\<close>}
 
   The @{verbatim "-l"} option specifies the session name of the logic
   image to be used for proof processing.  Additional session root
diff -r 7ba7b8103565 -r 9020a3ba6c9a src/Doc/JEdit/document/root.tex
--- a/src/Doc/JEdit/document/root.tex	Mon Oct 12 18:18:48 2015 +0200
+++ b/src/Doc/JEdit/document/root.tex	Mon Oct 12 19:32:25 2015 +0200
@@ -18,6 +18,7 @@
 \isadroptag{theory}
 
 \isabellestyle{literal}
+\def\isastylett{\footnotesize\tt}
 
 \title{\includegraphics[scale=0.5]{isabelle_jedit} \\[4ex] Isabelle/jEdit}