author | wenzelm |
Sun, 10 Mar 2019 21:12:29 +0100 | |
changeset 69891 | def3ec9cdb7e |
parent 67572 | a93cf1d6ba87 |
child 69965 | da5e7278286b |
permissions | -rw-r--r-- |
67425 | 1 |
(* Title: Pure/General/comment.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Formal comments. |
|
5 |
*) |
|
6 |
||
7 |
signature COMMENT = |
|
8 |
sig |
|
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
9 |
datatype kind = Comment | Cancel | Latex | Marker |
67506
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
10 |
val markups: kind -> Markup.T list |
67571
f858fe5531ac
more uniform treatment of formal comments within document source;
wenzelm
parents:
67506
diff
changeset
|
11 |
val is_symbol: Symbol.symbol -> bool |
67426 | 12 |
val scan_comment: (kind * Symbol_Pos.T list) scanner |
13 |
val scan_cancel: (kind * Symbol_Pos.T list) scanner |
|
67429 | 14 |
val scan_latex: (kind * Symbol_Pos.T list) scanner |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
15 |
val scan_marker: (kind * Symbol_Pos.T list) scanner |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
16 |
val scan_inner: (kind * Symbol_Pos.T list) scanner |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
17 |
val scan_outer: (kind * Symbol_Pos.T list) scanner |
67572 | 18 |
val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list |
67425 | 19 |
end; |
20 |
||
21 |
structure Comment: COMMENT = |
|
22 |
struct |
|
23 |
||
24 |
(* kinds *) |
|
25 |
||
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
26 |
datatype kind = Comment | Cancel | Latex | Marker; |
67425 | 27 |
|
28 |
val kinds = |
|
67506
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
29 |
[(Comment, |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
30 |
{symbol = Symbol.comment, blanks = true, |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
31 |
markups = [Markup.language_document true]}), |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
32 |
(Cancel, |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
33 |
{symbol = Symbol.cancel, blanks = false, |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
34 |
markups = [Markup.language_text true]}), |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
35 |
(Latex, |
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
36 |
{symbol = Symbol.latex, blanks = false, |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
37 |
markups = [Markup.language_latex true, Markup.no_words]}), |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
38 |
(Marker, |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
39 |
{symbol = Symbol.marker, blanks = false, |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
40 |
markups = [Markup.language_document_marker]})]; |
67425 | 41 |
|
42 |
val get_kind = the o AList.lookup (op =) kinds; |
|
43 |
val print_kind = quote o #symbol o get_kind; |
|
67506
30233285270a
more markup: disable spell-checker for raw latex;
wenzelm
parents:
67429
diff
changeset
|
44 |
val markups = #markups o get_kind; |
67425 | 45 |
|
46 |
fun is_symbol sym = exists (fn (_, {symbol, ...}) => symbol = sym) kinds; |
|
47 |
||
48 |
||
49 |
(* scan *) |
|
50 |
||
51 |
local |
|
52 |
||
53 |
open Basic_Symbol_Pos; |
|
54 |
||
55 |
val err_prefix = "Error in formal comment: "; |
|
56 |
||
57 |
val scan_blanks = Scan.many (Symbol.is_blank o Symbol_Pos.symbol); |
|
58 |
||
59 |
fun scan_symbol kind = |
|
67429 | 60 |
let val {blanks, symbol, ...} = get_kind kind |
67425 | 61 |
in if blanks then $$$ symbol @@@ scan_blanks else $$$ symbol end; |
62 |
||
63 |
fun scan_strict kind = |
|
64 |
scan_symbol kind @@@ |
|
65 |
Symbol_Pos.!!! (fn () => err_prefix ^ "cartouche expected after " ^ print_kind kind) |
|
66 |
(Symbol_Pos.scan_cartouche err_prefix) >> pair kind; |
|
67 |
||
68 |
fun scan_permissive kind = |
|
69 |
scan_symbol kind -- Scan.option (Symbol_Pos.scan_cartouche err_prefix) >> |
|
70 |
(fn (ss, NONE) => (NONE, ss) | (_, SOME ss) => (SOME kind, ss)); |
|
71 |
||
72 |
in |
|
73 |
||
74 |
val scan_comment = scan_strict Comment; |
|
75 |
val scan_cancel = scan_strict Cancel; |
|
67429 | 76 |
val scan_latex = scan_strict Latex; |
69891
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
77 |
val scan_marker = scan_strict Marker; |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
78 |
|
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
79 |
val scan_inner = scan_comment || scan_cancel || scan_latex; |
def3ec9cdb7e
document markers are formal comments, and may thus occur anywhere in the command-span;
wenzelm
parents:
67572
diff
changeset
|
80 |
val scan_outer = scan_inner || scan_marker; |
67425 | 81 |
|
82 |
val scan_body = |
|
83 |
Scan.many1 (fn (s, _) => not (is_symbol s) andalso Symbol.not_eof s) >> pair NONE || |
|
67429 | 84 |
scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex; |
67425 | 85 |
|
86 |
fun read_body syms = |
|
67572 | 87 |
(if exists (is_symbol o Symbol_Pos.symbol) syms then |
67425 | 88 |
Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms |
67572 | 89 |
else NONE) |> the_default [(NONE, syms)]; |
67425 | 90 |
|
91 |
end; |
|
92 |
||
93 |
end; |