--- 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.
--- 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
--- 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