inner syntax comments may be written as "\<comment> \<open>text\<close>";

--- a/NEWS	Sat Jan 06 15:08:42 2018 +0100
+++ b/NEWS	Sat Jan 06 16:56:07 2018 +0100
@@ -9,6 +9,9 @@
 
 *** General ***
 
+* Inner syntax comments may be written as "\<comment> \<open>text\<close>", similar to
+marginal comments in outer syntax.
+
 * The old 'def' command has been discontinued (legacy since
 Isbelle2016-1). INCOMPATIBILITY, use 'define' instead -- usually with
 object-logic equality or equivalence.

--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 06 15:08:42 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 06 16:56:07 2018 +0100
@@ -565,6 +565,7 @@
     @{syntax_def (inner) str_token} & = & \<^verbatim>\<open>''\<close> \<open>\<dots>\<close> \<^verbatim>\<open>''\<close> \\
     @{syntax_def (inner) string_token} & = & \<^verbatim>\<open>"\<close> \<open>\<dots>\<close> \<^verbatim>\<open>"\<close> \\
     @{syntax_def (inner) cartouche} & = & @{verbatim "\<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
+    @{syntax_def (inner) comment_cartouche} & = & @{verbatim "\<comment> \<open>"} \<open>\<dots>\<close> @{verbatim "\<close>"} \\
   \end{supertabular}
   \end{center}
 
@@ -578,6 +579,11 @@
   The derived categories @{syntax_def (inner) num_const}, and @{syntax_def
   (inner) float_const}, provide robust access to the respective tokens: the
   syntax tree holds a syntactic constant instead of a free variable.
+
+  A @{syntax (inner) comment_cartouche} resembles the outer syntax notation
+  for marginal @{syntax_ref comment} (\secref{sec:comments}), but is
+  syntactically more restrictive: only the symbol-form with \<^verbatim>\<open>\<comment>\<close> and text
+  cartouche is supported.
 \<close>
 
 

--- a/src/Pure/Syntax/lexicon.ML	Sat Jan 06 15:08:42 2018 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Sat Jan 06 16:56:07 2018 +0100
@@ -21,8 +21,8 @@
   val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val is_tid: string -> bool
   datatype token_kind =
-    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
-    FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF
+    Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy |
+    StrSy | StringSy | Cartouche | Space | Comment | Comment_Cartouche| EOF
   datatype token = Token of token_kind * string * Position.range
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
@@ -112,8 +112,8 @@
 (** datatype token **)
 
 datatype token_kind =
-  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy |
-  FloatSy | StrSy | StringSy | Cartouche | Space | Comment | EOF;
+  Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy | NumSy | FloatSy | StrSy |
+  StringSy | Cartouche | Space | Comment | Comment_Cartouche | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
@@ -122,6 +122,7 @@
 
 fun is_proper (Token (Space, _, _)) = false
   | is_proper (Token (Comment, _, _)) = false
+  | is_proper (Token (Comment_Cartouche, _, _)) = false
   | is_proper _ = true;
 
 
@@ -170,6 +171,7 @@
   | StringSy => Markup.inner_string
   | Cartouche => Markup.inner_cartouche
   | Comment => Markup.inner_comment
+  | Comment_Cartouche => Markup.inner_comment
   | _ => Markup.empty;
 
 fun report_of_token (Token (kind, s, (pos, _))) =
@@ -244,6 +246,12 @@
 val explode_str = explode_literal scan_str_body;
 
 
+(* comment cartouche *)
+
+val scan_comment_cartouche =
+  $$$ "\<comment>" @@@ Scan.many (Symbol.is_blank o Symbol_Pos.symbol) @@@
+    !!! "cartouche expected after \"\<comment>\"" (Symbol_Pos.scan_cartouche err_prefix);
+
 
 (** tokenize **)
 
@@ -270,6 +278,7 @@
     val scan_token =
       Symbol_Pos.scan_cartouche err_prefix >> token Cartouche ||
       Symbol_Pos.scan_comment err_prefix >> token Comment ||
+      scan_comment_cartouche >> token Comment_Cartouche ||
       Scan.max token_leq scan_lit scan_val ||
       scan_string >> token StringSy ||
       scan_str >> token StrSy ||