2282 |
2282 |
2283 \<^rail>\<open> |
2283 \<^rail>\<open> |
2284 @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*) |
2284 @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*) |
2285 ; |
2285 ; |
2286 export_target: |
2286 export_target: |
2287 @'in' target (@'module_name' @{syntax string})? \<newline> |
2287 @'in' target (@'module_name' @{syntax name})? \<newline> |
2288 (@'file' @{syntax string})? ('(' args ')')? |
2288 (@'file_prefix' @{syntax embedded})? ('(' args ')')? |
2289 ; |
2289 ; |
2290 target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval' |
2290 target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval' |
2291 ; |
2291 ; |
2292 const_expr: (const | 'name._' | '_') |
2292 const_expr: (const | 'name._' | '_') |
2293 ; |
2293 ; |
2388 |
2388 |
2389 By default, for each involved theory one corresponding name space module is |
2389 By default, for each involved theory one corresponding name space module is |
2390 generated. Alternatively, a module name may be specified after the @{keyword |
2390 generated. Alternatively, a module name may be specified after the @{keyword |
2391 "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module. |
2391 "module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module. |
2392 |
2392 |
2393 By default, generated code is treated as theory export which can be |
2393 Generated code is output as logical files within the theory context, as well |
2394 explicitly retrieved using @{tool_ref export}. For diagnostic purposes |
2394 as session exports that can be retrieved using @{tool_ref export} (or @{tool |
2395 generated code can also be written to the file system using @{keyword "file"}; |
2395 build} with option \<^verbatim>\<open>-e\<close> and suitable \isakeyword{export\_files} |
2396 for \<^emph>\<open>SML\<close>, \<^emph>\<open>OCaml\<close> and \<^emph>\<open>Scala\<close> the file specification refers to a single |
2396 specifications in the session \<^verbatim>\<open>ROOT\<close> entry). All files have a directory |
2397 file; for \<^emph>\<open>Haskell\<close>, it refers to a whole directory, where code is |
2397 prefix \<^verbatim>\<open>code\<close> plus an extra file prefix that may be given via |
2398 generated in multiple files reflecting the module hierarchy. |
2398 \<^theory_text>\<open>file_prefix\<close> --- the default is a numbered prefix \<^verbatim>\<open>export\<close>\<open>N\<close>. |
2399 Passing an empty file specification denotes standard output. |
|
2400 |
2399 |
2401 Serializers take an optional list of arguments in parentheses. |
2400 Serializers take an optional list of arguments in parentheses. |
2402 |
2401 |
2403 \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' |
2402 \<^item> For \<^emph>\<open>Haskell\<close> a module name prefix may be given using the ``\<open>root:\<close>'' |
2404 argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause |
2403 argument; ``\<open>string_classes\<close>'' adds a ``\<^verbatim>\<open>deriving (Read, Show)\<close>'' clause |