# HG changeset patch
# User haftmann
# Date 1393148697 -3600
# Node ID e99ed112d303d2ca0ed5f75f116dd8f86a88af97
# Parent  3f8bdc5364a9f2f6af1c7ee1e1ad64a3fdf720de
NEWS and documentation, including correction of long-overseen "*"

diff -r 3f8bdc5364a9 -r e99ed112d303 NEWS
--- a/NEWS	Sun Feb 23 10:33:43 2014 +0100
+++ b/NEWS	Sun Feb 23 10:44:57 2014 +0100
@@ -90,6 +90,8 @@
 
 *** HOL ***
 
+* Code generator: minimize exported identifiers by default.
+
 * Code generation for SML and OCaml: dropped arcane "no_signatures" option.
 
 * Simproc "finite_Collect" is no longer enabled by default, due to
diff -r 3f8bdc5364a9 -r e99ed112d303 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:33:43 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Sun Feb 23 10:44:57 2014 +0100
@@ -2393,7 +2393,7 @@
   \end{matharray}
 
   @{rail \<open>
-    @@{command (HOL) export_code} ( constexpr + ) \<newline>
+    @@{command (HOL) export_code} ( @'open' ) ? ( constexpr + ) \<newline>
        ( ( @'in' target ( @'module_name' @{syntax string} ) ? \<newline>
         ( @'file' @{syntax string} ) ? ( '(' args ')' ) ?) + ) ?
     ;
@@ -2521,8 +2521,12 @@
 
   Constants may be specified by giving them literally, referring to
   all executable constants within a certain theory by giving @{text
-  "name.*"}, or referring to \emph{all} executable constants currently
-  available by giving @{text "*"}.
+  "name._"}, or referring to \emph{all} executable constants currently
+  available by giving @{text "_"}.
+
+  By default, exported identifiers are minimized per module.  This
+  can be suppressed by prepending @{keyword "open"} before the list
+  of contants.
 
   By default, for each involved theory one corresponding name space
   module is generated.  Alternatively, a module name may be specified