1.1 --- a/src/Pure/Isar/comment.ML	Tue Aug 03 19:02:03 1999 +0200
     1.2 +++ b/src/Pure/Isar/comment.ML	Tue Aug 03 19:04:02 1999 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    val none: text
     1.5    val ignore: 'a * text -> 'a
     1.6    type interest
     1.7 +  val interest: int -> interest
     1.8    val no_interest: interest
     1.9    val default_interest: interest
    1.10    val ignore_interest: 'a * interest -> 'a
    1.11 @@ -33,9 +34,10 @@
    1.12  
    1.13  (** interest **)
    1.14  
    1.15 -datatype interest = Interest of bool;
    1.16 -val no_interest = Interest false;
    1.17 -val default_interest = Interest true;
    1.18 +datatype interest = Interest of int;
    1.19 +val interest = Interest;
    1.20 +val no_interest = interest ~1;
    1.21 +val default_interest = interest 0;
    1.22  
    1.23  fun ignore_interest (x, _) = x;
    1.24  fun ignore_interest' (_, x) = x;

     2.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Aug 03 19:02:03 1999 +0200
     2.2 +++ b/src/Pure/Isar/outer_parse.ML	Tue Aug 03 19:04:02 1999 +0200
     2.3 @@ -162,7 +162,9 @@
     2.4  
     2.5  val comment = text >> Comment.plain;
     2.6  val marg_comment = Scan.optional ($$$ "--" |-- comment) Comment.none;
     2.7 -val interest = Scan.optional ($$$ "%" >> K Comment.no_interest) Comment.default_interest;
     2.8 +
     2.9 +val interest = Scan.optional ($$$ "%%" >> K Comment.no_interest ||
    2.10 +  $$$ "%" |-- Scan.optional nat 1 >> Comment.interest) Comment.default_interest;
    2.11  
    2.12  
    2.13  (* sorts and arities *)