--- a/Admin/components/components.sha1 Wed Sep 07 08:58:27 2022 +0200
+++ b/Admin/components/components.sha1 Thu Sep 08 22:35:50 2022 +0200
@@ -381,6 +381,7 @@
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.tar.gz
f84c7ecafb07a0d763f1d70edc54f7c43c2e8c63 postgresql-42.4.0.tar.gz
+143d0d32a13d7d8e15b9bab866e14ad4308a6246 postgresql-42.5.0.tar.gz
f132329ca1045858ef456cc08b197c9eeea6881b postgresql-9.4.1212.tar.gz
f042bba5fb82c7eb8aee99f92eb6ec38c8a067f7 python-3.10.4.tar.gz
0885e1f1d8feaca78d2f204b6487e6eec6dfab4b scala-2.10.0.tar.gz
--- a/Admin/components/main Wed Sep 07 08:58:27 2022 +0200
+++ b/Admin/components/main Thu Sep 08 22:35:50 2022 +0200
@@ -20,7 +20,7 @@
opam-2.0.7
pdfjs-2.14.305
polyml-test-15c840d48c9a
-postgresql-42.4.0
+postgresql-42.5.0
scala-3.1.3
smbc-0.4.1
spass-3.8ds-2
--- a/NEWS Wed Sep 07 08:58:27 2022 +0200
+++ b/NEWS Thu Sep 08 22:35:50 2022 +0200
@@ -21,6 +21,28 @@
- "chapter_definition NAME description TEXT" to provide a description
for presentation purposes
+* System option "show_states" controls output of toplevel command states
+(notably proof states) in batch-builds; in interactive mode this is
+always done on demand. The option is relevant for tools that operate on
+exported PIDE markup, e.g. document presentation or diagnostics. For
+example:
+
+ isabelle build -o show_states FOL-ex
+ isabelle log -v -U FOL-ex
+
+Option "show_states" is also the default for the configuration option
+"show_results" within the formal context.
+
+Note that printing intermediate states may cause considerable slowdown
+in building a session.
+
+
+*** Isabelle/jEdit Prover IDE ***
+
+* Command 'print_state' outputs a plain message ("writeln" instead of
+"state"). Thus it is displayed in the Output panel, even if the option
+"editor_output_state" is disabled.
+
*** Isabelle/VSCode Prover IDE ***
@@ -265,6 +287,10 @@
Occasional INCOMPATIBILITY, see also the official Scala documentation
https://docs.scala-lang.org/scala3/guides/migration/compatibility-intro.html
+* Command-line tool "isabelle log" has been refined to support multiple
+sessions, and to match messages against regular expressions (using Java
+Pattern syntax).
+
* Command-line tool "isabelle scala_project" supports Gradle as
alternative to Maven: either option -G or -M needs to be specified
explicitly. This increases the chances that the Java/Scala IDE project
--- a/etc/build.props Wed Sep 07 08:58:27 2022 +0200
+++ b/etc/build.props Thu Sep 08 22:35:50 2022 +0200
@@ -25,6 +25,7 @@
src/Pure/Admin/build_minisat.scala \
src/Pure/Admin/build_pdfjs.scala \
src/Pure/Admin/build_polyml.scala \
+ src/Pure/Admin/build_postgresql.scala \
src/Pure/Admin/build_release.scala \
src/Pure/Admin/build_scala.scala \
src/Pure/Admin/build_spass.scala \
--- a/etc/options Wed Sep 07 08:58:27 2022 +0200
+++ b/etc/options Thu Sep 08 22:35:50 2022 +0200
@@ -59,11 +59,17 @@
option show_consts : bool = false
-- "show constants with types when printing proof state"
+option show_goal_inst : bool = true
+ -- "show goal instantiation (for schematic goals)"
option show_main_goal : bool = false
-- "show main goal when printing proof state"
option goals_limit : int = 10
-- "maximum number of subgoals to be printed"
+option show_states : bool = false
+ -- "show toplevel states even if outside of interactive mode"
+
+
option names_long : bool = false
-- "show fully qualified names"
option names_short : bool = false
--- a/src/CTT/ex/Elimination.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/CTT/ex/Elimination.thy Thu Sep 08 22:35:50 2022 +0200
@@ -2,7 +2,7 @@
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
-Some examples taken from P. Martin-L\"of, Intuitionistic type theory
+Some examples taken from P. Martin-Löf, Intuitionistic type theory
(Bibliopolis, 1984).
*)
--- a/src/Doc/Datatypes/Datatypes.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Thu Sep 08 22:35:50 2022 +0200
@@ -3679,7 +3679,7 @@
Lars Noschinski implemented the @{command simps_of_case} and @{command
case_of_simps} commands. Florian Haftmann, Christian Urban, and Makarius
Wenzel provided general advice on Isabelle and package writing. Stefan Milius
-and Lutz Schr\"oder found an elegant proof that eliminated one of the BNF
+and Lutz Schröder found an elegant proof that eliminated one of the BNF
proof obligations. Mamoun Filali-Amine, Gerwin Klein, Andreas Lochbihler,
Tobias Nipkow, and Christian Sternagel suggested many textual improvements to
this tutorial.
--- a/src/Doc/Isar_Ref/HOL_Specific.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy Thu Sep 08 22:35:50 2022 +0200
@@ -2076,7 +2076,7 @@
\<close>
-section \<open>Algebraic reasoning via Gr\"obner bases\<close>
+section \<open>Algebraic reasoning via Gröbner bases\<close>
text \<open>
\begin{matharray}{rcl}
@@ -2092,7 +2092,7 @@
@@{attribute (HOL) algebra} (() | 'add' | 'del')
\<close>
- \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gr\"obner bases,
+ \<^descr> @{method (HOL) algebra} performs algebraic reasoning via Gröbner bases,
see also @{cite "Chaieb-Wenzel:2007"} and @{cite \<open>\S3.2\<close> "Chaieb-thesis"}.
The method handles deals with two main classes of problems:
--- a/src/Doc/Locales/Examples3.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Doc/Locales/Examples3.thy Thu Sep 08 22:35:50 2022 +0200
@@ -506,7 +506,7 @@
mechanisms, which are described in another paper by Haftmann and
Wenzel~@{cite HaftmannWenzel2009}.
- The original work of Kamm\"uller on locales~@{cite KammullerEtAl1999}
+ The original work of Kammüller on locales~@{cite KammullerEtAl1999}
may be of interest from a historical perspective. My previous
report on locales and locale expressions~@{cite Ballarin2004a}
describes a simpler form of expressions than available now and is
--- a/src/Doc/System/Sessions.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Doc/System/Sessions.thy Thu Sep 08 22:35:50 2022 +0200
@@ -554,24 +554,31 @@
database of the given session. Its command-line usage is:
@{verbatim [display]
-\<open>Usage: isabelle log [OPTIONS] SESSION
+\<open>Usage: isabelle log [OPTIONS] [SESSIONS ...]
Options are:
+ -H REGEX filter messages by matching against head
+ -M REGEX filter messages by matching against body
-T NAME restrict to given theories (multiple options possible)
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: 76.0)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v print all messages, including information etc.
- Print messages from the build database of the given session, without any
- checks against current sources: results from a failed build can be
- printed as well.\<close>}
+ Print messages from the build database of the given sessions, without any
+ checks against current sources nor session structure: results from old
+ sessions or failed builds can be printed as well.
- The specified session database is taken as is, independently of the current
- session structure and theories sources. The order of messages follows the
- source positions of source files; thus the erratic evaluation of parallel
- processing rarely matters. There is \<^emph>\<open>no\<close> implicit build process involved,
- so it is possible to retrieve error messages from a failed session as well.
+ Multiple options -H and -M are conjunctive: all given patterns need to
+ match. Patterns match any substring, but ^ or $ may be used to match the
+ start or end explicitly.\<close>}
+
+ The specified session databases are taken as is, with formal checking
+ against current sources: There is \<^emph>\<open>no\<close> implicit build process involved, so
+ it is possible to retrieve error messages from a failed session as well. The
+ order of messages follows the source positions of source files; thus the
+ result is mostly deterministic, independent of the somewhat erratic
+ evaluation of parallel processing.
\<^medskip> Option \<^verbatim>\<open>-o\<close> allows to change system options, as in @{tool build}
(\secref{sec:tool-build}). This may affect the storage space for the build
@@ -588,6 +595,16 @@
\<^medskip> Option \<^verbatim>\<open>-v\<close> prints all messages from the session database that are
normally inlined into the source text, including information messages etc.
+
+ \<^medskip> Options \<^verbatim>\<open>-H\<close> and \<^verbatim>\<open>-M\<close> filter messages according to their header or body
+ content, respectively. The header follows a very basic format that makes it
+ easy to match message kinds (e.g. \<^verbatim>\<open>Warning\<close> or \<^verbatim>\<open>Error\<close>) and file names
+ (e.g. \<^verbatim>\<open>src/HOL/Nat.thy\<close>). The body is usually pretty-printed, but for
+ matching it is treated like one long line: blocks are ignored and breaks are
+ turned into plain spaces (according to their formal width).
+
+ The syntax for patters follows regular expressions of the Java
+ platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/en/java/javase/17/docs/api/java.base/java/util/regex/Pattern.html\<close>\<close>
\<close>
subsubsection \<open>Examples\<close>
@@ -596,6 +613,15 @@
Print messages from theory \<^verbatim>\<open>HOL.Nat\<close> of session \<^verbatim>\<open>HOL\<close>, using Unicode
rendering of Isabelle symbols and a margin of 100 characters:
@{verbatim [display] \<open> isabelle log -T HOL.Nat -U -m 100 HOL\<close>}
+
+ Print warnings about ambiguous input (inner syntax) of session
+ \<^verbatim>\<open>HOL-Library\<close>, which is built beforehand:
+ @{verbatim [display] \<open> isabelle build HOL-Library
+ isabelle log -H "Warning" -M "Ambiguous input" HOL-Library\<close>}
+
+ Print all errors from all sessions, e.g. from a partial build of
+ Isabelle/AFP:
+ @{verbatim [display] \<open> isabelle log -H "Error" $(isabelle sessions -a -d AFP/thys)\<close>}
\<close>
--- a/src/HOL/Analysis/Lindelof_Spaces.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Analysis/Lindelof_Spaces.thy Thu Sep 08 22:35:50 2022 +0200
@@ -1,4 +1,4 @@
-section\<open>Lindel\"of spaces\<close>
+section\<open>Lindelöf spaces\<close>
theory Lindelof_Spaces
imports T1_Spaces
--- a/src/HOL/Data_Structures/Brother12_Set.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Data_Structures/Brother12_Set.thy Thu Sep 08 22:35:50 2022 +0200
@@ -488,7 +488,7 @@
subsection \<open>Height-Size Relation\<close>
-text \<open>By Daniel St\"uwe\<close>
+text \<open>By Daniel Stüwe\<close>
fun fib_tree :: "nat \<Rightarrow> unit bro" where
"fib_tree 0 = N0"
--- a/src/HOL/Induct/Ordinals.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Induct/Ordinals.thy Thu Sep 08 22:35:50 2022 +0200
@@ -10,7 +10,7 @@
text \<open>
Some basic definitions of ordinal numbers. Draws an Agda
- development (in Martin-L\"of type theory) by Peter Hancock (see
+ development (in Martin-Löf type theory) by Peter Hancock (see
\<^url>\<open>http://www.dcs.ed.ac.uk/home/pgh/chat.html\<close>).
\<close>
--- a/src/HOL/Library/Omega_Words_Fun.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy Thu Sep 08 22:35:50 2022 +0200
@@ -31,7 +31,7 @@
We represent $\omega$-words as functions from the natural numbers
to the alphabet type. Other possible formalizations include
a coinductive definition or a uniform encoding of finite and
- infinite words, as studied by M\"uller et al.
+ infinite words, as studied by Müller et al.
\<close>
type_synonym
--- a/src/HOL/Prolog/HOHH.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Prolog/HOHH.thy Thu Sep 08 22:35:50 2022 +0200
@@ -10,6 +10,8 @@
ML_file \<open>prolog.ML\<close>
+declare [[show_main_goal]]
+
method_setup ptac =
\<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
"basic Lambda Prolog interpreter"
--- a/src/HOL/Prolog/prolog.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/Prolog/prolog.ML Thu Sep 08 22:35:50 2022 +0200
@@ -2,8 +2,6 @@
Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
*)
-Options.default_put_bool \<^system_option>\<open>show_main_goal\<close> true;
-
structure Prolog =
struct
--- a/src/HOL/TPTP/mash_export.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/HOL/TPTP/mash_export.ML Thu Sep 08 22:35:50 2022 +0200
@@ -285,7 +285,7 @@
#> Sledgehammer_MePo.mepo_suggested_facts ctxt params max_suggs NONE hyp_ts concl_t)
fun generate_mash_suggestions algorithm ctxt =
- (Options.put_default \<^system_option>\<open>MaSh\<close> algorithm;
+ (Options.put_default \<^system_option>\<open>MaSh\<close> algorithm; (* FIXME fragile *)
Sledgehammer_MaSh.mash_unlearn ctxt;
generate_mepo_or_mash_suggestions
(fn ctxt => fn thy_name => fn params as {provers = prover :: _, ...} =>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_postgresql.scala Thu Sep 08 22:35:50 2022 +0200
@@ -0,0 +1,129 @@
+/* Title: Pure/Admin/build_postgresql.scala
+ Author: Makarius
+
+Build Isabelle postgresql component from official download.
+*/
+
+package isabelle
+
+
+object Build_PostgreSQL {
+ /* URLs */
+
+ val notable_urls =
+ List("https://jdbc.postgresql.org", "https://jdbc.postgresql.org/download.html")
+
+ val default_download_url = "https://jdbc.postgresql.org/download/postgresql-42.5.0.jar"
+
+
+ /* build postgresql */
+
+ def build_postgresql(
+ download_url: String = default_download_url,
+ progress: Progress = new Progress,
+ target_dir: Path = Path.current
+ ): Unit = {
+ /* name and version */
+
+ def err(): Nothing = error("Malformed jar download URL: " + quote(download_url))
+
+ val Name = """^.*/([^/]+)\.jar""".r
+ val download_name = download_url match { case Name(name) => name case _ => err() }
+
+ val Version = """^.[^0-9]*([0-9].*)$""".r
+ val download_version = download_name match { case Version(version) => version case _ => err() }
+
+
+ /* component */
+
+ val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(download_name))
+ progress.echo("Component " + component_dir)
+
+
+ /* LICENSE */
+
+ File.write(component_dir + Path.basic("LICENSE"),
+"""Copyright (c) 1997, PostgreSQL Global Development Group
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice,
+ this list of conditions and the following disclaimer.
+2. Redistributions in binary form must reproduce the above copyright notice,
+ this list of conditions and the following disclaimer in the documentation
+ and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
+""")
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+"""This is PostgreSQL JDBC """ + download_version + """ from
+""" + notable_urls.mkString(" and ") + """
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+
+
+ /* settings */
+
+ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+
+ File.write(etc_dir + Path.basic("settings"),
+"""# -*- shell-script -*- :mode=shellscript:
+
+classpath "$COMPONENT/""" + download_name + """.jar"
+""")
+
+
+ /* jar */
+
+ val jar = component_dir + Path.basic(download_name).ext("jar")
+ Isabelle_System.download_file(download_url, jar, progress = progress)
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_postgresql", "build Isabelle postgresql component from official download",
+ Scala_Project.here,
+ { args =>
+ var target_dir = Path.current
+ var download_url = default_download_url
+
+ val getopts = Getopts("""
+Usage: isabelle build_postgresql [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+ -U URL download URL
+ (default: """" + default_download_url + """")
+
+ Build postgresql component from the specified download URL (JAR), see also
+ """ + notable_urls.mkString(" and "),
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_postgresql(download_url, progress = progress, target_dir = target_dir)
+ })
+}
--- a/src/Pure/General/pretty.scala Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/General/pretty.scala Thu Sep 08 22:35:50 2022 +0200
@@ -92,6 +92,23 @@
}
+ /* unformatted output */
+
+ def unformatted(input: XML.Body): XML.Body = {
+ input flatMap {
+ case XML.Wrapped_Elem(markup, body1, body2) =>
+ List(XML.Wrapped_Elem(markup, body1, unformatted(body2)))
+ case XML.Elem(markup, body) =>
+ markup match {
+ case Markup.Block(_, _) => unformatted(body)
+ case Markup.Break(width, _) => XML.string(Symbol.spaces(width))
+ case _ => List(XML.Elem(markup, unformatted(body)))
+ }
+ case XML.Text(text) => XML.string(split_lines(text).mkString(Symbol.space))
+ }
+ }
+
+
/* formatted output */
private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0) {
--- a/src/Pure/Isar/attrib.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Isar/attrib.ML Thu Sep 08 22:35:50 2022 +0200
@@ -601,7 +601,6 @@
register_config_bool Thm.show_consts #>
register_config_bool Thm.show_hyps #>
register_config_bool Thm.show_tags #>
- register_config_bool Proof_Display.show_results #>
register_config_bool Pattern.unify_trace_failure #>
register_config_int Unify.trace_bound #>
register_config_int Unify.search_bound #>
--- a/src/Pure/Isar/overloading.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Isar/overloading.ML Thu Sep 08 22:35:50 2022 +0200
@@ -53,7 +53,7 @@
Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = f syntax, secondary_pass = secondary_pass});
val mark_passed =
- Improvable_Syntax.map (fn {syntax, secondary_pass} => {syntax = syntax, secondary_pass = true});
+ Improvable_Syntax.map (fn {syntax, secondary_pass = _} => {syntax = syntax, secondary_pass = true});
fun improve_term_check ts ctxt =
let
--- a/src/Pure/Isar/proof.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Isar/proof.ML Thu Sep 08 22:35:50 2022 +0200
@@ -359,19 +359,12 @@
SOME ctxt_goal => ctxt_goal
| NONE => find_goal (close_block state handle ERROR _ => error "No proof goal"));
-fun get_goal state =
- let val (ctxt, {using, goal, ...}) = find_goal state
- in (ctxt, (using, goal)) end;
-
(** pretty_state **)
local
-fun pretty_facts _ _ NONE = []
- | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths];
-
fun pretty_sep prts [] = prts
| pretty_sep [] prts = prts
| pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2;
@@ -383,11 +376,19 @@
val {context = ctxt, facts, mode, goal = _} = top state;
val verbose = Config.get ctxt Proof_Context.verbose;
- fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) =
- pretty_sep
- (pretty_facts ctxt "using"
- (if mode <> Backward orelse null using then NONE else SOME using))
- ([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal)
+ val prt_facts = Proof_Display.pretty_goal_facts ctxt;
+
+ fun prt_goal (SOME (_, goal)) =
+ let
+ val {statement = (_, propss, _), using, goal, before_qed = _, after_qed = _} = goal;
+ val head = [Proof_Display.pretty_goal_header goal];
+ val body = Goal_Display.pretty_goals ctxt goal;
+ val foot = Proof_Display.pretty_goal_inst ctxt propss goal;
+ in
+ pretty_sep
+ (prt_facts "using" (if mode <> Backward orelse null using then NONE else SOME using))
+ (head @ body @ foot)
+ end
| prt_goal NONE = [];
val prt_ctxt =
@@ -401,8 +402,8 @@
[Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
- pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state))
- else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts)
+ pretty_sep (prt_facts "" (Option.map #1 facts)) (prt_goal (try find_goal state))
+ else if mode = Chain then prt_facts "picking" (Option.map #1 facts)
else prt_goal (try find_goal state))
end;
@@ -471,7 +472,7 @@
fun refine_goals print_rule result_ctxt result state =
let
- val (goal_ctxt, (_, goal)) = get_goal state;
+ val (goal_ctxt, {goal, ...}) = find_goal state;
fun refine rule st =
(print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st);
in
@@ -508,10 +509,11 @@
Conjunction.elim_balanced (length goal_propss) th
|> map2 Conjunction.elim_balanced (map length goal_propss)
handle THM _ => err_lost ();
+ val matcher =
+ Unify.matcher (Context.Proof ctxt)
+ (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (map Thm.prop_of (flat results));
val _ =
- Unify.matches_list (Context.Proof ctxt)
- (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (map Thm.prop_of (flat results))
- orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
+ is_none matcher andalso error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
@@ -522,7 +524,7 @@
val finished_goal_error = "Failed to finish proof";
fun finished_goal pos state =
- let val (ctxt, (_, goal)) = get_goal state in
+ let val (ctxt, {goal, ...}) = find_goal state in
if Thm.no_prems goal then Seq.Result state
else
Seq.Error (fn () =>
@@ -536,15 +538,15 @@
val goal_finished = Thm.no_prems o #goal o #2 o find_goal;
fun raw_goal state =
- let val (ctxt, (using, goal)) = get_goal state
+ let val (ctxt, {using, goal, ...}) = find_goal state
in {context = ctxt, facts = using, goal = goal} end;
val goal = raw_goal o refine_insert [];
fun simple_goal state =
let
- val (_, (using, _)) = get_goal state;
- val (ctxt, (_, goal)) = get_goal (refine_insert using state);
+ val (_, {using, ...}) = find_goal state;
+ val (ctxt, {goal, ...}) = find_goal (refine_insert using state);
in {context = ctxt, goal = goal} end;
fun method_error kind pos state =
@@ -992,8 +994,10 @@
let
val var_props = take_prefix is_var props;
val explicit_vars = fold Term.add_vars var_props [];
- val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
- in map (Logic.mk_term o Var) vars end;
+ in
+ fold Term.add_vars props [] |> map_filter (fn v =>
+ if member (op =) explicit_vars v then NONE else SOME (Logic.mk_term (Var v)))
+ end;
fun refine_terms n =
refine_singleton (Method.Basic (fn ctxt => CONTEXT_TACTIC o
@@ -1008,12 +1012,12 @@
val pos = Position.thread_data ();
val goal_props = flat goal_propss;
- val vars = implicit_vars goal_props;
- val propss' = vars :: goal_propss;
- val goal_propss = filter_out null propss';
+ val goal_vars = implicit_vars goal_props;
+ val propss' = goal_vars :: goal_propss;
+ val goal_propss' = filter_out null propss';
val goal =
- Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)
+ Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss')
|> Thm.cterm_of goal_ctxt
|> Thm.weaken_sorts' goal_ctxt;
val statement = ((kind, pos), propss', Thm.term_of goal);
@@ -1034,16 +1038,21 @@
|> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed'))
|> chaining ? (`the_facts #-> using_facts)
|> reset_facts
- |> not (null vars) ? refine_terms (length goal_propss)
- |> null goal_props ? refine_singleton (Method.Basic Method.assumption)
+ |> not (null goal_vars) ? refine_terms (length goal_propss')
+ |> forall null goal_propss' ? refine_singleton (Method.Basic Method.assumption)
end;
fun generic_qed state =
let
- val (goal_ctxt, {statement = (_, propss, _), goal, after_qed, ...}) =
- current_goal state;
+ val (goal_ctxt, goal_config) = current_goal state;
+ val {statement = (_, propss, _), goal, after_qed, ...} = goal_config;
val results = tl (conclude_goal goal_ctxt goal propss);
- in state |> close_block |> pair (after_qed, (goal_ctxt, results)) end;
+ val res =
+ {goal_ctxt = goal_ctxt,
+ goal_config = goal_config,
+ after_qed = after_qed,
+ results = results};
+ in state |> close_block |> pair res end;
end;
@@ -1106,8 +1115,8 @@
end;
fun local_qeds arg =
- end_proof false arg
- #> Seq.map_result (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
+ end_proof false arg #> Seq.map_result
+ (generic_qed #-> (fn {after_qed, goal_ctxt, results, ...} => #1 after_qed (goal_ctxt, results)));
fun local_qed arg =
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
@@ -1135,12 +1144,21 @@
val theorem_cmd = global_goal Proof_Context.read_propp;
fun global_qeds arg =
- end_proof true arg
- #> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) =>
- after_qed results (context_of state)));
+ end_proof true arg #> Seq.map_result
+ (generic_qed #> (fn ({goal_ctxt, goal_config, after_qed, results}, state) =>
+ ((goal_ctxt, Goal goal_config), #2 after_qed (goal_ctxt, results) (context_of state))));
+
+fun global_goal_inst ((goal_ctxt, Goal goal), result_ctxt: context) =
+ let
+ val {statement = (_, propss, _), goal, ...} = goal;
+ val _ =
+ (case Proof_Display.pretty_goal_inst goal_ctxt propss goal of
+ [] => ()
+ | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
+ in result_ctxt end;
fun global_qed arg =
- global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
+ global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error #> global_goal_inst;
(* relevant proof states *)
@@ -1184,10 +1202,12 @@
val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
-fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
+fun global_terminal_proof (text, opt_text) =
+ terminal_proof global_qeds text (opt_text, true) #> global_goal_inst;
val global_default_proof = global_terminal_proof ((Method.standard_text, Position.no_range), NONE);
val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
-val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
+val global_done_proof =
+ terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false) #> global_goal_inst;
end;
@@ -1290,8 +1310,8 @@
fun future_proof fork_proof state =
let
val _ = assert_backward state;
- val (goal_ctxt, goal_info) = find_goal state;
- val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal_info;
+ val (goal_ctxt, goal) = find_goal state;
+ val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal;
val _ = is_relevant state andalso error "Cannot fork relevant proof";
@@ -1314,7 +1334,7 @@
end;
-(* terminal proofs *) (* FIXME avoid toplevel imitation -- include in PIDE/document *)
+(* terminal proofs *)
local
--- a/src/Pure/Isar/proof_display.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML Thu Sep 08 22:35:50 2022 +0200
@@ -19,7 +19,9 @@
val string_of_rule: Proof.context -> string -> thm -> string
val pretty_goal_header: thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
- val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
+ val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
+ val show_goal_inst: bool Config.T
+ val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
val show_results: bool Config.T
@@ -98,9 +100,6 @@
fun pretty_abbrev (c, (ty, t)) = Pretty.block
(prt_const (c, ty) @ [Pretty.str " \<equiv>", Pretty.brk 1, prt_term_no_vars t]);
- fun pretty_axm (a, t) =
- Pretty.block [Pretty.mark_str a, Pretty.str ":", Pretty.brk 1, prt_term_no_vars t];
-
val tsig = Sign.tsig_of thy;
val consts = Sign.consts_of thy;
val {const_space, constants, constraints} = Consts.dest consts;
@@ -239,11 +238,75 @@
(* goal facts *)
-fun pretty_goal_facts ctxt s ths =
- (Pretty.block o Pretty.fbreaks)
- [if s = "" then Pretty.str "this:"
- else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
- Proof_Context.pretty_fact ctxt ("", ths)];
+fun pretty_goal_facts _ _ NONE = []
+ | pretty_goal_facts ctxt s (SOME ths) =
+ (single o Pretty.block o Pretty.fbreaks)
+ [if s = "" then Pretty.str "this:"
+ else Pretty.block [Pretty.keyword1 s, Pretty.brk 1, Pretty.str "this:"],
+ Proof_Context.pretty_fact ctxt ("", ths)];
+
+
+(* goal instantiation *)
+
+val show_goal_inst = Attrib.setup_option_bool (\<^system_option>\<open>show_goal_inst\<close>, \<^here>);
+
+fun pretty_goal_inst ctxt propss goal =
+ let
+ val title = "goal instantiation:";
+
+ fun prt_inst env =
+ if Envir.is_empty env then []
+ else
+ let
+ val Envir.Envir {tyenv, tenv, ...} = env;
+
+ val prt_type = Syntax.pretty_typ ctxt;
+ val prt_term = Syntax.pretty_term ctxt;
+
+ fun instT v =
+ let
+ val T = TVar v;
+ val T' = Envir.subst_type tyenv T;
+ in if T = T' then NONE else SOME (prt_type T, prt_type T') end;
+
+ fun inst v =
+ let
+ val t = Var v;
+ val t' = Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
+ in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
+
+ fun inst_pair (x, y) = Pretty.item [x, Pretty.str " \<leadsto>", Pretty.brk 1, y];
+
+ val prts =
+ ((fold o fold) Term.add_tvars propss [] |> sort Term_Ord.tvar_ord |> map_filter instT) @
+ ((fold o fold) Term.add_vars propss [] |> sort Term_Ord.var_ord |> map_filter inst);
+ in if null prts then [] else [Pretty.big_list title (map inst_pair prts)] end;
+
+ exception LOST_STRUCTURE;
+ fun goal_matcher () =
+ let
+ val concl =
+ Logic.unprotect (Thm.concl_of goal)
+ handle TERM _ => raise LOST_STRUCTURE;
+ val goal_propss = filter_out null propss;
+ val results =
+ Logic.dest_conjunction_balanced (length goal_propss) concl
+ |> map2 Logic.dest_conjunction_balanced (map length goal_propss)
+ handle TERM _ => raise LOST_STRUCTURE;
+ in
+ Unify.matcher (Context.Proof ctxt)
+ (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (flat results)
+ end;
+
+ fun failure msg = (warning (title ^ " " ^ msg); []);
+ in
+ if Config.get ctxt show_goal_inst then
+ (case goal_matcher () of
+ SOME env => prt_inst env
+ | NONE => failure "match failed")
+ handle LOST_STRUCTURE => failure "lost goal structure"
+ else []
+ end;
(* method_error *)
@@ -255,7 +318,7 @@
"proof method" ^ Position.here pos ^ ":\n";
val pr_facts =
if null facts then ""
- else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
+ else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
val pr_goal = string_of_goal ctxt goal;
in pr_header ^ pr_facts ^ pr_goal end);
@@ -268,7 +331,10 @@
Config.declare_bool ("interactive", \<^here>) (K false);
val show_results =
- Config.declare_bool ("show_results", \<^here>) (fn context => Config.get_generic context interactive);
+ Attrib.setup_config_bool \<^binding>\<open>show_results\<close>
+ (fn context =>
+ Config.get_generic context interactive orelse
+ Options.default_bool \<^system_option>\<open>show_states\<close>);
fun no_print int ctxt = not (Config.get (Config.put interactive int ctxt) show_results);
--- a/src/Pure/Isar/toplevel.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Isar/toplevel.ML Thu Sep 08 22:35:50 2022 +0200
@@ -628,10 +628,22 @@
local
+fun show_state (st', opt_err) =
+ let
+ val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
+ val opt_err' =
+ if enabled then
+ (case Exn.capture (Output.state o string_of_state) st' of
+ Exn.Exn exn => SOME exn
+ | Exn.Res _ => opt_err)
+ else opt_err;
+ in (st', opt_err') end;
+
fun app int (tr as Transition {name, markers, trans, ...}) =
setmp_thread_position tr
(Timing.protocol (name_of tr) (pos_of tr) (apply_trans int name markers trans)
- ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn));
+ ##> Option.map (fn UNDEF => ERROR (type_error tr) | exn => exn)
+ #> show_state);
in
--- a/src/Pure/PIDE/protocol.scala Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/PIDE/protocol.scala Thu Sep 08 22:35:50 2022 +0200
@@ -165,11 +165,22 @@
}
def is_inlined(msg: XML.Tree): Boolean =
- !(is_result(msg) || is_tracing(msg) || is_state(msg))
+ !(is_result(msg) || is_tracing(msg))
def is_exported(msg: XML.Tree): Boolean =
is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg)
+ def message_heading(elem: XML.Elem, pos: Position.T): String = {
+ val h =
+ if (is_warning(elem) || is_legacy(elem)) "Warning"
+ else if (is_error(elem)) "Error"
+ else if (is_information(elem)) "Information"
+ else if (is_tracing(elem)) "Tracing"
+ else if (is_state(elem)) "State"
+ else "Output"
+ h + Position.here(pos)
+ }
+
def message_text(elem: XML.Elem,
heading: Boolean = false,
pos: Position.T = Position.none,
@@ -177,18 +188,7 @@
breakgain: Double = Pretty.default_breakgain,
metric: Pretty.Metric = Pretty.Default_Metric
): String = {
- val text1 =
- if (heading) {
- val h =
- if (is_warning(elem) || is_legacy(elem)) "Warning"
- else if (is_error(elem)) "Error"
- else if (is_information(elem)) "Information"
- else if (is_tracing(elem)) "Tracing"
- else if (is_state(elem)) "State"
- else "Output"
- "\n" + h + Position.here(pos) + ":\n"
- }
- else ""
+ val text1 = if (heading) "\n" + message_heading(elem, pos) + ":\n" else ""
val body =
Pretty.string_of(Protocol_Message.expose_no_reports(List(elem)),
--- a/src/Pure/Pure.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Pure.thy Thu Sep 08 22:35:50 2022 +0200
@@ -1302,7 +1302,7 @@
Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
"print current proof state (if present)"
(opt_modes >> (fn modes =>
- Toplevel.keep (Print_Mode.with_modes modes (Output.state o Toplevel.string_of_state))));
+ Toplevel.keep (Print_Mode.with_modes modes (Output.writeln o Toplevel.string_of_state))));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
--- a/src/Pure/ROOT.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/ROOT.ML Thu Sep 08 22:35:50 2022 +0200
@@ -250,8 +250,8 @@
(*basic proof engine*)
ML_file "par_tactical.ML";
ML_file "context_tactic.ML";
+ML_file "Isar/attrib.ML";
ML_file "Isar/proof_display.ML";
-ML_file "Isar/attrib.ML";
ML_file "Isar/context_rules.ML";
ML_file "Isar/method.ML";
ML_file "Isar/proof.ML";
--- a/src/Pure/Syntax/syntax.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Syntax/syntax.ML Thu Sep 08 22:35:50 2022 +0200
@@ -70,7 +70,7 @@
val string_of_term_global: theory -> term -> string
val string_of_typ_global: theory -> typ -> string
val string_of_sort_global: theory -> sort -> string
- val pretty_flexpair: Proof.context -> term * term -> Pretty.T
+ val pretty_flexpair: Proof.context -> term * term -> Pretty.T list
type syntax
val eq_syntax: syntax * syntax -> bool
val force_syntax: syntax -> unit
@@ -346,7 +346,7 @@
(* derived operations *)
-fun pretty_flexpair ctxt (t, u) = Pretty.block
+fun pretty_flexpair ctxt (t, u) =
[pretty_term ctxt t, Pretty.str " \<equiv>\<^sup>?", Pretty.brk 1, pretty_term ctxt u];
--- a/src/Pure/System/isabelle_tool.scala Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala Thu Sep 08 22:35:50 2022 +0200
@@ -167,6 +167,7 @@
Build_PDFjs.isabelle_tool,
Build_PolyML.isabelle_tool1,
Build_PolyML.isabelle_tool2,
+ Build_PostgreSQL.isabelle_tool,
Build_SPASS.isabelle_tool,
Build_SQLite.isabelle_tool,
Build_Scala.isabelle_tool,
--- a/src/Pure/System/options.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/System/options.ML Thu Sep 08 22:35:50 2022 +0200
@@ -35,10 +35,6 @@
val default_real: string -> real
val default_seconds: string -> Time.time
val default_string: string -> string
- val default_put_bool: string -> bool -> unit
- val default_put_int: string -> int -> unit
- val default_put_real: string -> real -> unit
- val default_put_string: string -> string -> unit
val get_default: string -> string
val put_default: string -> string -> unit
val set_default: T -> unit
@@ -195,11 +191,6 @@
fun default_seconds name = seconds (default ()) name;
fun default_string name = string (default ()) name;
-val default_put_bool = change_default put_bool;
-val default_put_int = change_default put_int;
-val default_put_real = change_default put_real;
-val default_put_string = change_default put_string;
-
fun get_default name =
let val options = default () in get (typ options name) SOME options name end;
val put_default = change_default update;
--- a/src/Pure/Thy/document_antiquotation.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Thu Sep 08 22:35:50 2022 +0200
@@ -43,15 +43,15 @@
(* options *)
-val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>);
-val thy_output_break = Attrib.setup_option_bool ("thy_output_break", \<^here>);
-val thy_output_cartouche = Attrib.setup_option_bool ("thy_output_cartouche", \<^here>);
-val thy_output_quotes = Attrib.setup_option_bool ("thy_output_quotes", \<^here>);
-val thy_output_margin = Attrib.setup_option_int ("thy_output_margin", \<^here>);
-val thy_output_indent = Attrib.setup_option_int ("thy_output_indent", \<^here>);
-val thy_output_source = Attrib.setup_option_bool ("thy_output_source", \<^here>);
-val thy_output_source_cartouche = Attrib.setup_option_bool ("thy_output_source_cartouche", \<^here>);
-val thy_output_modes = Attrib.setup_option_string ("thy_output_modes", \<^here>);
+val thy_output_display = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_display\<close>, \<^here>);
+val thy_output_break = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_break\<close>, \<^here>);
+val thy_output_cartouche = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_cartouche\<close>, \<^here>);
+val thy_output_quotes = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_quotes\<close>, \<^here>);
+val thy_output_margin = Attrib.setup_option_int (\<^system_option>\<open>thy_output_margin\<close>, \<^here>);
+val thy_output_indent = Attrib.setup_option_int (\<^system_option>\<open>thy_output_indent\<close>, \<^here>);
+val thy_output_source = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_source\<close>, \<^here>);
+val thy_output_source_cartouche = Attrib.setup_option_bool (\<^system_option>\<open>thy_output_source_cartouche\<close>, \<^here>);
+val thy_output_modes = Attrib.setup_option_string (\<^system_option>\<open>thy_output_modes\<close>, \<^here>);
(* blanks *)
--- a/src/Pure/Tools/build_job.scala Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Thu Sep 08 22:35:50 2022 +0200
@@ -8,6 +8,7 @@
import scala.collection.mutable
+import scala.util.matching.Regex
object Build_Job {
@@ -83,8 +84,10 @@
def print_log(
options: Options,
- session_name: String,
+ sessions: List[String],
theories: List[String] = Nil,
+ message_head: List[Regex] = Nil,
+ message_body: List[Regex] = Nil,
verbose: Boolean = false,
progress: Progress = new Progress,
margin: Double = Pretty.default_margin,
@@ -95,58 +98,83 @@
val store = Sessions.store(options)
val session = new Session(options, Resources.empty)
- using(Export.open_session_context0(store, session_name)) { session_context =>
- val result =
- for {
- db <- session_context.session_db()
- theories = store.read_theories(db, session_name)
- errors = store.read_errors(db, session_name)
- info <- store.read_build(db, session_name)
- } yield (theories, errors, info.return_code)
- result match {
- case None => store.error_database(session_name)
- case Some((used_theories, errors, rc)) =>
- theories.filterNot(used_theories.toSet) match {
- case Nil =>
- case bad => error("Unknown theories " + commas_quote(bad))
- }
- val print_theories =
- if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
+ def check(filter: List[Regex], make_string: => String): Boolean =
+ filter.isEmpty || {
+ val s = Output.clean_yxml(make_string)
+ filter.forall(r => r.findFirstIn(Output.clean_yxml(s)).nonEmpty)
+ }
- for (thy <- print_theories) {
- val thy_heading = "\nTheory " + quote(thy) + ":"
+ def print(session_name: String): Unit = {
+ using(Export.open_session_context0(store, session_name)) { session_context =>
+ val result =
+ for {
+ db <- session_context.session_db()
+ theories = store.read_theories(db, session_name)
+ errors = store.read_errors(db, session_name)
+ info <- store.read_build(db, session_name)
+ } yield (theories, errors, info.return_code)
+ result match {
+ case None => store.error_database(session_name)
+ case Some((used_theories, errors, rc)) =>
+ theories.filterNot(used_theories.toSet) match {
+ case Nil =>
+ case bad => error("Unknown theories " + commas_quote(bad))
+ }
+ val print_theories =
+ if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
+
+ for (thy <- print_theories) {
+ val thy_heading = "\nTheory " + quote(thy) + " (in " + session_name + ")" + ":"
- read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
- case None => progress.echo(thy_heading + " MISSING")
- case Some(command) =>
- val snapshot = Document.State.init.snippet(command)
- val rendering = new Rendering(snapshot, options, session)
- val messages =
- rendering.text_messages(Text.Range.full)
- .filter(message => verbose || Protocol.is_exported(message.info))
- if (messages.nonEmpty) {
- val line_document = Line.Document(command.source)
- progress.echo(thy_heading)
- for (Text.Info(range, elem) <- messages) {
- val line = line_document.position(range.start).line1
- val pos = Position.Line_File(line, command.node_name.node)
- progress.echo(
- Protocol.message_text(elem, heading = true, pos = pos,
- margin = margin, breakgain = breakgain, metric = metric))
+ read_theory(session_context.theory(thy), unicode_symbols = unicode_symbols) match {
+ case None => progress.echo(thy_heading + " MISSING")
+ case Some(command) =>
+ val snapshot = Document.State.init.snippet(command)
+ val rendering = new Rendering(snapshot, options, session)
+ val messages =
+ rendering.text_messages(Text.Range.full)
+ .filter(message => verbose || Protocol.is_exported(message.info))
+ if (messages.nonEmpty) {
+ val line_document = Line.Document(command.source)
+ val buffer = new mutable.ListBuffer[String]
+ for (Text.Info(range, elem) <- messages) {
+ val line = line_document.position(range.start).line1
+ val pos = Position.Line_File(line, command.node_name.node)
+ def message_text: String =
+ Protocol.message_text(elem, heading = true, pos = pos,
+ margin = margin, breakgain = breakgain, metric = metric)
+ val ok =
+ check(message_head, Protocol.message_heading(elem, pos)) &&
+ check(message_body, XML.content(Pretty.unformatted(List(elem))))
+ if (ok) buffer += message_text
+ }
+ if (buffer.nonEmpty) {
+ progress.echo(thy_heading)
+ buffer.foreach(progress.echo)
+ }
}
- }
+ }
}
- }
- if (errors.nonEmpty) {
- val msg = Symbol.output(unicode_symbols, cat_lines(errors))
- progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
- }
- if (rc != Process_Result.RC.ok) {
- progress.echo("\n" + Process_Result.RC.print_long(rc))
- }
+ if (errors.nonEmpty) {
+ val msg = Symbol.output(unicode_symbols, cat_lines(errors))
+ progress.echo("\nBuild errors:\n" + Output.error_message_text(msg))
+ }
+ if (rc != Process_Result.RC.ok) {
+ progress.echo("\n" + Process_Result.RC.print_long(rc))
+ }
+ }
}
}
+
+ val errors = new mutable.ListBuffer[String]
+ for (session_name <- sessions) {
+ Exn.interruptible_capture(print(session_name)) match {
+ case Exn.Res(_) =>
+ case Exn.Exn(exn) => errors += Exn.message(exn)
+ }
+ }
+ if (errors.nonEmpty) error(cat_lines(errors.toList))
}
@@ -157,6 +185,8 @@
{ args =>
/* arguments */
+ var message_head = List.empty[Regex]
+ var message_body = List.empty[Regex]
var unicode_symbols = false
var theories: List[String] = Nil
var margin = Pretty.default_margin
@@ -164,36 +194,43 @@
var verbose = false
val getopts = Getopts("""
-Usage: isabelle log [OPTIONS] SESSION
+Usage: isabelle log [OPTIONS] [SESSIONS ...]
Options are:
+ -H REGEX filter messages by matching against head
+ -M REGEX filter messages by matching against body
-T NAME restrict to given theories (multiple options possible)
-U output Unicode symbols
-m MARGIN margin for pretty printing (default: """ + margin + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-v print all messages, including information etc.
- Print messages from the build database of the given session, without any
- checks against current sources: results from a failed build can be
- printed as well.
+ Print messages from the build database of the given sessions, without any
+ checks against current sources nor session structure: results from old
+ sessions or failed builds can be printed as well.
+
+ Multiple options -H and -M are conjunctive: all given patterns need to
+ match. Patterns match any substring, but ^ or $ may be used to match the
+ start or end explicitly.
""",
+ "H:" -> (arg => message_head = message_head ::: List(arg.r)),
+ "M:" -> (arg => message_body = message_body ::: List(arg.r)),
"T:" -> (arg => theories = theories ::: List(arg)),
"U" -> (_ => unicode_symbols = true),
"m:" -> (arg => margin = Value.Double.parse(arg)),
"o:" -> (arg => options = options + arg),
"v" -> (_ => verbose = true))
- val more_args = getopts(args)
- val session_name =
- more_args match {
- case List(session_name) => session_name
- case _ => getopts.usage()
- }
+ val sessions = getopts(args)
val progress = new Console_Progress()
- print_log(options, session_name, theories = theories, verbose = verbose, margin = margin,
- progress = progress, unicode_symbols = unicode_symbols)
+ if (sessions.isEmpty) progress.echo_warning("No sessions to print")
+ else {
+ print_log(options, sessions, theories = theories, message_head = message_head,
+ message_body = message_body, verbose = verbose, margin = margin, progress = progress,
+ unicode_symbols = unicode_symbols)
+ }
})
}
--- a/src/Pure/config.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/config.ML Thu Sep 08 22:35:50 2022 +0200
@@ -164,7 +164,7 @@
fun declare_option (name, pos) =
let
- val typ = Options.default_typ name;
+ val typ = Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
val default =
if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
else if typ = Options.intT then fn _ => Int (Options.default_int name)
--- a/src/Pure/ex/Guess.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/ex/Guess.thy Thu Sep 08 22:35:50 2022 +0200
@@ -145,7 +145,8 @@
|> Proof.map_context (fold Variable.unbind_term Auto_Bind.no_facts)
end;
- val goal = Var (("guess", 0), propT);
+ val guess = (("guess", 0), propT);
+ val goal = Var guess;
val pos = Position.thread_data ();
fun print_result ctxt' (k, [(s, [_, th])]) =
Proof_Display.print_results int pos ctxt' (k, [(s, [th])]);
@@ -154,11 +155,13 @@
Goal.conclude #> Raw_Simplifier.norm_hhf ctxt #>
(fn th => Goal.protect 0 (Conjunction.intr (Drule.mk_term (Thm.cprop_of th)) th)));
fun after_qed (result_ctxt, results) state' =
- let val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results)
+ let
+ val [_, res] = Proof_Context.export result_ctxt (Proof.context_of state') (flat results);
+ val res' = res RS Conjunction.conjunctionD2;
in
state'
|> Proof.end_block
- |> guess_context (Obtain.check_result ctxt thesis res)
+ |> guess_context (Obtain.check_result ctxt thesis res')
end;
in
state
@@ -170,8 +173,10 @@
(SOME before_qed) after_qed
[] [] [(Binding.empty_atts, [(Logic.mk_term goal, []), (goal, [])])]
|> snd
- |> Proof.refine_singleton
- (Method.primitive_text (fn _ => fn _ => Goal.init (Thm.cterm_of ctxt thesis)))
+ |> Proof.refine_singleton (Method.Basic (fn _ => fn _ => CONTEXT_TACTIC
+ (PRIMITIVE (Thm.instantiate (TVars.empty, Vars.make [(guess, Thm.cterm_of ctxt thesis)]))
+ THEN Goal.conjunction_tac 1
+ THEN resolve_tac ctxt [Drule.termI] 1)))
end;
in
--- a/src/Pure/goal.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/goal.ML Thu Sep 08 22:35:50 2022 +0200
@@ -206,9 +206,9 @@
|> Thm.check_hyps (Context.Proof ctxt'))
handle THM (msg, _, _) => err msg | ERROR msg => err msg;
in
- if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
- then res
- else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
+ if is_none (Unify.matcher (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res])
+ then err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
+ else res
end);
val res =
if immediate orelse schematic orelse not future orelse skip then result ()
--- a/src/Pure/goal_display.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/goal_display.ML Thu Sep 08 22:35:50 2022 +0200
@@ -72,7 +72,7 @@
Syntax.unparse_term ctxt;
fun prt_atoms prt prtT (X, xs) = Pretty.block
- [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::",
+ [Pretty.item (Pretty.commas (map prt xs)), Pretty.str " ::",
Pretty.brk 1, prtT X];
fun prt_var (x, ~1) = prt_term (Syntax.free x)
@@ -93,7 +93,7 @@
Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
- val pretty_ffpairs = pretty_list "flex-flex pairs:" (Syntax.pretty_flexpair ctxt);
+ val pretty_ffpairs = pretty_list "flex-flex pairs:" (Pretty.item o Syntax.pretty_flexpair ctxt);
val pretty_consts = pretty_list "constants:" prt_consts o consts_of;
val pretty_vars = pretty_list "variables:" prt_vars o vars_of;
--- a/src/Pure/more_thm.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/more_thm.ML Thu Sep 08 22:35:50 2022 +0200
@@ -731,7 +731,7 @@
if hlen = 0 then []
else if show_hyps orelse show_hyps' then
[Pretty.brk 2, Pretty.list "[" "]"
- (map (q o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
+ (map (q o Pretty.block o Syntax.pretty_flexpair ctxt) tpairs @ map prt_term hyps @
map (Syntax.pretty_sort ctxt) extra_shyps)]
else [Pretty.brk 2, Pretty.str ("[" ^ replicate_string hlen "." ^ "]")];
val tsymbs =
--- a/src/Pure/more_unify.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/more_unify.ML Thu Sep 08 22:35:50 2022 +0200
@@ -8,7 +8,7 @@
sig
include UNIFY
val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
- val matches_list: Context.generic -> term list -> term list -> bool
+ val matcher: Context.generic -> term list -> term list -> Envir.env option
end;
structure Unify: UNIFY =
@@ -75,11 +75,10 @@
(first_order_matchers thy pairs empty)
end;
-fun matches_list context ps os =
- length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
-
+fun matcher context ps os =
+ if length ps <> length os then NONE
+ else Seq.pull (matchers context (ps ~~ os)) |> Option.map #1;
open Unify;
end;
-
--- a/src/Pure/proofterm.ML Wed Sep 07 08:58:27 2022 +0200
+++ b/src/Pure/proofterm.ML Thu Sep 08 22:35:50 2022 +0200
@@ -1860,8 +1860,8 @@
fun search _ [] =
error ("Unsolvable constraints:\n" ^
Pretty.string_of (Pretty.chunks (map (fn (_, p, _) =>
- Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
- (apply2 (Envir.norm_term bigenv) p)) cs)))
+ Pretty.item (Syntax.pretty_flexpair (Syntax.init_pretty_global thy)
+ (apply2 (Envir.norm_term bigenv) p))) cs)))
| search env ((u, p as (t1, t2), vs)::ps) =
if u then
let
--- a/src/ZF/ex/misc.thy Wed Sep 07 08:58:27 2022 +0200
+++ b/src/ZF/ex/misc.thy Thu Sep 08 22:35:50 2022 +0200
@@ -71,7 +71,7 @@
text\<open>Given as a challenge problem in
R. Boyer et al.,
- Set Theory in First-Order Logic: Clauses for G\"odel's Axioms,
+ Set Theory in First-Order Logic: Clauses for Gödel's Axioms,
JAR 2 (1986), 287-327\<close>
text\<open>collecting the relevant lemmas\<close>