1(*  Title:      Pure/Thy/thy_header.ML
2    Author:     Makarius
3
4Static theory header information.
5*)
6
7signature THY_HEADER =
8sig
9  type keywords = ((string * Position.T) * Keyword.spec) list
10  type header =
11   {name: string * Position.T,
12    imports: (string * Position.T) list,
13    keywords: keywords}
14  val make: string * Position.T -> (string * Position.T) list -> keywords -> header
15  val theoryN: string
16  val bootstrap_keywords: Keyword.keywords
17  val add_keywords: keywords -> theory -> theory
18  val get_keywords: theory -> Keyword.keywords
19  val get_keywords': Proof.context -> Keyword.keywords
20  val ml_bootstrapN: string
21  val ml_roots: string list
22  val bootstrap_thys: string list
23  val is_base_name: string -> bool
24  val import_name: string -> string
25  val args: header parser
26  val read_tokens: Position.T -> Token.T list -> header
27  val read: Position.T -> string -> header
28end;
29
30structure Thy_Header: THY_HEADER =
31struct
32
33(** keyword declarations **)
34
35(* header *)
36
37type keywords = ((string * Position.T) * Keyword.spec) list;
38
39type header =
40 {name: string * Position.T,
41  imports: (string * Position.T) list,
42  keywords: keywords};
43
44fun make name imports keywords : header =
45  {name = name, imports = imports, keywords = keywords};
46
47
48(* bootstrap keywords *)
49
50val chapterN = "chapter";
51val sectionN = "section";
52val subsectionN = "subsection";
53val subsubsectionN = "subsubsection";
54val paragraphN = "paragraph";
55val subparagraphN = "subparagraph";
56val textN = "text";
57val txtN = "txt";
58val text_rawN = "text_raw";
59
60val theoryN = "theory";
61val importsN = "imports";
62val keywordsN = "keywords";
63val abbrevsN = "abbrevs";
64val beginN = "begin";
65
66val bootstrap_keywords =
67  Keyword.empty_keywords
68  |> Keyword.add_keywords
69    [(("%", \<^here>), Keyword.no_spec),
70     (("(", \<^here>), Keyword.no_spec),
71     ((")", \<^here>), Keyword.no_spec),
72     ((",", \<^here>), Keyword.no_spec),
73     (("::", \<^here>), Keyword.no_spec),
74     (("=", \<^here>), Keyword.no_spec),
75     (("and", \<^here>), Keyword.no_spec),
76     ((beginN, \<^here>), Keyword.quasi_command_spec),
77     ((importsN, \<^here>), Keyword.quasi_command_spec),
78     ((keywordsN, \<^here>), Keyword.quasi_command_spec),
79     ((abbrevsN, \<^here>), Keyword.quasi_command_spec),
80     ((chapterN, \<^here>), Keyword.document_heading_spec),
81     ((sectionN, \<^here>), Keyword.document_heading_spec),
82     ((subsectionN, \<^here>), Keyword.document_heading_spec),
83     ((subsubsectionN, \<^here>), Keyword.document_heading_spec),
84     ((paragraphN, \<^here>), Keyword.document_heading_spec),
85     ((subparagraphN, \<^here>), Keyword.document_heading_spec),
86     ((textN, \<^here>), Keyword.document_body_spec),
87     ((txtN, \<^here>), Keyword.document_body_spec),
88     ((text_rawN, \<^here>), ((Keyword.document_raw, []), ["document"])),
89     ((theoryN, \<^here>), ((Keyword.thy_begin, []), ["theory"])),
90     (("ML", \<^here>), ((Keyword.thy_decl, []), ["ML"]))];
91
92
93(* theory data *)
94
95structure Data = Theory_Data
96(
97  type T = Keyword.keywords;
98  val empty = bootstrap_keywords;
99  val extend = I;
100  val merge = Keyword.merge_keywords;
101);
102
103val add_keywords = Data.map o Keyword.add_keywords;
104
105val get_keywords = Data.get;
106val get_keywords' = get_keywords o Proof_Context.theory_of;
107
108
109
110(** concrete syntax **)
111
112(* names *)
113
114val ml_bootstrapN = "ML_Bootstrap";
115val ml_roots = ["ML_Root0", "ML_Root"];
116val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
117
118fun is_base_name s =
119  s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
120
121fun import_name s =
122  if String.isSuffix ".thy" s then
123    error ("Malformed theory import: " ^ quote s)
124  else Path.base_name (Path.explode s);
125
126
127(* header args *)
128
129local
130
131fun imports name =
132  if name = Context.PureN then Scan.succeed []
133  else Parse.$$$ importsN |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.theory_name));
134
135val opt_files =
136  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.list1 Parse.name) --| Parse.$$$ ")") [];
137
138val keyword_spec =
139  Parse.group (fn () => "outer syntax keyword specification")
140    (Parse.name -- opt_files -- Parse.tags);
141
142val keyword_decl =
143  Scan.repeat1 (Parse.position Parse.string) --
144  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
145  >> (fn (names, spec) => map (rpair spec) names);
146
147val abbrevs =
148  Parse.and_list1
149    (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text))
150      >> uncurry (map_product pair)) >> flat;
151
152val keyword_decls = Parse.and_list1 keyword_decl >> flat;
153
154in
155
156val args =
157  Parse.position Parse.theory_name :|-- (fn (name, pos) =>
158    imports name --
159    Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
160    (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
161    >> (fn (imports, keywords) => make (name, pos) imports keywords));
162
163end;
164
165
166(* read header *)
167
168val heading =
169  (Parse.command_name chapterN ||
170    Parse.command_name sectionN ||
171    Parse.command_name subsectionN ||
172    Parse.command_name subsubsectionN ||
173    Parse.command_name paragraphN ||
174    Parse.command_name subparagraphN ||
175    Parse.command_name textN ||
176    Parse.command_name txtN ||
177    Parse.command_name text_rawN) --
178  Parse.tags -- Parse.!!! Parse.document_source;
179
180val parse_header =
181  (Scan.repeat heading -- Parse.command_name theoryN -- Parse.tags) |-- Parse.!!! args;
182
183fun read_tokens pos toks =
184  filter Token.is_proper toks
185  |> Source.of_list
186  |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! parse_header)))
187  |> Source.get_single
188  |> (fn SOME (header, _) => header | NONE => error ("Unexpected end of input" ^ Position.here pos));
189
190local
191
192fun read_header pos text =
193  Symbol_Pos.explode (text, pos)
194  |> Token.tokenize bootstrap_keywords {strict = false}
195  |> read_tokens pos;
196
197val approx_length = 1024;
198
199in
200
201fun read pos text =
202  if size text <= approx_length then read_header pos text
203  else
204    let val approx_text = String.substring (text, 0, approx_length) in
205      if String.isSuffix "begin" approx_text then read_header pos text
206      else (read_header pos approx_text handle ERROR _ => read_header pos text)
207    end;
208
209end;
210
211end;
212