src/Pure/Isar/comment.ML
author wenzelm
Sat Sep 25 13:18:38 1999 +0200 (1999-09-25 ago)
changeset 7604 55566b9ec7d7
parent 7171 2a245a80a2c5
child 7631 1b6b51b17c4a
permissions -rw-r--r--
tuned;
     1 (*  Title:      Pure/Isar/comment.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Formal comments.
     6 *)
     7 
     8 signature COMMENT =
     9 sig
    10   type text
    11   val plain: string -> text
    12   val none: text
    13   val ignore: 'a * text -> 'a
    14   type interest
    15   val interest: int -> interest
    16   val no_interest: interest
    17   val default_interest: interest
    18   val ignore_interest: 'a * interest -> 'a
    19   val ignore_interest': interest * 'a -> 'a
    20 end;
    21 
    22 structure Comment: COMMENT =
    23 struct
    24 
    25 (** text **)
    26 
    27 datatype text = Text of string;
    28 val plain = Text;
    29 val none = plain "";
    30 
    31 fun ignore (x, _) = x;
    32 
    33 
    34 
    35 (** interest **)
    36 
    37 datatype interest = Interest of int;
    38 val interest = Interest;
    39 val no_interest = interest ~1;
    40 val default_interest = interest 0;
    41 
    42 fun ignore_interest (x, _) = x;
    43 fun ignore_interest' (_, x) = x;
    44 
    45 
    46 end;