"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
"export_code ... file" is legacy, the empty name form has been discontinued;
updated examples;

--- a/NEWS	Thu Mar 28 21:22:44 2019 +0100
+++ b/NEWS	Thu Mar 28 21:24:55 2019 +0100
@@ -132,12 +132,21 @@
 Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result]
 to lift specifications to the global theory level.
 
-* Code generation: command 'export_code' without file keyword exports
-code as regular theory export, which 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. To get generated code dumped into
-output, use "file \<open>\<close>". Minor INCOMPATIBILITY.
+* 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.
+
+* 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.
 
 * Code generation for OCaml: proper strings are used for literals.
 Minor INCOMPATIBILITY.

--- a/src/Doc/Codegen/Introduction.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Doc/Codegen/Introduction.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -69,7 +69,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 \<open>$ISABELLE_TMP/example.ML\<close>
+  module_name Example file_prefix example
 
 text \<open>\noindent resulting in the following code:\<close>
 
@@ -78,19 +78,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 module name.  A file
-  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:
+  \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>
+
+  %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:
 \<close>
 
 export_code %quote empty dequeue enqueue in Haskell
-  module_name Example file \<open>$ISABELLE_TMP/examples/\<close>
+  module_name Example file_prefix examples
 
 text \<open>
   \noindent This is the corresponding code:

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -2284,8 +2284,8 @@
     @@{command (HOL) export_code} @'open'? \<newline> (const_expr+) (export_target*)
     ;
     export_target:
-      @'in' target (@'module_name' @{syntax string})? \<newline>
-      (@'file' @{syntax string})? ('(' args ')')?
+      @'in' target (@'module_name' @{syntax name})? \<newline>
+      (@'file_prefix' @{syntax embedded})? ('(' args ')')?
     ;
     target: 'SML' | 'OCaml' | 'Haskell' | 'Scala' | 'Eval'
     ;
@@ -2390,13 +2390,12 @@
   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.
 
-  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.
-  Passing an empty file specification denotes standard output.
+  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
+  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>.
 
   Serializers take an optional list of arguments in parentheses.
 

--- a/src/HOL/Code_Numeral.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Code_Numeral.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -766,7 +766,7 @@
 code_identifier
   code_module Code_Numeral \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
-export_code divmod_integer in Haskell
+export_code divmod_integer in Haskell file_prefix divmod
 
 
 subsection \<open>Type of target language naturals\<close>

--- a/src/HOL/Quotient_Examples/Lift_DList.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Quotient_Examples/Lift_DList.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -50,5 +50,6 @@
 text \<open>We can export code:\<close>
 
 export_code empty insert remove map filter null member length fold foldr concat in SML
+  file_prefix dlist
 
 end

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -113,7 +113,8 @@
 
 text \<open>We can export code:\<close>
 
-export_code fnil fcons fappend fmap ffilter fset fmember in SML
+export_code fnil fcons fappend fmap ffilter fset fmember in SML file_prefix fset
+
 
 subsection \<open>Using transfer with type \<open>fset\<close>\<close>
 

--- a/src/HOL/Quotient_Examples/Lift_Set.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/Quotient_Examples/Lift_Set.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -28,6 +28,6 @@
 term "Lift_Set.insert"
 thm Lift_Set.insert_def
 
-export_code empty insert in SML
+export_code empty insert in SML file_prefix set
 
 end

--- a/src/HOL/ex/Code_Lazy_Demo.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/HOL/ex/Code_Lazy_Demo.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -62,7 +62,7 @@
 | "lfilter P (x ### xs) = 
    (if P x then x ### lfilter P xs else lfilter P xs)"
 
-export_code lfilter in SML
+export_code lfilter in SML file_prefix lfilter
 
 value [code] "lfilter odd llist"
 

--- a/src/Pure/Pure.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Pure/Pure.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -140,7 +140,7 @@
             val paths = Generated_Files.export_files thy other_thys;
           in
             if not (null paths) then
-              (writeln (Export.message thy "");
+              (writeln (Export.message thy Path.current);
                writeln (cat_lines (paths |> map (fn (path, pos) =>
                 Markup.markup (Markup.entityN, Position.def_properties_of pos)
                   (quote (Path.implode path))))))

--- a/src/Pure/Thy/export.ML	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Pure/Thy/export.ML	Thu Mar 28 21:24:55 2019 +0100
@@ -10,8 +10,8 @@
   val export_params: params -> string list -> unit
   val export: theory -> Path.T -> string list -> unit
   val export_executable: theory -> Path.T -> string list -> unit
-  val markup: theory -> string -> Markup.T
-  val message: theory -> string -> string
+  val markup: theory -> Path.T -> Markup.T
+  val message: theory -> Path.T -> string
 end;
 
 structure Export: EXPORT =
@@ -47,11 +47,13 @@
 
 (* information message *)
 
-fun markup thy s =
-  let val name = (Markup.nameN, Context.theory_long_name thy ^ (if s = "" then "" else "/" ^ s))
+fun markup thy path =
+  let
+    val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path;
+    val name = (Markup.nameN, Path.implode thy_path);
   in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;
 
-fun message thy s =
-  "See " ^ Markup.markup (markup thy s) "theory exports";
+fun message thy path =
+  "See " ^ Markup.markup (markup thy path) "theory exports";
 
 end;

--- a/src/Tools/Code/code_target.ML	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Tools/Code/code_target.ML	Thu Mar 28 21:24:55 2019 +0100
@@ -11,7 +11,7 @@
 
   datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
 
-  val export_code_for: Path.T option option -> string -> string -> int option -> Token.T list
+  val export_code_for: ({physical: bool} * Path.T) option -> string -> string -> int option -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
   val produce_code_for: Proof.context -> string -> string -> int option -> Token.T list
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string list * string) list * string option list
@@ -21,10 +21,10 @@
     -> Code_Thingol.program -> bool -> Code_Symbol.T list -> local_theory -> local_theory
 
   val export_code: bool -> string list
-    -> (((string * string) * Path.T option option) * Token.T list) list
+    -> (((string * string) * ({physical: bool} * Path.T) option) * Token.T list) list
     -> local_theory -> local_theory
   val export_code_cmd: bool -> string list
-    -> (((string * string) * (string * Position.T) option) * Token.T list) list
+    -> (((string * string) * ({physical: bool} * (string * Position.T)) option) * Token.T list) list
     -> local_theory -> local_theory
   val produce_code: Proof.context -> bool -> string list
     -> string -> string -> int option -> Token.T list -> (string list * string) list * string option list
@@ -33,6 +33,7 @@
   val check_code: bool -> string list -> ((string * bool) * Token.T list) list
     -> local_theory -> local_theory
 
+  val codeN: string
   val generatedN: string
   val compilation_text: Proof.context -> string -> Code_Thingol.program
     -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
@@ -148,7 +149,7 @@
   end;
 
 
-(** serializers **)
+(** theory data **)
 
 datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list;
 
@@ -166,65 +167,6 @@
   -> Code_Symbol.T list
   -> pretty_modules * (Code_Symbol.T -> string option);
 
-val generatedN = "Generated_Code";
-
-local
-
-fun flat_modules format pretty_modules =
-  (case pretty_modules of
-    Singleton (_, p) => format p
-  | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules));
-
-fun export_to_file root format pretty_modules =
-  (case pretty_modules of
-    Singleton (_, p) => File.write root (format p)
-  | Hierarchy code_modules =>
-      (Isabelle_System.mkdirs root;
-        List.app (fn (names, p) =>
-          File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
-
-fun export_to_exports format pretty_modules =
-  let
-    fun export name content thy = (Export.export thy name [content]; thy);
-  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)
-  end;
-
-in
-
-fun export_result some_file format (pretty_code, _) thy =
-  (case some_file of
-    NONE =>
-      let
-        val thy' = export_to_exports format pretty_code thy;
-        val _ = writeln (Export.message thy' "");
-      in thy' end
-  | SOME NONE => (writeln (flat_modules format pretty_code); thy)
-  | SOME (SOME relative_root) =>
-      let
-        val root = File.full_path (Resources.master_directory thy) relative_root;
-        val _ = File.check_dir (Path.dir root);
-        val _ = export_to_file root format pretty_code;
-      in thy end);
-
-fun produce_result syms width pretty_modules =
-  let val format = Code_Printer.format [] width in
-    (case pretty_modules of
-      (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms)
-    | (Hierarchy code_modules, deresolve) =>
-        ((map o apsnd) format code_modules, map deresolve syms))
-  end;
-
-fun present_result selects width (pretty_code, _) =
-  flat_modules (Code_Printer.format selects width) pretty_code;
-
-end;
-
-
-(** theory data **)
-
 type language = {serializer: serializer, literals: literals,
   check: {env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string},
   evaluation_args: Token.T list};
@@ -237,26 +179,33 @@
 
 structure Targets = Theory_Data
 (
-  type T = (target * Code_Printer.data) Symtab.table;
-  val empty = Symtab.empty;
-  val extend = I;
-  fun merge (targets1, targets2) : T =
-    Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
-      if #serial target1 = #serial target2 then
-      ({serial = #serial target1, language = #language target1,
-        ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
-        Code_Printer.merge_data (data1, data2))
-      else error ("Incompatible targets: " ^ quote target_name)
-    ) (targets1, targets2)
+  type T = (target * Code_Printer.data) Symtab.table * int;
+  val empty = (Symtab.empty, 0);
+  fun extend (targets, _) = (targets, 0);
+  fun merge ((targets1, _), (targets2, _)) : T =
+    let val targets' =
+      Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
+        if #serial target1 = #serial target2 then
+        ({serial = #serial target1, language = #language target1,
+          ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
+          Code_Printer.merge_data (data1, data2))
+        else error ("Incompatible targets: " ^ quote target_name)) (targets1, targets2)
+    in (targets', 0) end;
 );
 
-fun exists_target thy = Symtab.defined (Targets.get thy);
-fun lookup_target_data thy = Symtab.lookup (Targets.get thy);
+val exists_target = Symtab.defined o #1 o Targets.get;
+val lookup_target_data = Symtab.lookup o #1 o Targets.get;
 fun assert_target thy target_name =
   if exists_target thy target_name
   then target_name
   else error ("Unknown code target language: " ^ quote target_name);
 
+fun next_export thy =
+  let
+    val thy' = (Targets.map o apsnd) (fn i => i + 1) thy;
+    val i = #2 (Targets.get thy');
+  in ("export" ^ string_of_int i, thy') end;
+
 fun fold1 f xs = fold f (tl xs) (hd xs);
 
 fun join_ancestry thy target_name =
@@ -278,7 +227,7 @@
       else ();
   in
     thy
-    |> (Targets.map o Symtab.update) (target_name, (target, Code_Printer.empty_data))
+    |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))
   end;
 
 fun add_language (target_name, language) =
@@ -309,7 +258,7 @@
     val _ = assert_target thy target_name;
   in
     thy
-    |> (Targets.map o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
+    |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
   end;
 
 fun map_reserved target_name = map_data target_name o @{apply 3(1)};
@@ -317,6 +266,71 @@
 fun map_printings target_name = map_data target_name o @{apply 3(3)};
 
 
+(** serializers **)
+
+val codeN = "code";
+val generatedN = "Generated_Code";
+
+local
+
+fun export_logical file_prefix format pretty_modules =
+  let
+    val prefix = Path.append (Path.basic codeN) file_prefix;
+    fun export name 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))
+  end;
+
+fun export_physical root format pretty_modules =
+  (case pretty_modules of
+    Singleton (_, p) => File.write root (format p)
+  | Hierarchy code_modules =>
+      (Isabelle_System.mkdirs root;
+        List.app (fn (names, p) =>
+          File.write (Path.appends (root :: map Path.basic names)) (format p)) code_modules));
+
+in
+
+fun export_result some_file format (pretty_code, _) thy =
+  (case some_file of
+    NONE =>
+      let val (file_prefix, thy') = next_export thy;
+      in export_logical (Path.basic file_prefix) format pretty_code thy' end
+  | SOME ({physical = false}, file_prefix) =>
+      export_logical file_prefix format pretty_code thy
+  | SOME ({physical = true}, file) =>
+      let
+        val root = File.full_path (Resources.master_directory thy) file;
+        val _ = File.check_dir (Path.dir root);
+        val _ = export_physical root format pretty_code;
+      in thy end);
+
+fun produce_result syms width pretty_modules =
+  let val format = Code_Printer.format [] width in
+    (case pretty_modules of
+      (Singleton (_, p), deresolve) => ([([], format p)], map deresolve syms)
+    | (Hierarchy code_modules, deresolve) =>
+        ((map o apsnd) format code_modules, map deresolve syms))
+  end;
+
+fun present_result selects width (pretty_modules, _) =
+  let val format = Code_Printer.format selects width in
+    (case pretty_modules of
+      Singleton (_, p) => format p
+    | Hierarchy code_modules => space_implode "\n\n" (map (format o #2) code_modules))
+  end;
+
+end;
+
+
 (** serializer usage **)
 
 (* technical aside: pretty printing width *)
@@ -434,7 +448,7 @@
         val destination = make_destination p;
         val lthy' = lthy
           |> Local_Theory.background_theory
-            (export_result (SOME (SOME destination)) format
+            (export_result (SOME ({physical = true}, destination)) format
               (invoke_serializer lthy target_name generatedN args program all_public syms));
         val cmd = make_command generatedN;
         val context_cmd = "cd " ^ File.bash_path p ^ " && " ^ cmd ^ " 2>&1";
@@ -488,14 +502,23 @@
 
 (* code generation *)
 
-fun prep_destination (s, pos) =
-  if s = "" then NONE
+fun prep_destination (location, (s, pos)) =
+  if location = {physical = false} then
+    (location, Path.explode s handle ERROR msg => error (msg ^ Position.here pos))
   else
     let
+      val _ =
+        if s = ""
+        then error ("Bad bad empty " ^ Markup.markup Markup.keyword2 "file" ^ " argument")
+        else ();
+      val _ =
+        legacy_feature
+          (Markup.markup Markup.keyword1 "export_code" ^ " with " ^
+            Markup.markup Markup.keyword2 "file" ^ " argument" ^ Position.here pos);
       val _ = Position.report pos Markup.language_path;
       val path = Path.explode s;
       val _ = Position.report pos (Markup.path (Path.smart_implode path));
-    in SOME path end;
+    in (location, path) end;
 
 fun export_code all_public cs seris lthy =
   let
@@ -671,7 +694,9 @@
 fun code_expr_inP (all_public, raw_cs) =
   Scan.repeat (\<^keyword>\<open>in\<close> |-- Parse.!!! (Parse.name
     -- Scan.optional (\<^keyword>\<open>module_name\<close> |-- Parse.name) ""
-    -- Scan.option (\<^keyword>\<open>file\<close> |-- Parse.position Parse.path)
+    -- Scan.option
+        ((\<^keyword>\<open>file_prefix\<close> >> K {physical = false} || \<^keyword>\<open>file\<close> >> K {physical = true})
+          -- Parse.!!! (Parse.position Parse.path))
     -- code_expr_argsP))
       >> (fn seri_args => export_code_cmd all_public raw_cs seri_args);
 

--- a/src/Tools/Code_Generator.thy	Thu Mar 28 21:22:44 2019 +0100
+++ b/src/Tools/Code_Generator.thy	Thu Mar 28 21:24:55 2019 +0100
@@ -11,7 +11,7 @@
   "export_code" "code_identifier" "code_printing" "code_reserved"
     "code_monad" "code_reflect" :: thy_decl and
   "checking" and
-  "datatypes" "functions" "module_name" "file"
+  "datatypes" "functions" "module_name" "file" "file_prefix"
     "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"
     :: quasi_command
 begin