author | wenzelm |
Wed, 14 Oct 2015 17:24:03 +0200 | |
changeset 61440 | 8626c2fed037 |
parent 61434 | 46d6586eb04c |
child 61450 | 239a04ec2d4c |
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 |
55511
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
wenzelm
parents:
55107
diff
changeset
|
2 |
Author: Makarius |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
3 |
|
55511
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
wenzelm
parents:
55107
diff
changeset
|
4 |
Antiquotations within plain text. |
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 |
55526 | 9 |
type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} |
10 |
datatype 'a antiquote = Text of 'a | Antiq of antiq |
|
61434 | 11 |
type text_antiquote = Symbol_Pos.T list antiquote |
12 |
val split_lines: text_antiquote list -> text_antiquote list list |
|
55612 | 13 |
val antiq_reports: antiq -> Position.report list |
14 |
val antiquote_reports: ('a -> Position.report_text list) -> |
|
48768
abc45de5bb22
clarified "bad" markup: proper body text, invent missing serial on Scala side (counting backwards);
wenzelm
parents:
48764
diff
changeset
|
15 |
'a antiquote list -> Position.report_text list |
55526 | 16 |
val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list |
61434 | 17 |
val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list |
18 |
val read: Input.source -> text_antiquote list |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
19 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
20 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
21 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
22 |
struct |
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 |
(* datatype antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
25 |
|
55526 | 26 |
type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}; |
27 |
datatype 'a antiquote = Text of 'a | Antiq of antiq; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
28 |
|
61434 | 29 |
type text_antiquote = Symbol_Pos.T list antiquote; |
30 |
||
31 |
||
32 |
(* split lines *) |
|
33 |
||
34 |
fun split_lines input = |
|
35 |
let |
|
36 |
fun add a (line, lines) = (a :: line, lines); |
|
37 |
fun flush (line, lines) = ([], rev line :: lines); |
|
38 |
fun split (a as Text ss) = |
|
39 |
(case take_prefix (fn ("\n", _) => false | _ => true) ss of |
|
40 |
([], []) => I |
|
41 |
| (_, []) => add a |
|
42 |
| ([], _ :: rest) => flush #> split (Text rest) |
|
43 |
| (prefix, _ :: rest) => add (Text prefix) #> flush #> split (Text rest)) |
|
44 |
| split a = add a; |
|
61440 | 45 |
in if null input then [] else rev (#2 (flush (fold split input ([], [])))) end; |
61434 | 46 |
|
27342 | 47 |
|
44736 | 48 |
(* reports *) |
30641
72980f8d7ee8
export report -- version that actually covers all cases;
wenzelm
parents:
30635
diff
changeset
|
49 |
|
55612 | 50 |
fun antiq_reports ((_, {start, stop, range = (pos, _)}): antiq) = |
55653
528de9a20054
more markup -- complete symbols within antiquotation, notably with broken arguments;
wenzelm
parents:
55612
diff
changeset
|
51 |
[(start, Markup.antiquote), (stop, Markup.antiquote), |
528de9a20054
more markup -- complete symbols within antiquotation, notably with broken arguments;
wenzelm
parents:
55612
diff
changeset
|
52 |
(pos, Markup.antiquoted), (pos, Markup.language_antiquotation)]; |
55526 | 53 |
|
55612 | 54 |
fun antiquote_reports text = |
55 |
maps (fn Text x => text x | Antiq antiq => map (rpair "") (antiq_reports antiq)); |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
56 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
57 |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
58 |
(* scan *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
59 |
|
30573 | 60 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
61 |
|
22114 | 62 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
63 |
|
48764 | 64 |
val err_prefix = "Antiquotation lexical error: "; |
65 |
||
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
66 |
val scan_txt = |
55511
984e210d412e
antiquotations within plain text: Scala version in accordance to ML;
wenzelm
parents:
55107
diff
changeset
|
67 |
Scan.repeat1 ($$$ "@" --| Scan.ahead (~$$ "{") || |
58854 | 68 |
Scan.many1 (fn (s, _) => s <> "@" andalso Symbol.not_eof s)) >> flat; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
69 |
|
55512 | 70 |
val scan_antiq_body = |
48764 | 71 |
Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 || |
55105 | 72 |
Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 || |
58854 | 73 |
Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
74 |
|
42508
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
75 |
in |
e21362bf1d93
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;
wenzelm
parents:
42503
diff
changeset
|
76 |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
77 |
val scan_antiq = |
55526 | 78 |
Symbol_Pos.scan_pos -- ($$ "@" |-- $$ "{" |-- Symbol_Pos.scan_pos -- |
48764 | 79 |
Symbol_Pos.!!! (fn () => err_prefix ^ "missing closing brace") |
55526 | 80 |
(Scan.repeat scan_antiq_body -- Symbol_Pos.scan_pos -- ($$ "}" |-- Symbol_Pos.scan_pos))) |
81 |
>> (fn (pos1, (pos2, ((body, pos3), pos4))) => |
|
82 |
(flat body, |
|
83 |
{start = Position.set_range (pos1, pos2), |
|
84 |
stop = Position.set_range (pos3, pos4), |
|
85 |
range = Position.range pos1 pos4})); |
|
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset
|
86 |
|
55512 | 87 |
val scan_antiquote = scan_antiq >> Antiq || scan_txt >> Text; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
88 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
89 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
90 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
91 |
|
27767 | 92 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
93 |
|
59065 | 94 |
fun read source = |
95 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) (Input.source_explode source) of |
|
55612 | 96 |
SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs) |
59065 | 97 |
| NONE => |
98 |
error ("Malformed quotation/antiquotation source" ^ Position.here (Input.pos_of source))); |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
99 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
100 |
end; |