author | wenzelm |
Thu, 19 Mar 2009 15:44:14 +0100 | |
changeset 30589 | cbe27c4ef417 |
parent 30587 | ad19c99529eb |
child 30590 | 1d9c9fcf8513 |
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 |
27342 | 9 |
datatype antiquote = |
30589 | 10 |
Text of Symbol_Pos.T list | Antiq of Symbol_Pos.T list * Position.T | |
27342 | 11 |
Open of Position.T | Close of Position.T |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
12 |
val is_antiq: antiquote -> bool |
30573 | 13 |
val read: Symbol_Pos.T list * Position.T -> antiquote list |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
14 |
end; |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
15 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
16 |
structure Antiquote: ANTIQUOTE = |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
17 |
struct |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
18 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
19 |
(* datatype antiquote *) |
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 |
datatype antiquote = |
30589 | 22 |
Text of Symbol_Pos.T list | |
30573 | 23 |
Antiq of Symbol_Pos.T list * Position.T | |
27342 | 24 |
Open of Position.T | |
25 |
Close of Position.T; |
|
9138
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 |
fun is_antiq (Text _) = false |
27342 | 28 |
| is_antiq _ = true; |
29 |
||
30 |
||
31 |
(* check_nesting *) |
|
32 |
||
33 |
fun err_unbalanced pos = |
|
34 |
error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); |
|
35 |
||
36 |
fun check_nesting antiqs = |
|
37 |
let |
|
38 |
fun check [] [] = () |
|
39 |
| check [] (pos :: _) = err_unbalanced pos |
|
40 |
| check (Open pos :: ants) ps = check ants (pos :: ps) |
|
41 |
| check (Close pos :: _) [] = err_unbalanced pos |
|
42 |
| check (Close _ :: ants) (_ :: ps) = check ants ps |
|
43 |
| check (_ :: ants) ps = check ants ps; |
|
44 |
in check antiqs [] end; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
45 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
46 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
47 |
(* scan_antiquote *) |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
48 |
|
30573 | 49 |
open Basic_Symbol_Pos; |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
50 |
|
22114 | 51 |
local |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
52 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
53 |
val scan_txt = |
27767 | 54 |
$$$ "@" --| Scan.ahead (~$$$ "{") || |
55 |
Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" |
|
56 |
andalso Symbol.is_regular s) >> single; |
|
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
57 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
58 |
val scan_ant = |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
59 |
Symbol_Pos.scan_quoted || |
27767 | 60 |
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
|
61 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
62 |
val scan_antiq = |
30573 | 63 |
Symbol_Pos.scan_pos -- ($$$ "@" |-- $$$ "{" |-- |
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset
|
64 |
Symbol_Pos.!!! "missing closing brace of antiquotation" |
30573 | 65 |
(Scan.repeat scan_ant -- ($$$ "}" |-- Symbol_Pos.scan_pos))) |
27870
643673ebe065
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents:
27835
diff
changeset
|
66 |
>> (fn (pos1, (body, pos2)) => Antiq (flat body, Position.encode_range (pos1, pos2))); |
9138
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 |
in |
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
69 |
|
27779
4569003b8813
simplified Antiq: regular SymbolPos.text with position;
wenzelm
parents:
27767
diff
changeset
|
70 |
val scan_antiquote = |
30589 | 71 |
(Scan.repeat1 scan_txt >> (Text o flat) || |
27750 | 72 |
scan_antiq || |
30573 | 73 |
Symbol_Pos.scan_pos --| $$$ "\\<lbrace>" >> Open || |
74 |
Symbol_Pos.scan_pos --| $$$ "\\<rbrace>" >> Close); |
|
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; |
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 |
|
27767 | 79 |
(* read *) |
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
80 |
|
27880 | 81 |
fun report_antiq (Antiq (_, pos)) = Position.report Markup.antiq pos |
82 |
| report_antiq _ = (); |
|
83 |
||
27870
643673ebe065
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents:
27835
diff
changeset
|
84 |
fun read ([], _) = [] |
643673ebe065
use SymbolPos.T list directly, instead of encoded SymbolPos.text;
wenzelm
parents:
27835
diff
changeset
|
85 |
| read (syms, pos) = |
30573 | 86 |
(case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of |
27880 | 87 |
SOME xs => (List.app report_antiq xs; check_nesting xs; xs) |
27767 | 88 |
| 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
|
89 |
|
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset
|
90 |
end; |