--- 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.
--- 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.
--- 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 \<open>cartouche\<close> 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 \<open>cartouche\<close> 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 \<open>+\<close> 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 \<Union>, \<Inter>, \<Squnion>, \<Sqinter>
-(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 \<Union>, \<Inter>, \<Squnion>, \<Sqinter> (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 <Union># 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 <Union># 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" = \<open>
+ module Isabelle.Pure where
+ allConst, impConst, eqConst :: String
+ allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
+ impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
+ eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
+ \<close>
+
+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>\<open>abc\<close> 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" = \<open>
- module Isabelle.Pure where
- allConst, impConst, eqConst :: String
- allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
- impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
- eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
- \<close>
-
-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)
--- 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
--- 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 \<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 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} \<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/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;
--- 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>\<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*)
--- 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 =