# HG changeset patch
# User wenzelm
# Date 911998868 -3600
# Node ID 2bebd0d0a961c175aa08794aa3cb29d03dc6dcf1
# Parent  7af99477751b3e56cd0f23e28b07c35e6e2dded5
comment parser;

diff -r 7af99477751b -r 2bebd0d0a961 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Nov 25 14:00:43 1998 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Nov 25 14:01:08 1998 +0100
@@ -33,6 +33,7 @@
   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
@@ -133,11 +134,12 @@
 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 *)