--- a/src/Tools/Code/code_target.ML Sun Jan 13 19:42:06 2019 +0100
+++ b/src/Tools/Code/code_target.ML Sun Jan 13 20:25:41 2019 +0100
@@ -176,11 +176,14 @@
map (fn (names, p) => File.write (Path.appends (root :: map Path.basic names)) (Code_Printer.format [] width p)) code_modules;
());
+fun export_information thy name content =
+ (Export.export thy name [content]; Export.information thy "");
+
fun export_to_exports thy width (Singleton (extension, p)) =
- Export.export thy (generatedN ^ "." ^ extension) [Code_Printer.format [] width p]
+ export_information thy (generatedN ^ "." ^ extension) (Code_Printer.format [] width p)
| export_to_exports thy width (Hierarchy code_modules) = (
- map (fn (names, p) => Export.export thy (Path.implode (Path.make names))
- [Code_Printer.format [] width p]) code_modules;
+ map (fn (names, p) => export_information thy (Path.implode (Path.make names))
+ (Code_Printer.format [] width p)) code_modules;
());
fun export_result ctxt some_file width (pretty_code, _) =