src/Pure/Isar/comment.ML

--- a/src/Pure/Isar/comment.ML	Tue Aug 03 19:02:03 1999 +0200
+++ b/src/Pure/Isar/comment.ML	Tue Aug 03 19:04:02 1999 +0200
@@ -12,6 +12,7 @@
   val none: text
   val ignore: 'a * text -> 'a
   type interest
+  val interest: int -> interest
   val no_interest: interest
   val default_interest: interest
   val ignore_interest: 'a * interest -> 'a
@@ -33,9 +34,10 @@
 
 (** interest **)
 
-datatype interest = Interest of bool;
-val no_interest = Interest false;
-val default_interest = Interest true;
+datatype interest = Interest of int;
+val interest = Interest;
+val no_interest = interest ~1;
+val default_interest = interest 0;
 
 fun ignore_interest (x, _) = x;
 fun ignore_interest' (_, x) = x;