author | wenzelm |
Thu, 16 Jul 2009 16:24:49 +0200 | |
changeset 32015 | 7101feb5247e |
parent 30683 | e8ac1f9d9469 |
child 39507 | 839873937ddd |
permissions | -rw-r--r-- |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
1 |
(* Title: Pure/General/antiquote.ML |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
2 |
Author: Markus Wenzel, TU Muenchen |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
3 |
|
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
4 |
Text with antiquotations of inner items (types, terms, theorems etc.). |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
5 |
*) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
6 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
7 |
signature ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
8 |
sig |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
9 |
datatype 'a antiquote = |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
10 |
Text of 'a | |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30641
diff
changeset
|
11 |
Antiq of Symbol_Pos.T list * Position.range | |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
12 |
Open of Position.T | |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
13 |
Close of Position.T |
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
14 |
val is_text: 'a antiquote -> bool |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
15 |
val report: ('a -> unit) -> 'a antiquote -> unit |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
16 |
val check_nesting: 'a antiquote list -> unit |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
17 |
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
18 |
val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
19 |
val read: Symbol_Pos.T list * Position.T -> Symbol_Pos.T list antiquote list |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
20 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
21 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
22 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
23 |
struct |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
24 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
25 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
26 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
27 |
datatype 'a antiquote = |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
28 |
Text of 'a | |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30641
diff
changeset
|
29 |
Antiq of Symbol_Pos.T list * Position.range | |
27342 | 30 |
Open of Position.T | |
31 |
Close of Position.T; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
32 |
|
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
33 |
fun is_text (Text _) = true |
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
34 |
| is_text _ = false; |
27342 | 35 |
|
36 |
||
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
37 |
(* report *) |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
38 |
|
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
39 |
val report_antiq = Position.report Markup.antiq; |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
40 |
|
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
41 |
fun report report_text (Text x) = report_text x |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30641
diff
changeset
|
42 |
| report _ (Antiq (_, (pos, _))) = report_antiq pos |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
43 |
| report _ (Open pos) = report_antiq pos |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
44 |
| report _ (Close pos) = report_antiq pos; |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
45 |
|
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
46 |
|
27342 | 47 |
(* check_nesting *) |
48 |
||
49 |
fun err_unbalanced pos = |
|
50 |
error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); |
|
51 |
||
52 |
fun check_nesting antiqs = |
|
53 |
let |
|
54 |
fun check [] [] = () |
|
55 |
| check [] (pos :: _) = err_unbalanced pos |
|
56 |
| check (Open pos :: ants) ps = check ants (pos :: ps) |
|
57 |
| check (Close pos :: _) [] = err_unbalanced pos |
|
58 |
| check (Close _ :: ants) (_ :: ps) = check ants ps |
|
59 |
| check (_ :: ants) ps = check ants ps; |
|
60 |
in check antiqs [] end; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
61 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
62 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
63 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
64 |
|
30573 | 65 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
66 |
|
22114 | 67 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
68 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
69 |
val scan_txt = |
27767 | 70 |
$$$ "@" --| Scan.ahead (~$$$ "{") || |
71 |
Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" |
|
72 |
andalso Symbol.is_regular s) >> single; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
73 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
74 |
val scan_ant = |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
75 |
Symbol_Pos.scan_quoted || |
27767 | 76 |
Scan.one (fn (s, _) => s <> "}" andalso Symbol.is_regular s) >> single; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
77 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
78 |
val scan_antiq = |
30573 | 79 |
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
80 |
Symbol_Pos.!!! "missing closing brace of antiquotation" |
30573 | 81 |
(Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
30683
e8ac1f9d9469
datatype antiquote: maintain original Position.range, which is eventually attached to the resulting ML tokens;
wenzelm
parents:
30641
diff
changeset
|
82 |
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
83 |
|
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
84 |
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>"; |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
85 |
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>"; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
86 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
87 |
in |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
88 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
89 |
fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x; |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
90 |
val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
91 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
92 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
93 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
94 |
|
27767 | 95 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
96 |
|
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
97 |
fun read (syms, pos) = |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
98 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
99 |
SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs) |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
100 |
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
101 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
102 |
end; |