'code_reflect' only supports new-style 'file_prefix';
avoid fragile file "$ISABELLE_TMP/rat.ML";

--- a/NEWS	Mon Apr 01 21:51:46 2019 +0200
+++ b/NEWS	Mon Apr 01 21:58:45 2019 +0200
@@ -148,6 +148,10 @@
 has been discontinued already: it is superseded by the file-browser in
 Isabelle/jEdit on "isabelle-export:". Minor INCOMPATIBILITY.
 
+* Command 'code_reflect' no longer supports the 'file' argument: it has
+been superseded by 'file_prefix' for stateless file management as in
+'export_code'. Minor INCOMPATIBILITY.
+
 * Code generation for OCaml: proper strings are used for literals.
 Minor INCOMPATIBILITY.
 

--- a/src/Doc/Codegen/Further.thy	Mon Apr 01 21:51:46 2019 +0200
+++ b/src/Doc/Codegen/Further.thy	Mon Apr 01 21:58:45 2019 +0200
@@ -48,7 +48,7 @@
   functions Fract
     "(plus :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(minus :: rat \<Rightarrow> rat \<Rightarrow> rat)"
     "(times :: rat \<Rightarrow> rat \<Rightarrow> rat)" "(divide :: rat \<Rightarrow> rat \<Rightarrow> rat)"
-  file "$ISABELLE_TMP/rat.ML"
+  file_prefix rat
 
 text \<open>
   \noindent This merely generates the referenced code to the given

--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Apr 01 21:51:46 2019 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Apr 01 21:58:45 2019 +0200
@@ -2367,7 +2367,7 @@
     ;
     @@{command (HOL) code_reflect} @{syntax string} \<newline>
       (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \<newline>
-      (@'functions' (@{syntax string} +))? (@'file' @{syntax path})?
+      (@'functions' (@{syntax string} +))? (@'file_prefix' @{syntax path})?
     ;
     @@{command (HOL) code_pred} \<newline> ('(' @'modes' ':' modedecl ')')? \<newline> const
     ;
@@ -2485,12 +2485,13 @@
   the discretion of the user to ensure that name prefixes of identifiers in
   compound statements like type classes or datatypes are still the same.
 
-  \<^descr> @{command (HOL) "code_reflect"} without a ``\<open>file\<close>'' argument compiles
-  code into the system runtime environment and modifies the code generator
-  setup that future invocations of system runtime code generation referring to
-  one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use these precompiled
-  entities. With a ``\<open>file\<close>'' argument, the corresponding code is generated
-  into that specified file without modifying the code generator setup.
+  \<^descr> @{command (HOL) "code_reflect"} without a ``\<^theory_text>\<open>file_prefix\<close>'' argument
+  compiles code into the system runtime environment and modifies the code
+  generator setup that future invocations of system runtime code generation
+  referring to one of the ``\<open>datatypes\<close>'' or ``\<open>functions\<close>'' entities use
+  these precompiled entities. With a ``\<^theory_text>\<open>file_prefix\<close>'' argument, the
+  corresponding code is generated/exported to the specified file (as for
+  \<^theory_text>\<open>export_code\<close>) without modifying the code generator setup.
 
   \<^descr> @{command (HOL) "code_pred"} creates code equations for a predicate given
   a set of introduction rules. Optional mode annotations determine which

--- a/src/Tools/Code/code_runtime.ML	Mon Apr 01 21:51:46 2019 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon Apr 01 21:58:45 2019 +0200
@@ -19,7 +19,9 @@
     -> ((term -> term) -> 'a -> 'a) -> term -> string list -> 'a Exn.result
   val dynamic_holds_conv: Proof.context -> conv
   val code_reflect: (string * string list option) list -> string list -> string
-    -> string option -> theory -> theory
+    -> Path.binding option -> theory -> theory
+  val code_reflect_cmd: (string * string list option) list -> string list -> string
+    -> Path.binding option -> theory -> theory
   datatype truth = Holds
   val put_truth: (unit -> truth) -> Proof.context -> Proof.context
   val mount_computation: Proof.context -> (string * typ) list -> typ
@@ -711,18 +713,18 @@
       |> fold (add_eval_tyco o apsnd Code_Printer.str) tyco_map
       |> fold (add_eval_constr o apsnd Code_Printer.str) constr_map
       |> fold (add_eval_const o apsnd Code_Printer.str) const_map
-  | process_reflection (code, _) _ (SOME file_name) thy =
+  | process_reflection (code, _) _ (SOME binding) thy =
       let
+        val code_binding = Path.map_binding Code_Target.code_path binding;
         val preamble =
           "(* Generated from " ^
             Path.implode (Resources.thy_path (Path.basic (Context.theory_name thy))) ^
           "; DO NOT EDIT! *)";
-        val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code);
-      in
-        thy
-      end;
+        val thy' = Code_Target.export code_binding (preamble ^ "\n\n" ^ code) thy;
+        val _ = Code_Target.code_export_message thy';
+      in thy' end;
 
-fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name some_file thy  =
+fun gen_code_reflect prep_type prep_const raw_datatypes raw_functions module_name file_prefix thy =
   let
     val ctxt = Proof_Context.init_global thy;
     val datatypes = map (fn (raw_tyco, raw_cos) =>
@@ -736,7 +738,7 @@
       |> (apsnd o apsnd) (chop (length constrs));
   in
     thy
-    |> process_reflection result module_name some_file
+    |> process_reflection result module_name file_prefix
   end;
 
 val code_reflect = gen_code_reflect Code_Target.cert_tyco (K I);
@@ -780,9 +782,11 @@
     (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.embedded)
-    >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
-      (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
+    -- Scan.option (\<^keyword>\<open>file_prefix\<close> |-- Parse.!!! (Parse.position Parse.embedded))
+    >> (fn (((module_name, raw_datatypes), raw_functions), file_prefix) =>
+      Toplevel.theory (fn thy =>
+        code_reflect_cmd raw_datatypes raw_functions module_name
+          (Option.map Path.explode_binding file_prefix) thy)));
 
 end; (*local*)