# HG changeset patch
# User wenzelm
# Date 1553863337 -3600
# Node ID 9dde788b0128a2d5ececb93da503e2b4104179f6
# Parent  499896e3a7b0aa788193b094aaba714f58bb06d3
clarified 'file_prefix';

diff -r 499896e3a7b0 -r 9dde788b0128 NEWS
--- 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.
diff -r 499896e3a7b0 -r 9dde788b0128 src/Doc/Codegen/Introduction.thy
--- 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:
diff -r 499896e3a7b0 -r 9dde788b0128 src/Doc/Isar_Ref/HOL_Specific.thy
--- 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.
 
diff -r 499896e3a7b0 -r 9dde788b0128 src/Pure/Thy/export.ML
--- 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
diff -r 499896e3a7b0 -r 9dde788b0128 src/Tools/Code/code_runtime.ML
--- 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)));
 
diff -r 499896e3a7b0 -r 9dde788b0128 src/Tools/Code/code_target.ML
--- 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 _ =