# HG changeset patch # User paulson # Date 1554206181 -3600 # Node ID e8da1fe4d61c45b5a73748e6f9de5ba666a8bd49 # Parent 16042475c511256696273e887813c1c0dc3e938c# Parent 94494b92d8d02daca6c2105ea6498328627b34fe merged diff -r 94494b92d8d0 -r e8da1fe4d61c CONTRIBUTORS --- a/CONTRIBUTORS Tue Apr 02 12:56:05 2019 +0100 +++ b/CONTRIBUTORS Tue Apr 02 12:56:21 2019 +0100 @@ -3,31 +3,41 @@ listed as an author in one of the source files of this Isabelle distribution. -Contributions to this Isabelle version --------------------------------------- - -* January 2019: Florian Haftmann - Clarified syntax and congruence rules for big operators on sets - involving the image operator. +Contributions to Isabelle2019 +----------------------------- -* January 2919: Florian Haftmann - Renovation of code generation, particularly export into session data - and proper strings and proper integers based on zarith for OCaml. - -* February 2019: Jeremy Sylvestre - Formal Laurent Series and overhaul of Formal power series. +* February/March 2019: Makarius Wenzel + Stateless management of export artifacts in the Isabelle/HOL code generator. * February 2019: Manuel Eberl Exponentiation by squaring, used to implement "power" in monoid_mult and fast modular exponentiation. * February 2019: Manuel Eberl - Carmichael's function, primitive roots in residue rings, more properties - of the order in residue rings. + Carmichael's function, primitive roots in residue rings, more properties of + the order in residue rings. + +* February 2019: Jeremy Sylvestre + Formal Laurent Series and overhaul of Formal power series. + +* January 2019: Florian Haftmann + Clarified syntax and congruence rules for big operators on sets involving + the image operator. + +* January 2019: Florian Haftmann + Renovation of code generation, particularly export into session data and + proper strings and proper integers based on zarith for OCaml. * January 2019: Andreas Lochbihler - New implementation for case_of_simps based on Code_Lazy's - pattern matching elimination algorithm. + New implementation for case_of_simps based on Code_Lazy's pattern matching + elimination algorithm. + +* November/December 2018: Makarius Wenzel + Support for Isabelle/Haskell applications of Isabelle/PIDE. + +* August/September 2018: Makarius Wenzel + Improvements of headless Isabelle/PIDE session and server, and systematic + exports from theory documents. * December 2018: Florian Haftmann Generic executable sorting algorithms based on executable comparators. diff -r 94494b92d8d0 -r e8da1fe4d61c COPYRIGHT --- a/COPYRIGHT Tue Apr 02 12:56:05 2019 +0100 +++ b/COPYRIGHT Tue Apr 02 12:56:21 2019 +0100 @@ -1,6 +1,6 @@ ISABELLE COPYRIGHT NOTICE, LICENCE AND DISCLAIMER. -Copyright (c) 1986-2018, +Copyright (c) 1986-2019, University of Cambridge, Technische Universitaet Muenchen, and contributors. diff -r 94494b92d8d0 -r e8da1fe4d61c NEWS --- a/NEWS Tue Apr 02 12:56:05 2019 +0100 +++ b/NEWS Tue Apr 02 12:56:21 2019 +0100 @@ -4,15 +4,11 @@ (Note: Isabelle/jEdit shows a tree-view of the NEWS file in Sidekick.) -New in this Isabelle version ----------------------------- +New in Isabelle2019 (June 2019) +------------------------------- *** General *** -* Old-style {* verbatim *} tokens are explicitly marked as legacy -feature and will be removed soon. Use \cartouche\ syntax instead, e.g. -via "isabelle update_cartouches -t" (available since Isabelle2015). - * The font family "Isabelle DejaVu" is systematically derived from the existing "DejaVu" collection, with variants "Sans Mono", "Sans", "Serif" and styles "Normal", "Bold", "Italic/Oblique", "Bold-Italic/Oblique". @@ -28,8 +24,13 @@ * Old-style inner comments (* ... *) within the term language are no longer supported (legacy feature in Isabelle2018). +* Old-style {* verbatim *} tokens are explicitly marked as legacy +feature and will be removed soon. Use \cartouche\ syntax instead, e.g. +via "isabelle update_cartouches -t" (available since Isabelle2015). + * Infix operators that begin or end with a "*" can now be paranthesized -without additional spaces, eg "(*)" instead of "( * )". +without additional spaces, eg "(*)" instead of "( * )". Minor +INCOMPATIBILITY. * Mixfix annotations may use cartouches instead of old-style double quotes, e.g. (infixl \+\ 60). The command-line tool "isabelle update -u @@ -40,13 +41,16 @@ need to provide a closed expression -- without trailing semicolon. Minor INCOMPATIBILITY. -* Command keywords of kind thy_decl / thy_goal may be more specifically -fit into the traditional document model of "definition-statement-proof" -via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. - *** Isabelle/jEdit Prover IDE *** +* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle +DejaVu" collection by default, which provides uniform rendering quality +with the usual Isabelle symbols. Line spacing no longer needs to be +adjusted: properties for the old IsabelleText font had "Global Options / +Text Area / Extra vertical line spacing (in pixels): -2", now it +defaults to 0. + * The jEdit File Browser is more prominent in the default GUI layout of Isabelle/jEdit: various virtual file-systems provide access to Isabelle resources, notably via "favorites:" (or "Edit Favorites"). @@ -61,29 +65,23 @@ entries are structured according to chapter / session names, the open operation is redirected to the session ROOT file. -* System option "jedit_text_overview" allows to disable the text -overview column. - -* Fonts for the text area, gutter, GUI elements etc. use the "Isabelle -DejaVu" collection by default, which provides uniform rendering quality -with the usual Isabelle symbols. Line spacing no longer needs to be -adjusted: properties for the old IsabelleText font had "Global Options / -Text Area / Extra vertical line spacing (in pixels): -2", now it -defaults to 0. - -* Improved sub-pixel font rendering (especially on Linux), thanks to -OpenJDK 11. - * Support for user-defined file-formats via class isabelle.File_Format in Isabelle/Scala (e.g. see isabelle.Bibtex.File_Format), configured via the shell function "isabelle_file_format" in etc/settings (e.g. of an Isabelle component). +* System option "jedit_text_overview" allows to disable the text +overview column. + * Command-line options "-s" and "-u" of "isabelle jedit" override the default for system option "system_heaps" that determines the heap storage directory for "isabelle build". Option "-n" is now clearly separated from option "-s". +* Update to OpenJDK 11, which is the current long-term support line +after Java 8. It provides a very different font renderer, with improved +sub-pixel font rendering. + *** Document preparation *** @@ -102,36 +100,20 @@ *** Isar *** -* More robust treatment of structural errors: begin/end blocks take -precedence over goal/proof. - * Implicit cases goal1, goal2, goal3, etc. have been discontinued (legacy feature since Isabelle2016). +* More robust treatment of structural errors: begin/end blocks take +precedence over goal/proof. This is particularly relevant for the +headless PIDE session and server. + +* Command keywords of kind thy_decl / thy_goal may be more specifically +fit into the traditional document model of "definition-statement-proof" +via thy_defn / thy_stmt / thy_goal_defn / thy_goal_stmt. + *** HOL *** -* Formal Laurent series and overhaul of Formal power series -in session HOL-Computational_Algebra. - -* Exponentiation by squaring in session HOL-Library; used for computing -powers in class monoid_mult and modular exponentiation in session -HOL-Number_Theory. - -* More material on residue rings in session HOL-Number_Theory: -Carmichael's function, primitive roots, more properties for "ord". - -* The functions \, \, \, \ -(not the corresponding binding operators) now have the same precedence -as any other prefix function symbol. Minor INCOMPATIBILITY. - -* Slightly more conventional naming schema in structure Inductive. -Minor INCOMPATIBILITY. - -* Various _global variants of specification tools have been removed. -Minor INCOMPATIBILITY, prefer combinators Named_Target.theory_map[_result] -to lift specifications to the global theory level. - * Command 'export_code' produces output as logical files within the theory context, as well as formal session exports that can be materialized via command-line tools "isabelle export" or "isabelle build @@ -148,6 +130,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. @@ -161,16 +147,15 @@ proper module frame, nothing is added magically any longer. INCOMPATIBILITY. -* Code generation: slightly more conventional syntax for -'code_stmts' antiquotation. Minor INCOMPATIBILITY. - -* The simplifier uses image_cong_simp as a congruence rule. The historic -and not really well-formed congruence rules INF_cong*, SUP_cong*, -are not used by default any longer. INCOMPATIBILITY; consider using -declare image_cong_simp [cong del] in extreme situations. - -* INF_image and SUP_image are no default simp rules any longer. -INCOMPATIBILITY, prefer image_comp as simp rule if needed. +* Code generation: slightly more conventional syntax for 'code_stmts' +antiquotation. Minor INCOMPATIBILITY. + +* Theory List: the precedence of the list_update operator has changed: +"f a [n := x]" now needs to be written "(f a)[n := x]". + +* The functions \, \, \, \ (not the corresponding binding operators) +now have the same precedence as any other prefix function symbol. Minor +INCOMPATIBILITY. * Simplified syntax setup for big operators under image. In rare situations, type conversions are not inserted implicitly any longer @@ -178,53 +163,87 @@ SUPREMUM, UNION, INTER should now rarely occur in output and are just retained as migration auxiliary. INCOMPATIBILITY. -* Theory List: the precedence of the list_update operator has changed: -"f a [n := x]" now needs to be written "(f a)[n := x]". - -* Theory "HOL-Library.Multiset": the # operator now has the same -precedence as any other prefix function symbol. - -* Retired lemma card_Union_image; use the simpler card_UN_disjoint instead. - -* Facts sum_mset.commute and prod_mset.commute renamed to sum_mset.swap -and prod_mset.swap, similarly to sum.swap and prod.swap. -INCOMPATIBILITY. +* The simplifier uses image_cong_simp as a congruence rule. The historic +and not really well-formed congruence rules INF_cong*, SUP_cong*, are +not used by default any longer. INCOMPATIBILITY; consider using declare +image_cong_simp [cong del] in extreme situations. + +* INF_image and SUP_image are no default simp rules any longer. +INCOMPATIBILITY, prefer image_comp as simp rule if needed. * Strong congruence rules (with =simp=> in the premises) for constant f are now uniformly called f_cong_simp, in accordance with congruence rules produced for mappers by the datatype package. INCOMPATIBILITY. -* Sledgehammer: - - The URL for SystemOnTPTP, which is used by remote provers, has - been updated. - - The machine-learning-based filter MaSh has been optimized to take - less time (in most cases). - -* SMT: reconstruction is now possible using the SMT solver veriT. - -* HOL-Library.Simps_Case_Conv: case_of_simps now supports overlapping -and non-exhaustive patterns and handles arbitrarily nested patterns. -It uses on the same algorithm as HOL-Library.Code_Lazy, which assumes -sequential left-to-right pattern matching. The generated +* Retired lemma card_Union_image; use the simpler card_UN_disjoint +instead. INCOMPATIBILITY. + +* Facts sum_mset.commute and prod_mset.commute have been renamed to +sum_mset.swap and prod_mset.swap, similarly to sum.swap and prod.swap. +INCOMPATIBILITY. + +* ML structure Inductive: slightly more conventional naming schema. +Minor INCOMPATIBILITY. + +* ML: Various _global variants of specification tools have been removed. +Minor INCOMPATIBILITY, prefer combinators +Named_Target.theory_map[_result] to lift specifications to the global +theory level. + +* Theory HOL-Library.Simps_Case_Conv: 'case_of_simps' now supports +overlapping and non-exhaustive patterns and handles arbitrarily nested +patterns. It uses on the same algorithm as HOL-Library.Code_Lazy, which +assumes sequential left-to-right pattern matching. The generated equation no longer tuples the arguments on the right-hand side. INCOMPATIBILITY. +* Theory HOL-Library.Multiset: the # operator now has the same +precedence as any other prefix function symbol. + +* Session HOL-Library and HOL-Number_Theory: Exponentiation by squaring, +used for computing powers in class "monoid_mult" and modular +exponentiation. + +* Session HOL-Computational_Algebra: Formal Laurent series and overhaul +of Formal power series. + +* Session HOL-Number_Theory: More material on residue rings in +Carmichael's function, primitive roots, more properties for "ord". + * Session HOL-SPARK: .prv files are no longer written to the file-system, but exported to the session database. Results may be retrieved with the "isabelle export" command-line tool like this: isabelle export -x "*:**.prv" HOL-SPARK-Examples +* Sledgehammer: + - The URL for SystemOnTPTP, which is used by remote provers, has been + updated. + - The machine-learning-based filter MaSh has been optimized to take + less time (in most cases). + +* SMT: reconstruction is now possible using the SMT solver veriT. + *** ML *** -* Local_Theory.reset is no longer available in user space. Regular -definitional packages should use balanced blocks of -Local_Theory.open_target versus Local_Theory.close_target instead, -or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. - -* Original PolyML.pointerEq is retained as a convenience for tools that -don't use Isabelle/ML (where this is called "pointer_eq"). +* Command 'generate_file' allows to produce sources for other languages, +with antiquotations in the Isabelle context (only the control-cartouche +form). The default "cartouche" antiquotation evaluates an ML expression +of type string and inlines the result as a string literal of the target +language. For example, this works for Haskell as follows: + + generate_file "Pure.hs" = \ + module Isabelle.Pure where + allConst, impConst, eqConst :: String + allConst = \\<^const_name>\Pure.all\\ + impConst = \\<^const_name>\Pure.imp\\ + eqConst = \\<^const_name>\Pure.eq\\ + \ + +The ML function Generate_File.generate writes all generated files from a +given theory to the file-system, e.g. a temporary directory where some +external compiler is applied. * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to option ML_environment to select a named environment, such as "Isabelle" @@ -253,36 +272,44 @@ preserving newlines literally. The short form \<^verbatim>\abc\ is particularly useful. -* Command 'generate_file' allows to produce sources for other languages, -with antiquotations in the Isabelle context (only the control-cartouche -form). The default "cartouche" antiquotation evaluates an ML expression -of type string and inlines the result as a string literal of the target -language. For example, this works for Haskell as follows: - - generate_file "Pure.hs" = \ - module Isabelle.Pure where - allConst, impConst, eqConst :: String - allConst = \\<^const_name>\Pure.all\\ - impConst = \\<^const_name>\Pure.imp\\ - eqConst = \\<^const_name>\Pure.eq\\ - \ - -The ML function Generate_File.generate writes all generated files from a -given theory to the file-system, e.g. a temporary directory where some -external compiler is applied. +* Local_Theory.reset is no longer available in user space. Regular +definitional packages should use balanced blocks of +Local_Theory.open_target versus Local_Theory.close_target instead, or +the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. + +* Original PolyML.pointerEq is retained as a convenience for tools that +don't use Isabelle/ML (where this is called "pointer_eq"). *** System *** -* The command-line option "isabelle build -e" retrieves theory exports -from the session build database, using 'export_files' in session ROOT -entries. - -* The system option "system_heaps" determines where to store the session +* Update to Java 11: the current long-term support version of OpenJDK. + +* Update to Poly/ML 5.8 allows to use the native x86_64 platform without +the full overhead of 64-bit values everywhere. This special x86_64_32 +mode provides up to 16GB ML heap, while program code and stacks are +allocated elsewhere. Thus approx. 5 times more memory is available for +applications compared to old x86 mode (which is no longer used by +Isabelle). The switch to the x86_64 CPU architecture also avoids +compatibility problems with Linux and macOS, where 32-bit applications +are gradually phased out. + +* System option "checkpoint" has been discontinued: obsolete thanks to +improved memory management in Poly/ML. + +* System option "system_heaps" determines where to store the session image of "isabelle build" (and other tools using that internally). Former option "-s" is superseded by option "-o system_heaps". INCOMPATIBILITY in command-line syntax. +* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some +source modules for Isabelle tools implemented in Haskell, notably for +Isabelle/PIDE. + +* The command-line tool "isabelle build -e" retrieves theory exports +from the session build database, using 'export_files' in session ROOT +entries. + * The command-line tool "isabelle update" uses Isabelle/PIDE in batch-mode to update theory sources based on semantic markup produced in Isabelle/ML. Actual updates depend on system options that may be enabled @@ -299,11 +326,7 @@ function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle component). -* Session directory $ISABELLE_HOME/src/Tools/Haskell provides some -source modules for Isabelle tools implemented in Haskell, notably for -Isabelle/PIDE. - -* Isabelle server command "use_theories" supports "nodes_status_delay" +* Isabelle Server command "use_theories" supports "nodes_status_delay" for continuous output of node status information. The time interval is specified in seconds; a negative value means it is disabled (default). @@ -347,20 +370,6 @@ ISABELLE_OPAM_ROOT, or by resetting these variables in $ISABELLE_HOME_USER/etc/settings. -* Update to Java 11: the latest long-term support version of OpenJDK. - -* System option "checkpoint" has been discontinued: obsolete thanks to -improved memory management in Poly/ML. - -* Update to Poly/ML 5.8 allows to use the native x86_64 platform without -the full overhead of 64-bit values everywhere. This special x86_64_32 -mode provides up to 16GB ML heap, while program code and stacks are -allocated elsewhere. Thus approx. 5 times more memory is available for -applications compared to old x86 mode (which is no longer used by -Isabelle). The switch to the x86_64 CPU architecture also avoids -compatibility problems with Linux and macOS, where 32-bit applications -are gradually phased out. - New in Isabelle2018 (August 2018) diff -r 94494b92d8d0 -r e8da1fe4d61c README --- a/README Tue Apr 02 12:56:05 2019 +0100 +++ b/README Tue Apr 02 12:56:21 2019 +0100 @@ -10,7 +10,7 @@ Installation Isabelle works on the three main platform families: Linux, Windows, - and Mac OS X. The application bundles from the Isabelle web page + and macOS. The application bundles from the Isabelle web page include sources, documentation, and add-on tools for all supported platforms. @@ -36,7 +36,7 @@ * https://www.cl.cam.ac.uk/research/hvg/Isabelle * https://isabelle.in.tum.de - * http://mirror.cse.unsw.edu.au/pub/isabelle + * https://mirror.cse.unsw.edu.au/pub/isabelle * https://mirror.clarkson.edu/isabelle Mailing list diff -r 94494b92d8d0 -r e8da1fe4d61c src/Doc/Codegen/Further.thy --- a/src/Doc/Codegen/Further.thy Tue Apr 02 12:56:05 2019 +0100 +++ b/src/Doc/Codegen/Further.thy Tue Apr 02 12:56:21 2019 +0100 @@ -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 94494b92d8d0 -r e8da1fe4d61c src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Tue Apr 02 12:56:05 2019 +0100 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Tue Apr 02 12:56:21 2019 +0100 @@ -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 94494b92d8d0 -r e8da1fe4d61c src/Pure/General/path.ML --- a/src/Pure/General/path.ML Tue Apr 02 12:56:05 2019 +0100 +++ b/src/Pure/General/path.ML Tue Apr 02 12:56:21 2019 +0100 @@ -41,7 +41,7 @@ eqtype binding val binding: T * Position.T -> binding val binding0: T -> binding - val binding_map: (T -> T) -> binding -> binding + val map_binding: (T -> T) -> binding -> binding val dest_binding: binding -> T * Position.T val implode_binding: binding -> string val explode_binding: string * Position.T -> binding @@ -264,7 +264,8 @@ else error ("Bad path binding: " ^ print path ^ Position.here pos); fun binding0 path = binding (path, Position.none); -fun binding_map f (Binding (path, pos)) = binding (f path, pos); + +fun map_binding f (Binding (path, pos)) = binding (f path, pos); fun dest_binding (Binding args) = args; diff -r 94494b92d8d0 -r e8da1fe4d61c src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Tue Apr 02 12:56:05 2019 +0100 +++ b/src/Tools/Code/code_runtime.ML Tue Apr 02 12:56:21 2019 +0100 @@ -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*) diff -r 94494b92d8d0 -r e8da1fe4d61c src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Tue Apr 02 12:56:05 2019 +0100 +++ b/src/Tools/Code/code_target.ML Tue Apr 02 12:56:21 2019 +0100 @@ -10,6 +10,7 @@ val read_tyco: Proof.context -> string -> string datatype pretty_modules = Singleton of string * Pretty.T | Hierarchy of (string list * Pretty.T) list; + val next_export: theory -> string * theory val export_code_for: ({physical: bool} * (Path.T * Position.T)) option -> string -> string -> int option -> Token.T list -> Code_Thingol.program -> bool -> Code_Symbol.T list @@ -36,6 +37,9 @@ val codeN: string val generatedN: string + val code_path: Path.T -> Path.T + val code_export_message: theory -> unit + val export: Path.binding -> string -> theory -> theory val compilation_text: Proof.context -> string -> Code_Thingol.program -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm -> (string list * string) list * string @@ -272,23 +276,28 @@ val codeN = "code"; val generatedN = "Generated_Code"; +val code_path = Path.append (Path.basic codeN); +fun code_export_message thy = writeln (Export.message thy (Path.basic codeN)); + +fun export binding content thy = + let + val thy' = thy |> Generated_Files.add_files (binding, content); + val _ = Export.export thy' binding [content]; + in thy' end; + local fun export_logical (file_prefix, file_pos) format pretty_modules = let - val prefix = Path.append (Path.basic codeN) file_prefix; - fun export path content thy = - let - val binding = Path.binding (path, file_pos); - val thy' = thy |> Generated_Files.add_files (binding, content); - val _ = Export.export thy' binding [content]; - in thy' end; + fun binding path = Path.binding (path, file_pos); + val prefix = code_path file_prefix; in (case pretty_modules of - Singleton (ext, p) => export (Path.ext ext prefix) (format p) + Singleton (ext, p) => export (binding (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))) + fold (fn (names, p) => + export (binding (Path.append prefix (Path.make names))) (format p)) modules) + #> tap code_export_message end; fun export_physical root format pretty_modules =