--- a/NEWS Fri Mar 29 12:24:34 2019 +0100
+++ b/NEWS Fri Mar 29 13:42:17 2019 +0100
@@ -133,20 +133,20 @@
to lift specifications to the global theory level.
* Command 'export_code' produces output as logical files within the
-theory context, as well as session exports that can be materialized
-using the command-line tools "isabelle export" or "isabelle build -e"
-(with 'export_files' in the session ROOT), or browsed in Isabelle/jEdit
-via the "isabelle-export:" file-system. A 'file_prefix' argument allows
-to specify an explicit prefix, the default is "export" with a
-consecutive number within each theory. The overall prefix "code" is
-always prepended.
+theory context, as well as formal session exports that can be
+materialized via command-line tools "isabelle export" or "isabelle build
+-e" (with 'export_files' in the session ROOT). Isabelle/jEdit also
+provides a virtual file-system "isabelle-export:" that can be explored
+in the regular file-browser. A 'file_prefix' argument allows to specify
+an explicit name prefix for the target file (SML, OCaml, Scala) or
+directory (Haskell); the default is "export" with a consecutive number
+within each theory.
* Command 'export_code': the 'file' argument is now legacy and will be
removed soon: writing to the physical file-system is not well-defined in
-a reactive/parallel application like Isabelle. The empty 'file' has been
-discontinued already: it has been superseded by the file-browser in
-Isabelle/jEdit with "isabelle-export:" as file-system. Minor
-INCOMPATIBILITY.
+a reactive/parallel application like Isabelle. The empty 'file' argument
+has been discontinued already: it is superseded by the file-browser in
+Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
* Code generation for OCaml: proper strings are used for literals.
Minor INCOMPATIBILITY.
--- a/src/Doc/Codegen/Introduction.thy Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Doc/Codegen/Introduction.thy Fri Mar 29 13:42:17 2019 +0100
@@ -68,8 +68,7 @@
text \<open>\noindent Then we can generate code e.g.~for \<open>SML\<close> as follows:\<close>
-export_code %quote empty dequeue enqueue in SML
- module_name Example file_prefix example
+export_code %quote empty dequeue enqueue in SML module_name Example
text \<open>\noindent resulting in the following code:\<close>
@@ -78,29 +77,29 @@
\<close>
text \<open>
- \noindent The @{command_def export_code} command takes a space-separated
- list of constants for which code shall be generated; anything else needed
- for those is added implicitly. Then follows a target language identifier
- and a freely chosen \<^theory_text>\<open>module_name\<close>. A \<^theory_text>\<open>file_prefix\<close> introduces
- sub-directory structure for the output of logical files (within the
- theory context), as well as session exports; the default is \<^verbatim>\<open>export\<close>
- with a consecutive number within the current theory. The prefix \<^verbatim>\<open>code\<close>
- is always prepended to the code output directory. For \<open>SML\<close>, \<open>OCaml\<close> and
- \<open>Scala\<close> the result is a single file, for \<open>Haskell\<close> each module gets its
- own file with the module name and extension \<^verbatim>\<open>.hs\<close>. Here is an example:\<^footnote>\<open>
- The exports may be explored within the Isabelle/jEdit Prover IDE using
- the file-browser on the \<^verbatim>\<open>isabelle-export:\<close> virtual file-system.\<close>
+ \noindent The @{command_def export_code} command takes multiple constants
+ for which code shall be generated; anything else needed for those is
+ added implicitly. Then follows a target language identifier and a freely
+ chosen \<^theory_text>\<open>module_name\<close>.
- %FIXME old/new "name"
- %name denotes the destination to store the generated
- %code. Note that the semantics of the destination depends on the target
- %language: for \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close> it denotes a \emph{file}, for
- %\<open>Haskell\<close> it denotes a \emph{directory} where a file named as the module
- %name (with extension \<open>.hs\<close>) is written:
+ Output is written to a logical file-system within the theory context,
+ with the theory name and ``\<^verbatim>\<open>code\<close>'' as overall prefix. There is also a
+ formal session export using the same name: the result may be explored in
+ the Isabelle/jEdit Prover IDE using the file-browser on the URL
+ ``\<^verbatim>\<open>isabelle-export:\<close>''.
+
+ The file name is determined by the target language together with an
+ optional \<^theory_text>\<open>file_prefix\<close> (the default is ``\<^verbatim>\<open>export\<close>'' with a consecutive
+ number within the current theory). For \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close>, the
+ file prefix becomes a plain file with extension (e.g.\ ``\<^verbatim>\<open>.ML\<close>'' for
+ SML). For \<open>Haskell\<close> the file prefix becomes a directory that is populated
+ with a separate file for each module (with extension ``\<^verbatim>\<open>.hs\<close>'').
+
+ Consider the following example:
\<close>
export_code %quote empty dequeue enqueue in Haskell
- module_name Example file_prefix examples
+ module_name Example file_prefix example
text \<open>
\noindent This is the corresponding code:
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Fri Mar 29 13:42:17 2019 +0100
@@ -2285,7 +2285,7 @@
;
export_target:
@'in' target (@'module_name' @{syntax name})? \<newline>
- (@'file_prefix' @{syntax embedded})? ('(' args ')')?
+ (@'file_prefix' @{syntax path})? ('(' args ')')?
;
target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
;
@@ -2297,6 +2297,8 @@
;
class: @{syntax name}
;
+ path: @{syntax embedded}
+ ;
@@{attribute (HOL) code} ('equation' | 'nbe' | 'abstype' | 'abstract'
| 'del' | 'drop:' (const+) | 'abort:' (const+))?
;
@@ -2365,7 +2367,7 @@
;
@@{command (HOL) code_reflect} @{syntax string} \<newline>
(@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \<newline>
- (@'functions' (@{syntax string} +))? (@'file' @{syntax string})?
+ (@'functions' (@{syntax string} +))? (@'file' @{syntax path})?
;
@@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
;
@@ -2391,11 +2393,16 @@
"module_name"} keyword; then \<^emph>\<open>all\<close> code is placed in this module.
Generated code is output as logical files within the theory context, as well
- as session exports that can be retrieved using @{tool_ref export} (or @{tool
+ as session exports that can be retrieved using @{tool_ref export}, or @{tool
build} with option \<^verbatim>\<open>-e\<close> and suitable \isakeyword{export\_files}
- specifications in the session \<^verbatim>\<open>ROOT\<close> entry). All files have a directory
- prefix \<^verbatim>\<open>code\<close> plus an extra file prefix that may be given via
- \<^theory_text>\<open>file_prefix\<close> --- the default is a numbered prefix \<^verbatim>\<open>export\<close>\<open>N\<close>.
+ specifications in the session \<^verbatim>\<open>ROOT\<close> entry. All files have a common
+ directory prefix: the long theory name plus ``\<^verbatim>\<open>code\<close>''. The actual file
+ name is determined by the target language together with an optional
+ \<^theory_text>\<open>file_prefix\<close> (the default is ``\<^verbatim>\<open>export\<close>'' with a consecutive number
+ within the current theory). For \<open>SML\<close>, \<open>OCaml\<close> and \<open>Scala\<close>, the file prefix
+ becomes a plain file with extension (e.g.\ ``\<^verbatim>\<open>.ML\<close>'' for SML). For
+ \<open>Haskell\<close> the file prefix becomes a directory that is populated with a
+ separate file for each module (with extension ``\<^verbatim>\<open>.hs\<close>'').
Serializers take an optional list of arguments in parentheses.
--- a/src/Pure/Thy/export.ML Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Pure/Thy/export.ML Fri Mar 29 13:42:17 2019 +0100
@@ -6,6 +6,7 @@
signature EXPORT =
sig
+ val check_name: Path.T -> string
type params = {theory: theory, path: Path.T, executable: bool, compress: bool}
val export_params: params -> string list -> unit
val export: theory -> Path.T -> string list -> unit
--- a/src/Tools/Code/code_runtime.ML Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Tools/Code/code_runtime.ML Fri Mar 29 13:42:17 2019 +0100
@@ -780,7 +780,7 @@
(Parse.name -- Scan.optional (\<^keyword>\<open>datatypes\<close> |-- Parse.!!! (parse_datatype
::: Scan.repeat (\<^keyword>\<open>and\<close> |-- parse_datatype))) []
-- Scan.optional (\<^keyword>\<open>functions\<close> |-- Parse.!!! (Scan.repeat1 Parse.name)) []
- -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.name)
+ -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.!!! Parse.embedded)
>> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
(code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
--- a/src/Tools/Code/code_target.ML Fri Mar 29 12:24:34 2019 +0100
+++ b/src/Tools/Code/code_target.ML Fri Mar 29 13:42:17 2019 +0100
@@ -276,17 +276,17 @@
fun export_logical file_prefix format pretty_modules =
let
val prefix = Path.append (Path.basic codeN) file_prefix;
- fun export name content thy =
+ fun export path content thy =
let
- val path = Path.append prefix name;
val thy' = thy |> Generated_Files.add_files ((path, Position.none), content);
val _ = Export.export thy' path [content];
in thy' end;
in
(case pretty_modules of
- Singleton (ext, p) => export (Path.basic (generatedN ^ "." ^ ext)) (format p)
- | Hierarchy modules => fold (fn (names, p) => export (Path.make names) (format p)) modules)
- #> tap (fn thy => writeln (Export.message thy prefix))
+ Singleton (ext, p) => export (Path.ext ext prefix) (format p)
+ | Hierarchy modules =>
+ fold (fn (names, p) => export (Path.append prefix (Path.make names)) (format p)) modules)
+ #> tap (fn thy => writeln (Export.message thy (Path.basic codeN)))
end;
fun export_physical root format pretty_modules =
@@ -504,7 +504,10 @@
fun prep_destination (location, (s, pos)) =
if location = {physical = false} then
- (location, Path.explode s handle ERROR msg => error (msg ^ Position.here pos))
+ let
+ val path = (Path.explode s |> tap Export.check_name)
+ handle ERROR msg => error (msg ^ Position.here pos)
+ in (location, path) end
else
let
val _ =