equal
deleted
inserted
replaced
175 Isabelle_System.mkdirs root; |
175 Isabelle_System.mkdirs root; |
176 map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules; |
176 map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules; |
177 ()); |
177 ()); |
178 |
178 |
179 fun export_information thy name content = |
179 fun export_information thy name content = |
180 (Export.export thy name [content]; Export.information thy ""); |
180 (Export.export thy name [content]; writeln (Export.message thy "")); |
181 |
181 |
182 fun export_to_exports thy width (Singleton (extension, p)) = |
182 fun export_to_exports thy width (Singleton (extension, p)) = |
183 export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p) |
183 export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p) |
184 | export_to_exports thy width (Hierarchy code_modules) = ( |
184 | export_to_exports thy width (Hierarchy code_modules) = ( |
185 map (fn (names, p) => export_information thy (Path.implode (Path.make names)) |
185 map (fn (names, p) => export_information thy (Path.implode (Path.make names)) |