author  wenzelm 
Fri, 20 Mar 2009 20:21:38 +0100  
changeset 30613  b22d35d9ef28 
parent 30590  1d9c9fcf8513 
child 30635  a7d175c48228 
permissions  rwrr 
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  
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

11 
Antiq of Symbol_Pos.T list * Position.T  
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 
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

14 
val is_antiq: 'a antiquote > bool 
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

15 
val scan: Symbol_Pos.T list > 'a antiquote * Symbol_Pos.T list 
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 
30613  17 
val read: ('a > unit) > (Symbol_Pos.T list > 'a antiquote * Symbol_Pos.T list) > 
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

18 
Symbol_Pos.T list * Position.T > 'a 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 

30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

26 
datatype 'a antiquote = 
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

27 
Text of 'a  
30573  28 
Antiq of Symbol_Pos.T list * Position.T  
27342  29 
Open of Position.T  
30 
Close of Position.T; 

9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

31 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

32 
fun is_antiq (Text _) = false 
27342  33 
 is_antiq _ = true; 
34 

35 

36 
(* check_nesting *) 

37 

38 
fun err_unbalanced pos = 

39 
error ("Unbalanced antiquotation block parentheses" ^ Position.str_of pos); 

40 

41 
fun check_nesting antiqs = 

42 
let 

43 
fun check [] [] = () 

44 
 check [] (pos :: _) = err_unbalanced pos 

45 
 check (Open pos :: ants) ps = check ants (pos :: ps) 

46 
 check (Close pos :: _) [] = err_unbalanced pos 

47 
 check (Close _ :: ants) (_ :: ps) = check ants ps 

48 
 check (_ :: ants) ps = check ants ps; 

49 
in check antiqs [] end; 

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 

30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

52 
(* scan *) 
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

53 

30573  54 
open Basic_Symbol_Pos; 
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

55 

22114  56 
local 
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_txt = 
27767  59 
$$$ "@"  Scan.ahead (~$$$ "{")  
60 
Scan.one (fn (s, _) => s <> "@" andalso s <> "\\<lbrace>" andalso s <> "\\<rbrace>" 

61 
andalso Symbol.is_regular s) >> single; 

9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

62 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

63 
val scan_ant = 
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset

64 
Symbol_Pos.scan_quoted  
27767  65 
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

66 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

67 
val scan_antiq = 
30573  68 
Symbol_Pos.scan_pos  ($$$ "@"  $$$ "{"  
30587
ad19c99529eb
moved Isar/antiquote.ML to General/antiquote.ML, which is loaded early;
wenzelm
parents:
30573
diff
changeset

69 
Symbol_Pos.!!! "missing closing brace of antiquotation" 
30573  70 
(Scan.repeat scan_ant  ($$$ "}"  Symbol_Pos.scan_pos))) 
30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

71 
>> (fn (pos1, (body, pos2)) => (flat body, Position.encode_range (pos1, pos2))); 
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

72 

1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

73 
val scan_open = Symbol_Pos.scan_pos  $$$ "\\<lbrace>"; 
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

74 
val scan_close = Symbol_Pos.scan_pos  $$$ "\\<rbrace>"; 
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 
in 
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

77 

30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

78 
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

79 
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

80 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

81 
end; 
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

82 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

83 

27767  84 
(* read *) 
9138
6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

85 

30613  86 
fun read _ _ ([], _) = [] 
87 
 read report scanner (syms, pos) = 

30590
1d9c9fcf8513
parameterized datatype antiquote and read operation;
wenzelm
parents:
30589
diff
changeset

88 
(case Scan.read Symbol_Pos.stopper (Scan.repeat scanner) syms of 
30613  89 
SOME xs => 
90 
(List.app (fn Antiq (_, pos) => Position.report Markup.antiq pos  Text x => report x) xs; 

91 
check_nesting xs; xs) 

27767  92 
 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

93 

6a4fae41a75f
Text with antiquotations of inner items (terms, types etc.).
wenzelm
parents:
diff
changeset

94 
end; 