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;
wenzelm@6549
     1
(*  Title:      Pure/Isar/comment.ML
wenzelm@6549
     2
    ID:         $Id$
wenzelm@6549
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6549
     4
wenzelm@6549
     5
Formal comments.
wenzelm@6549
     6
*)
wenzelm@6549
     7
wenzelm@6549
     8
signature COMMENT =
wenzelm@6549
     9
sig
wenzelm@6549
    10
  type text
wenzelm@7631
    11
  val string_of: text -> string
wenzelm@6549
    12
  val plain: string -> text
wenzelm@6725
    13
  val none: text
wenzelm@6725
    14
  val ignore: 'a * text -> 'a
wenzelm@6549
    15
  type interest
wenzelm@7171
    16
  val interest: int -> interest
wenzelm@6549
    17
  val no_interest: interest
wenzelm@6549
    18
  val default_interest: interest
wenzelm@6725
    19
  val ignore_interest: 'a * interest -> 'a
wenzelm@6725
    20
  val ignore_interest': interest * 'a -> 'a
wenzelm@6549
    21
end;
wenzelm@6549
    22
wenzelm@6549
    23
structure Comment: COMMENT =
wenzelm@6549
    24
struct
wenzelm@6549
    25
wenzelm@6549
    26
(** text **)
wenzelm@6549
    27
wenzelm@6549
    28
datatype text = Text of string;
wenzelm@7631
    29
wenzelm@7631
    30
fun string_of (Text s) = s;
wenzelm@6549
    31
val plain = Text;
wenzelm@6725
    32
val none = plain "";
wenzelm@6725
    33
wenzelm@6725
    34
fun ignore (x, _) = x;
wenzelm@6725
    35
wenzelm@6549
    36
wenzelm@6549
    37
wenzelm@6549
    38
(** interest **)
wenzelm@6549
    39
wenzelm@7171
    40
datatype interest = Interest of int;
wenzelm@7171
    41
val interest = Interest;
wenzelm@7171
    42
val no_interest = interest ~1;
wenzelm@7171
    43
val default_interest = interest 0;
wenzelm@6549
    44
wenzelm@6725
    45
fun ignore_interest (x, _) = x;
wenzelm@6725
    46
fun ignore_interest' (_, x) = x;
wenzelm@6725
    47
wenzelm@6725
    48
wenzelm@6549
    49
end;