--- a/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 10 12:07:05 2019 +0000
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Jan 10 12:07:08 2019 +0000
@@ -2386,10 +2386,13 @@
generated. Alternatively, a module name may be specified after the @{keyword
"module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
- For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
+ By default, generated code is treated as theory export which can be
+ explicitly retrieved using @{tool_ref export}. For diagnostic purposes
+ generated code can also be written to the file system using @{keyword "file"};
+ for \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single
file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is
- generated in multiple files reflecting the module hierarchy. Omitting the
- file specification denotes standard output.
+ generated in multiple files reflecting the module hierarchy.
+ Passing an empty file specification denotes standard output.
Serializers take an optional list of arguments in parentheses.