# HG changeset patch
# User wenzelm
# Date 1516388944 -3600
# Node ID 44b018d4aa5f5c48f020bb0f004e4d30340e14cc
# Parent  1a279ad4c6a46a98a299931bbe4cbddcd4c7332b
avoid evaluation of embedded comment;

diff -r 1a279ad4c6a4 -r 44b018d4aa5f src/Doc/Isar_Ref/Outer_Syntax.thy
--- a/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jan 19 19:41:28 2018 +0100
+++ b/src/Doc/Isar_Ref/Outer_Syntax.thy	Fri Jan 19 20:09:04 2018 +0100
@@ -255,8 +255,8 @@
   document preparation (\chref{ch:document-prep}) supports various styles,
   according to the following kinds of comments.
 
-    \<^item> Marginal comment of the form \<^verbatim>\<open>\<comment>\<close>~\<open>\<open>text\<close>\<close> or \<open>\<comment> \<open>text\<close>\<close>, usually with a
-    single space between the comment symbol and the argument cartouche. The
+    \<^item> Marginal comment of the form \<^verbatim>\<open>\<comment>\<close>~\<open>\<open>text\<close>\<close> or \<open>\<comment>\<close>~\<open>\<open>text\<close>\<close>, usually with
+    a single space between the comment symbol and the argument cartouche. The
     given argument is typeset as regular text, with formal antiquotations
     (\secref{sec:antiq}).