--- a/src/Pure/Isar/comment.ML Tue May 25 20:19:59 1999 +0200
+++ b/src/Pure/Isar/comment.ML Tue May 25 20:21:05 1999 +0200
@@ -9,10 +9,13 @@
sig
type text
val plain: string -> text
- val empty: text
+ val none: text
+ val ignore: 'a * text -> 'a
type interest
val no_interest: interest
val default_interest: interest
+ val ignore_interest: 'a * interest -> 'a
+ val ignore_interest': interest * 'a -> 'a
end;
structure Comment: COMMENT =
@@ -22,7 +25,10 @@
datatype text = Text of string;
val plain = Text;
-val empty = plain "";
+val none = plain "";
+
+fun ignore (x, _) = x;
+
(** interest **)
@@ -31,4 +37,8 @@
val no_interest = Interest false;
val default_interest = Interest true;
+fun ignore_interest (x, _) = x;
+fun ignore_interest' (_, x) = x;
+
+
end;