src/Tools/Code/code_target.ML
changeset 69650 c95edf19133b
parent 69649 e61b0b819d28
child 69660 2bc2a8599369
equal deleted inserted replaced
69649:e61b0b819d28 69650:c95edf19133b
   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))