--- a/Admin/components/components.sha1 Thu Nov 24 10:02:26 2022 +0100
+++ b/Admin/components/components.sha1 Tue Dec 06 08:43:43 2022 +0100
@@ -178,6 +178,7 @@
85707cfe369d0d32accbe3d96a0730c87e8639b5 jdk-17.0.1+12.tar.gz
699ab2d723b2f1df151a7dbcbdf33ddad36c7978 jdk-17.0.2+8.tar.gz
260f5e03e8fc7185f7987a6d2961a23abdce6a0b jdk-17.0.4.1+1.tar.gz
+8f417fcbe5d0fef3a958aeb9740499230aa00046 jdk-17.0.5.tar.gz
8d83e433c1419e0c0cc5fd1762903d11b4a5752c jdk-6u31.tar.gz
38d2d2a91c66714c18430e136e7e5191af3996e6 jdk-7u11.tar.gz
d765bc4ad2f34d494429b2a8c1563c49db224944 jdk-7u13.tar.gz
@@ -440,6 +441,7 @@
87c8e53100df4bc85cd8d4f55028088646d70fb4 scala-3.2.0-1.tar.gz
c58db22b9e1e90f5b7a3f5edd8bdb4ddab4947fd scala-3.2.0-2.tar.gz
7677b02fe06c992ca6cf82bf68adb16287294256 scala-3.2.0.tar.gz
+bee1c9416a086e553057171e5cb571271ed02c60 scala-3.2.1.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
cbd491c0feba1d21019d05564e76dd04f592ccb4 spass-3.8ds-1.tar.gz
edaa1268d82203067657aabcf0371ce7d4b579b9 spass-3.8ds-2.tar.gz
@@ -453,6 +455,7 @@
cba2b194114216b226d75d49a70d1bd12b141ac8 sqlite-jdbc-3.32.3.2.tar.gz
29306acd6ce9f4c87032b2c271c6df035fe7d4d3 sqlite-jdbc-3.34.0.tar.gz
8a2ca4d02cfedbfe4dad4490f1ed3ddba33a009a sqlite-jdbc-3.36.0.3.tar.gz
+d2c707638b08ad56469b92dc2941d403efbb3394 sqlite-jdbc-3.39.4.1.tar.gz
8d20968603f45a2c640081df1ace6a8b0527452a sqlite-jdbc-3.8.11.2.tar.gz
2369f06e8d095f9ba26df938b1a96000e535afff ssh-java-20161009.tar.gz
a2335d28b5b95d8d26500a53f1a9303fc5beaf36 ssh-java-20190323.tar.gz
--- a/Admin/components/main Thu Nov 24 10:02:26 2022 +0100
+++ b/Admin/components/main Tue Dec 06 08:43:43 2022 +0100
@@ -13,7 +13,7 @@
idea-icons-20210508
isabelle_fonts-20211004
isabelle_setup-20221028
-jdk-17.0.4.1+1
+jdk-17.0.5
jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
@@ -28,10 +28,10 @@
polyml-test-bafe319bc3a6-1
postgresql-42.5.0
prismjs-1.29.0
-scala-3.2.0-2
+scala-3.2.1
smbc-0.4.1
spass-3.8ds-2
-sqlite-jdbc-3.36.0.3
+sqlite-jdbc-3.39.4.1
stack-2.7.3
vampire-4.6
verit-2021.06.2-rmx
--- a/etc/build.props Thu Nov 24 10:02:26 2022 +0100
+++ b/etc/build.props Tue Dec 06 08:43:43 2022 +0100
@@ -21,7 +21,6 @@
src/Pure/Admin/build_foiltex.scala \
src/Pure/Admin/build_fonts.scala \
src/Pure/Admin/build_history.scala \
- src/Pure/Admin/build_jcef.scala \
src/Pure/Admin/build_jdk.scala \
src/Pure/Admin/build_jedit.scala \
src/Pure/Admin/build_lipics.scala \
@@ -265,6 +264,7 @@
src/Tools/jEdit/src/isabelle_vfs.scala \
src/Tools/jEdit/src/jedit_bibtex.scala \
src/Tools/jEdit/src/jedit_editor.scala \
+ src/Tools/jEdit/src/jedit_jar.scala \
src/Tools/jEdit/src/jedit_lib.scala \
src/Tools/jEdit/src/jedit_main.scala \
src/Tools/jEdit/src/jedit_options.scala \
@@ -297,6 +297,7 @@
src/Tools/jEdit/src/text_overview.scala \
src/Tools/jEdit/src/text_structure.scala \
src/Tools/jEdit/src/theories_dockable.scala \
+ src/Tools/jEdit/src/theories_status.scala \
src/Tools/jEdit/src/timing_dockable.scala \
src/Tools/jEdit/src/token_markup.scala
services = \
@@ -318,6 +319,7 @@
isabelle.Tools \
isabelle.jedit.JEdit_Plugin0 \
isabelle.jedit.JEdit_Plugin1 \
+ isabelle.jedit.JEdit_JAR$Scala_Functions \
isabelle.nitpick.Kodkod$Handler \
isabelle.nitpick.Scala_Functions \
isabelle.spark.SPARK$Load_Command1 \
--- a/src/CTT/ex/Elimination.thy Thu Nov 24 10:02:26 2022 +0100
+++ b/src/CTT/ex/Elimination.thy Tue Dec 06 08:43:43 2022 +0100
@@ -6,13 +6,13 @@
(Bibliopolis, 1984).
*)
-section "Examples with elimination rules"
+section \<open>Examples with elimination rules\<close>
theory Elimination
imports "../CTT"
begin
-text "This finds the functions fst and snd!"
+text \<open>This finds the functions fst and snd!\<close>
schematic_goal [folded basic_defs]: "A type \<Longrightarrow> ?a : (A \<times> A) \<longrightarrow> A"
apply pc
@@ -23,7 +23,7 @@
back
done
-text "Double negation of the Excluded Middle"
+text \<open>Double negation of the Excluded Middle\<close>
schematic_goal "A type \<Longrightarrow> ?a : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
apply intr
apply (rule ProdE)
@@ -31,13 +31,25 @@
apply pc
done
+text \<open>Experiment: the proof above in Isar\<close>
+lemma
+ assumes "A type" shows "(\<^bold>\<lambda>f. f ` inr(\<^bold>\<lambda>y. f ` inl(y))) : ((A + (A\<longrightarrow>F)) \<longrightarrow> F) \<longrightarrow> F"
+proof intr
+ fix f
+ assume f: "f : A + (A \<longrightarrow> F) \<longrightarrow> F"
+ with assms have "inr(\<^bold>\<lambda>y. f ` inl(y)) : A + (A \<longrightarrow> F)"
+ by pc
+ then show "f ` inr(\<^bold>\<lambda>y. f ` inl(y)) : F"
+ by (rule ProdE [OF f])
+qed (rule assms)+
+
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B) \<longrightarrow> (B \<times> A)"
apply pc
done
(*The sequent version (ITT) could produce an interesting alternative
by backtracking. No longer.*)
-text "Binary sums and products"
+text \<open>Binary sums and products\<close>
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A + B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> C) \<times> (B \<longrightarrow> C)"
apply pc
done
@@ -55,7 +67,7 @@
apply (pc assms)
done
-text "Construction of the currying functional"
+text \<open>Construction of the currying functional\<close>
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<times> B \<longrightarrow> C) \<longrightarrow> (A \<longrightarrow> (B \<longrightarrow> C))"
apply pc
done
@@ -70,7 +82,7 @@
apply (pc assms)
done
-text "Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)"
+text \<open>Martin-Löf (1984), page 48: axiom of sum-elimination (uncurry)\<close>
schematic_goal "\<lbrakk>A type; B type; C type\<rbrakk> \<Longrightarrow> ?a : (A \<longrightarrow> (B \<longrightarrow> C)) \<longrightarrow> (A \<times> B \<longrightarrow> C)"
apply pc
done
@@ -85,12 +97,12 @@
apply (pc assms)
done
-text "Function application"
+text \<open>Function application\<close>
schematic_goal "\<lbrakk>A type; B type\<rbrakk> \<Longrightarrow> ?a : ((A \<longrightarrow> B) \<times> A) \<longrightarrow> B"
apply pc
done
-text "Basic test of quantifier reasoning"
+text \<open>Basic test of quantifier reasoning\<close>
schematic_goal
assumes "A type"
and "B type"
@@ -101,7 +113,7 @@
apply (pc assms)
done
-text "Martin-Löf (1984) pages 36-7: the combinator S"
+text \<open>Martin-Löf (1984) pages 36-7: the combinator S\<close>
schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
@@ -111,7 +123,7 @@
apply (pc assms)
done
-text "Martin-Löf (1984) page 58: the axiom of disjunction elimination"
+text \<open>Martin-Löf (1984) page 58: the axiom of disjunction elimination\<close>
schematic_goal
assumes "A type"
and "B type"
@@ -129,7 +141,7 @@
(*Martin-Löf (1984) page 50*)
-text "AXIOM OF CHOICE! Delicate use of elimination rules"
+text \<open>AXIOM OF CHOICE! Delicate use of elimination rules\<close>
schematic_goal
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
@@ -168,7 +180,7 @@
by (intro replace_type [OF subst_eqtyparg]) (typechk SumE_fst assms \<open>a : A\<close>)
qed
-text "Axiom of choice. Proof without fst, snd. Harder still!"
+text \<open>Axiom of choice. Proof without fst, snd. Harder still!\<close>
schematic_goal [folded basic_defs]:
assumes "A type"
and "\<And>x. x:A \<Longrightarrow> B(x) type"
@@ -192,7 +204,7 @@
apply assumption
done
-text "Example of sequent-style deduction"
+text \<open>Example of sequent-style deduction\<close>
(*When splitting z:A \<times> B, the assumption C(z) is affected; ?a becomes
\<^bold>\<lambda>u. split(u,\<lambda>v w.split(v,\<lambda>x y.\<^bold> \<lambda>z. <x,<y,z>>) ` w) *)
schematic_goal
--- a/src/CTT/ex/Synthesis.thy Thu Nov 24 10:02:26 2022 +0100
+++ b/src/CTT/ex/Synthesis.thy Tue Dec 06 08:43:43 2022 +0100
@@ -3,13 +3,13 @@
Copyright 1991 University of Cambridge
*)
-section "Synthesis examples, using a crude form of narrowing"
+section \<open>Synthesis examples, using a crude form of narrowing\<close>
theory Synthesis
imports "../CTT"
begin
-text "discovery of predecessor function"
+text \<open>discovery of predecessor function\<close>
schematic_goal "?a : \<Sum>pred:?A . Eq(N, pred`0, 0) \<times> (\<Prod>n:N. Eq(N, pred ` succ(n), n))"
apply intr
apply eqintr
@@ -18,7 +18,7 @@
apply rew
done
-text "the function fst as an element of a function type"
+text \<open>the function fst as an element of a function type\<close>
schematic_goal [folded basic_defs]:
"A type \<Longrightarrow> ?a: \<Sum>f:?B . \<Prod>i:A. \<Prod>j:A. Eq(A, f ` <i,j>, i)"
apply intr
@@ -30,7 +30,7 @@
apply assumption+
done
-text "An interesting use of the eliminator, when"
+text \<open>An interesting use of the eliminator, when\<close>
(*The early implementation of unification caused non-rigid path in occur check
See following example.*)
schematic_goal "?a : \<Prod>i:N. Eq(?A, ?b(inl(i)), <0 , i>)
@@ -49,7 +49,7 @@
\<times> Eq(?A(i), ?b(inr(i)), <succ(0),i>)"
oops
- text "A tricky combination of when and split"
+ text \<open>A tricky combination of when and split\<close>
(*Now handled easily, but caused great problems once*)
schematic_goal [folded basic_defs]:
"?a : \<Prod>i:N. \<Prod>j:N. Eq(?A, ?b(inl(<i,j>)), i)
@@ -74,7 +74,7 @@
oops
- text "Deriving the addition operator"
+ text \<open>Deriving the addition operator\<close>
schematic_goal [folded arith_defs]:
"?c : \<Prod>n:N. Eq(N, ?f(0,n), n)
\<times> (\<Prod>m:N. Eq(N, ?f(succ(m), n), succ(?f(m,n))))"
@@ -84,7 +84,7 @@
apply rew
done
-text "The addition function -- using explicit lambdas"
+text \<open>The addition function -- using explicit lambdas\<close>
schematic_goal [folded arith_defs]:
"?c : \<Sum>plus : ?A .
\<Prod>x:N. Eq(N, plus`0`x, x)
--- a/src/CTT/ex/Typechecking.thy Thu Nov 24 10:02:26 2022 +0100
+++ b/src/CTT/ex/Typechecking.thy Tue Dec 06 08:43:43 2022 +0100
@@ -3,7 +3,7 @@
Copyright 1991 University of Cambridge
*)
-section "Easy examples: type checking and type deduction"
+section \<open>Easy examples: type checking and type deduction\<close>
theory Typechecking
imports "../CTT"
@@ -44,15 +44,15 @@
schematic_goal "\<Prod>x:N . \<Prod>y:N . Eq(?A,x,y) type"
apply typechk done
-text "typechecking an application of fst"
+text \<open>typechecking an application of fst\<close>
schematic_goal "(\<^bold>\<lambda>u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A"
apply typechk done
-text "typechecking the predecessor function"
+text \<open>typechecking the predecessor function\<close>
schematic_goal "\<^bold>\<lambda>n. rec(n, 0, \<lambda>x y. x) : ?A"
apply typechk done
-text "typechecking the addition function"
+text \<open>typechecking the addition function\<close>
schematic_goal "\<^bold>\<lambda>n. \<^bold>\<lambda>m. rec(n, m, \<lambda>x y. succ(y)) : ?A"
apply typechk done
@@ -71,7 +71,7 @@
apply N
done
-text "typechecking fst (as a function object)"
+text \<open>typechecking fst (as a function object)\<close>
schematic_goal "\<^bold>\<lambda>i. split(i, \<lambda>j k. j) : ?A"
apply typechk
apply N
--- a/src/Doc/System/Presentation.thy Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Doc/System/Presentation.thy Tue Dec 06 08:43:43 2022 +0100
@@ -65,7 +65,7 @@
\<close>
-section \<open>Preparing session root directories \label{sec:tool-mkroot}\<close>
+section \<open>Creating session root directories \label{sec:tool-mkroot}\<close>
text \<open>
The @{tool_def mkroot} tool configures a given directory as session root,
@@ -78,8 +78,9 @@
-I init Mercurial repository and add generated files
-T LATEX provide title in LaTeX notation (default: session name)
-n NAME alternative session name (default: directory base name)
+ -q quiet mode: less verbosity
- Prepare session root directory (default: current directory).
+ Create session root directory (default: current directory).
\<close>}
The results are placed in the given directory \<open>dir\<close>, which refers to the
@@ -100,6 +101,8 @@
Option \<^verbatim>\<open>-n\<close> specifies an alternative session name; otherwise the base name
of the given directory is used.
+ Option \<^verbatim>\<open>-q\<close> reduces verbosity.
+
\<^medskip>
The implicit Isabelle settings variable @{setting ISABELLE_LOGIC} specifies
the parent session.
@@ -110,12 +113,12 @@
text \<open>
Produce session \<^verbatim>\<open>Test\<close> within a separate directory of the same name:
- @{verbatim [display] \<open>isabelle mkroot Test && isabelle build -D Test\<close>}
+ @{verbatim [display] \<open>isabelle mkroot -q Test && isabelle build -D Test\<close>}
\<^medskip>
Upgrade the current directory into a session ROOT with document preparation,
and build it:
- @{verbatim [display] \<open>isabelle mkroot && isabelle build -D .\<close>}
+ @{verbatim [display] \<open>isabelle mkroot -q && isabelle build -D .\<close>}
\<close>
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Nov 24 10:02:26 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Tue Dec 06 08:43:43 2022 +0100
@@ -340,7 +340,7 @@
if exhaustive_preplay then
preplay_results
|> map
- (fn (meth, play_outcome, used_facts) =>
+ (fn (meth, (play_outcome, used_facts)) =>
"Preplay: " ^
Sledgehammer_Proof_Methods.string_of_proof_method (map fst used_facts) meth ^
" (" ^ Sledgehammer_Proof_Methods.string_of_play_outcome play_outcome ^ ")")
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 24 10:02:26 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Tue Dec 06 08:43:43 2022 +0100
@@ -19,7 +19,7 @@
type prover_problem = Sledgehammer_Prover.prover_problem
type prover_result = Sledgehammer_Prover.prover_result
- type preplay_result = proof_method * play_outcome * (string * stature) list
+ type preplay_result = proof_method * (play_outcome * (string * stature) list)
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
@@ -52,7 +52,7 @@
open Sledgehammer_Prover_Minimize
open Sledgehammer_MaSh
-type preplay_result = proof_method * play_outcome * (string * stature) list
+type preplay_result = proof_method * (play_outcome * (string * stature) list)
datatype sledgehammer_outcome =
SH_Some of prover_result * preplay_result list
@@ -129,19 +129,21 @@
in
try_methss [] methss
end)
- |> map (fn (meth, play_outcome, used_facts) => (meth, play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts))
- |> sort (play_outcome_ord o apply2 (fn (_, play_outcome, _) => play_outcome))
+ |> map (fn (meth, play_outcome, used_facts) =>
+ (meth, (play_outcome, filter_out (fn (_, (sc, _)) => sc = Chained) used_facts)))
+ |> sort (play_outcome_ord o apply2 (fn (_, (play_outcome, _)) => play_outcome))
fun select_one_line_proof used_facts preferred_meth preplay_results =
(case preplay_results of
(* Select best method if preplay succeeded *)
- (best_meth, best_outcome as Played _, best_used_facts) :: _ =>
+ (best_meth, (best_outcome as Played _, best_used_facts)) :: _ =>
(best_used_facts, (best_meth, best_outcome))
(* Otherwise select preferred method *)
- | (fst_meth, fst_outcome, _) :: _ =>
+ | _ =>
(used_facts, (preferred_meth,
- if fst_meth = preferred_meth then fst_outcome else Play_Timed_Out Time.zeroTime))
- | [] => (used_facts, (preferred_meth, Play_Timed_Out Time.zeroTime)))
+ (case AList.lookup (op =) preplay_results preferred_meth of
+ SOME (outcome, _) => outcome
+ | NONE => Play_Timed_Out Time.zeroTime))))
|> apfst (filter_out (fn (_, (sc, _)) => sc = Chained))
fun launch_prover (params as {verbose, spy, slices, timeout, ...}) mode learn
@@ -243,7 +245,7 @@
(case (expect, outcome) of
("some", SH_Some _) => ()
| ("some_preplayed", SH_Some (_, preplay_results)) =>
- if exists (fn (_, Played _, _) => true | _ => false) preplay_results then
+ if exists (fn (_, (Played _, _)) => true | _ => false) preplay_results then
()
else
error ("Unexpected outcome: the external prover found a some proof but preplay failed")
--- a/src/Pure/Admin/build_csdp.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala Tue Dec 06 08:43:43 2022 +0100
@@ -76,7 +76,7 @@
val component_name = "csdp-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
@@ -95,33 +95,30 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
- val source_name = File.get_dir(tmp_dir)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building CSDP for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
build_flags.find(flags => flags.platform == platform_name) match {
case None => error("No build flags for platform " + quote(platform_name))
case Some(flags) =>
- File.find_files(build_dir.file, pred = file => file.getName == "Makefile").
+ File.find_files(source_dir.file, pred = file => file.getName == "Makefile").
foreach(file => flags.change(File.path(file)))
}
- progress.bash(mingw.bash_script("make"), cwd = build_dir.file, echo = verbose).check
+ progress.bash(mingw.bash_script("make"), cwd = source_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
- Isabelle_System.copy_file(build_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("solver/csdp").platform_exe, platform_dir)
if (Platform.is_windows) {
Executable.libraries_closure(platform_dir + Path.explode("csdp.exe"), mingw = mingw,
@@ -133,9 +130,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_CSDP="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/csdp"
""")
--- a/src/Pure/Admin/build_cvc5.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_cvc5.scala Tue Dec 06 08:43:43 2022 +0100
@@ -40,7 +40,7 @@
val component = "cvc5-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download executables */
@@ -59,9 +59,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
CVC5_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
CVC5_VERSION=""" + Bash.string(version) + """
--- a/src/Pure/Admin/build_cygwin.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_cygwin.scala Tue Dec 06 08:43:43 2022 +0100
@@ -11,11 +11,13 @@
val default_mirror: String = "https://isabelle.sketis.net/cygwin_2022"
val packages: List[String] =
- List("curl", "libgmp-devel", "nano", "openssh", "rsync", "unzip")
+ List("curl", "libgmp-devel", "nano", "openssh", "rsync")
- def build_cygwin(progress: Progress,
+ def build_cygwin(
+ target_dir: Path = Path.current,
mirror: String = default_mirror,
- more_packages: List[String] = Nil
+ more_packages: List[String] = Nil,
+ progress: Progress = new Progress
): Unit = {
require(Platform.is_windows, "Windows platform expected")
@@ -50,8 +52,9 @@
(cygwin + Path.explode("Cygwin.bat")).file.delete
- val archive = "cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz"
- Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
+ val archive =
+ target_dir + Path.explode("cygwin-" + Date.Format.alt_date(Date.now()) + ".tar.gz")
+ Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " cygwin", dir = tmp_dir).check
}
}
@@ -62,6 +65,7 @@
Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle",
Scala_Project.here,
{ args =>
+ var target_dir = Path.current
var mirror = default_mirror
var more_packages: List[String] = Nil
@@ -70,18 +74,23 @@
Usage: isabelle build_cygwin [OPTIONS]
Options are:
+ -D DIR target directory (default ".")
-R MIRROR Cygwin mirror site (default """ + quote(default_mirror) + """)
-p NAME additional Cygwin package
Produce pre-canned Cygwin distribution for Isabelle: this requires
Windows administrator mode.
""",
+ "D:" -> (arg => target_dir = Path.explode(arg)),
"R:" -> (arg => mirror = arg),
"p:" -> (arg => more_packages ::= arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
+ val progress = new Console_Progress()
+
+ build_cygwin(target_dir = target_dir, mirror = mirror, more_packages = more_packages,
+ progress = progress)
})
}
--- a/src/Pure/Admin/build_e.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_e.scala Tue Dec 06 08:43:43 2022 +0100
@@ -25,7 +25,7 @@
val component_name = "e-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
@@ -41,35 +41,34 @@
val archive_path = tmp_dir + Path.explode("E.tgz")
Isabelle_System.download_file(archive_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash("tar xzf " + archive_path + " && mv E src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = archive_url)
+
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building E prover for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic("E")
val build_options = {
- val result = Isabelle_System.bash("./configure --help", cwd = build_dir.file)
+ val result = Isabelle_System.bash("./configure --help", cwd = source_dir.file)
if (result.check.out.containsSlice("--enable-ho")) " --enable-ho" else ""
}
val build_script = "./configure" + build_options + " && make"
- Isabelle_System.bash(build_script,
- cwd = build_dir.file,
+ Isabelle_System.bash(build_script, cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("COPYING"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("COPYING"), component_dir.LICENSE)
val install_files = List("epclextract", "eprover", "eprover-ho")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic("PROVER") + Path.basic(name)
+ val path = source_dir + Path.basic("PROVER") + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
Isabelle_System.bash("if [ -f eprover-ho ]; then mv eprover-ho eprover; fi",
@@ -78,13 +77,12 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
E_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
E_VERSION=""" + quote(version) + """
""")
+
/* README */
File.write(component_dir.README,
--- a/src/Pure/Admin/build_easychair.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_easychair.scala Tue Dec 06 08:43:43 2022 +0100
@@ -19,24 +19,15 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
- val easychair_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
+ val easychair_dir = File.get_dir(download_dir, title = download_url)
/* component */
@@ -47,18 +38,14 @@
val component = "easychair-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(easychair_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_EASYCHAIR_HOME="$COMPONENT"
""")
--- a/src/Pure/Admin/build_eptcs.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_eptcs.scala Tue Dec 06 08:43:43 2022 +0100
@@ -23,14 +23,11 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
-
/* component */
val component = "eptcs-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download */
@@ -39,16 +36,13 @@
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(download_file, component_dir.path)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_EPTCS_HOME="$COMPONENT"
""")
--- a/src/Pure/Admin/build_foiltex.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_foiltex.scala Tue Dec 06 08:43:43 2022 +0100
@@ -19,61 +19,49 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
- val foiltex_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
-
- val README = Path.explode("README")
- val README_flt = Path.explode("README.flt")
- Isabelle_System.move_file(foiltex_dir + README, foiltex_dir + README_flt)
-
- Isabelle_System.bash("pdflatex foiltex.ins", cwd = foiltex_dir.file).check
+ val foiltex_dir = File.get_dir(download_dir, title = download_url)
/* component */
+ val README = Path.explode("README")
val version = {
val Version = """^.*Instructions for FoilTeX Version\s*(.*)$""".r
- split_lines(File.read(foiltex_dir + README_flt))
+ split_lines(File.read(foiltex_dir + README))
.collectFirst({ case Version(v) => v })
- .getOrElse(error("Failed to detect version in " + README_flt))
+ .getOrElse(error("Failed to detect version in " + README))
}
val component = "foiltex-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(foiltex_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
+
+ Isabelle_System.bash("pdflatex foiltex.ins", cwd = component_dir.path.file).check
+ (component_dir.path + Path.basic("foiltex.log")).file.delete()
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_FOILTEX_HOME="$COMPONENT"
""")
/* README */
+ Isabelle_System.move_file(component_dir.README,
+ component_dir.path + Path.basic("README.flt"))
+
File.write(component_dir.README,
"""This is FoilTeX from
""" + download_url + """
--- a/src/Pure/Admin/build_fonts.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_fonts.scala Tue Dec 06 08:43:43 2022 +0100
@@ -185,7 +185,7 @@
File.bash_path(source) + " " + File.bash_path(target)).check
}
- private def hinted_path(hinted: Boolean): Path =
+ private def make_path(hinted: Boolean = false): Path =
if (hinted) Path.basic("ttf-hinted") else Path.basic("ttf")
private val hinting = List(false, true)
@@ -204,132 +204,152 @@
}
}
+ val default_download_url =
+ "https://github.com/dejavu-fonts/dejavu-fonts/releases/download/version_2_37/dejavu-fonts-ttf-2.37.zip"
+
val default_sources: List[Family] =
List(Family.deja_vu_sans_mono, Family.deja_vu_sans, Family.deja_vu_serif)
- val default_target_dir: Path = Path.explode("isabelle_fonts")
-
def build_fonts(
+ download_url: String = default_download_url,
+ target_dir: Path = Path.current,
+ target_prefix: String = "Isabelle",
sources: List[Family] = default_sources,
- source_dirs: List[Path] = Nil,
- target_prefix: String = "Isabelle",
- target_version: String = "",
- target_dir: Path = default_target_dir,
progress: Progress = new Progress
): Unit = {
Isabelle_System.require_command("ttfautohint")
- progress.echo("Directory " + target_dir)
- hinting.foreach(hinted => Isabelle_System.make_directory(target_dir + hinted_path(hinted)))
+ Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
+ Isabelle_System.with_tmp_dir("download") { download_dir =>
+
- val font_dirs = source_dirs ::: List(Path.explode("~~/Admin/isabelle_fonts"))
- for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
+ /* download */
+
+ Isabelle_System.download_file(download_url, download_file, progress = progress)
+ Isabelle_System.extract(download_file, download_dir)
+
+ val dejavu_dir = File.get_dir(download_dir, title = download_url) + Path.basic("ttf")
- // Isabelle fonts
-
- val targets =
- for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
- yield {
- val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))
-
- val source_file = find_file(font_dirs, source_font)
- val source_names = Fontforge.font_names(source_file)
-
- val target_names = source_names.update(prefix = target_prefix, version = target_version)
-
- Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
- for (hinted <- hinting) {
- val target_file = target_dir + hinted_path(hinted) + target_names.ttf
- progress.echo("Font " + target_file.toString + " ...")
-
- if (hinted) auto_hint(source_file, tmp_file)
- else Isabelle_System.copy_file(source_file, tmp_file)
+ /* component */
- Fontforge.execute(
- Fontforge.commands(
- Fontforge.open(isabelle_file),
- Fontforge.select(Range.isabelle_font),
- Fontforge.copy,
- Fontforge.close,
+ val component_date = Date.Format.alt_date(Date.now())
+ val component_name = "isabelle_fonts-" + component_date
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
- Fontforge.open(tmp_file),
- Fontforge.select(Range.base_font),
- Fontforge.select_invert,
- Fontforge.clear,
- Fontforge.select(Range.isabelle_font),
- Fontforge.paste,
-
- target_names.set,
- Fontforge.generate(target_file),
- Fontforge.close)
- ).check
- }
+ for (hinted <- hinting) {
+ Isabelle_System.make_directory(component_dir.path + make_path(hinted = hinted))
}
- (target_names.ttf, index)
- }
+ val font_dirs = List(dejavu_dir, Path.explode("~~/Admin/isabelle_fonts"))
+ for (dir <- font_dirs if !dir.is_dir) error("Bad source directory: " + dir)
- // Vacuous font
+ // Isabelle fonts
- {
- val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
+ val fonts =
+ for { source <- sources; (source_font, index) <- source.fonts.zipWithIndex }
+ yield {
+ val isabelle_file = find_file(font_dirs, Family.isabelle_symbols.get(index))
+
+ val source_file = find_file(font_dirs, source_font)
+ val source_names = Fontforge.font_names(source_file)
- val target_names = Fontforge.font_names(vacuous_file)
- val target_file = target_dir + hinted_path(false) + target_names.ttf
-
- progress.echo("Font " + target_file.toString + " ...")
+ val font_names = source_names.update(prefix = target_prefix, version = component_date)
- val domain =
- (for ((name, index) <- targets if index == 0)
- yield Fontforge.font_domain(target_dir + hinted_path(false) + name))
- .flatten.distinct.sorted
+ Isabelle_System.with_tmp_file("font", "ttf") { tmp_file =>
+ for (hinted <- hinting) {
+ val font_file = component_dir.path + make_path(hinted = hinted) + font_names.ttf
+ progress.echo("Font " + font_file + " ...")
+
+ if (hinted) auto_hint(source_file, tmp_file)
+ else Isabelle_System.copy_file(source_file, tmp_file)
- Fontforge.execute(
- Fontforge.commands(
- Fontforge.open(vacuous_file),
- Fontforge.select(Range.vacuous_font),
- Fontforge.copy) +
+ Fontforge.execute(
+ Fontforge.commands(
+ Fontforge.open(isabelle_file),
+ Fontforge.select(Range.isabelle_font),
+ Fontforge.copy,
+ Fontforge.close,
- domain.map(code =>
- Fontforge.commands(
- Fontforge.select(Seq(code)),
- Fontforge.paste))
- .mkString("\n", "\n", "\n") +
+ Fontforge.open(tmp_file),
+ Fontforge.select(Range.base_font),
+ Fontforge.select_invert,
+ Fontforge.clear,
+ Fontforge.select(Range.isabelle_font),
+ Fontforge.paste,
- Fontforge.commands(
- Fontforge.generate(target_file),
- Fontforge.close)
- ).check
- }
+ font_names.set,
+ Fontforge.generate(font_file),
+ Fontforge.close)
+ ).check
+ }
+ }
+
+ (font_names.ttf, index)
+ }
- // etc/settings
+ // Vacuous font
+
+ {
+ val vacuous_file = find_file(font_dirs, Family.vacuous.get(0))
+
+ val font_dir = component_dir.path + make_path()
+ val font_names = Fontforge.font_names(vacuous_file)
+ val font_file = font_dir + font_names.ttf
+
+ progress.echo("Font " + font_file + " ...")
- val settings_path = Components.Directory(target_dir).settings
- Isabelle_System.make_directory(settings_path.dir)
+ val domain =
+ (for ((name, index) <- fonts if index == 0)
+ yield Fontforge.font_domain(font_dir + name))
+ .flatten.distinct.sorted
+
+ Fontforge.execute(
+ Fontforge.commands(
+ Fontforge.open(vacuous_file),
+ Fontforge.select(Range.vacuous_font),
+ Fontforge.copy) +
- def fonts_settings(hinted: Boolean): String =
- "\n isabelle_fonts \\\n" +
- (for ((target, _) <- targets) yield
- """ "$COMPONENT/""" + hinted_path(hinted).file_name + "/" + target.file_name + "\"")
- .mkString(" \\\n")
+ domain.map(code =>
+ Fontforge.commands(
+ Fontforge.select(Seq(code)),
+ Fontforge.paste))
+ .mkString("\n", "\n", "\n") +
+
+ Fontforge.commands(
+ Fontforge.generate(font_file),
+ Fontforge.close)
+ ).check
+ }
+
- File.write(settings_path,
- """# -*- shell-script -*- :mode=shellscript:
+ /* settings */
+ def make_settings(hinted: Boolean = false): String =
+ "\n isabelle_fonts \\\n" +
+ (for ((ttf, _) <- fonts) yield
+ """ "$COMPONENT/""" + make_path(hinted = hinted).file_name + "/" + ttf.file_name + "\"")
+ .mkString(" \\\n")
+
+ component_dir.write_settings("""
if grep "isabelle_fonts_hinted.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null
-then""" + fonts_settings(false) + """
-else""" + fonts_settings(true) + """
+then""" + make_settings() + """
+else""" + make_settings(hinted = true) + """
fi
-isabelle_fonts_hidden "$COMPONENT/""" + hinted_path(false).file_name + """/Vacuous.ttf"
+isabelle_fonts_hidden "$COMPONENT/""" + make_path().file_name + """/Vacuous.ttf"
""")
- // README
- Isabelle_System.copy_file(Path.explode("~~/Admin/isabelle_fonts/README"), target_dir)
+ /* README */
+
+ Isabelle_System.copy_file(
+ Path.explode("~~/Admin/isabelle_fonts/README"), component_dir.README)
+ }
+ }
}
@@ -338,27 +358,26 @@
val isabelle_tool =
Isabelle_Tool("build_fonts", "construct Isabelle fonts", Scala_Project.here,
{ args =>
- var source_dirs: List[Path] = Nil
+ var target_dir = Path.current
+ var download_url = default_download_url
val getopts = Getopts("""
Usage: isabelle build_fonts [OPTIONS]
Options are:
- -d DIR additional source directory
+ -D DIR target directory (default ".")
+ -U URL download URL (default: """" + default_download_url + """")
Construct Isabelle fonts from DejaVu font families and Isabelle symbols.
""",
- "d:" -> (arg => source_dirs = source_dirs ::: List(Path.explode(arg))))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg))
val more_args = getopts(args)
if (more_args.nonEmpty) getopts.usage()
- val target_version = Date.Format.alt_date(Date.now())
- val target_dir = Path.explode("isabelle_fonts-" + target_version)
-
val progress = new Console_Progress
- build_fonts(source_dirs = source_dirs, target_dir = target_dir,
- target_version = target_version, progress = progress)
+ build_fonts(download_url = download_url, target_dir = target_dir, progress = progress)
})
}
--- a/src/Pure/Admin/build_jcef.scala Thu Nov 24 10:02:26 2022 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,172 +0,0 @@
-/* Title: Pure/Admin/build_jcef.scala
- Author: Makarius
-
-Build Isabelle component for Java Chromium Embedded Framework (JCEF).
-See also:
-
- - https://github.com/jcefmaven/jcefbuild
- - https://github.com/chromiumembedded/java-cef
-*/
-
-package isabelle
-
-
-object Build_JCEF {
- /* platform information */
-
- sealed case class JCEF_Platform(
- platform_name: String, archive: String, lib: String, library: String)
-
- private val linux_library =
- """ISABELLE_JCEF_LIBRARY="$ISABELLE_JCEF_LIB/libcef.so"
- export LD_LIBRARY_PATH="$ISABELLE_JCEF_LIB:$JAVA_HOME/lib:$LD_LIBRARY_PATH""""
-
- private val macos_library =
- """export JAVA_LIBRARY_PATH="$ISABELLE_JCEF_HOME/bin/jcef_app.app/Contents/Java:$ISABELLE_JCEF_LIB:$JAVA_LIBRARY_PATH""""
-
- private val windows_library =
- """export PATH="$ISABELLE_JCEF_LIB:$PATH""""
-
- val platforms: List[JCEF_Platform] =
- List(
- JCEF_Platform("x86_64-linux", "linux-amd64.tar.gz", "bin/lib/linux64", linux_library),
- JCEF_Platform("arm64-linux", "linux-arm64.tar.gz", "bin/lib/linux64", linux_library),
- JCEF_Platform("x86_64-darwin", "macosx-amd64.tar.gz",
- "bin/jcef_app.app/Contents/Frameworks/Chromium Embedded Framework.framework/Libraries", macos_library),
- JCEF_Platform("arm64-darwin", "macosx-arm64.tar.gz",
- "bin/jcef_app.app/Contents/Frameworks/Chromium Embedded Framework.framework/Libraries", macos_library),
- JCEF_Platform("x86_64-windows", "windows-amd64.tar.gz", "bin/lib/win64", windows_library))
-
-
- /* build JCEF */
-
- val default_url = "https://github.com/jcefmaven/jcefbuild/releases/download"
- val default_version = "1.0.18"
-
- def build_jcef(
- base_url: String = default_url,
- version: String = default_version,
- target_dir: Path = Path.current,
- progress: Progress = new Progress
- ): Unit = {
- /* component name */
-
- val component = "jcef-" + version
- val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
-
-
- /* download and assemble platforms */
-
- val platform_settings: List[String] =
- for (platform <- platforms) yield {
- Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_file =>
- val url = base_url + "/" + version + "/" + platform.archive
- Isabelle_System.download_file(url, archive_file, progress = progress)
-
- val platform_dir = component_dir.path + Path.explode(platform.platform_name)
- Isabelle_System.make_directory(platform_dir)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive_file), dir = platform_dir).check
-
- for {
- file <- File.find_files(platform_dir.file).iterator
- name = file.getName
- if File.is_dll(name) || File.is_exe(name)
- } File.set_executable(File.path(file), true)
-
- val classpath =
- File.find_files(platform_dir.file, pred = file => File.is_jar(file.getName))
- .flatMap(file => File.relative_path(platform_dir, File.path(file)))
- .map(jar => " " + quote("$ISABELLE_JCEF_HOME/" + jar.implode))
- .mkString(" \\\n")
-
- " " + platform.platform_name + ")\n" +
- " " + "classpath \\\n" + classpath + "\n" +
- " " + "ISABELLE_JCEF_LIB=\"$ISABELLE_JCEF_HOME/" + platform.lib + "\"\n" +
- " " + platform.library + "\n" +
- " " + ";;"
- }
- }
-
-
- /* settings */
-
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
-ISABELLE_JCEF_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_APPLE_PLATFORM64:-$ISABELLE_PLATFORM64}}"
-if [ -d "$COMPONENT/$ISABELLE_JCEF_PLATFORM" ]
-then
- ISABELLE_JCEF_HOME="$COMPONENT/$ISABELLE_JCEF_PLATFORM"
- ISABELLE_JCEF_LIBRARY=""
- case "$ISABELLE_JCEF_PLATFORM" in
-""" + cat_lines(platform_settings) + """
- esac
-fi
-""")
-
-
- /* README */
-
- File.write(component_dir.README,
- """This distribution of Java Chromium Embedded Framework (JCEF)
-has been assembled from the binary builds from
-https://github.com/jcefmaven/jcefbuild/releases/tag/""" +version + """
-
-Examples invocations:
-
-* Command-line
-
- isabelle env bash -c 'isabelle java -Djava.library.path="$(platform_path "$ISABELLE_JCEF_LIB")" tests.detailed.MainFrame'
-
-* Scala REPL (e.g. Isabelle/jEdit Console)
-
- import isabelle._
- System.setProperty("java.library.path", File.platform_path(Path.explode("$ISABELLE_JCEF_LIB")))
- org.cef.CefApp.startup(Array())
- GUI_Thread.later { val frame = new tests.detailed.MainFrame(false, false, false, Array()); frame.setSize(1200,900); frame.setVisible(true) }
-
-* Demo websites
-
- https://mozilla.github.io/pdf.js/web/viewer.html
- https://www.w3schools.com/w3css/w3css_demo.asp
-
-
- Makarius
- """ + Date.Format.date(Date.now()) + "\n")
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("build_jcef", "build component for Java Chromium Embedded Framework",
- Scala_Project.here,
- { args =>
- var target_dir = Path.current
- var base_url = default_url
- var version = default_version
-
- val getopts = Getopts("""
-Usage: isabelle build_jcef [OPTIONS]
-
- Options are:
- -D DIR target directory (default ".")
- -U URL download URL (default: """" + default_url + """")
- -V VERSION version (default: """" + default_version + """")
-
- Build component for Java Chromium Embedded Framework.
-""",
- "D:" -> (arg => target_dir = Path.explode(arg)),
- "U:" -> (arg => base_url = arg),
- "V:" -> (arg => version = arg))
-
- val more_args = getopts(args)
- if (more_args.nonEmpty) getopts.usage()
-
- val progress = new Console_Progress()
-
- build_jcef(base_url = base_url, version = version, target_dir = target_dir,
- progress = progress)
- })
-}
--- a/src/Pure/Admin/build_jdk.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_jdk.scala Tue Dec 06 08:43:43 2022 +0100
@@ -1,90 +1,95 @@
/* Title: Pure/Admin/build_jdk.scala
Author: Makarius
-Build Isabelle jdk component from original platform installations.
+Build Isabelle jdk component using downloads from Azul.
*/
package isabelle
-import java.io.{File => JFile}
import java.nio.file.Files
import java.nio.file.attribute.PosixFilePermission
-import scala.util.matching.Regex
-
object Build_JDK {
- /* platform and version information */
-
- sealed case class JDK_Platform(
- platform_name: String,
- platform_regex: Regex,
- exe: String = "java",
- macos_home: Boolean = false,
- jdk_version: String = ""
- ) {
- override def toString: String = platform_name
-
- def platform_path: Path = Path.explode(platform_name)
+ /* platform information */
- def detect(jdk_dir: Path): Option[JDK_Platform] = {
- val major_version = {
- val Major_Version = """.*jdk(\d+).*$""".r
- val jdk_name = jdk_dir.file.getName
- jdk_name match {
- case Major_Version(s) => s
- case _ => error("Cannot determine major version from " + quote(jdk_name))
- }
- }
+ sealed case class JDK_Platform(name: String, url_template: String) {
+ override def toString: String = name
- val path = jdk_dir + Path.explode("bin") + Path.explode(exe)
- if (path.is_file) {
- val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
- if (platform_regex.matches(file_descr)) {
- val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
- val version_lines =
- Isabelle_System.bash("strings " + File.bash_path(path)).check
- .out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
- version_lines match {
- case List(jdk_version) => Some(copy(jdk_version = jdk_version))
- case _ => error("Expected unique version within executable " + path)
- }
- }
- else None
- }
- else None
- }
+ def url(base_url: String, jdk_version: String, zulu_version: String): String =
+ base_url + "/" + url_template.replace("{V}", jdk_version).replace("{Z}", zulu_version)
}
- val templates: List[JDK_Platform] =
+ val platforms: List[JDK_Platform] =
List(
- JDK_Platform("arm64-darwin", """.*Mach-O 64-bit.*arm64.*""".r, macos_home = true),
- JDK_Platform("arm64-linux", """.*ELF 64-bit.*ARM aarch64.*""".r),
- JDK_Platform("x86_64-darwin", """.*Mach-O 64-bit.*x86[-_]64.*""".r, macos_home = true),
- JDK_Platform("x86_64-linux", """.*ELF 64-bit.*x86[-_]64.*""".r),
- JDK_Platform("x86_64-windows", """.*PE32\+ executable.*x86[-_]64.*""".r, exe = "java.exe"))
+ JDK_Platform("arm64-darwin", "zulu{Z}-jdk{V}-macosx_aarch64.tar.gz"),
+ JDK_Platform("arm64-linux", "zulu{Z}-jdk{V}-linux_aarch64.tar.gz"),
+ JDK_Platform("x86_64-darwin", "zulu{Z}-jdk{V}-macosx_x64.tar.gz"),
+ JDK_Platform("x86_64-linux", "zulu{Z}-jdk{V}-linux_x64.tar.gz"),
+ JDK_Platform("x86_64-windows", "zulu{Z}-jdk{V}-win_x64.zip"))
+
+
+ /* build jdk */
+
+ val default_base_url = "https://cdn.azul.com/zulu/bin"
+ val default_jdk_version = "17.0.5"
+ val default_zulu_version = "17.38.21-ca"
+
+ def build_jdk(
+ target_dir: Path = Path.current,
+ base_url: String = default_base_url,
+ jdk_version: String = default_jdk_version,
+ zulu_version: String = default_zulu_version,
+ progress: Progress = new Progress,
+ ): Unit = {
+ if (Platform.is_windows) error("Cannot build on Windows")
+
+
+ /* component */
+
+ val component = "jdk-" + jdk_version
+ val component_dir =
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
- /* README */
-
- def readme(jdk_version: String): String =
- """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
-https://www.azul.com/downloads/zulu-community/?package=jdk
+ /* download */
-The main license is GPL2, but some modules are covered by other (more liberal)
-licenses, see legal/* for details.
+ for (platform <- platforms) {
+ Isabelle_System.with_tmp_dir("download", component_dir.path.file) { dir =>
+ val url = platform.url(base_url, jdk_version, zulu_version)
+ val name = Library.take_suffix(_ != '/', url.toList)._2.mkString
+ val file = dir + Path.basic(name)
+ Isabelle_System.download_file(url, file, progress = progress)
-Linux, Windows, macOS all work uniformly, depending on platform-specific
-subdirectories.
-"""
+ val platform_dir = component_dir.path + Path.basic(platform.name)
+ Isabelle_System.extract(file, platform_dir, strip = true)
+ }
+ }
- /* settings */
+ /* permissions */
- val settings: String =
- """# -*- shell-script -*- :mode=shellscript:
+ for (file <- File.find_files(component_dir.path.file, include_dirs = true)) {
+ val path = file.toPath
+ val perms = Files.getPosixFilePermissions(path)
+ perms.add(PosixFilePermission.OWNER_READ)
+ perms.add(PosixFilePermission.GROUP_READ)
+ perms.add(PosixFilePermission.OTHERS_READ)
+ perms.add(PosixFilePermission.OWNER_WRITE)
+ if (file.isDirectory) {
+ perms.add(PosixFilePermission.OWNER_WRITE)
+ perms.add(PosixFilePermission.OWNER_EXECUTE)
+ perms.add(PosixFilePermission.GROUP_EXECUTE)
+ perms.add(PosixFilePermission.OTHERS_EXECUTE)
+ }
+ Files.setPosixFilePermissions(path, perms)
+ }
+
+ /* settings */
+
+ component_dir.write_settings("""
case "$ISABELLE_PLATFORM_FAMILY" in
linux)
ISABELLE_JAVA_PLATFORM="$ISABELLE_PLATFORM64"
@@ -104,131 +109,57 @@
ISABELLE_JDK_HOME="$COMPONENT/$ISABELLE_JAVA_PLATFORM"
;;
esac
-"""
-
-
- /* extract archive */
-
- def extract_archive(dir: Path, archive: Path): JDK_Platform = {
- try {
- val tmp_dir = Isabelle_System.make_directory(dir + Path.explode("tmp"))
-
- if (archive.get_ext == "zip") {
- Isabelle_System.bash(
- "unzip -x " + File.bash_path(archive.absolute), cwd = tmp_dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- }
-
- val dir_entry =
- File.read_dir(tmp_dir) match {
- case List(s) => s
- case _ => error("Archive contains multiple directories")
- }
-
- val jdk_dir = tmp_dir + Path.explode(dir_entry)
- val platform =
- templates.view.flatMap(_.detect(jdk_dir))
- .headOption.getOrElse(error("Failed to detect JDK platform"))
-
- val platform_dir = dir + platform.platform_path
- if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
-
- Isabelle_System.move_file(jdk_dir, platform_dir)
-
- platform
- }
- catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred for " + archive) }
- }
+""")
- /* build jdk */
-
- def build_jdk(
- archives: List[Path],
- progress: Progress = new Progress,
- target_dir: Path = Path.current
- ): Unit = {
- if (Platform.is_windows) error("Cannot build jdk on Windows")
-
- Isabelle_System.with_tmp_dir("jdk") { dir =>
- progress.echo("Extracting ...")
- val platforms = archives.map(extract_archive(dir, _))
+ /* README */
- val jdk_version =
- platforms.map(_.jdk_version).distinct match {
- case List(version) => version
- case Nil => error("No archives")
- case versions =>
- error("Archives contain multiple JDK versions: " + commas_quote(versions))
- }
-
- templates.filterNot(p1 => platforms.exists(p2 => p1.platform_name == p2.platform_name))
- match {
- case Nil =>
- case missing => error("Missing platforms: " + commas_quote(missing.map(_.platform_name)))
- }
+ File.write(component_dir.README,
+ """This is OpenJDK """ + jdk_version + """ based on downloads by Azul, see also
+https://www.azul.com/downloads/?package=jdk
- val jdk_name = "jdk-" + jdk_version
- val jdk_path = Path.explode(jdk_name)
- val component_dir = Components.Directory.create(dir + jdk_path, progress = progress)
-
- File.write(component_dir.settings, settings)
- File.write(component_dir.README, readme(jdk_version))
-
- for (platform <- platforms) {
- Isabelle_System.move_file(dir + platform.platform_path, component_dir.path)
- }
+The main license is GPL2, but some modules are covered by other (more liberal)
+licenses, see legal/* for details.
- for (file <- File.find_files(component_dir.path.file, include_dirs = true)) {
- val path = file.toPath
- val perms = Files.getPosixFilePermissions(path)
- perms.add(PosixFilePermission.OWNER_READ)
- perms.add(PosixFilePermission.GROUP_READ)
- perms.add(PosixFilePermission.OTHERS_READ)
- perms.add(PosixFilePermission.OWNER_WRITE)
- if (file.isDirectory) {
- perms.add(PosixFilePermission.OWNER_WRITE)
- perms.add(PosixFilePermission.OWNER_EXECUTE)
- perms.add(PosixFilePermission.GROUP_EXECUTE)
- perms.add(PosixFilePermission.OTHERS_EXECUTE)
- }
- Files.setPosixFilePermissions(path, perms)
- }
-
- progress.echo("Archiving ...")
- Isabelle_System.gnutar(
- "-czf " + File.bash_path(target_dir + jdk_path.tar.gz) + " " + jdk_name, dir = dir).check
- }
+Linux, Windows, macOS all work uniformly, depending on platform-specific
+subdirectories.
+""")
}
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("build_jdk", "build Isabelle jdk component from original archives",
+ Isabelle_Tool("build_jdk", "build Isabelle jdk component using downloads from Azul",
Scala_Project.here,
{ args =>
var target_dir = Path.current
+ var base_url = default_base_url
+ var jdk_version = default_jdk_version
+ var zulu_version = default_zulu_version
val getopts = Getopts("""
-Usage: isabelle build_jdk [OPTIONS] ARCHIVES...
+Usage: isabelle build_jdk [OPTIONS]
Options are:
-D DIR target directory (default ".")
+ -U URL base URL (default: """" + default_base_url + """")
+ -V NAME JDK version (default: """" + default_jdk_version + """")
+ -Z NAME Zulu version (default: """" + default_zulu_version + """")
- Build jdk component from tar.gz archives, with original jdk archives
- for Linux, Windows, and macOS.
+ Build Isabelle jdk component using downloads from Azul.
""",
- "D:" -> (arg => target_dir = Path.explode(arg)))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => base_url = arg),
+ "V:" -> (arg => jdk_version = arg),
+ "Z:" -> (arg => zulu_version = arg))
val more_args = getopts(args)
- if (more_args.isEmpty) getopts.usage()
+ if (more_args.nonEmpty) getopts.usage()
- val archives = more_args.map(Path.explode)
val progress = new Console_Progress()
- build_jdk(archives = archives, progress = progress, target_dir = target_dir)
+ build_jdk(target_dir = target_dir, base_url = base_url,
+ jdk_version = jdk_version, zulu_version = zulu_version, progress = progress)
})
}
--- a/src/Pure/Admin/build_jedit.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_jedit.scala Tue Dec 06 08:43:43 2022 +0100
@@ -111,9 +111,8 @@
): Unit = {
Isabelle_System.require_command("ant", test = "-version")
Isabelle_System.require_command("patch")
- Isabelle_System.require_command("unzip", test = "-h")
- val component_dir = Components.Directory.create(component_path, progress = progress)
+ val component_dir = Components.Directory(component_path).create(progress = progress)
/* jEdit directory */
@@ -144,7 +143,7 @@
File.bash_platform_path(jedit_dir) + " unix-script=off unix-man=off").check
val source_path = download_jedit(tmp_dir, "source.tar.bz2")
- Isabelle_System.gnutar("-xjf " + File.bash_path(source_path), dir = jedit_dir).check
+ Isabelle_System.extract(source_path, jedit_dir)
/* patched version */
@@ -157,7 +156,7 @@
progress.echo("Patching jEdit sources ...")
for {
- file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).iterator
+ file <- File.find_files(Path.explode("~~/src/Tools/jEdit/patches").file).sortBy(_.getName)
name = file.getName
if !File.is_backup(name)
} {
@@ -178,11 +177,11 @@
Isabelle_System.copy_file(tmp_source_dir + Path.explode("build/jedit.jar"), jedit_patched_dir)
val java_sources =
- for {
+ (for {
file <- File.find_files(org_source_dir.file, file => File.is_java(file.getName))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
- } yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode
+ } yield File.path(component_path.java_path.relativize(file.toPath).toFile).implode).sorted
File.write(component_dir.build_props,
"module = " + jedit_patched + "/jedit.jar\n" +
@@ -206,7 +205,7 @@
"https://sourceforge.net/projects/jedit-plugins/files/" + name + "/" + vers + "/" +
name + "-" + vers + "-bin.zip/download"
Isabelle_System.download_file(url, zip_path, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(zip_path), cwd = jars_dir.file).check
+ Isabelle_System.extract(zip_path, jars_dir)
}
}
@@ -470,9 +469,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
JEDIT_HOME="$COMPONENT/""" + jedit_patched + """"
JEDIT_JARS=""" + quote(File.read_dir(jars_dir).map("$JEDIT_HOME/jars/" + _).mkString(":")) + """
JEDIT_JAR="$JEDIT_HOME/jedit.jar"
--- a/src/Pure/Admin/build_lipics.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_lipics.scala Tue Dec 06 08:43:43 2022 +0100
@@ -36,8 +36,7 @@
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.gnutar("-xzf " + File.bash_path(download_file),
- dir = download_dir, strip = 1).check
+ Isabelle_System.extract(download_file, download_dir, strip = true)
val lipics_dir = download_dir + Path.explode("LIPIcs/authors")
@@ -54,16 +53,14 @@
val component = "lipics-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
Isabelle_System.copy_dir(lipics_dir, component_dir.path)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_LIPICS_HOME="$COMPONENT/authors"
""")
--- a/src/Pure/Admin/build_llncs.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_llncs.scala Tue Dec 06 08:43:43 2022 +0100
@@ -22,58 +22,45 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download", ext = "zip") { download_file =>
Isabelle_System.with_tmp_dir("download") { download_dir =>
/* download */
Isabelle_System.download_file(download_url, download_file, progress = progress)
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file),
- cwd = download_dir.file).check
+ Isabelle_System.extract(download_file, download_dir)
- val llncs_dir =
- File.read_dir(download_dir) match {
- case List(name) => download_dir + Path.explode(name)
- case bad =>
- error("Expected exactly one directory entry in " + download_file +
- bad.mkString("\n", "\n ", ""))
- }
-
- val readme = Path.explode("README.md")
- File.change(llncs_dir + readme)(_.replace(" ", "\u00a0"))
+ val llncs_dir = File.get_dir(download_dir, title = download_url)
/* component */
+ val README_md = Path.explode("README.md")
val version = {
val Version = """^_.* v(.*)_$""".r
- split_lines(File.read(llncs_dir + readme))
+ split_lines(File.read(llncs_dir + README_md))
.collectFirst({ case Version(v) => v })
- .getOrElse(error("Failed to detect version in " + readme))
+ .getOrElse(error("Failed to detect version in " + README_md))
}
val component = "llncs-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
- Isabelle_System.rm_tree(component_dir.path)
- Isabelle_System.copy_dir(llncs_dir, component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
+ Isabelle_System.extract(download_file, component_dir.path, strip = true)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_LLNCS_HOME="$COMPONENT"
""")
/* README */
+ File.change(component_dir.path + README_md)(_.replace(" ", "\u00a0"))
+
File.write(component_dir.README,
"""This is the Springer LaTeX LNCS style for authors from
""" + download_url + """
--- a/src/Pure/Admin/build_minisat.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_minisat.scala Tue Dec 06 08:43:43 2022 +0100
@@ -42,7 +42,7 @@
val component = proper_string(component_name) getOrElse make_component_name(version)
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* platform */
@@ -60,30 +60,27 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
- val source_name = File.get_dir(tmp_dir)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building Minisat for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
if (Platform.is_macos) {
- File.change(build_dir + Path.explode("Makefile")) {
+ File.change(source_dir + Path.explode("Makefile")) {
_.replaceAll("--static", "").replaceAll("-Wl,-soname\\S+", "")
}
}
- progress.bash("make r", build_dir.file, echo = verbose).check
+ progress.bash("make r", source_dir.file, echo = verbose).check
Isabelle_System.copy_file(
- build_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
+ source_dir + Path.explode("build/release/bin/minisat").platform_exe, platform_dir)
if (Platform.is_windows) {
Isabelle_System.copy_file(Path.explode("/bin/cygwin1.dll"), platform_dir)
@@ -92,9 +89,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
MINISAT_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_MINISAT="$MINISAT_HOME/minisat"
--- a/src/Pure/Admin/build_pdfjs.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_pdfjs.scala Tue Dec 06 08:43:43 2022 +0100
@@ -25,14 +25,11 @@
target_dir: Path = Path.current,
progress: Progress = new Progress
): Unit = {
- Isabelle_System.require_command("unzip", test = "-h")
-
-
/* component name */
val component = "pdfjs-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download */
@@ -41,16 +38,13 @@
Isabelle_System.with_tmp_file("archive", ext = "zip") { archive_file =>
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.path.file).check
+ Isabelle_System.extract(archive_file, component_dir.path)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_PDFJS_HOME="$COMPONENT"
""")
--- a/src/Pure/Admin/build_polyml.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_polyml.scala Tue Dec 06 08:43:43 2022 +0100
@@ -146,13 +146,7 @@
/** skeleton for component **/
private def extract_sources(source_archive: Path, component_dir: Path): Unit = {
- if (source_archive.get_ext == "zip") {
- Isabelle_System.bash(
- "unzip -x " + File.bash_path(source_archive.absolute), cwd = component_dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(source_archive), dir = component_dir).check
- }
+ Isabelle_System.extract(source_archive, component_dir)
val src_dir = component_dir + Path.explode("src")
File.read_dir(component_dir) match {
@@ -181,7 +175,7 @@
component_path: Path,
sha1_root: Option[Path] = None
): Unit = {
- val component_dir = Components.Directory.create(component_path)
+ val component_dir = Components.Directory(component_path).create()
extract_sources(source_archive, component_path)
Isabelle_System.copy_file(Path.explode("~~/Admin/polyml/settings"), component_dir.etc)
--- a/src/Pure/Admin/build_postgresql.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_postgresql.scala Tue Dec 06 08:43:43 2022 +0100
@@ -37,7 +37,7 @@
/* component */
val component_dir =
- Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
/* LICENSE */
@@ -81,9 +81,7 @@
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
classpath "$COMPONENT/""" + download_name + """.jar"
""")
--- a/src/Pure/Admin/build_prismjs.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_prismjs.scala Tue Dec 06 08:43:43 2022 +0100
@@ -28,7 +28,7 @@
val component = "prismjs-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* download */
@@ -46,9 +46,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_PRISMJS_HOME="$COMPONENT"
""")
--- a/src/Pure/Admin/build_release.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_release.scala Tue Dec 06 08:43:43 2022 +0100
@@ -13,7 +13,7 @@
private def execute(dir: Path, script: String): Unit =
Isabelle_System.bash(script, cwd = dir.file).check
- private def execute_tar(dir: Path, args: String, strip: Int = 0): Process_Result =
+ private def execute_tar(dir: Path, args: String, strip: Boolean = false): Process_Result =
Isabelle_System.gnutar(args, dir = dir, strip = strip).check
private def bash_java_opens(args: String*): String =
@@ -107,7 +107,7 @@
val isabelle_dir = Isabelle_System.make_directory(dir + ISABELLE)
Bytes.write(archive_path, bytes)
- execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = 1)
+ execute_tar(isabelle_dir, "-xzf " + File.bash_path(archive_path), strip = true)
val id = File.read(isabelle_dir + ISABELLE_ID)
val tags = File.read(isabelle_dir + ISABELLE_TAGS)
@@ -208,7 +208,7 @@
component_dir.read_components().flatMap(line =>
line match {
case Bundled(name) =>
- if (Components.Directory(Components.contrib(dir, name)).check) Some(contrib_name(name))
+ if (Components.Directory(Components.contrib(dir, name)).ok) Some(contrib_name(name))
else None
case _ => if (Bundled.detect(line)) None else Some(line)
}) ::: more_names.map(contrib_name))
--- a/src/Pure/Admin/build_scala.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_scala.scala Tue Dec 06 08:43:43 2022 +0100
@@ -28,14 +28,6 @@
def get(path: Path, progress: Progress = new Progress): Unit =
Isabelle_System.download_file(proper_url, path, progress = progress)
- def get_unpacked(dir: Path, strip: Int = 0, progress: Progress = new Progress): Unit =
- Isabelle_System.with_tmp_file("archive"){ archive_path =>
- get(archive_path, progress = progress)
- progress.echo("Unpacking " + artifact)
- Isabelle_System.gnutar(
- "-xzf " + File.bash_path(archive_path), dir = dir, strip = strip).check
- }
-
def print: String =
" * " + name + " " + version +
(if (base_version.nonEmpty) " for Scala " + base_version else "") +
@@ -43,7 +35,7 @@
}
val main_download: Download =
- Download("scala", "3.2.0", base_version = "",
+ Download("scala", "3.2.1", base_version = "",
url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
val lib_downloads: List[Download] = List(
@@ -72,12 +64,15 @@
val component_name = main_download.name + "-" + main_download.version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* download */
- main_download.get_unpacked(component_dir.path, strip = 1, progress = progress)
+ Isabelle_System.with_tmp_file("archive", ext = "tar.gz") { archive_path =>
+ main_download.get(archive_path, progress = progress)
+ Isabelle_System.extract(archive_path, component_dir.path, strip = true)
+ }
lib_downloads.foreach(download =>
download.get(component_dir.lib + Path.basic(download.artifact), progress = progress))
@@ -113,9 +108,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
SCALA_HOME="$COMPONENT"
SCALA_INTERFACES="$SCALA_HOME/lib/""" + interfaces + """"
""" + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
--- a/src/Pure/Admin/build_spass.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_spass.scala Tue Dec 06 08:43:43 2022 +0100
@@ -29,9 +29,9 @@
val Component_Name = """^(.+)-src\.tar.gz$""".r
val Version = """^[^-]+-([^-]+)$""".r
- val (archive_name, archive_base_name) =
+ val archive_name =
download_url match {
- case Archive_Name(name) => (name, Library.perhaps_unsuffix(".tar.gz", name))
+ case Archive_Name(name) => name
case _ => error("Failed to determine source archive name from " + quote(download_url))
}
@@ -52,7 +52,7 @@
}
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
val platform_name =
proper_string(Isabelle_System.getenv("ISABELLE_PLATFORM64"))
@@ -67,51 +67,47 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + archive_path, cwd = tmp_dir.file).check
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(archive_base_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
+
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building SPASS for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(archive_base_name)
-
if (Platform.is_windows) {
- File.change(build_dir + Path.basic("misc.c")) {
+ File.change(source_dir + Path.basic("misc.c")) {
_.replace("""#include "execinfo.h" """, "")
.replaceAll("""void misc_DumpCore\(void\)[^}]+}""", "void misc_DumpCore(void) { abort(); }")
}
}
- Isabelle_System.bash("make",
- cwd = build_dir.file,
+ Isabelle_System.bash("make", cwd = source_dir.file,
progress_stdout = progress.echo_if(verbose, _),
progress_stderr = progress.echo_if(verbose, _)).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.basic("LICENCE"), component_dir.LICENSE)
+ Isabelle_System.copy_file(source_dir + Path.basic("LICENCE"), component_dir.LICENSE)
val install_files = List("SPASS")
for (name <- install_files ::: install_files.map(_ + ".exe")) {
- val path = build_dir + Path.basic(name)
+ val path = source_dir + Path.basic(name)
if (path.is_file) Isabelle_System.copy_file(path, platform_dir)
}
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
SPASS_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
SPASS_VERSION=""" + quote(version) + """
""")
+
/* README */
File.write(component_dir.README,
--- a/src/Pure/Admin/build_sqlite.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_sqlite.scala Tue Dec 06 08:43:43 2022 +0100
@@ -10,8 +10,11 @@
object Build_SQLite {
/* build sqlite */
+ val default_download_url =
+ "https://repo1.maven.org/maven2/org/xerial/sqlite-jdbc/3.39.4.1/sqlite-jdbc-3.39.4.1.jar"
+
def build_sqlite(
- download_url: String,
+ download_url: String = default_download_url,
progress: Progress = new Progress,
target_dir: Path = Path.current
): Unit = {
@@ -26,7 +29,7 @@
/* component */
val component_dir =
- Components.Directory.create(target_dir + Path.basic(download_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(download_name)).create(progress = progress)
/* README */
@@ -38,24 +41,21 @@
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_SQLITE_HOME="$COMPONENT"
-classpath "$ISABELLE_SQLITE_HOME/""" + download_name + """.jar"
+classpath "$ISABELLE_SQLITE_HOME/lib/""" + download_name + """.jar"
""")
/* jar */
- val jar = component_dir.path + Path.basic(download_name).ext("jar")
+ val jar = component_dir.lib + Path.basic(download_name).ext("jar")
+ Isabelle_System.make_directory(jar.dir)
Isabelle_System.download_file(download_url, jar, progress = progress)
Isabelle_System.with_tmp_dir("build") { jar_dir =>
- progress.echo("Unpacking " + jar)
- Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
- cwd = jar_dir.file).check
+ Isabelle_System.extract(jar, jar_dir)
val jar_files =
List(
@@ -84,28 +84,28 @@
Scala_Project.here,
{ args =>
var target_dir = Path.current
+ var download_url = default_download_url
val getopts = Getopts("""
Usage: isabelle build_sqlite [OPTIONS] DOWNLOAD
Options are:
-D DIR target directory (default ".")
+ -U URL download URL
+ (default: """" + default_download_url + """")
Build sqlite-jdbc component from the specified download URL (JAR), see also
https://github.com/xerial/sqlite-jdbc and
https://oss.sonatype.org/content/repositories/releases/org/xerial/sqlite-jdbc
""",
- "D:" -> (arg => target_dir = Path.explode(arg)))
+ "D:" -> (arg => target_dir = Path.explode(arg)),
+ "U:" -> (arg => download_url = arg))
val more_args = getopts(args)
- val download_url =
- more_args match {
- case List(download_url) => download_url
- case _ => getopts.usage()
- }
+ if (more_args.nonEmpty) getopts.usage()
val progress = new Console_Progress()
- build_sqlite(download_url, progress = progress, target_dir = target_dir)
+ build_sqlite(download_url = download_url, progress = progress, target_dir = target_dir)
})
}
--- a/src/Pure/Admin/build_vampire.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_vampire.scala Tue Dec 06 08:43:43 2022 +0100
@@ -47,7 +47,7 @@
val component = proper_string(component_name) getOrElse make_component_name(version)
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component), progress = progress)
+ Components.Directory(target_dir + Path.basic(component)).create(progress = progress)
/* platform */
@@ -65,42 +65,37 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
- val source_name = File.get_dir(tmp_dir)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
progress.echo("Building Vampire for " + platform_name + " ...")
- val build_dir = tmp_dir + Path.basic(source_name)
- Isabelle_System.copy_file(build_dir + Path.explode("LICENCE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENCE"), component_dir.path)
val cmake_opts = if (Platform.is_linux) "-DBUILD_SHARED_LIBS=0 " else ""
val cmake_out =
progress.bash("cmake " + cmake_opts + """-G "Unix Makefiles" .""",
- cwd = build_dir.file, echo = verbose).check.out
+ cwd = source_dir.file, echo = verbose).check.out
val Pattern = """-- Setting binary name to '?([^\s']*)'?""".r
val binary =
split_lines(cmake_out).collectFirst({ case Pattern(name) => name })
.getOrElse(error("Failed to determine binary name from cmake output:\n" + cmake_out))
- progress.bash("make -j" + jobs, cwd = build_dir.file, echo = verbose).check
+ progress.bash("make -j" + jobs, cwd = source_dir.file, echo = verbose).check
- Isabelle_System.copy_file(build_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
+ Isabelle_System.copy_file(source_dir + Path.basic("bin") + Path.basic(binary).platform_exe,
platform_dir + Path.basic("vampire").platform_exe)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
VAMPIRE_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
ISABELLE_VAMPIRE="$VAMPIRE_HOME/vampire"
--- a/src/Pure/Admin/build_verit.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_verit.scala Tue Dec 06 08:43:43 2022 +0100
@@ -42,7 +42,7 @@
val component_name = "verit-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
@@ -61,12 +61,10 @@
val archive_path = tmp_dir + Path.basic(archive_name)
Isabelle_System.download_file(download_url, archive_path, progress = progress)
- Isabelle_System.bash("tar xzf " + File.bash_path(archive_path), cwd = tmp_dir.file).check
- val source_name = File.get_dir(tmp_dir)
+ Isabelle_System.extract(archive_path, tmp_dir)
+ val source_dir = File.get_dir(tmp_dir, title = download_url)
- Isabelle_System.bash(
- "tar xzf " + archive_path + " && mv " + Bash.string(source_name) + " src",
- cwd = component_dir.path.file).check
+ Isabelle_System.extract(archive_path, component_dir.src, strip = true)
/* build */
@@ -76,25 +74,22 @@
val configure_options =
if (Platform.is_linux) "LDFLAGS=-Wl,-rpath,_DUMMY_" else ""
- val build_dir = tmp_dir + Path.basic(source_name)
progress.bash(mingw.bash_script("set -e\n./configure " + configure_options + "\nmake"),
- cwd = build_dir.file, echo = verbose).check
+ cwd = source_dir.file, echo = verbose).check
/* install */
- Isabelle_System.copy_file(build_dir + Path.explode("LICENSE"), component_dir.path)
+ Isabelle_System.copy_file(source_dir + Path.explode("LICENSE"), component_dir.path)
val exe_path = Path.basic("veriT").platform_exe
- Isabelle_System.copy_file(build_dir + exe_path, platform_dir)
+ Isabelle_System.copy_file(source_dir + exe_path, platform_dir)
Executable.libraries_closure(platform_dir + exe_path, filter = Set("libgmp"), mingw = mingw)
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_VERIT="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}/veriT"
""")
--- a/src/Pure/Admin/build_zipperposition.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_zipperposition.scala Tue Dec 06 08:43:43 2022 +0100
@@ -27,7 +27,7 @@
val component_name = "zipperposition-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* platform */
@@ -68,9 +68,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ZIPPERPOSITION_HOME="$COMPONENT/$ISABELLE_PLATFORM64"
""")
--- a/src/Pure/Admin/build_zstd.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Admin/build_zstd.scala Tue Dec 06 08:43:43 2022 +0100
@@ -44,7 +44,7 @@
val component_name = "zstd-jni-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
File.write(component_dir.README,
"This is " + component_name + " from\n" + download_url +
@@ -61,18 +61,14 @@
download_url + "/" + version + "/" + jar_name, jar, progress = progress)
Isabelle_System.with_tmp_dir("build") { jar_dir =>
- progress.echo("Unpacking " + jar)
- Isabelle_System.bash("isabelle_jdk jar xf " + File.bash_path(jar.absolute),
- cwd = jar_dir.file).check
+ Isabelle_System.extract(jar, jar_dir)
for (platform <- platforms) platform.install(jar_dir, component_dir.path, version)
}
/* settings */
- File.write(component_dir.settings,
-"""# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_ZSTD_HOME="$COMPONENT"
classpath "$ISABELLE_ZSTD_HOME/""" + jar_name + """"
--- a/src/Pure/Concurrent/par_list.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Concurrent/par_list.scala Tue Dec 06 08:43:43 2022 +0100
@@ -47,12 +47,16 @@
def map[A, B](f: A => B, xs: List[A], sequential: Boolean = false): List[B] =
Exn.release_first(managed_results(f, xs, sequential = sequential))
+ private class Found(val res: Any) extends Exception
+
def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] = {
- class Found(val res: B) extends Exception
val results =
managed_results(
(x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
- results.collectFirst({ case Exn.Exn(found: Found) => found.res }) match {
+ results.collectFirst({
+ case Exn.Exn(found) if found.isInstanceOf[Found] =>
+ found.asInstanceOf[Found].res.asInstanceOf[B]
+ }) match {
case None => Exn.release_first(results); None
case some => some
}
--- a/src/Pure/General/exn.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/General/exn.scala Tue Dec 06 08:43:43 2022 +0100
@@ -78,6 +78,12 @@
def failure_rc(exn: Throwable): Int =
isabelle.setup.Exn.failure_rc(exn)
+ def is_interrupt_exn[A](result: Result[A]): Boolean =
+ result match {
+ case Exn(exn) if is_interrupt(exn) => true
+ case _ => false
+ }
+
def interruptible_capture[A](e: => A): Result[A] =
try { Res(e) }
catch { case exn: Throwable if !is_interrupt(exn) => Exn[A](exn) }
--- a/src/Pure/General/file.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/General/file.scala Tue Dec 06 08:43:43 2022 +0100
@@ -61,6 +61,8 @@
def canonical_name(file: JFile): String = canonical(file).getPath
def path(file: JFile): Path = Path.explode(standard_path(file))
+ def path(java_path: JPath): Path = path(java_path.toFile)
+
def pwd(): Path = path(Path.current.absolute_file)
def uri(file: JFile): URI = file.toURI
@@ -83,6 +85,9 @@
def is_node(s: String): Boolean = s.endsWith(".node")
def is_pdf(s: String): Boolean = s.endsWith(".pdf")
def is_png(s: String): Boolean = s.endsWith(".png")
+ def is_tar_bz2(s: String): Boolean = s.endsWith(".tar.bz2")
+ def is_tar_gz(s: String): Boolean = s.endsWith(".tar.gz")
+ def is_tgz(s: String): Boolean = s.endsWith(".tgz")
def is_thy(s: String): Boolean = s.endsWith(".thy")
def is_xz(s: String): Boolean = s.endsWith(".xz")
def is_zip(s: String): Boolean = s.endsWith(".zip")
@@ -128,13 +133,26 @@
else files.toList.map(_.getName).sorted
}
- def get_dir(dir: Path): String =
- read_dir(dir).filter(name => (dir + Path.basic(name)).is_dir) match {
- case List(entry) => entry
- case dirs =>
- error("Exactly one directory entry expected: " + commas_quote(dirs.sorted))
+ def get_entry(
+ dir: Path,
+ pred: Path => Boolean = _ => true,
+ title: String = ""
+ ): Path =
+ read_dir(dir).filter(name => pred(dir + Path.basic(name))) match {
+ case List(entry) => dir + Path.basic(entry)
+ case bad =>
+ error("Bad directory content in " + (if (title.nonEmpty) title else dir.toString) +
+ "\nexpected a single entry, but found" +
+ (if (bad.isEmpty) " nothing"
+ else bad.sorted.map(quote).mkString(":\n ", "\n ", "")))
}
+ def get_file(dir: Path, title: String = ""): Path =
+ get_entry(dir, pred = _.is_file, title = title)
+
+ def get_dir(dir: Path, title: String = ""): Path =
+ get_entry(dir, pred = _.is_dir, title = title)
+
def find_files(
start: JFile,
pred: JFile => Boolean = _ => true,
--- a/src/Pure/General/mercurial.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/General/mercurial.scala Tue Dec 06 08:43:43 2022 +0100
@@ -74,7 +74,7 @@
Bytes.write(archive_path, content.bytes)
progress.echo("Unpacking " + rev + ".tar.gz")
Isabelle_System.gnutar("-xzf " + File.bash_path(archive_path),
- dir = dir, original_owner = true, strip = 1).check
+ dir = dir, original_owner = true, strip = true).check
}
}
}
--- a/src/Pure/General/sql.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/General/sql.scala Tue Dec 06 08:43:43 2022 +0100
@@ -367,11 +367,8 @@
lazy val init_jdbc: Unit = {
val lib_path = Path.explode("$ISABELLE_SQLITE_HOME/" + Platform.jvm_platform)
- val lib_name =
- File.find_files(lib_path.file) match {
- case List(file) => file.getName
- case _ => error("Exactly one file expected in directory " + lib_path.expand)
- }
+ val lib_name = File.get_file(lib_path).file_name
+
System.setProperty("org.sqlite.lib.path", File.platform_path(lib_path))
System.setProperty("org.sqlite.lib.name", lib_name)
--- a/src/Pure/General/zstd.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/General/zstd.scala Tue Dec 06 08:43:43 2022 +0100
@@ -18,12 +18,9 @@
"Zstd library already initialized by other means than isabelle.Zstd.init()")
val lib_dir = Path.explode("$ISABELLE_ZSTD_HOME/" + Platform.jvm_platform)
- val lib_file =
- File.find_files(lib_dir.file) match {
- case List(file) => file
- case _ => error("Exactly one file expected in directory " + lib_dir.expand)
- }
- System.load(File.platform_path(lib_file.getAbsolutePath))
+ val lib_file = File.get_file(lib_dir)
+
+ System.load(lib_file.absolute_file.getPath)
zstd.util.Native.assumeLoaded()
assert(zstd.util.Native.isLoaded())
--- a/src/Pure/ROOT.ML Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/ROOT.ML Tue Dec 06 08:43:43 2022 +0100
@@ -366,3 +366,4 @@
ML_file "Tools/jedit.ML";
ML_file "Tools/ghc.ML";
ML_file "Tools/generated_files.ML";
+
--- a/src/Pure/ROOT.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/ROOT.scala Tue Dec 06 08:43:43 2022 +0100
@@ -21,4 +21,3 @@
val proper_string = Library.proper_string _
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
}
-
--- a/src/Pure/System/classpath.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/System/classpath.scala Tue Dec 06 08:43:43 2022 +0100
@@ -29,7 +29,8 @@
} yield File.absolute(new JFile(s))
val jar_files1 =
- jar_files.flatMap(start => File.find_files(start, file => File.is_jar(file.getName)))
+ jar_files.flatMap(start =>
+ File.find_files(start, file => File.is_jar(file.getName)).sortBy(_.getName))
.map(File.absolute)
val tmp_jars =
--- a/src/Pure/System/components.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/System/components.scala Tue Dec 06 08:43:43 2022 +0100
@@ -48,7 +48,7 @@
def unpack(dir: Path, archive: Path, progress: Progress = new Progress): String = {
val name = Archive.get_name(archive.file_name)
progress.echo("Unpacking " + name)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = dir).check
+ Isabelle_System.extract(archive, dir)
name
}
@@ -104,14 +104,6 @@
object Directory {
def apply(path: Path): Directory = new Directory(path.absolute)
-
- def create(path: Path, progress: Progress = new Progress): Directory = {
- val component_dir = new Directory(path.absolute)
- progress.echo("Creating component directory " + component_dir.path)
- Isabelle_System.new_directory(component_dir.path)
- Isabelle_System.make_directory(component_dir.etc)
- component_dir
- }
}
class Directory private(val path: Path) {
@@ -126,12 +118,30 @@
def README: Path = path + Path.basic("README")
def LICENSE: Path = path + Path.basic("LICENSE")
- def check: Boolean = settings.is_file || components.is_file
+ def create(progress: Progress = new Progress): Directory = {
+ progress.echo("Creating component directory " + path)
+ Isabelle_System.new_directory(path)
+ Isabelle_System.make_directory(etc)
+ this
+ }
+
+ def ok: Boolean = settings.is_file || components.is_file || Sessions.is_session_dir(path)
+
+ def check: Directory =
+ if (!path.is_dir) error("Bad component directory: " + path)
+ else if (!ok) {
+ error("Malformed component directory: " + path +
+ "\n (missing \"etc/settings\" or \"etc/components\" or \"ROOT\" or \"ROOTS\")")
+ }
+ else this
def read_components(): List[String] =
split_lines(File.read(components)).filter(_.nonEmpty)
def write_components(lines: List[String]): Unit =
File.write(components, terminate_lines(lines))
+
+ def write_settings(text: String): Unit =
+ File.write(settings, "# -*- shell-script -*- :mode=shellscript:\n" + text)
}
@@ -170,9 +180,7 @@
def update_components(add: Boolean, path0: Path, progress: Progress = new Progress): Unit = {
val path = path0.expand.absolute
- if (!Directory(path).check && !Sessions.is_session_dir(path)) {
- error("Bad component directory: " + path)
- }
+ if (add) Directory(path).check
val lines1 = read_components()
val lines2 =
@@ -218,27 +226,21 @@
path.file_name match {
case Archive(_) => path
case name =>
- if (!path.is_dir) error("Bad component directory: " + path)
- else if (!Directory(path).check) {
- error("Malformed component directory: " + path +
- "\n (requires etc/settings or etc/components)")
- }
- else {
- val component_path = path.expand
- val archive_dir = component_path.dir
- val archive_name = Archive(name)
+ Directory(path).check
+ val component_path = path.expand
+ val archive_dir = component_path.dir
+ val archive_name = Archive(name)
- val archive = archive_dir + Path.explode(archive_name)
- if (archive.is_file && !force) {
- error("Component archive already exists: " + archive)
- }
+ val archive = archive_dir + Path.explode(archive_name)
+ if (archive.is_file && !force) {
+ error("Component archive already exists: " + archive)
+ }
- progress.echo("Packaging " + archive_name)
- Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
- dir = archive_dir).check
+ progress.echo("Packaging " + archive_name)
+ Isabelle_System.gnutar("-czf " + File.bash_path(archive) + " " + Bash.string(name),
+ dir = archive_dir).check
- archive
- }
+ archive
}
}
@@ -271,8 +273,8 @@
// contrib directory
val is_standard_component =
Isabelle_System.with_tmp_dir("component") { tmp_dir =>
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- Directory(tmp_dir + Path.explode(name)).check
+ Isabelle_System.extract(archive, tmp_dir)
+ Directory(tmp_dir + Path.explode(name)).ok
}
if (is_standard_component) {
if (ssh.is_dir(remote_contrib)) {
--- a/src/Pure/System/isabelle_system.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/System/isabelle_system.scala Tue Dec 06 08:43:43 2022 +0100
@@ -8,12 +8,15 @@
import java.util.{Map => JMap, HashMap}
+import java.util.zip.ZipFile
import java.io.{File => JFile, IOException}
import java.net.ServerSocket
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult,
StandardCopyOption, FileSystemException}
import java.nio.file.attribute.BasicFileAttributes
+import scala.jdk.CollectionConverters._
+
object Isabelle_System {
/* settings environment */
@@ -421,18 +424,57 @@
args: String,
dir: Path = Path.current,
original_owner: Boolean = false,
- strip: Int = 0,
+ strip: Boolean = false,
redirect: Boolean = false
): Process_Result = {
val options =
(if (dir.is_current) "" else "-C " + File.bash_path(dir) + " ") +
(if (original_owner) "" else "--owner=root --group=staff ") +
- (if (strip <= 0) "" else "--strip-components=" + strip + " ")
+ (if (!strip) "" else "--strip-components=1 ")
if (gnutar_check) bash("tar " + options + args, redirect = redirect)
else error("Expected to find GNU tar executable")
}
+ def extract(archive: Path, dir: Path, strip: Boolean = false): Unit = {
+ val name = archive.file_name
+ make_directory(dir)
+ if (File.is_zip(name) || File.is_jar(name)) {
+ using(new ZipFile(archive.file)) { zip_file =>
+ val items =
+ for (entry <- zip_file.entries().asScala.toList)
+ yield {
+ val input = JPath.of(entry.getName)
+ val count = input.getNameCount
+ val output =
+ if (strip && count <= 1) None
+ else if (strip) Some(input.subpath(1, count))
+ else Some(input)
+ val result = output.map(dir.java_path.resolve(_))
+ for (res <- result) {
+ if (entry.isDirectory) Files.createDirectories(res)
+ else {
+ val bytes = using(zip_file.getInputStream(entry))(Bytes.read_stream(_))
+ Files.createDirectories(res.getParent)
+ Files.write(res, bytes.array)
+ }
+ }
+ (entry, result)
+ }
+ for {
+ (entry, Some(res)) <- items
+ if !entry.isDirectory
+ t <- Option(entry.getLastModifiedTime)
+ } Files.setLastModifiedTime(res, t)
+ }
+ }
+ else if (File.is_tar_bz2(name) || File.is_tgz(name) || File.is_tar_gz(name)) {
+ val flags = if (File.is_tar_bz2(name)) "-xjf " else "-xzf "
+ Isabelle_System.gnutar(flags + File.bash_path(archive), dir = dir, strip = strip).check
+ }
+ else error("Cannot extract " + archive)
+ }
+
def make_patch(base_dir: Path, src: Path, dst: Path, diff_options: String = ""): String = {
with_tmp_file("patch") { patch =>
Isabelle_System.bash(
--- a/src/Pure/System/isabelle_tool.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/System/isabelle_tool.scala Tue Dec 06 08:43:43 2022 +0100
@@ -164,7 +164,6 @@
Build_EPTCS.isabelle_tool,
Build_Foiltex.isabelle_tool,
Build_Fonts.isabelle_tool,
- Build_JCEF.isabelle_tool,
Build_JDK.isabelle_tool,
Build_JEdit.isabelle_tool,
Build_LIPIcs.isabelle_tool,
--- a/src/Pure/System/scala.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/System/scala.scala Tue Dec 06 08:43:43 2022 +0100
@@ -184,7 +184,8 @@
def compile(source: String, state: repl.State = init_state): Result = {
out.flush()
out_stream.reset()
- val state1 = driver.run(source)(state)
+ given repl.State = state
+ val state1 = driver.run(source)
out.flush()
val messages = Message.split(out_stream.toString(UTF8.charset))
out_stream.reset()
--- a/src/Pure/Thy/sessions.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Dec 06 08:43:43 2022 +0100
@@ -1075,7 +1075,10 @@
def check_session_dir(dir: Path): Path =
if (is_session_dir(dir)) File.pwd() + dir.expand
- else error("Bad session root directory (missing ROOT or ROOTS): " + dir.expand.toString)
+ else {
+ error("Bad session root directory: " + dir.expand.toString +
+ "\n (missing \"ROOT\" or \"ROOTS\")")
+ }
def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] = {
val default_dirs = Components.directories().filter(is_session_dir)
--- a/src/Pure/Tools/build_docker.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Tools/build_docker.scala Tue Dec 06 08:43:43 2022 +0100
@@ -15,7 +15,7 @@
private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux(?:_arm)?\.tar\.gz$""".r
val packages: List[String] =
- List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen", "rsync", "unzip")
+ List("curl", "less", "libfontconfig1", "libgomp1", "openssh-client", "pwgen", "rsync")
val package_collections: Map[String, List[String]] =
Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
--- a/src/Pure/Tools/dotnet_setup.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Tools/dotnet_setup.scala Tue Dec 06 08:43:43 2022 +0100
@@ -83,8 +83,7 @@
progress.echo("Component " + component_dir)
Isabelle_System.make_directory(component_dir.etc)
- File.write(component_dir.settings, """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_DOTNET_ROOT="$COMPONENT"
if [ -n "$ISABELLE_WINDOWS_PLATFORM64" -a -d "$ISABELLE_DOTNET_ROOT/$ISABELLE_WINDOWS_PLATFORM64" ]; then
--- a/src/Pure/Tools/jedit.ML Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Tools/jedit.ML Tue Dec 06 08:43:43 2022 +0100
@@ -30,29 +30,17 @@
| parse_dockables _ = [];
-(* XML resources *)
-
-val xml_file = XML.parse o File.read;
+(* actions *)
-fun xml_resource name =
- let
- val res =
- Isabelle_System.bash_process (Bash.script ("unzip -p \"$JEDIT_JAR\" " ^ Bash.string name));
- val rc = Process_Result.rc res;
- in
- res |> Process_Result.check |> Process_Result.out |> XML.parse
- handle ERROR _ => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc)
- end;
-
-
-(* actions *)
+fun parse_resources [actions, dockables] =
+ parse_actions (XML.parse actions) @ parse_dockables (XML.parse dockables);
val lazy_actions =
Lazy.lazy (fn () =>
- (parse_actions (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>) @
- parse_dockables (xml_file \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>) @
- parse_actions (xml_resource "org/gjt/sp/jedit/actions.xml") @
- parse_dockables (xml_resource "org/gjt/sp/jedit/dockables.xml"))
+ (parse_resources o map File.read)
+ [\<^file>\<open>~~/src/Tools/jEdit/jedit_main/actions.xml\<close>,
+ \<^file>\<open>~~/src/Tools/jEdit/jedit_main/dockables.xml\<close>] @
+ (parse_resources o \<^scala>\<open>jEdit.resources\<close>) ["actions.xml", "dockables.xml"]
|> sort_strings);
fun get_actions () = Lazy.force lazy_actions;
--- a/src/Pure/Tools/mkroot.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Tools/mkroot.scala Tue Dec 06 08:43:43 2022 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/mkroot.scala
Author: Makarius
-Prepare session root directory.
+Create session root directory.
*/
package isabelle
@@ -24,6 +24,7 @@
init_repos: Boolean = false,
title: String = "",
author: String = "",
+ quiet: Boolean = false,
progress: Progress = new Progress
): Unit = {
Isabelle_System.make_directory(session_dir)
@@ -40,12 +41,14 @@
val root_tex = session_dir + Path.explode("document/root.tex")
- progress.echo("\nPreparing session " + quote(name) + " in " + session_dir)
+ progress.echo(
+ (if (quiet) "" else "\n") +
+ "Initializing session " + quote(name) + " in " + session_dir.absolute)
/* ROOT */
- progress.echo(" creating " + root_path)
+ progress.echo_if(!quiet, " creating " + root_path)
File.write(root_path,
"session " + root_name(name) + " = " + root_name(parent) + """ +
@@ -64,7 +67,7 @@
/* document directory */
{
- progress.echo(" creating " + root_tex)
+ progress.echo_if(!quiet, " creating " + root_tex)
Isabelle_System.make_directory(root_tex.dir)
@@ -136,7 +139,9 @@
/* Mercurial repository */
if (init_repos) {
- progress.echo(" \nInitializing Mercurial repository " + session_dir)
+ progress.echo(
+ (if (quiet) "" else "\n") +
+ "Initializing Mercurial repository " + session_dir.absolute)
val hg = Mercurial.init_repository(session_dir)
@@ -164,7 +169,7 @@
{
val print_dir = session_dir.implode
- progress.echo("""
+ progress.echo_if(!quiet, """
Now use the following command line to build the session:
isabelle build -D """ +
@@ -176,13 +181,14 @@
/** Isabelle tool wrapper **/
- val isabelle_tool = Isabelle_Tool("mkroot", "prepare session root directory",
+ val isabelle_tool = Isabelle_Tool("mkroot", "create session root directory",
Scala_Project.here,
{ args =>
var author = ""
var init_repos = false
var title = ""
var session_name = ""
+ var quiet = false
val getopts = Getopts("""
Usage: isabelle mkroot [OPTIONS] [DIRECTORY]
@@ -192,13 +198,15 @@
-I init Mercurial repository and add generated files
-T LATEX provide title in LaTeX notation (default: session name)
-n NAME alternative session name (default: directory base name)
+ -q quiet mode: less verbosity
- Prepare session root directory (default: current directory).
+ Create session root directory (default: current directory).
""",
"A:" -> (arg => author = arg),
- "I" -> (arg => init_repos = true),
+ "I" -> (_ => init_repos = true),
"T:" -> (arg => title = arg),
- "n:" -> (arg => session_name = arg))
+ "n:" -> (arg => session_name = arg),
+ "q" -> (_ => quiet = true))
val more_args = getopts(args)
@@ -209,7 +217,9 @@
case _ => getopts.usage()
}
+ val progress = new Console_Progress
+
mkroot(session_name = session_name, session_dir = session_dir, init_repos = init_repos,
- author = author, title = title, progress = new Console_Progress)
+ author = author, title = title, quiet = quiet, progress = progress)
})
}
--- a/src/Pure/Tools/phabricator.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Pure/Tools/phabricator.scala Tue Dec 06 08:43:43 2022 +0100
@@ -204,8 +204,8 @@
}
else Path.explode(mercurial_source)
- Isabelle_System.gnutar("-xzf " + File.bash_path(archive), dir = tmp_dir).check
- val build_dir = tmp_dir + Path.basic(File.get_dir(tmp_dir))
+ Isabelle_System.extract(archive, tmp_dir)
+ val build_dir = File.get_dir(tmp_dir, title = mercurial_source)
progress.bash("make all && make install", cwd = build_dir.file, echo = true).check
}
--- a/src/Tools/VSCode/src/build_vscode_extension.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala Tue Dec 06 08:43:43 2022 +0100
@@ -151,7 +151,7 @@
val component_name = "vscode_extension-" + Date.Format.alt_date(Date.now())
val component_dir =
- Components.Directory.create(target_dir + Path.basic(component_name), progress = progress)
+ Components.Directory(target_dir + Path.basic(component_name)).create(progress = progress)
/* build */
@@ -190,9 +190,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_VSCODE_VSIX="$COMPONENT/""" + vsix_name + "\"\n")
--- a/src/Tools/VSCode/src/build_vscodium.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Tools/VSCode/src/build_vscodium.scala Tue Dec 06 08:43:43 2022 +0100
@@ -66,22 +66,14 @@
def is_linux: Boolean = platform == Platform.Family.linux
def download_name: String = "VSCodium-" + download_template.replace("{VERSION}", version)
- def download_zip: Boolean = File.is_zip(download_name)
def download(dir: Path, progress: Progress = new Progress): Unit = {
- if (download_zip) Isabelle_System.require_command("unzip", test = "-h")
-
Isabelle_System.with_tmp_file("download") { download_file =>
Isabelle_System.download_file(vscodium_download + "/" + version + "/" + download_name,
download_file, progress = progress)
progress.echo("Extract ...")
- if (download_zip) {
- Isabelle_System.bash("unzip -x " + File.bash_path(download_file), cwd = dir.file).check
- }
- else {
- Isabelle_System.gnutar("-xzf " + File.bash_path(download_file), dir = dir).check
- }
+ Isabelle_System.extract(download_file, dir)
}
}
@@ -277,10 +269,6 @@
if (platforms.contains(Platform.Family.windows)) {
Isabelle_System.require_command("wine")
}
-
- if (platforms.exists(platform => the_platform_info(platform).download_zip)) {
- Isabelle_System.require_command("unzip", test = "-h")
- }
}
@@ -327,7 +315,7 @@
val component_name = "vscodium-" + version
val component_dir =
- Components.Directory.create(target_dir + Path.explode(component_name), progress = progress)
+ Components.Directory(target_dir + Path.explode(component_name)).create(progress = progress)
/* patches */
@@ -384,9 +372,7 @@
/* settings */
- File.write(component_dir.settings,
- """# -*- shell-script -*- :mode=shellscript:
-
+ component_dir.write_settings("""
ISABELLE_VSCODIUM_HOME="$COMPONENT/${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}"
if [ "$ISABELLE_PLATFORM_FAMILY" = "macos" ]; then
--- a/src/Tools/jEdit/src/document_dockable.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Tue Dec 06 08:43:43 2022 +0100
@@ -34,20 +34,19 @@
private val syslog = PIDE.session.make_syslog()
- private def update(text: String = syslog.content()): Unit = GUI_Thread.require { show(text) }
+ private def update(text: String = syslog.content()): Unit = show(text)
private val delay =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
- override def theory(theory: Progress.Theory): Unit = echo(theory.message)
- def load(): Unit = {
+ def load(): Unit = GUI_Thread.require {
val path = document_output().log
val text = if (path.is_file) File.read(path) else ""
GUI_Thread.later { delay.revoke(); update(text) }
}
- update()
+ GUI_Thread.later { update() }
}
@@ -157,6 +156,9 @@
val progress = init_progress()
val process =
Future.thread[Unit](name = "document_build") {
+ show_page(theories_page)
+ Time.seconds(2.0).sleep()
+
show_page(log_page)
val res =
Exn.capture {
@@ -175,7 +177,9 @@
val result = Document_Dockable.Result(output = List(msg))
current_state.change(_ => Document_Dockable.State.finish(result))
show_state()
- show_page(output_page)
+
+ show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
+ GUI_Thread.later { progress.load() }
}
st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
}
@@ -228,6 +232,13 @@
/* message pane with pages */
+ private val theories = new Theories_Status(view)
+
+ private val theories_page =
+ new TabbedPane.Page("Theories", new BorderPanel {
+ layout(theories.gui) = BorderPanel.Position.Center
+ }, "Selection and status of document theories")
+
private val output_controls =
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
@@ -237,22 +248,12 @@
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}, "Output from build process")
- private val load_button =
- new GUI.Button("Load") {
- tooltip = "Load final log file"
- override def clicked(): Unit = current_state.value.progress.load()
- }
-
- private val log_controls =
- Wrap_Panel(List(load_button))
-
private val log_page =
new TabbedPane.Page("Log", new BorderPanel {
- layout(log_controls) = BorderPanel.Position.North
layout(scroll_log_area) = BorderPanel.Position.Center
}, "Raw log of build process")
- message_pane.pages ++= List(log_page, output_page)
+ message_pane.pages ++= List(theories_page, log_page, output_page)
set_content(message_pane)
@@ -260,19 +261,29 @@
/* main */
private val main =
- Session.Consumer[Session.Global_Options](getClass.getName) {
+ Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
- GUI_Thread.later { handle_resize() }
+ GUI_Thread.later {
+ handle_resize()
+ theories.reinit()
+ }
+ case changed: Session.Commands_Changed =>
+ GUI_Thread.later {
+ theories.update(domain = Some(changed.nodes), trim = changed.assignment)
+ }
}
override def init(): Unit = {
init_state()
PIDE.session.global_options += main
+ PIDE.session.commands_changed += main
+ theories.update()
handle_resize()
}
override def exit(): Unit = {
PIDE.session.global_options -= main
+ PIDE.session.commands_changed -= main
delay_resize.revoke()
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_jar.scala Tue Dec 06 08:43:43 2022 +0100
@@ -0,0 +1,28 @@
+/* Title: Tools/jEdit/src/jedit_jar.scala
+ Author: Makarius
+
+Offline access to jEdit jar resources.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+object JEdit_JAR {
+ /* jEdit jar resources */
+
+ def get_resource(name: String): String = {
+ val s = classOf[org.gjt.sp.jedit.jEdit].getResourceAsStream(name)
+ if (s == null) error("Bad jEdit resource: " + quote(name))
+ else using(s)(File.read_stream)
+ }
+
+ object JEdit_Resources extends Scala.Fun_Strings("jEdit.resources") {
+ val here = Scala_Project.here
+ def apply(args: List[String]): List[String] = args.map(get_resource)
+ }
+
+ class Scala_Functions extends Scala.Functions(JEdit_Resources)
+}
--- a/src/Tools/jEdit/src/theories_dockable.scala Thu Nov 24 10:02:26 2022 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Dec 06 08:43:43 2022 +0100
@@ -9,68 +9,15 @@
import isabelle._
-import scala.swing.{Button, TextArea, Label, ListView, Alignment,
- ScrollPane, Component, CheckBox, BorderPanel, BoxPanel, Orientation}
-import scala.swing.event.{MouseClicked, MouseMoved}
+import scala.swing.{Button, TextArea, Label, ListView, ScrollPane, Component}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
-import javax.swing.{JList, BorderFactory, UIManager}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}
class Theories_Dockable(view: View, position: String) extends Dockable(view, position) {
- /* status */
-
- private val status = new ListView(List.empty[Document.Node.Name]) {
- background = {
- // enforce default value
- val c = UIManager.getDefaults.getColor("Panel.background")
- new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
- }
- listenTo(mouse.clicks)
- listenTo(mouse.moves)
- reactions += {
- case MouseClicked(_, point, _, clicks, _) =>
- val index = peer.locationToIndex(point)
- if (index >= 0) {
- val index_location = peer.indexToLocation(index)
- val a = in_required(index_location, point)
- val b = in_required(index_location, point, document = true)
- if (a || b) {
- if (clicks == 1) {
- Document_Model.node_required(listData(index), toggle = true, document = b)
- }
- }
- else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
- }
- case MouseMoved(_, point, _) =>
- val index = peer.locationToIndex(point)
- val index_location = peer.indexToLocation(index)
- if (index >= 0 && in_required(index_location, point)) {
- tooltip = "Mark as required for continuous checking"
- }
- else if (index >= 0 && in_required(index_location, point, document = true)) {
- tooltip = "Mark as required for continuous checking, with inclusion in document"
- }
- else if (index >= 0 && in_label(index_location, point)) {
- val name = listData(index)
- val st = nodes_status.overall_node_status(name)
- tooltip =
- "theory " + quote(name.theory) +
- (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
- }
- else tooltip = null
- }
- }
- status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
- status.peer.setVisibleRowCount(0)
- status.selection.intervalMode = ListView.IntervalMode.Single
-
- set_content(new ScrollPane(status))
-
-
/* controls */
def phase_text(phase: Session.Phase): String = "Prover: " + phase.print
@@ -79,8 +26,7 @@
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Status of prover session"
- private def handle_phase(phase: Session.Phase): Unit = {
- GUI_Thread.require {}
+ private def handle_phase(phase: Session.Phase): Unit = GUI_Thread.require {
session_phase.text = " " + phase_text(phase) + " "
}
@@ -100,171 +46,10 @@
add(controls.peer, BorderLayout.NORTH)
- /* component state -- owned by GUI thread */
-
- private var nodes_status = Document_Status.Nodes_Status.empty
- private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
- private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
-
- private class Geometry {
- private var location: Point = null
- private var size: Dimension = null
-
- def in(location0: Point, p: Point): Boolean =
- location != null && size != null && location0 != null && p != null && {
- val x = location0.x + location.x
- val y = location0.y + location.y
- x <= p.x && p.x < x + size.width &&
- y <= p.y && p.y < y + size.height
- }
-
- def update(new_location: Point, new_size: Dimension): Unit = {
- if (new_location != null && new_size != null) {
- location = new_location
- size = new_size
- }
- }
- }
-
- private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean =
- Node_Renderer_Component != null && {
- val required =
- if (document) Node_Renderer_Component.document_required
- else Node_Renderer_Component.theory_required
- required.geometry.in(location0, p)
- }
-
- private def in_label(location0: Point, p: Point): Boolean =
- Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
-
- private class Required extends CheckBox {
- val geometry = new Geometry
- opaque = false
- override def paintComponent(gfx: Graphics2D): Unit = {
- super.paintComponent(gfx)
- geometry.update(location, size)
- }
- }
-
- private object Node_Renderer_Component extends BorderPanel {
- opaque = true
- border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
-
- var node_name: Document.Node.Name = Document.Node.Name.empty
-
- val theory_required = new Required
- val document_required = new Required
-
- val label_geometry = new Geometry
- val label: Label = new Label {
- background = view.getTextArea.getPainter.getBackground
- foreground = view.getTextArea.getPainter.getForeground
- opaque = false
- xAlignment = Alignment.Leading
-
- override def paintComponent(gfx: Graphics2D): Unit = {
- def paint_segment(x: Int, w: Int, color: Color): Unit = {
- gfx.setColor(color)
- gfx.fillRect(x, 0, w, size.height)
- }
-
- paint_segment(0, size.width, background)
- nodes_status.get(node_name) match {
- case Some(node_status) =>
- val segments =
- List(
- (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
- (node_status.running, PIDE.options.color_value("running_color")),
- (node_status.warned, PIDE.options.color_value("warning_color")),
- (node_status.failed, PIDE.options.color_value("error_color"))
- ).filter(_._1 > 0)
+ /* main */
- segments.foldLeft(size.width - 2) {
- case (last, (n, color)) =>
- val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
- paint_segment(last - w, w, color)
- last - w - 1
- }
-
- case None =>
- paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
- }
- super.paintComponent(gfx)
-
- label_geometry.update(location, size)
- }
- }
-
- def label_border(name: Document.Node.Name): Unit = {
- val st = nodes_status.overall_node_status(name)
- val color =
- st match {
- case Document_Status.Overall_Node_Status.ok =>
- PIDE.options.color_value("ok_color")
- case Document_Status.Overall_Node_Status.failed =>
- PIDE.options.color_value("failed_color")
- case _ => label.foreground
- }
- val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
- val thickness2 = 4 - thickness1
-
- label.border =
- BorderFactory.createCompoundBorder(
- BorderFactory.createLineBorder(color, thickness1),
- BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
- }
-
- val required = new BoxPanel(Orientation.Horizontal)
- required.contents += theory_required
- // FIXME required.contents += document_required
-
- layout(required) = BorderPanel.Position.West
- layout(label) = BorderPanel.Position.Center
- }
-
- private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
- def componentFor(
- list: ListView[_ <: isabelle.Document.Node.Name],
- isSelected: Boolean,
- focused: Boolean,
- name: Document.Node.Name,
- index: Int
- ): Component = {
- val component = Node_Renderer_Component
- component.node_name = name
- component.theory_required.selected = theory_required.contains(name)
- component.document_required.selected = document_required.contains(name)
- component.label_border(name)
- component.label.text = name.theory_base_name
- component
- }
- }
- status.renderer = new Node_Renderer
-
- private def handle_update(
- domain: Option[Set[Document.Node.Name]] = None,
- trim: Boolean = false
- ): Unit = {
- GUI_Thread.require {}
-
- val snapshot = PIDE.session.snapshot()
-
- val (nodes_status_changed, nodes_status1) =
- nodes_status.update(
- PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
-
- nodes_status = nodes_status1
- if (nodes_status_changed) {
- status.listData =
- (for {
- (name, node_status) <- nodes_status1.present.iterator
- if !node_status.is_suppressed && node_status.total > 0
- } yield name).toList
- }
- }
-
-
- /* main */
+ val status = new Theories_Status(view)
+ set_content(new ScrollPane(status.gui))
private val main =
Session.Consumer[Any](getClass.getName) {
@@ -274,14 +59,12 @@
case _: Session.Global_Options =>
GUI_Thread.later {
continuous_checking.load()
- logic.load ()
- theory_required = Document_Model.required_nodes(false)
- document_required = Document_Model.required_nodes(true)
- status.repaint()
+ logic.load()
+ status.reinit()
}
case changed: Session.Commands_Changed =>
- GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
+ GUI_Thread.later { status.update(domain = Some(changed.nodes), trim = changed.assignment) }
}
override def init(): Unit = {
@@ -290,7 +73,7 @@
PIDE.session.commands_changed += main
handle_phase(PIDE.session.phase)
- handle_update()
+ status.update()
}
override def exit(): Unit = {
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Dec 06 08:43:43 2022 +0100
@@ -0,0 +1,249 @@
+/* Title: Tools/jEdit/src/theories_status.scala
+ Author: Makarius
+
+GUI panel for status of theories.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import scala.swing.{ListView, Alignment, Label, CheckBox, BorderPanel, BoxPanel, Orientation,
+ Component}
+import scala.swing.event.{MouseClicked, MouseMoved}
+
+import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
+import javax.swing.border.{BevelBorder, SoftBevelBorder}
+import javax.swing.{JList, BorderFactory, UIManager}
+
+import org.gjt.sp.jedit.View
+
+
+class Theories_Status(view: View) {
+ /* component state -- owned by GUI thread */
+
+ private var nodes_status = Document_Status.Nodes_Status.empty
+ private var theory_required: Set[Document.Node.Name] = Document_Model.required_nodes(false)
+ private var document_required: Set[Document.Node.Name] = Document_Model.required_nodes(true)
+
+
+ /* node renderer */
+
+ private class Geometry {
+ private var location: Point = null
+ private var size: Dimension = null
+
+ def in(location0: Point, p: Point): Boolean =
+ location != null && size != null && location0 != null && p != null && {
+ val x = location0.x + location.x
+ val y = location0.y + location.y
+ x <= p.x && p.x < x + size.width &&
+ y <= p.y && p.y < y + size.height
+ }
+
+ def update(new_location: Point, new_size: Dimension): Unit = {
+ if (new_location != null && new_size != null) {
+ location = new_location
+ size = new_size
+ }
+ }
+ }
+
+ private class Required extends CheckBox {
+ val geometry = new Geometry
+ opaque = false
+ override def paintComponent(gfx: Graphics2D): Unit = {
+ super.paintComponent(gfx)
+ geometry.update(location, size)
+ }
+ }
+
+ private object Node_Renderer_Component extends BorderPanel {
+ opaque = true
+ border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
+
+ var node_name: Document.Node.Name = Document.Node.Name.empty
+
+ val theory_required = new Required
+ val document_required = new Required
+
+ val label_geometry = new Geometry
+ val label: Label = new Label {
+ background = view.getTextArea.getPainter.getBackground
+ foreground = view.getTextArea.getPainter.getForeground
+ opaque = false
+ xAlignment = Alignment.Leading
+
+ override def paintComponent(gfx: Graphics2D): Unit = {
+ def paint_segment(x: Int, w: Int, color: Color): Unit = {
+ gfx.setColor(color)
+ gfx.fillRect(x, 0, w, size.height)
+ }
+
+ paint_segment(0, size.width, background)
+ nodes_status.get(node_name) match {
+ case Some(node_status) =>
+ val segments =
+ List(
+ (node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+ (node_status.running, PIDE.options.color_value("running_color")),
+ (node_status.warned, PIDE.options.color_value("warning_color")),
+ (node_status.failed, PIDE.options.color_value("error_color"))
+ ).filter(_._1 > 0)
+
+ segments.foldLeft(size.width - 2) {
+ case (last, (n, color)) =>
+ val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
+ paint_segment(last - w, w, color)
+ last - w - 1
+ }
+
+ case None =>
+ paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
+ }
+ super.paintComponent(gfx)
+
+ label_geometry.update(location, size)
+ }
+ }
+
+ def label_border(name: Document.Node.Name): Unit = {
+ val st = nodes_status.overall_node_status(name)
+ val color =
+ st match {
+ case Document_Status.Overall_Node_Status.ok =>
+ PIDE.options.color_value("ok_color")
+ case Document_Status.Overall_Node_Status.failed =>
+ PIDE.options.color_value("failed_color")
+ case _ => label.foreground
+ }
+ val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+ val thickness2 = 4 - thickness1
+
+ label.border =
+ BorderFactory.createCompoundBorder(
+ BorderFactory.createLineBorder(color, thickness1),
+ BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
+ }
+
+ val required = new BoxPanel(Orientation.Horizontal)
+ required.contents += theory_required
+ // FIXME required.contents += document_required
+
+ layout(required) = BorderPanel.Position.West
+ layout(label) = BorderPanel.Position.Center
+ }
+
+ private def in_required(location0: Point, p: Point, document: Boolean = false): Boolean =
+ Node_Renderer_Component != null && {
+ val required =
+ if (document) Node_Renderer_Component.document_required
+ else Node_Renderer_Component.theory_required
+ required.geometry.in(location0, p)
+ }
+
+ private def in_label(location0: Point, p: Point): Boolean =
+ Node_Renderer_Component != null && Node_Renderer_Component.label_geometry.in(location0, p)
+
+ private class Node_Renderer extends ListView.Renderer[Document.Node.Name] {
+ def componentFor(
+ list: ListView[_ <: isabelle.Document.Node.Name],
+ isSelected: Boolean,
+ focused: Boolean,
+ name: Document.Node.Name,
+ index: Int
+ ): Component = {
+ val component = Node_Renderer_Component
+ component.node_name = name
+ component.theory_required.selected = theory_required.contains(name)
+ component.document_required.selected = document_required.contains(name)
+ component.label_border(name)
+ component.label.text = name.theory_base_name
+ component
+ }
+ }
+
+
+ /* GUI component */
+
+ val gui: ListView[Document.Node.Name] = new ListView[Document.Node.Name](Nil) {
+ background = {
+ // enforce default value
+ val c = UIManager.getDefaults.getColor("Panel.background")
+ new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
+ }
+ listenTo(mouse.clicks)
+ listenTo(mouse.moves)
+ reactions += {
+ case MouseClicked(_, point, _, clicks, _) =>
+ val index = peer.locationToIndex(point)
+ if (index >= 0) {
+ val index_location = peer.indexToLocation(index)
+ val a = in_required(index_location, point)
+ val b = in_required(index_location, point, document = true)
+ if (a || b) {
+ if (clicks == 1) {
+ Document_Model.node_required(listData(index), toggle = true, document = b)
+ }
+ }
+ else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
+ }
+ case MouseMoved(_, point, _) =>
+ val index = peer.locationToIndex(point)
+ val index_location = peer.indexToLocation(index)
+ if (index >= 0 && in_required(index_location, point)) {
+ tooltip = "Mark as required for continuous checking"
+ }
+ else if (index >= 0 && in_required(index_location, point, document = true)) {
+ tooltip = "Mark as required for continuous checking, with inclusion in document"
+ }
+ else if (index >= 0 && in_label(index_location, point)) {
+ val name = listData(index)
+ val st = nodes_status.overall_node_status(name)
+ tooltip =
+ "theory " + quote(name.theory) +
+ (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
+ }
+ else tooltip = null
+ }
+ }
+
+ gui.renderer = new Node_Renderer
+ gui.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
+ gui.peer.setVisibleRowCount(0)
+ gui.selection.intervalMode = ListView.IntervalMode.Single
+
+
+ /* update */
+
+ def update(domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit = {
+ GUI_Thread.require {}
+
+ val snapshot = PIDE.session.snapshot()
+
+ val (nodes_status_changed, nodes_status1) =
+ nodes_status.update(
+ PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
+
+ nodes_status = nodes_status1
+ if (nodes_status_changed) {
+ gui.listData =
+ (for {
+ (name, node_status) <- nodes_status1.present.iterator
+ if !node_status.is_suppressed && node_status.total > 0
+ } yield name).toList
+ }
+ }
+
+
+ /* reinit */
+
+ def reinit(): Unit = {
+ GUI_Thread.require {}
+
+ theory_required = Document_Model.required_nodes(false)
+ document_required = Document_Model.required_nodes(true)
+ gui.repaint()
+ }
+}