4 Text with antiquotations of inner items (types, terms, theorems etc.). |
4 Text with antiquotations of inner items (types, terms, theorems etc.). |
5 *) |
5 *) |
6 |
6 |
7 signature ANTIQUOTE = |
7 signature ANTIQUOTE = |
8 sig |
8 sig |
9 datatype antiquote = |
9 datatype 'a antiquote = |
10 Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T | |
10 Text of 'a | |
11 Open of Position.T | Close of Position.T |
11 Antiq of Symbol_Pos.T list * Position.T | |
12 val is_antiq: antiquote -> bool |
12 Open of Position.T | |
13 val read: Symbol_Pos.T list * Position.T -> antiquote list |
13 Close of Position.T |
|
14 val is_antiq: 'a antiquote -> bool |
|
15 val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list |
|
16 val scan_text: Symbol_Pos.T list -> Symbol_Pos.T list antiquote * Symbol_Pos.T list |
|
17 val read: (Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list) -> |
|
18 Symbol_Pos.T list * Position.T -> 'a antiquote list |
14 end; |
19 end; |
15 |
20 |
16 structure Antiquote: ANTIQUOTE = |
21 structure Antiquote: ANTIQUOTE = |
17 struct |
22 struct |
18 |
23 |
19 (* datatype antiquote *) |
24 (* datatype antiquote *) |
20 |
25 |
21 datatype antiquote = |
26 datatype 'a antiquote = |
22 Text of Symbol_Pos.T list | |
27 Text of 'a | |
23 Antiq of Symbol_Pos.T list * Position.T | |
28 Antiq of Symbol_Pos.T list * Position.T | |
24 Open of Position.T | |
29 Open of Position.T | |
25 Close of Position.T; |
30 Close of Position.T; |
26 |
31 |
27 fun is_antiq (Text _) = false |
32 fun is_antiq (Text _) = false |
61 |
66 |
62 val scan_antiq = |
67 val scan_antiq = |
63 Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
68 Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
64 Symbol_Pos.!!! "missing closing brace of antiquotation" |
69 Symbol_Pos.!!! "missing closing brace of antiquotation" |
65 (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
70 (Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
66 >> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2))); |
71 >> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2))); |
|
72 |
|
73 val scan_open = Symbol_Pos.scan_pos --| $$$ "\\<lbrace>"; |
|
74 val scan_close = Symbol_Pos.scan_pos --| $$$ "\\<rbrace>"; |
67 |
75 |
68 in |
76 in |
69 |
77 |
70 val scan_antiquote = |
78 fun scan x = (scan_antiq >> Antiq || scan_open >> Open || scan_close >> Close) x; |
71 (Scan.repeat1 scan_txt >> (Text o flat) || |
79 val scan_text = scan || Scan.repeat1 scan_txt >> (Text o flat); |
72 scan_antiq || |
|
73 Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open || |
|
74 Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close); |
|
75 |
80 |
76 end; |
81 end; |
77 |
82 |
78 |
83 |
79 (* read *) |
84 (* read *) |
80 |
85 |
81 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos |
86 fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos |
82 | report_antiq _ = (); |
87 | report_antiq _ = (); |
83 |
88 |
84 fun read ([], _) = [] |
89 fun read _ ([], _) = [] |
85 | read (syms, pos) = |
90 | read scanner (syms, pos) = |
86 (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of |
91 (case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of |
87 SOME xs => (List.app report_antiq xs; check_nesting xs; xs) |
92 SOME xs => (List.app report_antiq xs; check_nesting xs; xs) |
88 | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); |
93 | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos)); |
89 |
94 |
90 end; |
95 end; |