author | wenzelm |
Mon, 28 Nov 2011 22:05:32 +0100 | |
changeset 45666 | d83797ef0d2d |
parent 44736 | c2a3f1c84179 |
child 48764 | 4fe0920d5049 |
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 |
44736 | 15 |
val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
16 |
val check_nesting: 'a antiquote list -> unit |
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
17 |
val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
18 |
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
19 |
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
|
20 |
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
|
21 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
22 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
23 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
24 |
struct |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
25 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
26 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
27 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
28 |
datatype 'a antiquote = |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
29 |
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
|
30 |
Antiq of Symbol_Pos.T list * Position.range | |
27342 | 31 |
Open of Position.T | |
32 |
Close of Position.T; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
33 |
|
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
34 |
fun is_text (Text _) = true |
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
35 |
| is_text _ = false; |
27342 | 36 |
|
37 |
||
44736 | 38 |
(* reports *) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
39 |
|
44736 | 40 |
fun reports_of text = |
41 |
maps |
|
42 |
(fn Text x => text x |
|
45666 | 43 |
| Antiq (_, (pos, _)) => [(pos, Isabelle_Markup.antiq)] |
44 |
| Open pos => [(pos, Isabelle_Markup.antiq)] |
|
45 |
| Close pos => [(pos, Isabelle_Markup.antiq)]); |
|
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
46 |
|
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
47 |
|
27342 | 48 |
(* check_nesting *) |
49 |
||
50 |
fun err_unbalanced pos = |
|
51 |
error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); |
|
52 |
||
53 |
fun check_nesting antiqs = |
|
54 |
let |
|
55 |
fun check [] [] = () |
|
56 |
| check [] (pos :: _) = err_unbalanced pos |
|
57 |
| check (Open pos :: ants) ps = check ants (pos :: ps) |
|
58 |
| check (Close pos :: _) [] = err_unbalanced pos |
|
59 |
| check (Close _ :: ants) (_ :: ps) = check ants ps |
|
60 |
| check (_ :: ants) ps = check ants ps; |
|
61 |
in check antiqs [] end; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
62 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
63 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
64 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
65 |
|
30573 | 66 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
67 |
|
22114 | 68 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
69 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
70 |
val scan_txt = |
27767 | 71 |
$$$ "@" --| Scan.ahead (~$$$ "{") || |
72 |
Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" |
|
73 |
andalso Symbol.is_regular s) >> single; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
74 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
75 |
val scan_ant = |
42503 | 76 |
Scan.trace (Symbol_Pos.scan_string_qq || Symbol_Pos.scan_string_bq) >> #2 || |
27767 | 77 |
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
|
78 |
|
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
79 |
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>"; |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
80 |
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>"; |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
81 |
|
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
82 |
in |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
83 |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
84 |
val scan_antiq = |
30573 | 85 |
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via ||);
wenzelm
parents:
42508
diff
changeset
|
86 |
Symbol_Pos.!!! (fn () => "missing closing brace of antiquotation") |
30573 | 87 |
(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
|
88 |
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
89 |
|
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
93 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
94 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
95 |
|
27767 | 96 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
97 |
|
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
98 |
fun read (syms, pos) = |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
99 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of |
44736 | 100 |
SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
101 |
| 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
|
102 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
103 |
end; |