--- a/Admin/components/components.sha1 Tue Aug 02 13:23:57 2022 +0200
+++ b/Admin/components/components.sha1 Tue Aug 02 13:24:19 2022 +0200
@@ -99,6 +99,7 @@
9908e5ab721f1c0035c0ab04dc7ad0bd00a8db27 flatlaf-1.2.tar.gz
9534b721b7b78344f3225067ee4df28a5440b87e flatlaf-1.6.4.tar.gz
212a0f1f867511722024cc60156fd71872a16f92 flatlaf-1.6.tar.gz
+6d4dbb6f2bde5804298d9008e3edceb0b9ee20ae flatlaf-2.4.tar.gz
f339234ec18369679be0095264e0c0af7762f351 gnu-utils-20210414.tar.gz
71259aa46134e6cf2c6473b4fc408051b3336490 gnu-utils-20211030.tar.gz
683acd94761ef460cca1a628f650355370de5afb hol-light-bundle-0.5-126.tar.gz
@@ -295,6 +296,7 @@
fc66802c169f44511d3be30435eb89a11e635742 opam-2.0.7.tar.gz
108e947d17e9aa6170872614492d8f647802f483 opam-2.1.0.tar.gz
f8d0218371457eabe2b4214427d9570de92ed861 pdfjs-2.12.313.tar.gz
+aa7fc4a3d2cbd6c8744ddfeefd863828ea602bcd pdfjs-2.14.305.tar.gz
1c8cb6a8f4cbeaedce2d6d1ba8fc7e2ab3663aeb polyml-5.4.1.tar.gz
a3f9c159a0ee9a63b7a5d0c835ed9c2c908f8b56 polyml-5.5.0-1.tar.gz
7d604a99355efbfc1459d80db3279ffa7ade3e39 polyml-5.5.0-2.tar.gz
@@ -373,6 +375,7 @@
1aaa38429dc9aa7b1095394d9a7ba3465f8d6e04 postgresql-42.2.24.tar.gz
231b33c9c3c27d47e3ba01b399103d70509e0731 postgresql-42.2.5.tar.gz
6335fbc0658e447b5b9bc48c9ad36e33a05bb72b postgresql-42.2.9.tar.gz
+f84c7ecafb07a0d763f1d70edc54f7c43c2e8c63 postgresql-42.4.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 Tue Aug 02 13:23:57 2022 +0200
+++ b/Admin/components/main Tue Aug 02 13:24:19 2022 +0200
@@ -6,7 +6,7 @@
csdp-6.1.1
cvc4-1.8
e-2.6-1
-flatlaf-1.6.4
+flatlaf-2.4
idea-icons-20210508
isabelle_fonts-20211004
isabelle_setup-20220701
@@ -18,9 +18,9 @@
minisat-2.2.1-1
nunchaku-0.5
opam-2.0.7
-pdfjs-2.12.313
+pdfjs-2.14.305
polyml-test-15c840d48c9a
-postgresql-42.2.24
+postgresql-42.4.0
scala-3.1.3
smbc-0.4.1
spass-3.8ds-2
--- a/etc/build.props Tue Aug 02 13:23:57 2022 +0200
+++ b/etc/build.props Tue Aug 02 13:24:19 2022 +0200
@@ -135,6 +135,7 @@
src/Pure/PIDE/yxml.scala \
src/Pure/ROOT.scala \
src/Pure/System/bash.scala \
+ src/Pure/System/classpath.scala \
src/Pure/System/command_line.scala \
src/Pure/System/components.scala \
src/Pure/System/executable.scala \
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Tue Aug 02 13:24:19 2022 +0200
@@ -220,7 +220,9 @@
Then define a function \<open>sum_tree ::\<close> \<^typ>\<open>nat tree \<Rightarrow> nat\<close>
that sums up all values in a tree of natural numbers
and prove \<^prop>\<open>sum_tree t = sum_list(contents t)\<close>
-(where \<^const>\<open>sum_list\<close> is predefined).
+where \<^const>\<open>sum_list\<close> is predefined by the equations
+@{thm sum_list.Nil[where 'a=nat]} and
+@{thm sum_list.Cons}.
\end{exercise}
\begin{exercise}
@@ -272,8 +274,7 @@
empty. Note that \<^const>\<open>itrev\<close> is tail-recursive: it can be
compiled into a loop; no stack is necessary for executing it.
-Naturally, we would like to show that \<^const>\<open>itrev\<close> does indeed reverse
-its first argument provided the second one is empty:
+Naturally, we would like to show that \<^const>\<open>itrev\<close> reverses its first argument:
\<close>
lemma "itrev xs [] = rev xs"
@@ -323,7 +324,7 @@
(*>*)
apply(induction xs arbitrary: ys)
-txt\<open>The induction hypothesis in the induction step is now universally quantified over \<open>ys\<close>:
+txt\<open>The induction hypothesis is now universally quantified over \<open>ys\<close>:
@{subgoals[display,margin=65]}
Thus the proof succeeds:
\<close>
--- a/src/Doc/System/Presentation.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Doc/System/Presentation.thy Tue Aug 02 13:24:19 2022 +0200
@@ -186,8 +186,7 @@
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>.
+ \<^scala_type>\<open>isabelle.Document_Build.Engine\<close>.
\<close>
--- a/src/HOL/Analysis/Infinite_Products.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Tue Aug 02 13:24:19 2022 +0200
@@ -145,6 +145,30 @@
by blast
qed (auto simp: prod_defs)
+lemma raw_has_prod_norm:
+ fixes a :: "'a ::real_normed_field"
+ assumes "raw_has_prod f M a"
+ shows "raw_has_prod (\<lambda>n. norm (f n)) M (norm a)"
+ using assms by (auto simp: raw_has_prod_def prod_norm tendsto_norm)
+
+lemma has_prod_norm:
+ fixes a :: "'a ::real_normed_field"
+ assumes f: "f has_prod a"
+ shows "(\<lambda>n. norm (f n)) has_prod (norm a)"
+ using f [unfolded has_prod_def]
+proof (elim disjE exE conjE)
+ assume f0: "raw_has_prod f 0 a"
+ then show "(\<lambda>n. norm (f n)) has_prod norm a"
+ using has_prod_def raw_has_prod_norm by blast
+next
+ fix i p
+ assume "a = 0" and "f i = 0" and p: "raw_has_prod f (Suc i) p"
+ then have "Ex (raw_has_prod (\<lambda>n. norm (f n)) (Suc i))"
+ using raw_has_prod_norm by blast
+ then show ?thesis
+ by (metis \<open>a = 0\<close> \<open>f i = 0\<close> has_prod_0_iff norm_zero)
+qed
+
subsection\<open>Absolutely convergent products\<close>
--- a/src/HOL/Data_Structures/Set2_Join.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Tue Aug 02 13:24:19 2022 +0200
@@ -64,18 +64,19 @@
subsection "\<open>join2\<close>"
-definition join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
-"join2 l r = (if r = Leaf then l else let (m,r') = split_min r in join l m r')"
+fun join2 :: "('a*'b) tree \<Rightarrow> ('a*'b) tree \<Rightarrow> ('a*'b) tree" where
+"join2 l \<langle>\<rangle> = l" |
+"join2 l r = (let (m,r') = split_min r in join l m r')"
lemma set_join2[simp]: "set_tree (join2 l r) = set_tree l \<union> set_tree r"
-by(simp add: join2_def split_min_set split: prod.split)
+by(cases r)(simp_all add: split_min_set split: prod.split)
lemma bst_join2: "\<lbrakk> bst l; bst r; \<forall>x \<in> set_tree l. \<forall>y \<in> set_tree r. x < y \<rbrakk>
\<Longrightarrow> bst (join2 l r)"
-by(simp add: join2_def bst_join split_min_set split_min_bst split: prod.split)
+by(cases r)(simp_all add: bst_join split_min_set split_min_bst split: prod.split)
lemma inv_join2: "\<lbrakk> inv l; inv r \<rbrakk> \<Longrightarrow> inv (join2 l r)"
-by(simp add: join2_def inv_join split_min_set split_min_inv split: prod.split)
+by(cases r)(simp_all add: inv_join split_min_set split_min_inv split: prod.split)
subsection "\<open>split\<close>"
--- a/src/HOL/Library/Infinite_Set.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/HOL/Library/Infinite_Set.thy Tue Aug 02 13:24:19 2022 +0200
@@ -267,6 +267,10 @@
"infinite S \<Longrightarrow> enumerate S m < enumerate S n \<longleftrightarrow> m < n"
by (metis enumerate_mono less_asym less_linear)
+lemma enumerate_mono_le_iff [simp]:
+ "infinite S \<Longrightarrow> enumerate S m \<le> enumerate S n \<longleftrightarrow> m \<le> n"
+ by (meson enumerate_mono_iff not_le)
+
lemma le_enumerate:
assumes S: "infinite S"
shows "n \<le> enumerate S n"
--- a/src/HOL/Library/List_Lenlexorder.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/HOL/Library/List_Lenlexorder.thy Tue Aug 02 13:24:19 2022 +0200
@@ -3,6 +3,8 @@
section \<open>Lexicographic order on lists\<close>
+text \<open>This version prioritises length and can yield wellorderings\<close>
+
theory List_Lenlexorder
imports Main
begin
@@ -51,6 +53,14 @@
by (auto simp add: total_on_def list_le_def list_less_def)
qed
+instance list :: (wellorder) wellorder
+proof
+ fix P :: "'a list \<Rightarrow> bool" and a
+ assume "\<And>x. (\<And>y. y < x \<Longrightarrow> P y) \<Longrightarrow> P x"
+ then show "P a"
+ unfolding list_less_def by (metis wf_lenlex wf_induct wf_lenlex wf)
+qed
+
instantiation list :: (linorder) distrib_lattice
begin
--- a/src/HOL/ex/Word_Lsb_Msb.thy Tue Aug 02 13:23:57 2022 +0200
+++ b/src/HOL/ex/Word_Lsb_Msb.thy Tue Aug 02 13:24:19 2022 +0200
@@ -5,8 +5,8 @@
class word = ring_bit_operations +
fixes word_length :: \<open>'a itself \<Rightarrow> nat\<close>
assumes word_length_positive [simp]: \<open>0 < word_length TYPE('a)\<close>
- and possible_bit_msb [simp]: \<open>possible_bit TYPE('a) (word_length TYPE('a) - Suc 0)\<close>
- and not_possible_bit_length [simp]: \<open>\<not> possible_bit TYPE('a) (word_length TYPE('a))\<close>
+ and possible_bit_msb: \<open>possible_bit TYPE('a) (word_length TYPE('a) - Suc 0)\<close>
+ and not_possible_bit_length: \<open>\<not> possible_bit TYPE('a) (word_length TYPE('a))\<close>
begin
lemma word_length_not_0 [simp]:
@@ -14,6 +14,27 @@
using word_length_positive
by simp
+lemma possible_bit_iff_less_word_length:
+ \<open>possible_bit TYPE('a) n \<longleftrightarrow> n < word_length TYPE('a)\<close> (is \<open>?P \<longleftrightarrow> ?Q\<close>)
+proof
+ assume \<open>?P\<close>
+ show ?Q
+ proof (rule ccontr)
+ assume \<open>\<not> n < word_length TYPE('a)\<close>
+ then have \<open>word_length TYPE('a) \<le> n\<close>
+ by simp
+ with \<open>?P\<close> have \<open>possible_bit TYPE('a) (word_length TYPE('a))\<close>
+ by (rule possible_bit_less_imp)
+ with not_possible_bit_length show False ..
+ qed
+next
+ assume \<open>?Q\<close>
+ then have \<open>n \<le> word_length TYPE('a) - Suc 0\<close>
+ by simp
+ with possible_bit_msb show ?P
+ by (rule possible_bit_less_imp)
+qed
+
end
instantiation word :: (len) word
@@ -46,7 +67,7 @@
lemma msb_minus_1 [simp]:
\<open>msb (- 1)\<close>
- by (simp add: msb_def)
+ by (simp add: msb_def possible_bit_iff_less_word_length)
lemma msb_1_iff [simp]:
\<open>msb 1 \<longleftrightarrow> word_length TYPE('a) = 1\<close>
@@ -54,11 +75,11 @@
lemma msb_minus_iff [simp]:
\<open>msb (- w) \<longleftrightarrow> \<not> msb (w - 1)\<close>
- by (simp add: msb_def bit_simps)
+ by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
lemma msb_not_iff [simp]:
\<open>msb (NOT w) \<longleftrightarrow> \<not> msb w\<close>
- by (simp add: msb_def bit_simps)
+ by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
lemma msb_and_iff [simp]:
\<open>msb (v AND w) \<longleftrightarrow> msb v \<and> msb w\<close>
@@ -74,11 +95,11 @@
lemma msb_exp_iff [simp]:
\<open>msb (2 ^ n) \<longleftrightarrow> n = word_length TYPE('a) - Suc 0\<close>
- by (simp add: msb_def bit_simps)
+ by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
lemma msb_mask_iff [simp]:
\<open>msb (mask n) \<longleftrightarrow> word_length TYPE('a) \<le> n\<close>
- by (simp add: msb_def bit_simps less_diff_conv2 Suc_le_eq less_Suc_eq_le)
+ by (simp add: msb_def bit_simps less_diff_conv2 Suc_le_eq less_Suc_eq_le possible_bit_iff_less_word_length)
lemma msb_set_bit_iff [simp]:
\<open>msb (set_bit n w) \<longleftrightarrow> n = word_length TYPE('a) - Suc 0 \<or> msb w\<close>
@@ -94,25 +115,29 @@
lemma msb_push_bit_iff:
\<open>msb (push_bit n w) \<longleftrightarrow> n < word_length TYPE('a) \<and> bit w (word_length TYPE('a) - Suc n)\<close>
- by (simp add: msb_def bit_simps le_diff_conv2 Suc_le_eq)
+ by (simp add: msb_def bit_simps le_diff_conv2 Suc_le_eq possible_bit_iff_less_word_length)
-(*lemma msb_drop_bit_iff [simp]:
+lemma msb_drop_bit_iff [simp]:
\<open>msb (drop_bit n w) \<longleftrightarrow> n = 0 \<and> msb w\<close>
- apply (cases n)
- apply simp_all
- apply (auto simp add: msb_def bit_simps)
- oops*)
+ by (cases n)
+ (auto simp add: msb_def bit_simps possible_bit_iff_less_word_length intro!: impossible_bit)
lemma msb_take_bit_iff [simp]:
\<open>msb (take_bit n w) \<longleftrightarrow> word_length TYPE('a) \<le> n \<and> msb w\<close>
by (simp add: take_bit_eq_mask ac_simps)
-(*lemma msb_signed_take_bit_iff:
- \<open>msb (signed_take_bit n w) \<longleftrightarrow> P w n\<close>
- unfolding signed_take_bit_def
- apply (simp add: signed_take_bit_def not_le)
- apply auto
- oops*)
+lemma msb_signed_take_bit_iff:
+ \<open>msb (signed_take_bit n w) \<longleftrightarrow> bit w (min n (word_length TYPE('a) - Suc 0))\<close>
+ by (simp add: msb_def bit_simps possible_bit_iff_less_word_length)
+
+definition signed_drop_bit :: \<open>nat \<Rightarrow> 'a \<Rightarrow> 'a\<close>
+ where \<open>signed_drop_bit n w = drop_bit n w
+ OR (of_bool (bit w (word_length TYPE('a) - Suc 0)) * NOT (mask (word_length TYPE('a) - Suc n)))\<close>
+
+lemma msb_signed_drop_bit_iff [simp]:
+ \<open>msb (signed_drop_bit n w) \<longleftrightarrow> msb w\<close>
+ by (simp add: signed_drop_bit_def bit_simps not_le not_less)
+ (simp add: msb_def)
end
--- a/src/Pure/Admin/build_pdfjs.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/Admin/build_pdfjs.scala Tue Aug 02 13:24:19 2022 +0200
@@ -17,7 +17,7 @@
/* build pdfjs component */
val default_url = "https://github.com/mozilla/pdf.js/releases/download"
- val default_version = "2.12.313"
+ val default_version = "2.14.305"
def build_pdfjs(
base_url: String = default_url,
@@ -39,7 +39,7 @@
val download_url = base_url + "/v" + version
Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
- Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-dist.zip",
+ Isabelle_System.download_file(download_url + "/pdfjs-" + version + "-legacy-dist.zip",
archive_file, progress = progress)
Isabelle_System.bash("unzip -x " + File.bash_path(archive_file),
cwd = component_dir.file).check
--- a/src/Pure/General/bytes.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/General/bytes.scala Tue Aug 02 13:24:19 2022 +0200
@@ -57,12 +57,11 @@
val buf = new Array[Byte](8192)
var m = 0
- var cont = true
- while (cont) {
+ while ({
m = stream.read(buf, 0, buf.length min (limit - out.size))
if (m != -1) out.write(buf, 0, m)
- cont = (m != -1 && limit > out.size)
- }
+ m != -1 && limit > out.size
+ }) ()
new Bytes(out.toByteArray, 0, out.size)
}
--- a/src/Pure/General/file.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/General/file.scala Tue Aug 02 13:24:19 2022 +0200
@@ -13,7 +13,7 @@
import java.nio.file.{StandardOpenOption, Path => JPath, Files, SimpleFileVisitor,
FileVisitOption, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, MalformedURLException}
+import java.net.{URI, URL, MalformedURLException}
import java.util.zip.{GZIPInputStream, GZIPOutputStream}
import java.util.EnumSet
@@ -62,6 +62,12 @@
def path(file: JFile): Path = Path.explode(standard_path(file))
def pwd(): Path = path(Path.current.absolute_file)
+ def uri(file: JFile): URI = file.toURI
+ def uri(path: Path): URI = path.file.toURI
+
+ def url(file: JFile): URL = uri(file).toURL
+ def url(path: Path): URL = url(path.file)
+
/* relative paths */
--- a/src/Pure/General/sha1.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/General/sha1.scala Tue Aug 02 13:24:19 2022 +0200
@@ -36,12 +36,11 @@
make_digest(sha => using(new FileInputStream(file)) { stream =>
val buf = new Array[Byte](65536)
var m = 0
- var cont = true
- while (cont) {
+ while ({
m = stream.read(buf, 0, buf.length)
if (m != -1) sha.update(buf, 0, m)
- cont = (m != -1)
- }
+ m != -1
+ }) ()
})
def digest(path: Path): Digest = digest(path.file)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/classpath.scala Tue Aug 02 13:24:19 2022 +0200
@@ -0,0 +1,95 @@
+/* Title: Pure/System/classpath.scala
+ Author: Makarius
+
+Java classpath and Scala services.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+import java.nio.file.Files
+import java.net.URLClassLoader
+
+import scala.jdk.CollectionConverters._
+
+
+object Classpath {
+ abstract class Service
+ type Service_Class = Class[Service]
+
+ def apply(
+ jar_files: List[JFile] = Nil,
+ jar_contents: List[File.Content_Bytes] = Nil): Classpath =
+ {
+ val jar_files0 =
+ for {
+ s <- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
+ if s.nonEmpty
+ } yield File.absolute(new JFile(s))
+
+ val jar_files1 =
+ jar_files.flatMap(start => File.find_files(start, _.getName.endsWith(".jar")))
+ .map(File.absolute)
+
+ val tmp_jars =
+ for (jar <- jar_contents) yield {
+ val tmp_jar = Files.createTempFile("jar", "jar").toFile
+ tmp_jar.deleteOnExit()
+ Bytes.write(tmp_jar, jar.content)
+ tmp_jar
+ }
+ new Classpath(jar_files0 ::: jar_files1, tmp_jars)
+ }
+}
+
+class Classpath private(static_jars: List[JFile], dynamic_jars: List[JFile]) {
+ def jars: List[JFile] = static_jars ::: dynamic_jars
+ override def toString: String = jars.mkString("Classpath(", ", ", ")")
+
+ def platform_path: String = jars.map(_.getPath).mkString(JFile.pathSeparator)
+
+ val class_loader: ClassLoader =
+ {
+ val this_class_loader = this.getClass.getClassLoader
+ if (dynamic_jars.isEmpty) this_class_loader
+ else {
+ new URLClassLoader(dynamic_jars.map(File.url).toArray, this_class_loader) {
+ override def finalize(): Unit = {
+ for (jar <- dynamic_jars) {
+ try { jar.delete() }
+ catch { case _: Throwable => }
+ }
+ }
+ }
+ }
+ }
+
+ private def init_services(where: String, names: List[String]): List[Classpath.Service_Class] = {
+ for (name <- names) yield {
+ def err(msg: String): Nothing =
+ error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
+ try { Class.forName(name, true, class_loader).asInstanceOf[Classpath.Service_Class] }
+ catch {
+ case _: ClassNotFoundException => err("Class not found")
+ case exn: Throwable => err(Exn.message(exn))
+ }
+ }
+ }
+
+ val services: List[Classpath.Service_Class] =
+ {
+ val variable = "ISABELLE_SCALA_SERVICES"
+ val services_env =
+ init_services(quote(variable), space_explode(':', Isabelle_System.getenv_strict(variable)))
+ val services_jars =
+ jars.flatMap(jar =>
+ init_services(File.standard_path(jar),
+ isabelle.setup.Build.get_services(jar.toPath).asScala.toList))
+ services_env ::: services_jars
+ }
+
+ def make_services[C](c: Class[C]): List[C] =
+ for { c1 <- services if Library.is_subclass(c1, c) }
+ yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
+}
--- a/src/Pure/System/isabelle_system.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Tue Aug 02 13:24:19 2022 +0200
@@ -13,8 +13,6 @@
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
-import scala.jdk.CollectionConverters._
-
object Isabelle_System {
/* settings environment */
@@ -39,52 +37,24 @@
/* services */
- abstract class Service
+ type Service = Classpath.Service
- @volatile private var _services: Option[List[Class[Service]]] = None
+ @volatile private var _classpath: Option[Classpath] = None
- def services(): List[Class[Service]] = {
- if (_services.isEmpty) init() // unsynchronized check
- _services.get
+ def classpath(): Classpath = {
+ if (_classpath.isEmpty) init() // unsynchronized check
+ _classpath.get
}
- def make_services[C](c: Class[C]): List[C] =
- for { c1 <- services() if Library.is_subclass(c1, c) }
- yield c1.getDeclaredConstructor().newInstance().asInstanceOf[C]
+ def make_services[C](c: Class[C]): List[C] = classpath().make_services(c)
- /* init settings + services */
-
- private def init_services(where: String, names: List[String]): List[Class[Service]] = {
- for (name <- names) yield {
- def err(msg: String): Nothing =
- error("Bad Isabelle/Scala service " + quote(name) + " in " + where + "\n" + msg)
- try { Class.forName(name).asInstanceOf[Class[Service]] }
- catch {
- case _: ClassNotFoundException => err("Class not found")
- case exn: Throwable => err(Exn.message(exn))
- }
- }
- }
-
- def init_services_env(): List[Class[Service]] =
- {
- val variable = "ISABELLE_SCALA_SERVICES"
- init_services(quote(variable), space_explode(':', getenv_strict(variable)))
- }
-
- def init_services_jar(jar: Path): List[Class[Service]] =
- init_services(jar.toString, isabelle.setup.Build.get_services(jar.java_path).asScala.toList)
-
- def init_services_jar(platform_jar: String): List[Class[Service]] =
- init_services_jar(Path.explode(File.standard_path(platform_jar)))
+ /* init settings + classpath */
def init(isabelle_root: String = "", cygwin_root: String = ""): Unit = {
isabelle.setup.Environment.init(isabelle_root, cygwin_root)
synchronized {
- if (_services.isEmpty) {
- _services = Some(init_services_env() ::: Scala.get_classpath().flatMap(init_services_jar))
- }
+ if (_classpath.isEmpty) _classpath = Some(Classpath())
}
}
--- a/src/Pure/System/scala.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/System/scala.scala Tue Aug 02 13:24:19 2022 +0200
@@ -100,10 +100,6 @@
/** compiler **/
- def get_classpath(): List[String] =
- space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
- .filter(_.nonEmpty)
-
object Compiler {
object Message {
object Kind extends Enumeration {
@@ -162,25 +158,23 @@
def context(
settings: List[String] = Nil,
- jar_dirs: List[JFile] = Nil,
+ jar_files: List[JFile] = Nil,
class_loader: Option[ClassLoader] = None
): Context = {
val isabelle_settings =
Word.explode(Isabelle_System.getenv_strict("ISABELLE_SCALAC_OPTIONS"))
-
- def find_jars(dir: JFile): List[String] =
- File.find_files(dir, file => file.getName.endsWith(".jar")).
- map(File.absolute_name)
-
- val classpath = (get_classpath() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
- val settings1 = isabelle_settings ::: settings ::: List("-classpath", classpath)
- new Context(settings1, class_loader)
+ val classpath = Classpath(jar_files = jar_files)
+ new Context(isabelle_settings ::: settings, classpath, class_loader)
}
class Context private [Compiler](
- val settings: List[String],
+ _settings: List[String],
+ val classpath: Classpath,
val class_loader: Option[ClassLoader] = None
) {
+ def settings: List[String] =
+ _settings ::: List("-classpath", classpath.platform_path)
+
private val out_stream = new ByteArrayOutputStream(1024)
private val out = new PrintStream(out_stream)
private val driver: ReplDriver = new ReplDriver(settings.toArray, out, class_loader)
--- a/src/Pure/Thy/document_build.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/Thy/document_build.scala Tue Aug 02 13:24:19 2022 +0200
@@ -155,7 +155,8 @@
def get_engine(): Engine = {
val name = document_build
- engines.find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
+ Classpath(jar_contents = classpath).make_services(classOf[Engine])
+ .find(_.name == name).getOrElse(error("Bad document_build engine " + quote(name)))
}
def get_export(theory: String, name: String): Export.Entry =
@@ -301,8 +302,6 @@
/* build engines */
- lazy val engines: List[Engine] = Isabelle_System.make_services(classOf[Engine])
-
abstract class Engine(val name: String) extends Isabelle_System.Service {
override def toString: String = name
--- a/src/Pure/Thy/sessions.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Tue Aug 02 13:24:19 2022 +0200
@@ -1136,12 +1136,11 @@
val buf = ByteBuffer.allocate(n)
var i = 0
var m = 0
- var cont = true
- while (cont) {
+ while ({
m = file.read(buf)
if (m != -1) i += m
- cont = (m != -1 && n > i)
- }
+ m != -1 && n > i
+ }) ()
if (i == n) {
val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
--- a/src/Pure/library.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Pure/library.scala Tue Aug 02 13:24:19 2022 +0200
@@ -70,11 +70,10 @@
private def next_chunk(i: Int): Option[(CharSequence, Int)] = {
if (i < end) {
var j = i
- var cont = true
- while (cont) {
+ while ({
j += 1
- cont = (j < end && !sep(source.charAt(j)))
- }
+ j < end && !sep(source.charAt(j))
+ }) ()
Some((source.subSequence(i + 1, j), j))
}
else None
--- a/src/Tools/VSCode/src/dynamic_output.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Tue Aug 02 13:24:19 2022 +0200
@@ -42,7 +42,7 @@
thy_file <- Position.Def_File.unapply(props)
def_line <- Position.Def_Line.unapply(props)
source <- resources.source_file(thy_file)
- uri = Path.explode(source).absolute_file.toURI
+ uri = File.uri(Path.explode(source).absolute_file)
} yield HTML.link(uri.toString + "#" + def_line, body)
}
val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
--- a/src/Tools/VSCode/src/language_server.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Tue Aug 02 13:24:19 2022 +0200
@@ -84,7 +84,7 @@
// prevent spurious garbage on the main protocol channel
val orig_out = System.out
try {
- System.setOut(new PrintStream(new OutputStream { def write(n: Int): Unit = {} }))
+ System.setOut(new PrintStream(OutputStream.nullOutputStream()))
server.start()
}
finally { System.setOut(orig_out) }
--- a/src/Tools/VSCode/src/state_panel.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Tue Aug 02 13:24:19 2022 +0200
@@ -66,7 +66,7 @@
thy_file <- Position.Def_File.unapply(props)
def_line <- Position.Def_Line.unapply(props)
source <- server.resources.source_file(thy_file)
- uri = Path.explode(source).absolute_file.toURI
+ uri = File.uri(Path.explode(source).absolute_file)
} yield HTML.link(uri.toString + "#" + def_line, body)
}
val elements = Presentation.elements2.copy(entity = Markup.Elements.full)
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala Tue Aug 02 13:24:19 2022 +0200
@@ -90,7 +90,7 @@
override def openConsole(console: Console): Unit = {
val context =
Scala.Compiler.context(
- jar_dirs = JEdit_Lib.directories,
+ jar_files = JEdit_Lib.directories,
class_loader = Some(new JARClassLoader))
val interpreter = new Scala_Console.Interpreter(context, console)
--- a/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 02 13:23:57 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala Tue Aug 02 13:24:19 2022 +0200
@@ -287,7 +287,7 @@
def load_icon(name: String): Icon = {
val name1 =
if (name.startsWith("idea-icons/")) {
- val file = Path.explode("$ISABELLE_IDEA_ICONS").file.toURI.toASCIIString
+ val file = File.uri(Path.explode("$ISABELLE_IDEA_ICONS")).toASCIIString
"jar:" + file + "!/" + name
}
else name