author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 17978  b48885914c1d 
permissions  rwrr 
9139  1 
(* Title: Pure/Isar/thy_header.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

17978  5 
Theory headers  processed separately with minimal outer syntax. 
9139  6 
*) 
7 

8 
signature THY_HEADER = 

9 
sig 

10 
val args: OuterLex.token list > 

11 
(string * string list * (string * bool) list) * OuterLex.token list 

17933
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

12 
val read: (string, 'a) Source.source * Position.T > 
16265
ee2497cde564
new Isar header: reject ':', accept both 'files' and 'uses';
wenzelm
parents:
15531
diff
changeset

13 
string * string list * (string * bool) list 
9139  14 
end; 
15 

16 
structure ThyHeader: THY_HEADER = 

17 
struct 

18 

19 
structure T = OuterLex; 

20 
structure P = OuterParse; 

21 

22 

17933
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

23 
(* keywords *) 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

24 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

25 
val headerN = "header"; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

26 
val theoryN = "theory"; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

27 
val importsN = "imports"; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

28 
val usesN = "uses"; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

29 
val beginN = "begin"; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

30 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

31 
val header_lexicon = T.make_lexicon 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

32 
["%", "(", ")", ";", beginN, headerN, importsN, theoryN, usesN]; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

33 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

34 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

35 
(* header args *) 
9139  36 

17933
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

37 
val file = (P.$$$ "("  P.!!! (P.name  P.$$$ ")")) >> rpair false  P.name >> rpair true; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

38 
val uses = Scan.optional (P.$$$ usesN  P.!!! (Scan.repeat1 file)) []; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

39 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

40 
val args = 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

41 
P.name  (P.$$$ importsN  P.!!! (Scan.repeat1 P.name  uses  P.$$$ beginN)) 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

42 
>> P.triple2; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

43 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

44 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

45 
(* read header *) 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

46 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

47 
val header = 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

48 
(P.$$$ headerN  P.tags)  (P.!!! (P.text  Scan.repeat P.semicolon  
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

49 
(P.$$$ theoryN  P.tags)  args))  
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

50 
(P.$$$ theoryN  P.tags)  P.!!! args; 
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

51 

b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

52 
fun read (src, pos) = 
12840  53 
let val res = 
54 
src 

55 
> Symbol.source false 

17933
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

56 
> T.source false (fn () => (header_lexicon, Scan.empty_lexicon)) pos 
12840  57 
> T.source_proper 
17933
b8f2dd8858f6
removed obsolete nonIsar theory format and old Isar theory headers;
wenzelm
parents:
17075
diff
changeset

58 
> Source.source T.stopper (Scan.single (Scan.error header)) NONE 
12840  59 
> Source.get_single; 
60 
in 

15531  61 
(case res of SOME (x, _) => x 
62 
 NONE => error ("Unexpected end of input" ^ Position.str_of pos)) 

12840  63 
end; 
9139  64 

65 
end; 