--- a/.hgtags Sun Nov 28 19:15:12 2021 +0100
+++ b/.hgtags Sat Dec 04 12:38:51 2021 +0100
@@ -43,3 +43,4 @@
b92b5a57521b27cf592b835caa8e8d73e05070d2 Isabelle2021-1-RC2
2b212c8138a57096487461fa353386f753ff7a11 Isabelle2021-1-RC3
2336356d4180b948eb9070f3f9f8986cda7e8f76 Isabelle2021-1-RC4
+8baf2e8b16e2218edaeb6dee402b21f97a49a505 Isabelle2021-1-RC5
--- a/src/Doc/Implementation/Logic.thy Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Doc/Implementation/Logic.thy Sat Dec 04 12:38:51 2021 +0100
@@ -168,6 +168,8 @@
@{ML_antiquotation_def "type_abbrev"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "nonterminal"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "typ"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "Type"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "Type_fn"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
\<^rail>\<open>
@@ -180,6 +182,8 @@
@@{ML_antiquotation nonterminal}) embedded
;
@@{ML_antiquotation typ} type
+ ;
+ (@@{ML_antiquotation Type} | @@{ML_antiquotation Type_fn}) embedded
\<close>
\<^descr> \<open>@{class c}\<close> inlines the internalized class \<open>c\<close> --- as \<^ML_type>\<open>string\<close>
@@ -199,6 +203,51 @@
\<^descr> \<open>@{typ \<tau>}\<close> inlines the internalized type \<open>\<tau>\<close> --- as constructor term for
datatype \<^ML_type>\<open>typ\<close>.
+
+ \<^descr> \<open>@{Type source}\<close> refers to embedded source text to produce a type
+ constructor with name (formally checked) and arguments (inlined ML text).
+ The embedded \<open>source\<close> follows the syntax category @{syntax type_const}
+ defined below.
+
+ \<^descr> \<open>@{Type_fn source}\<close> is similar to \<open>@{Type source}\<close>, but produces a partial
+ ML function that matches against a type constructor pattern, following
+ syntax category @{syntax type_const_fn} below.
+
+
+ \<^rail>\<open>
+ @{syntax_def type_const}: @{syntax name} (@{syntax embedded_ml}*)
+ ;
+ @{syntax_def type_const_fn}: @{syntax type_const} @'=>' @{syntax embedded}
+ ;
+ @{syntax_def embedded_ml}: @{syntax embedded} |
+ @{syntax control_symbol} @{syntax embedded} | @'_'
+ \<close>
+
+ The text provided as @{syntax embedded_ml} is treated as regular Isabelle/ML
+ source, possibly with nested antiquotations. ML text that only consists of a
+ single antiquotation in compact control-cartouche notation, can be written
+ without an extra level of nesting embedded text (see the last example
+ below).
+\<close>
+
+text %mlex \<open>
+ Here are some minimal examples for type constructor antiquotations.
+\<close>
+
+ML \<open>
+ \<comment> \<open>type constructor without arguments:\<close>
+ val natT = \<^Type>\<open>nat\<close>;
+
+ \<comment> \<open>type constructor with arguments:\<close>
+ fun mk_funT (A, B) = \<^Type>\<open>fun A B\<close>;
+
+ \<comment> \<open>type constructor decomposition as partial function:\<close>
+ val dest_funT = \<^Type_fn>\<open>fun A B => \<open>(A, B)\<close>\<close>;
+
+ \<comment> \<open>nested type constructors:\<close>
+ fun mk_relT A = \<^Type>\<open>fun A \<^Type>\<open>fun A \<^Type>\<open>bool\<close>\<close>\<close>;
+
+ \<^assert> (mk_relT natT = \<^typ>\<open>nat \<Rightarrow> nat \<Rightarrow> bool\<close>);
\<close>
@@ -387,6 +436,9 @@
@{ML_antiquotation_def "const"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "term"} & : & \<open>ML_antiquotation\<close> \\
@{ML_antiquotation_def "prop"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "Const"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "Const_"} & : & \<open>ML_antiquotation\<close> \\
+ @{ML_antiquotation_def "Const_fn"} & : & \<open>ML_antiquotation\<close> \\
\end{matharray}
\<^rail>\<open>
@@ -398,6 +450,9 @@
@@{ML_antiquotation term} term
;
@@{ML_antiquotation prop} prop
+ ;
+ (@@{ML_antiquotation Const} | @@{ML_antiquotation Const_} | @@{ML_antiquotation Const_fn})
+ embedded
\<close>
\<^descr> \<open>@{const_name c}\<close> inlines the internalized logical constant name \<open>c\<close> ---
@@ -414,6 +469,57 @@
\<^descr> \<open>@{prop \<phi>}\<close> inlines the internalized proposition \<open>\<phi>\<close> --- as constructor
term for datatype \<^ML_type>\<open>term\<close>.
+
+ \<^descr> \<open>@{Const source}\<close> refers to embedded source text to produce a term
+ constructor with name (formally checked), type arguments and term arguments
+ (inlined ML text). The embedded \<open>source\<close> follows the syntax category
+ @{syntax term_const} defined below, using @{syntax embedded_ml} from
+ antiquotation @{ML_antiquotation Type} (\secref{sec:types}).
+
+ \<^descr> \<open>@{Const_ source}\<close> is similar to \<open>@{Const source}\<close> for patterns instead of
+ closed values. This distinction is required due to redundant type
+ information within term constants: subtrees with duplicate ML pattern
+ variable need to be suppressed (replaced by dummy patterns). The embedded \<open>source\<close> follows
+ the syntax category @{syntax term_const} defined below.
+
+ \<^descr> \<open>@{Const_fn source}\<close> is similar to \<open>@{Const_ source}\<close>, but produces a
+ proper \<^verbatim>\<open>fn\<close> expression with function body. The embedded \<open>source\<close> follows
+ the syntax category @{syntax term_const_fn} defined below.
+
+
+ \<^rail>\<open>
+ @{syntax_def term_const}:
+ @{syntax name} (@{syntax embedded_ml}*) (@{syntax for_args})?
+ ;
+ @{syntax_def type_const_fn}: @{ syntax term_const} @'=>' @{syntax embedded}
+ ;
+ @{syntax_def for_args}: @'for' (@{syntax embedded_ml}*)
+ \<close>
+\<close>
+
+text %mlex \<open>
+ Here are some minimal examples for term constant antiquotations. Type
+ arguments for constants are analogous to type constructors
+ (\secref{sec:types}). Term arguments are different: a flexible number of
+ arguments is inserted via curried applications (\<^ML>\<open>op $\<close>).
+\<close>
+
+ML \<open>
+ \<comment> \<open>constant without type argument:\<close>
+ fun mk_conj (A, B) = \<^Const>\<open>conj for A B\<close>;
+ val dest_conj = \<^Const_fn>\<open>conj for A B => \<open>(A, B)\<close>\<close>;
+
+ \<comment> \<open>constant with type argument:\<close>
+ fun mk_eq T (t, u) = \<^Const>\<open>HOL.eq T for t u\<close>;
+ val dest_eq = \<^Const_fn>\<open>HOL.eq T for t u => \<open>(T, (t, u))\<close>\<close>;
+
+ \<comment> \<open>constant with variable number of term arguments:\<close>
+ val c = Const (\<^const_name>\<open>conj\<close>, \<^typ>\<open>bool \<Rightarrow> bool \<Rightarrow> bool\<close>);
+ val P = \<^term>\<open>P::bool\<close>;
+ val Q = \<^term>\<open>Q::bool\<close>;
+ \<^assert> (\<^Const>\<open>conj\<close> = c);
+ \<^assert> (\<^Const>\<open>conj for P\<close> = c $ P);
+ \<^assert> (\<^Const>\<open>conj for P Q\<close> = c $ P $ Q);
\<close>
--- a/src/Doc/System/Presentation.thy Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Doc/System/Presentation.thy Sat Dec 04 12:38:51 2021 +0100
@@ -161,17 +161,33 @@
\<^medskip> Isabelle is usually smart enough to create the PDF from the given
\<^verbatim>\<open>root.tex\<close> and optional \<^verbatim>\<open>root.bib\<close> (bibliography) and \<^verbatim>\<open>root.idx\<close> (index)
using standard {\LaTeX} tools. Actual command-lines are given by settings
- @{setting_ref ISABELLE_PDFLATEX}, @{setting_ref ISABELLE_LUALATEX},
+ @{setting_ref ISABELLE_LUALATEX} (or @{setting_ref ISABELLE_PDFLATEX}),
@{setting_ref ISABELLE_BIBTEX}, @{setting_ref ISABELLE_MAKEINDEX}: these
variables are used without quoting in shell scripts, and thus may contain
additional options.
- Alternatively, the session \<^verbatim>\<open>ROOT\<close> may include an option
- \<^verbatim>\<open>document_build=build\<close> together with an executable \<^verbatim>\<open>build\<close> script in
- \isakeyword{document\_files}: it is invoked with command-line arguments for
- the document format (\<^verbatim>\<open>pdf\<close>) and the document variant name. The script needs
- to produce corresponding output files, e.g.\ \<^verbatim>\<open>root.pdf\<close> for default
- document variants.
+ The system option @{system_option_def "document_build"} specifies an
+ alternative build engine, e.g. within the session \<^verbatim>\<open>ROOT\<close> file as
+ ``\<^verbatim>\<open>options [document_build = pdflatex]\<close>''. The following standard engines
+ are available:
+
+ \<^item> \<^verbatim>\<open>lualatex\<close> (default) uses the shell command \<^verbatim>\<open>$ISABELLE_LUALATEX\<close> on
+ the main \<^verbatim>\<open>root.tex\<close> file, with further runs of \<^verbatim>\<open>$ISABELLE_BIBTEX\<close> and
+ \<^verbatim>\<open>$ISABELLE_MAKEINDEX\<close> as required.
+
+ \<^item> \<^verbatim>\<open>pdflatex\<close> uses \<^verbatim>\<open>$ISABELLE_PDFLATEX\<close> instead of \<^verbatim>\<open>$ISABELLE_LUALATEX\<close>,
+ and the other tools as above.
+
+ \<^item> \<^verbatim>\<open>build\<close> invokes an executable script of the same name in a private
+ directory containing all \isakeyword{document\_files} and other generated
+ document sources. The script is invoked as ``\<^verbatim>\<open>./build pdf\<close>~\<open>name\<close>'' for
+ the document variant name; it needs to produce a corresponding
+ \<open>name\<close>\<^verbatim>\<open>.pdf\<close> file by arbitrary means on its own.
+
+ Further engines can be defined by add-on components in Isabelle/Scala
+ (\secref{sec:scala-build}), providing a service class derived from
+ \<^scala_type>\<open>isabelle.Document_Build.Engine\<close>. Available classes are listed
+ in \<^scala>\<open>isabelle.Document_Build.engines\<close>.
\<close>
--- a/src/Doc/System/Sessions.thy Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Doc/System/Sessions.thy Sat Dec 04 12:38:51 2021 +0100
@@ -212,6 +212,9 @@
default configuration with output readily available to the author of the
document.
+ \<^item> @{system_option_def "document_echo"} informs about document file names
+ during session presentation.
+
\<^item> @{system_option_def "document_variants"} specifies document variants as
a colon-separated list of \<open>name=tags\<close> entries. The default name
\<^verbatim>\<open>document\<close>, without additional tags.
@@ -239,10 +242,21 @@
is occasionally useful to control the global visibility of commands via
session options (e.g.\ in \<^verbatim>\<open>ROOT\<close>).
+ \<^item> @{system_option_def "document_comment_latex"} enables regular {\LaTeX}
+ \<^verbatim>\<open>comment.sty\<close>, instead of the historic version for plain {\TeX}
+ (default). The latter is much faster, but in conflict with {\LaTeX}
+ classes like Dagstuhl
+ LIPIcs\<^footnote>\<open>\<^url>\<open>https://github.com/dagstuhl-publishing/styles\<close>\<close>.
+
\<^item> @{system_option_def "document_bibliography"} explicitly enables the use
of \<^verbatim>\<open>bibtex\<close>; the default is to check the presence of \<^verbatim>\<open>root.bib\<close>, but it
could have a different name.
+ \<^item> @{system_option_def "document_heading_prefix"} specifies a prefix for
+ the {\LaTeX} macro names generated from Isar commands like \<^theory_text>\<open>chapter\<close>,
+ \<^theory_text>\<open>section\<close> etc. The default is \<^verbatim>\<open>isamarkup\<close>, e.g. \<^theory_text>\<open>section\<close> becomes
+ \<^verbatim>\<open>\isamarkupsection\<close>.
+
\<^item> @{system_option_def "threads"} determines the number of worker threads
for parallel checking of theories and proofs. The default \<open>0\<close> means that a
sensible maximum value is determined by the underlying hardware. For
--- a/src/HOL/Tools/try0.ML Sun Nov 28 19:15:12 2021 +0100
+++ b/src/HOL/Tools/try0.ML Sat Dec 04 12:38:51 2021 +0100
@@ -24,7 +24,7 @@
fun can_apply timeout_opt pre post tac st =
let val {goal, ...} = Proof.goal st in
(case (case timeout_opt of
- SOME timeout => Timeout.apply timeout
+ SOME timeout => Timeout.apply_physical timeout
| NONE => fn f => fn x => f x) (Seq.pull o tac) (pre st) of
SOME (x, _) => Thm.nprems_of (post x) < Thm.nprems_of goal
| NONE => false)
--- a/src/Pure/Concurrent/timeout.ML Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Pure/Concurrent/timeout.ML Sat Dec 04 12:38:51 2021 +0100
@@ -14,6 +14,7 @@
val scale_time: Time.time -> Time.time
val end_time: Time.time -> Time.time
val apply: Time.time -> ('a -> 'b) -> 'a -> 'b
+ val apply_physical: Time.time -> ('a -> 'b) -> 'a -> 'b
val print: Time.time -> string
end;
@@ -29,7 +30,7 @@
fun end_time timeout = Time.now () + scale_time timeout;
-fun apply timeout f x =
+fun apply' {physical, timeout} f x =
if ignored timeout then f x
else
Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn orig_atts =>
@@ -38,7 +39,7 @@
val start = Time.now ();
val request =
- Event_Timer.request {physical = false} (start + scale_time timeout)
+ Event_Timer.request {physical = physical} (start + scale_time timeout)
(fn () => Isabelle_Thread.interrupt_unsynchronized self);
val result =
Exn.capture (fn () => Thread_Attributes.with_attributes orig_atts (fn _ => f x)) ();
@@ -52,6 +53,9 @@
else (Exn.release test; Exn.release result)
end);
+fun apply timeout f x = apply' {physical = false, timeout = timeout} f x;
+fun apply_physical timeout f x = apply' {physical = true, timeout = timeout} f x;
+
fun print t = "Timeout after " ^ Value.print_time t ^ "s";
end;
--- a/src/Tools/Haskell/Haskell.thy Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Tools/Haskell/Haskell.thy Sat Dec 04 12:38:51 2021 +0100
@@ -322,7 +322,7 @@
Just y -> Just (i, y)
separate :: a -> [a] -> [a]
-separate s (x : (xs @ (_ : _))) = x : s : separate s xs
+separate s (x : xs@(_ : _)) = x : s : separate s xs
separate _ xs = xs;
@@ -342,7 +342,7 @@
space_explode :: Char -> String -> [String]
space_explode c = Split.split (Split.dropDelims (Split.whenElt (== c)))
trim_line :: String -> String
- trim_line s = gen_trim_line (length s) ((!!) s) take s
+ trim_line s = gen_trim_line (length s) (s !!) take s
instance StringLike Text where
space_explode :: Char -> Text -> [Text]
@@ -699,10 +699,7 @@
get props name = List.lookup name props
get_value :: (Bytes -> Maybe a) -> T -> Bytes -> Maybe a
-get_value parse props name =
- case get props name of
- Nothing -> Nothing
- Just s -> parse s
+get_value parse props name = maybe Nothing parse (get props name)
put :: Entry -> T -> T
put entry props = entry : remove (fst entry) props
@@ -2746,7 +2743,6 @@
Type classes for XML data representation.
-}
-{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE FlexibleInstances #-}
module Isabelle.XML.Classes
--- a/src/Tools/quickcheck.ML Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Tools/quickcheck.ML Sat Dec 04 12:38:51 2021 +0100
@@ -281,7 +281,7 @@
fun limit timeout (limit_time, is_interactive) f exc () =
if limit_time then
- Timeout.apply timeout f ()
+ Timeout.apply_physical timeout f ()
handle timeout_exn as Timeout.TIMEOUT _ =>
if is_interactive then exc () else Exn.reraise timeout_exn
else f ();
--- a/src/Tools/try.ML Sun Nov 28 19:15:12 2021 +0100
+++ b/src/Tools/try.ML Sat Dec 04 12:38:51 2021 +0100
@@ -89,7 +89,7 @@
val auto_time_limit = Options.default_real \<^system_option>\<open>auto_time_limit\<close>
in
if auto_time_limit > 0.0 then
- (case Timeout.apply (seconds auto_time_limit) (fn () => body true state) () of
+ (case Timeout.apply_physical (seconds auto_time_limit) (fn () => body true state) () of
(true, (_, outcome)) => List.app Output.information outcome
| _ => ())
else ()