author | wenzelm |
Sun, 19 Jan 2014 20:53:40 +0100 | |
changeset 55046 | 9e83995c8e98 |
parent 53167 | 4e7ddd76e632 |
child 55105 | 75815b3b38a1 |
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 | |
53167 | 11 |
Antiq of Symbol_Pos.T list * Position.range |
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
12 |
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
|
13 |
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
|
14 |
'a antiquote list -> Position.report_text list |
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
15 |
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
|
16 |
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
|
17 |
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
|
18 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
19 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
20 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
21 |
struct |
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 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
24 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
25 |
datatype 'a antiquote = |
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
26 |
Text of 'a | |
53167 | 27 |
Antiq of Symbol_Pos.T list * Position.range; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
28 |
|
30635
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
29 |
fun is_text (Text _) = true |
a7d175c48228
replaced Antiquote.is_antiq by Antiquote.is_text;
wenzelm
parents:
30613
diff
changeset
|
30 |
| is_text _ = false; |
27342 | 31 |
|
32 |
||
44736 | 33 |
(* reports *) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
34 |
|
44736 | 35 |
fun reports_of text = |
53167 | 36 |
maps (fn Text x => text x | Antiq (_, (pos, _)) => [((pos, Markup.antiq), "")]); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
37 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
38 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
39 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
40 |
|
30573 | 41 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
42 |
|
22114 | 43 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
44 |
|
48764 | 45 |
val err_prefix = "Antiquotation lexical error: "; |
46 |
||
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
47 |
val scan_txt = |
27767 | 48 |
$$$ "@" --| Scan.ahead (~$$$ "{") || |
53167 | 49 |
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
|
50 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
51 |
val scan_ant = |
48764 | 52 |
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
55046 | 53 |
Scan.trace (Symbol_Pos.scan_cartouche (fn s => Symbol_Pos.!!! (fn () => err_prefix ^ s))) >> #2 || |
27767 | 54 |
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
|
55 |
|
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
56 |
in |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
57 |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
58 |
val scan_antiq = |
30573 | 59 |
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
48764 | 60 |
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
30573 | 61 |
(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
|
62 |
>> (fn (pos1, (body, pos2)) => (flat body, Position.range pos1 pos2)); |
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
63 |
|
53167 | 64 |
val scan_text = scan_antiq >> Antiq || Scan.repeat1 scan_txt >> (Text o flat); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
65 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
66 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
67 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
68 |
|
27767 | 69 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
70 |
|
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
71 |
fun read (syms, pos) = |
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
72 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of |
53167 | 73 |
SOME xs => (Position.reports_text (reports_of (K []) xs); xs) |
48992 | 74 |
| NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos)); |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
75 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
76 |
end; |