# HG changeset patch # User wenzelm # Date 1554148725 -7200 # Node ID 49e178cbf92339b132935f006cc22d8c9b4a64b2 # Parent e6e63483655601dc87466402ab113a65b8950114 'code_reflect' only supports new-style 'file_prefix'; avoid fragile file "$ISABELLE_TMP/rat.ML"; diff -r e6e634836556 -r 49e178cbf923 NEWS --- 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. diff -r e6e634836556 -r 49e178cbf923 src/Doc/Codegen/Further.thy --- 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 \ rat \ rat)" "(minus :: rat \ rat \ rat)" "(times :: rat \ rat \ rat)" "(divide :: rat \ rat \ rat)" - file "$ISABELLE_TMP/rat.ML" + file_prefix rat text \ \noindent This merely generates the referenced code to the given diff -r e6e634836556 -r 49e178cbf923 src/Doc/Isar_Ref/HOL_Specific.thy --- 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} \ (@'datatypes' (@{syntax string} '=' ('_' | (@{syntax string} + '|') + @'and')))? \ - (@'functions' (@{syntax string} +))? (@'file' @{syntax path})? + (@'functions' (@{syntax string} +))? (@'file_prefix' @{syntax path})? ; @@{command (HOL) code_pred} \ ('(' @'modes' ':' modedecl ')')? \ 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 ``\file\'' 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 ``\datatypes\'' or ``\functions\'' entities use these precompiled - entities. With a ``\file\'' 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>\file_prefix\'' 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 ``\datatypes\'' or ``\functions\'' entities use + these precompiled entities. With a ``\<^theory_text>\file_prefix\'' argument, the + corresponding code is generated/exported to the specified file (as for + \<^theory_text>\export_code\) 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 diff -r e6e634836556 -r 49e178cbf923 src/Tools/Code/code_runtime.ML --- 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>\datatypes\ |-- Parse.!!! (parse_datatype ::: Scan.repeat (\<^keyword>\and\ |-- parse_datatype))) [] -- Scan.optional (\<^keyword>\functions\ |-- Parse.!!! (Scan.repeat1 Parse.name)) [] - -- Scan.option (\<^keyword>\file\ |-- 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>\file_prefix\ |-- 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*)