--- a/Admin/components/components.sha1 Tue Nov 02 17:01:47 2021 +0000
+++ b/Admin/components/components.sha1 Wed Nov 03 10:55:05 2021 +0000
@@ -195,6 +195,7 @@
33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz
0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz
258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
+f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
--- a/Admin/components/main Tue Nov 02 17:01:47 2021 +0000
+++ b/Admin/components/main Wed Nov 03 10:55:05 2021 +0000
@@ -10,7 +10,7 @@
isabelle_fonts-20211004
isabelle_setup-20210922
jdk-17.0.1+12
-jedit-20211019
+jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
kodkodi-1.5.7
--- a/src/Doc/Datatypes/Datatypes.thy Tue Nov 02 17:01:47 2021 +0000
+++ b/src/Doc/Datatypes/Datatypes.thy Wed Nov 03 10:55:05 2021 +0000
@@ -996,6 +996,9 @@
\item[\<open>t.\<close>\hthm{pred_map}\rm:] ~ \\
@{thm list.pred_map[no_vars]}
+\item[\<open>t.\<close>\hthm{pred_mono} \<open>[mono]\<close>\rm:] ~ \\
+@{thm list.pred_mono[no_vars]}
+
\item[\<open>t.\<close>\hthm{pred_mono_strong}\rm:] ~ \\
@{thm list.pred_mono_strong[no_vars]}
--- a/src/Doc/System/Scala.thy Tue Nov 02 17:01:47 2021 +0000
+++ b/src/Doc/System/Scala.thy Wed Nov 03 10:55:05 2021 +0000
@@ -292,12 +292,9 @@
\<^medskip>
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
- develop Isabelle/Scala/jEdit modules within an external IDE. Note that the
- result cannot be built within the IDE: it requires implicit or explicit
- \<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}) instead.
-
- The default is to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has
- no permanent effect on the originals.
+ develop Isabelle/Scala/jEdit modules within an external IDE. The default is
+ to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has no permanent
+ effect on the originals.
\<^medskip>
Option \<^verbatim>\<open>-D\<close> specifies an explicit project directory, instead of the default
--- a/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Tue Nov 02 17:01:47 2021 +0000
+++ b/src/HOL/Analysis/ex/Metric_Arith_Examples.thy Wed Nov 03 10:55:05 2021 +0000
@@ -54,7 +54,7 @@
by metric
lemma "dist a e \<le> dist a b + dist b c + dist c d + dist d e"
- by metric
+ using [[argo_timeout = 25]] by metric
lemma "max (dist x y) \<bar>dist x z - dist z y\<bar> = dist x y"
by metric
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Tue Nov 02 17:01:47 2021 +0000
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Nov 03 10:55:05 2021 +0000
@@ -2312,7 +2312,9 @@
SOME ({pred_sym, in_conj, ...} : sym_info) => (pred_sym, in_conj)
| NONE => (false, false))
val decl_sym =
- (case type_enc of Guards _ => not pred_sym | _ => true) andalso is_tptp_user_symbol s
+ (case type_enc of Guards _ => not pred_sym | _ => true) andalso
+ not (String.isPrefix let_bound_var_prefix s) andalso
+ is_tptp_user_symbol s
in
if decl_sym then
Symtab.map_default (s, [])
@@ -2724,7 +2726,10 @@
fun undeclared_in_problem problem =
let
fun do_sym (name as (s, _)) value =
- if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
+ if is_tptp_user_symbol s andalso not (String.isPrefix let_bound_var_prefix s) then
+ Symtab.default (s, (name, value))
+ else
+ I
fun do_class name = apfst (apfst (do_sym name ()))
val do_bound_tvars = fold do_class o snd
fun do_type (AType ((name, _), tys)) =
--- a/src/HOL/Tools/BNF/bnf_def.ML Tue Nov 02 17:01:47 2021 +0000
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Nov 03 10:55:05 2021 +0000
@@ -940,8 +940,8 @@
(map_id0N, [#map_id0 axioms], []),
(map_transferN, [Lazy.force (#map_transfer facts)], []),
(map_identN, [Lazy.force (#map_ident facts)], []),
+ (pred_monoN, [Lazy.force (#pred_mono facts)], mono_attrs),
(pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
- (pred_monoN, [Lazy.force (#pred_mono facts)], []),
(pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
(pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
(pred_mapN, [Lazy.force (#pred_map facts)], []),
--- a/src/Pure/Admin/build_jedit.scala Tue Nov 02 17:01:47 2021 +0000
+++ b/src/Pure/Admin/build_jedit.scala Wed Nov 03 10:55:05 2021 +0000
@@ -161,6 +161,7 @@
Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
val source_dir = jedit_patched_dir + Path.basic("jEdit")
+ val org_source_dir = source_dir + Path.basic("org")
val tmp_source_dir = tmp_dir + Path.basic("jEdit")
progress.echo("Patching jEdit sources ...")
@@ -187,7 +188,7 @@
val java_sources =
for {
- file <- File.find_files(source_dir.file, file => file.getName.endsWith(".java"))
+ file <- File.find_files(org_source_dir.file, file => file.getName.endsWith(".java"))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
} yield File.path(component_dir.java_path.relativize(file.toPath).toFile)
--- a/src/Pure/Tools/scala_project.scala Tue Nov 02 17:01:47 2021 +0000
+++ b/src/Pure/Tools/scala_project.scala Wed Nov 03 10:55:05 2021 +0000
@@ -58,7 +58,7 @@
</plugins>
</build>
- "<dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
+ <dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
</project>"""
}