src/Pure/Isar/outer_parse.ML

   val list: (token list -> 'a * token list) -> token list -> 'a list * token list
   val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
   val name: token list -> bstring * token list
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
+  val comment: token list -> string * token list
   val sort: token list -> xsort * token list
   val arity: token list -> (xsort list * xsort) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
   val opt_infix: token list -> Syntax.mixfix * token list

 
 fun list1 scan = enum1 "," scan;
 fun list scan = enum "," scan;
 
 
-(* names *)
+(* names and text *)
 
 val name = group "name declaration" (short_ident || sym_ident || string);
 val xname = group "name reference" (short_ident || long_ident || sym_ident || string);
 val text = group "text" (short_ident || long_ident || string || verbatim);
+val comment = Scan.optional ($$$ "--" |-- text) "";
 
 
 (* sorts *)
 
 val sort =