# HG changeset patch
# User wenzelm
# Date 1547407541 -3600
# Node ID e61b0b819d288bb01c7df55fad9935dd715cc6b4
# Parent  97ddaec3e2ae692b997ae2c1b3e721ce227038a6
information with hyperlink to "isabelle-export:";

diff -r 97ddaec3e2ae -r e61b0b819d28 NEWS
--- a/NEWS	Sun Jan 13 19:42:06 2019 +0100
+++ b/NEWS	Sun Jan 13 20:25:41 2019 +0100
@@ -75,9 +75,10 @@
 *** HOL ***
 
 * Code generation: command 'export_code' without file keyword exports
-code as regular theory export, which can be materialized using tool
-'isabelle export'; to get generated code dumped into output, use
-'file ""'.  Minor INCOMPATIBILITY.
+code as regular theory export, which can be materialized using the
+command-line tool "isabelle export", or browsed in Isabelle/jEdit via
+the "isabelle-export:" file-system. To get generated code dumped into
+output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
 
 * Simplified syntax setup for big operators under image. In rare
 situations, type conversions are not inserted implicitly any longer
diff -r 97ddaec3e2ae -r e61b0b819d28 src/Tools/Code/code_target.ML
--- 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, _) =