# HG changeset patch
# User wenzelm
# Date 927656465 -7200
# Node ID b91772e592dc83bfbb95451d4a0a195025ab42d5
# Parent  b5007e5e8a1bca8e9a11ee07223c3a06cecd5aa9
renamed empty to none;
added ignore, ignore_interest, ignore_interest';

diff -r b5007e5e8a1b -r b91772e592dc src/Pure/Isar/comment.ML
--- 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;