# HG changeset patch
# User wenzelm
# Date 1445193836 -7200
# Node ID 6cc07122ca1486f8ed268c78fea2a3bc563177dd
# Parent  34d1913f0b208c865246af02780da2e89e700dd7
clarified;

diff -r 34d1913f0b20 -r 6cc07122ca14 src/Doc/Isar_Ref/Document_Preparation.thy
--- a/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Oct 18 20:28:29 2015 +0200
+++ b/src/Doc/Isar_Ref/Document_Preparation.thy	Sun Oct 18 20:43:56 2015 +0200
@@ -134,15 +134,18 @@
   \<^medskip>
   Antiquotations are in general written @{verbatim "@{"}@{text "name
   [options] arguments"}@{verbatim "}"}. The short form @{verbatim
-  "\<^name>"}@{text "\<open>argument\<close>"} (without surrounding @{verbatim
-  "@{"}@{text "\<dots>"}@{verbatim "}"}) works for a single argument that is a
-  cartouche.
+  \<open>\\<close>}@{verbatim "<^"}@{text name}@{verbatim ">"}@{text
+  "\<open>argument_content\<close>"} (without surrounding @{verbatim "@{"}@{text
+  "\<dots>"}@{verbatim "}"}) works for a single argument that is a cartouche.
 
+  \begingroup
+  \def\isasymcontrolstart{\isatt{\isacharbackslash\isacharless\isacharcircum}}
   @{rail \<open>
     @{syntax_def antiquotation}:
-      '@' '{' antiquotation_body '}' |
-      '\\' '<' '^' @{syntax_ref name} '>' @{syntax_ref cartouche}
+      '@{' antiquotation_body '}' |
+      '\<controlstart>' @{syntax_ref name} '>' @{syntax_ref cartouche}
   \<close>}
+  \endgroup
 
   %% FIXME less monolithic presentation, move to individual sections!?
   @{rail \<open>
@@ -492,7 +495,7 @@
   below.
 
   \begingroup
-  \def\isasymnewline{\isatext{\tt\isacharbackslash<newline>}}
+  \def\isasymnewline{\isatt{\isacharbackslash\isacharless newline\isachargreater}}
   @{rail \<open>
   rule? + ';'
   ;