# HG changeset patch
# User haftmann
# Date 1279112024 -7200
# Node ID ffaca9167c1605a68c5a793c50acf4b2fddb8284
# Parent  0000493352471960616e1db29049cb3ed6f83870
export_code without file prints to standard output

diff -r 000049335247 -r ffaca9167c16 NEWS
--- a/NEWS	Wed Jul 14 14:20:47 2010 +0200
+++ b/NEWS	Wed Jul 14 14:53:44 2010 +0200
@@ -17,6 +17,9 @@
 
 *** HOL ***
 
+* code generator: export_code without explicit file declaration prints
+to standard output.  INCOMPATIBILITY.
+
 * Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
 respectively.  INCOMPATIBILITY.
 
diff -r 000049335247 -r ffaca9167c16 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 14 14:20:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Wed Jul 14 14:53:44 2010 +0200
@@ -998,9 +998,9 @@
   \end{matharray}
 
   \begin{rail}
-    'export\_code' ( constexpr + ) \\
-      ( ( 'in' target ( 'module\_name' string ) ? \\
-        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
+     'export\_code' ( constexpr + ) \\
+       ( ( 'in' target ( 'module\_name' string ) ? \\
+        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     ;
 
     const: term
@@ -1091,7 +1091,7 @@
   For \emph{SML} and \emph{OCaml}, the file specification refers to a
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
-  hierarchy.  The file specification ``@{text "-"}'' denotes standard
+  hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For
diff -r 000049335247 -r ffaca9167c16 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 14 14:20:47 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Wed Jul 14 14:53:44 2010 +0200
@@ -1014,9 +1014,9 @@
   \end{matharray}
 
   \begin{rail}
-    'export\_code' ( constexpr + ) \\
-      ( ( 'in' target ( 'module\_name' string ) ? \\
-        'file' ( string | '-' ) ( '(' args ')' ) ?) + ) ?
+     'export\_code' ( constexpr + ) \\
+       ( ( 'in' target ( 'module\_name' string ) ? \\
+        ( 'file' ( string | '-' ) ) ? ( '(' args ')' ) ?) + ) ?
     ;
 
     const: term
@@ -1106,7 +1106,7 @@
   For \emph{SML} and \emph{OCaml}, the file specification refers to a
   single file; for \emph{Haskell}, it refers to a whole directory,
   where code is generated in multiple files reflecting the module
-  hierarchy.  The file specification ``\isa{{\isachardoublequote}{\isacharminus}{\isachardoublequote}}'' denotes standard
+  hierarchy.  Omitting the file specification denotes standard
   output.
 
   Serializers take an optional list of arguments in parentheses.  For