2384 |
2384 |
2385 By default, for each involved theory one corresponding name space module is |
2385 By default, for each involved theory one corresponding name space module is |
2386 generated. Alternatively, a module name may be specified after the @{keyword |
2386 generated. Alternatively, a module name may be specified after the @{keyword |
2387 "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module. |
2387 "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module. |
2388 |
2388 |
2389 For \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single |
2389 By default, generated code is treated as theory export which can be |
|
2390 explicitly retrieved using @{tool_ref export}. For diagnostic purposes |
|
2391 generated code can also be written to the file system using @{keyword "file"}; |
|
2392 for \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single |
2390 file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is |
2393 file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is |
2391 generated in multiple files reflecting the module hierarchy. Omitting the |
2394 generated in multiple files reflecting the module hierarchy. |
2392 file specification denotes standard output. |
2395 Passing an empty file specification denotes standard output. |
2393 |
2396 |
2394 Serializers take an optional list of arguments in parentheses. |
2397 Serializers take an optional list of arguments in parentheses. |
2395 |
2398 |
2396 \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' |
2399 \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' |
2397 argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause |
2400 argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause |