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