# HG changeset patch
# User wenzelm
# Date 933699842 -7200
# Node ID 2a245a80a2c591744c9eaabd3f33a2e1334b8fd7
# Parent  cb8afc731bee8aab053404576f4e443c36a13f94
improved interest;

diff -r cb8afc731bee -r 2a245a80a2c5 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;
diff -r cb8afc731bee -r 2a245a80a2c5 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Tue Aug 03 19:02:03 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Tue Aug 03 19:04:02 1999 +0200
@@ -162,7 +162,9 @@
 
 val comment = text >> Comment.plain;
 val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
-val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest;
+
+val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
+  $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;
 
 
 (* sorts and arities *)