--- a/Admin/Release/CHECKLIST Wed Jan 08 05:37:40 2025 +0100
+++ b/Admin/Release/CHECKLIST Wed Jan 08 05:38:13 2025 +0100
@@ -78,19 +78,19 @@
- regular packaging:
#on fast Linux machine, with access to build_host for each platform
- Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2024 -j2 -l
+ Admin/build_release -D ~/tmp/isadist -b HOL -R Isabelle2025 -j2 -l
- Docker image:
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024 Isabelle2024_linux.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_X11_Latex -P X11 -P latex Isabelle2024_linux.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2025 Isabelle2025_linux.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2025_X11_Latex -P X11 -P latex Isabelle2025_linux.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_ARM Isabelle2024_linux_arm.tar.gz
- isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2024_ARM_X11_Latex -P X11 -P latex Isabelle2024_linux_arm.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2025_ARM Isabelle2025_linux_arm.tar.gz
+ isabelle docker_build -o Dockerfile -E -t makarius/isabelle:Isabelle2025_ARM_X11_Latex -P X11 -P latex Isabelle2025_linux_arm.tar.gz
docker login
- docker push makarius/isabelle:Isabelle2024
+ docker push makarius/isabelle:Isabelle2025
docker tag ... latest
docker push makarius/isabelle:latest
--- a/NEWS Wed Jan 08 05:37:40 2025 +0100
+++ b/NEWS Wed Jan 08 05:38:13 2025 +0100
@@ -82,6 +82,11 @@
adapted accordingly, but it is often better to use "unbundle no
foobar_syntax", as explained for HOL libraries below.
+* The option "show_brackets" has been discontinued: its inaccurate
+placement of extra parentheses has been superseded by markup of mixfix
+blocks (which allows to explore subterm structure in the Prover IDE via
+C-mouse hovering).
+
* Command "unbundle b" and its variants like "context includes b" allow
an optional name prefix with the reserved word "no": "unbundle no b"
etc. This reverses both the order and polarity of bundled declarations
@@ -137,6 +142,7 @@
'structure'). Rare INCOMPATIBILITY, e.g. in "subgoal_tac", "rule_tac".
+
*** Isabelle/jEdit Prover IDE ***
* Action isabelle.select_structure (with keyboard shortcut C+7) extends
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Wed Jan 08 05:38:13 2025 +0100
@@ -113,7 +113,6 @@
@{attribute_def show_sorts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def show_consts} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def show_abbrevs} & : & \<open>attribute\<close> & default \<open>true\<close> \\
- @{attribute_def show_brackets} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def names_long} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def names_short} & : & \<open>attribute\<close> & default \<open>false\<close> \\
@{attribute_def names_unique} & : & \<open>attribute\<close> & default \<open>true\<close> \\
@@ -158,13 +157,6 @@
\<^descr> @{attribute show_abbrevs} controls folding of constant abbreviations.
- \<^descr> @{attribute show_brackets} controls bracketing in pretty printed output.
- If enabled, all sub-expressions of the pretty printing tree will be
- parenthesized, even if this produces malformed term syntax! This crude way
- of showing the internal structure of pretty printed entities may
- occasionally help to diagnose problems with operator priorities, for
- example.
-
\<^descr> @{attribute names_long}, @{attribute names_short}, and @{attribute
names_unique} control the way of printing fully qualified internal names in
external form. See also \secref{sec:antiq} for the document antiquotation
--- a/src/Doc/JEdit/JEdit.thy Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Doc/JEdit/JEdit.thy Wed Jan 08 05:38:13 2025 +0100
@@ -304,7 +304,7 @@
The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
different server name. The default server name is the official distribution
- name (e.g.\ \<^verbatim>\<open>Isabelle2024\<close>). Thus @{tool jedit_client} can connect to the
+ name (e.g.\ \<^verbatim>\<open>Isabelle2025\<close>). Thus @{tool jedit_client} can connect to the
Isabelle desktop application without further options.
The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
--- a/src/Doc/System/Environment.thy Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Doc/System/Environment.thy Wed Jan 08 05:38:13 2025 +0100
@@ -56,7 +56,7 @@
\<^enum> The file \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close> (if it
exists) is run in the same way as the site default settings. Note that the
variable @{setting ISABELLE_HOME_USER} has already been set before ---
- usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2024\<close>.
+ usually to something like \<^verbatim>\<open>$USER_HOME/.isabelle/Isabelle2025\<close>.
Thus individual users may override the site-wide defaults. Typically, a
user settings file contains only a few lines, with some assignments that
@@ -135,7 +135,7 @@
of the @{executable isabelle} executable.
\<^descr>[@{setting_def ISABELLE_IDENTIFIER}\<open>\<^sup>*\<close>] refers to the name of this
- Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2024\<close>''.
+ Isabelle distribution, e.g.\ ``\<^verbatim>\<open>Isabelle2025\<close>''.
\<^descr>[@{setting_def ML_SYSTEM}, @{setting_def ML_HOME}, @{setting_def
ML_OPTIONS}, @{setting_def ML_PLATFORM}, @{setting_def ML_IDENTIFIER}\<open>\<^sup>*\<close>]
--- a/src/Doc/System/Misc.thy Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Doc/System/Misc.thy Wed Jan 08 05:38:13 2025 +0100
@@ -71,7 +71,7 @@
\<^medskip>
Option \<^verbatim>\<open>-B\<close> specifies the Docker image taken as starting point for the
Isabelle installation: it needs to be a suitable version of Ubuntu Linux,
- see also \<^url>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2024
+ see also \<^url>\<open>https://hub.docker.com/_/ubuntu\<close>. The default for Isabelle2025
is \<^verbatim>\<open>ubuntu:22.04\<close>, but \<^verbatim>\<open>ubuntu:20.04\<close> and \<^verbatim>\<open>ubuntu:24.04\<close> should work as
well. Other versions might require experimentation with the package
selection.
@@ -107,22 +107,22 @@
Produce a Dockerfile (without image) from a remote Isabelle distribution:
@{verbatim [display]
\<open> isabelle docker_build -E -n -o Dockerfile
- https://isabelle.in.tum.de/website-Isabelle2024/dist/Isabelle2024_linux.tar.gz\<close>}
+ https://isabelle.in.tum.de/website-Isabelle2025/dist/Isabelle2025_linux.tar.gz\<close>}
Build a standard Isabelle Docker image from a local Isabelle distribution,
with \<^verbatim>\<open>bin/isabelle\<close> as executable entry point:
@{verbatim [display]
-\<open> isabelle docker_build -E -t test/isabelle:Isabelle2024 Isabelle2024_linux.tar.gz\<close>}
+\<open> isabelle docker_build -E -t test/isabelle:Isabelle2025 Isabelle2025_linux.tar.gz\<close>}
Invoke the raw Isabelle/ML process within that image:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2024 process -e "Session.welcome ()"\<close>}
+\<open> docker run test/isabelle:Isabelle2025 process -e "Session.welcome ()"\<close>}
Invoke a Linux command-line tool within the contained Isabelle system
environment:
@{verbatim [display]
-\<open> docker run test/isabelle:Isabelle2024 env uname -a\<close>}
+\<open> docker run test/isabelle:Isabelle2025 env uname -a\<close>}
The latter should always report a Linux operating system, even when running
on Windows or macOS.
\<close>
@@ -455,7 +455,7 @@
\<^medskip>
The default is to output the Isabelle distribution name, e.g.\
- ``\<^verbatim>\<open>Isabelle2024\<close>''.
+ ``\<^verbatim>\<open>Isabelle2025\<close>''.
\<^medskip>
Option \<^verbatim>\<open>-i\<close> produces a short identification derived from the Mercurial id
--- a/src/HOL/Record.thy Wed Jan 08 05:37:40 2025 +0100
+++ b/src/HOL/Record.thy Wed Jan 08 05:38:13 2025 +0100
@@ -435,13 +435,13 @@
"_record_type" :: "field_types => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
"_record_type_scheme" :: "field_types => type => type" (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>\<dots> ::/ _)\<rparr>)\<close>)
- "_field" :: "ident => 'a => field" (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
+ "_field" :: "ident => 'a => field" (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>(\<open>open_block markup=\<open>const\<close>\<close>_) =/ _)\<close>)
"" :: "field => fields" (\<open>_\<close>)
"_fields" :: "field => fields => fields" (\<open>_,/ _\<close>)
"_record" :: "fields => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
"_record_scheme" :: "fields => 'a => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>\<dots> =/ _)\<rparr>)\<close>)
- "_field_update" :: "ident => 'a => field_update" (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
+ "_field_update" :: "ident => 'a => field_update" (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>(\<open>open_block markup=\<open>const\<close>\<close>_) :=/ _)\<close>)
"" :: "field_update => field_updates" (\<open>_\<close>)
"_field_updates" :: "field_update => field_updates => field_updates" (\<open>_,/ _\<close>)
"_record_update" :: "'a => field_updates => 'b" (\<open>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3\<lparr>_\<rparr>))\<close> [900, 0] 900)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Jan 08 05:37:40 2025 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Wed Jan 08 05:38:13 2025 +0100
@@ -204,10 +204,10 @@
val old_e_config : atp_config = make_e_config default_max_new_mono_instances (let
val (format, type_enc, lam_trans, extra_options) =
- if is_greater_equal (string_ord (getenv "E_VERSION", "3.0")) then
+ if getenv "E_VERSION" >= "3.0" then
(* '$ite' support appears to be unsound. *)
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule=4 --serialize-schedule=true --demod-under-lambda=true")
- else if is_greater_equal (string_ord (getenv "E_VERSION", "2.6")) then
+ else if getenv "E_VERSION" >= "2.6" then
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice), "mono_native_higher", keep_lamsN, "--auto-schedule")
else
(THF (Monomorphic, {with_ite = false, with_let = false}, THF_Lambda_Free), "mono_native_higher", combsN, "--auto-schedule")
--- a/src/Pure/Isar/attrib.ML Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Jan 08 05:38:13 2025 +0100
@@ -602,7 +602,6 @@
register_config_bool Goal.quick_and_dirty #>
register_config_bool Ast.trace #>
register_config_bool Ast.stats #>
- register_config_bool Printer.show_brackets #>
register_config_bool Printer.show_sorts #>
register_config_bool Printer.show_types #>
register_config_bool Printer.show_markup #>
--- a/src/Pure/Syntax/printer.ML Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Pure/Syntax/printer.ML Wed Jan 08 05:38:13 2025 +0100
@@ -7,7 +7,6 @@
signature BASIC_PRINTER =
sig
- val show_brackets: bool Config.T
val show_types: bool Config.T
val show_sorts: bool Config.T
val show_markup: bool Config.T
@@ -51,7 +50,6 @@
(** options for printing **)
-val show_brackets = Config.declare_option_bool ("show_brackets", \<^here>);
val show_types = Config.declare_option_bool ("show_types", \<^here>);
val show_sorts = Config.declare_option_bool ("show_sorts", \<^here>);
val show_markup_default = Unsynchronized.ref false;
@@ -236,8 +234,6 @@
fun pretty {type_mode, curried} ctxt prtabs (ops: pretty_ops) =
let
- val show_brackets = Config.get ctxt show_brackets;
-
val application =
if type_mode then Syntax_Trans.tappl_ast_tr'
else if curried then Syntax_Trans.applC_ast_tr'
@@ -297,9 +293,7 @@
and parens p q a (symbs, args) constraint =
let
- val symbs' =
- if p > q orelse (show_brackets andalso q <> 1000 andalso not (is_chain symbs))
- then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
+ val symbs' = if p > q then [Block (par_block, par_bg :: symbs @ [par_en])] else symbs;
val output =
(case constraint of
SOME (Ast.Appl [Ast.Constant "_constrain", _, ty]) =>
--- a/src/Pure/Syntax/syntax_phases.ML Wed Jan 08 05:37:40 2025 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Jan 08 05:38:13 2025 +0100
@@ -432,8 +432,6 @@
val errs = map snd (failed_results results');
val checked = map snd (proper_results results');
val checked_len = length checked;
-
- val pretty_term = Syntax.pretty_term (Config.put Printer.show_brackets true ctxt);
in
if checked_len = 0 then
report_result ctxt pos []
@@ -452,7 +450,7 @@
(("Ambiguous input\n" ^ string_of_int checked_len ^ " terms are type correct" ^
(if checked_len <= limit then ""
else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
- map (Pretty.string_of o Pretty.item o single o pretty_term)
+ map (Pretty.string_of o Pretty.item o single o Syntax.pretty_term ctxt)
(take limit checked))))))]
end handle ERROR msg => parse_failed ctxt pos msg kind)
end;