comment parser;
authorwenzelm
Wed, 25 Nov 1998 14:01:08 +0100
changeset 5960 2bebd0d0a961
parent 5959 7af99477751b
child 5961 6cf4e46ce95a
comment parser;
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 *)