author | wenzelm |
Sun, 25 Nov 2012 19:49:24 +0100 | |
changeset 50201 | c26369c9eda6 |
parent 48992 | 0518bf89c777 |
child 53167 | 4e7ddd76e632 |
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 |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48764
diff
changeset
|
15 |
val reports_of: ('a -> Position.report_text list) -> |
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48764
diff
changeset
|
16 |
'a antiquote list -> Position.report_text list |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
17 |
val check_nesting: 'a antiquote list -> unit |
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
18 |
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
|
19 |
val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
20 |
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
|
21 |
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
|
22 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
23 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
24 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
25 |
struct |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
26 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
27 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
28 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
29 |
datatype 'a antiquote = |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
30 |
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
|
31 |
Antiq of Symbol_Pos.T list * Position.range | |
27342 | 32 |
Open of Position.T | |
33 |
Close of Position.T; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
34 |
|
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
35 |
fun is_text (Text _) = true |
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
36 |
| is_text _ = false; |
27342 | 37 |
|
38 |
||
44736 | 39 |
(* reports *) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
40 |
|
44736 | 41 |
fun reports_of text = |
42 |
maps |
|
43 |
(fn Text x => text x |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
44 |
| Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")] |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
45 |
| Open pos => [((pos, Markup.antiq), "")] |
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
48992
diff
changeset
|
46 |
| Close pos => [((pos, Markup.antiq), "")]); |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
47 |
|
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
48 |
|
27342 | 49 |
(* check_nesting *) |
50 |
||
51 |
fun err_unbalanced pos = |
|
48992 | 52 |
error ("Unbalanced antiquotation block parentheses" ^ Position.here pos); |
27342 | 53 |
|
54 |
fun check_nesting antiqs = |
|
55 |
let |
|
56 |
fun check [] [] = () |
|
57 |
| check [] (pos :: _) = err_unbalanced pos |
|
58 |
| check (Open pos :: ants) ps = check ants (pos :: ps) |
|
59 |
| check (Close pos :: _) [] = err_unbalanced pos |
|
60 |
| check (Close _ :: ants) (_ :: ps) = check ants ps |
|
61 |
| check (_ :: ants) ps = check ants ps; |
|
62 |
in check antiqs [] end; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
63 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
64 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
65 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
66 |
|
30573 | 67 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
68 |
|
22114 | 69 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
70 |
|
48764 | 71 |
val err_prefix = "Antiquotation lexical error: "; |
72 |
||
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
73 |
val scan_txt = |
27767 | 74 |
$$$ "@" --| Scan.ahead (~$$$ "{") || |
75 |
Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" |
|
76 |
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_ant = |
48764 | 79 |
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
27767 | 80 |
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
|
81 |
|
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
82 |
val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>"; |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
83 |
val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>"; |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
84 |
|
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
85 |
in |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
86 |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
87 |
val scan_antiq = |
30573 | 88 |
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
48764 | 89 |
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
30573 | 90 |
(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
|
91 |
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
92 |
|
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
93 |
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
|
94 |
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
|
95 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
96 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
97 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
98 |
|
27767 | 99 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
100 |
|
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
101 |
fun read (syms, pos) = |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
102 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of |
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48764
diff
changeset
|
103 |
SOME xs => (Position.reports_text (reports_of (K []) xs); check_nesting xs; xs) |
48992 | 104 |
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
105 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
106 |
end; |