src/Pure/Isar/comment.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7631 1b6b51b17c4a
child 8076 ef78716f39ef
permissions -rw-r--r--
removed extra shyps error;
     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 string_of: text -> string
    12   val plain: string -> text
    13   val none: text
    14   val ignore: 'a * text -> 'a
    15   type interest
    16   val interest: int -> interest
    17   val no_interest: interest
    18   val default_interest: interest
    19   val ignore_interest: 'a * interest -> 'a
    20   val ignore_interest': interest * 'a -> 'a
    21 end;
    22 
    23 structure Comment: COMMENT =
    24 struct
    25 
    26 (** text **)
    27 
    28 datatype text = Text of string;
    29 
    30 fun string_of (Text s) = s;
    31 val plain = Text;
    32 val none = plain "";
    33 
    34 fun ignore (x, _) = x;
    35 
    36 
    37 
    38 (** interest **)
    39 
    40 datatype interest = Interest of int;
    41 val interest = Interest;
    42 val no_interest = interest ~1;
    43 val default_interest = interest 0;
    44 
    45 fun ignore_interest (x, _) = x;
    46 fun ignore_interest' (_, x) = x;
    47 
    48 
    49 end;