src/Pure/Isar/comment.ML
author wenzelm
Sun Sep 26 16:42:14 1999 +0200 (1999-09-26 ago)
changeset 7613 fe818734c387
parent 7171 2a245a80a2c5
child 7631 1b6b51b17c4a
permissions -rw-r--r--
help: unknown theory context;
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@6549
    11
  val plain: string -> text
wenzelm@6725
    12
  val none: text
wenzelm@6725
    13
  val ignore: 'a * text -> 'a
wenzelm@6549
    14
  type interest
wenzelm@7171
    15
  val interest: int -> interest
wenzelm@6549
    16
  val no_interest: interest
wenzelm@6549
    17
  val default_interest: interest
wenzelm@6725
    18
  val ignore_interest: 'a * interest -> 'a
wenzelm@6725
    19
  val ignore_interest': interest * 'a -> 'a
wenzelm@6549
    20
end;
wenzelm@6549
    21
wenzelm@6549
    22
structure Comment: COMMENT =
wenzelm@6549
    23
struct
wenzelm@6549
    24
wenzelm@6549
    25
(** text **)
wenzelm@6549
    26
wenzelm@6549
    27
datatype text = Text of string;
wenzelm@6549
    28
val plain = Text;
wenzelm@6725
    29
val none = plain "";
wenzelm@6725
    30
wenzelm@6725
    31
fun ignore (x, _) = x;
wenzelm@6725
    32
wenzelm@6549
    33
wenzelm@6549
    34
wenzelm@6549
    35
(** interest **)
wenzelm@6549
    36
wenzelm@7171
    37
datatype interest = Interest of int;
wenzelm@7171
    38
val interest = Interest;
wenzelm@7171
    39
val no_interest = interest ~1;
wenzelm@7171
    40
val default_interest = interest 0;
wenzelm@6549
    41
wenzelm@6725
    42
fun ignore_interest (x, _) = x;
wenzelm@6725
    43
fun ignore_interest' (_, x) = x;
wenzelm@6725
    44
wenzelm@6725
    45
wenzelm@6549
    46
end;