author | wenzelm |
Wed, 13 Sep 2000 22:31:19 +0200 | |
changeset 9952 | 24914e42b857 |
parent 9127 | b1dc56410b63 |
permissions | -rw-r--r-- |
6549 | 1 |
(* Title: Pure/Isar/comment.ML |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
8807 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
6549 | 5 |
|
9127
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
6 |
Internal markup of formal comments -- mostly dummy. |
6549 | 7 |
*) |
8 |
||
9 |
signature COMMENT = |
|
10 |
sig |
|
11 |
type text |
|
7631 | 12 |
val string_of: text -> string |
8076 | 13 |
val plain: string list -> text |
6725 | 14 |
val none: text |
15 |
val ignore: 'a * text -> 'a |
|
6549 | 16 |
type interest |
7171 | 17 |
val interest: int -> interest |
6549 | 18 |
val no_interest: interest |
19 |
val default_interest: interest |
|
6725 | 20 |
val ignore_interest: 'a * interest -> 'a |
21 |
val ignore_interest': interest * 'a -> 'a |
|
9127
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
22 |
exception OUTPUT_FAIL of (string * Position.T) * exn |
6549 | 23 |
end; |
24 |
||
25 |
structure Comment: COMMENT = |
|
26 |
struct |
|
27 |
||
9127
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
28 |
(* text *) |
6549 | 29 |
|
8076 | 30 |
datatype text = Text of string list; |
7631 | 31 |
|
8076 | 32 |
fun string_of (Text ss) = cat_lines ss; |
6549 | 33 |
val plain = Text; |
8076 | 34 |
val none = plain []; |
6725 | 35 |
|
36 |
fun ignore (x, _) = x; |
|
37 |
||
6549 | 38 |
|
9127
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
39 |
(* interest *) |
6549 | 40 |
|
7171 | 41 |
datatype interest = Interest of int; |
42 |
val interest = Interest; |
|
43 |
val no_interest = interest ~1; |
|
44 |
val default_interest = interest 0; |
|
6549 | 45 |
|
6725 | 46 |
fun ignore_interest (x, _) = x; |
47 |
fun ignore_interest' (_, x) = x; |
|
48 |
||
49 |
||
9127
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
50 |
(* output errors *) |
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
51 |
|
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
52 |
(*note: actually belongs to isar_output.ML*) |
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
53 |
exception OUTPUT_FAIL of (string * Position.T) * exn; |
b1dc56410b63
exception OUTPUT_FAIL of (string * Position.T) * exn
wenzelm
parents:
8807
diff
changeset
|
54 |
|
6549 | 55 |
end; |