--- a/Admin/components/components.sha1 Tue Nov 02 13:51:29 2021 +0100
+++ b/Admin/components/components.sha1 Wed Nov 03 10:44:54 2021 +0100
@@ -195,6 +195,7 @@
33dd96cd83f2c6a26c035b7a0ee57624655224c5 jedit-20210724.tar.gz
0e4fd4d66388ddc760fa5fbd8d4a9a3b77cf59c7 jedit-20210802.tar.gz
258d527819583d740a3aa52dfef630eed389f8c6 jedit-20211019.tar.gz
+f4f3fcbd54488297a5d2fcd23a2595912d5ba80b jedit-20211103.tar.gz
44775a22f42a9d665696bfb49e53c79371c394b0 jedit_build-20111217.tar.gz
a242a688810f2bccf24587b0062ce8027bf77fa2 jedit_build-20120304.tar.gz
4c948dee53f74361c097c08f49a1a5ff9b17bd1d jedit_build-20120307.tar.gz
@@ -385,6 +386,7 @@
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
+1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz
b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz
5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz
abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz
--- a/Admin/components/main Tue Nov 02 13:51:29 2021 +0100
+++ b/Admin/components/main Wed Nov 03 10:44:54 2021 +0100
@@ -10,7 +10,7 @@
isabelle_fonts-20211004
isabelle_setup-20210922
jdk-17.0.1+12
-jedit-20211019
+jedit-20211103
jfreechart-1.5.3
jortho-1.0-2
kodkodi-1.5.7
@@ -19,7 +19,7 @@
opam-2.0.7
polyml-5.9-960de0cd0795
postgresql-42.2.24
-scala-2.13.5
+scala-2.13.7
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
--- a/NEWS Tue Nov 02 13:51:29 2021 +0100
+++ b/NEWS Wed Nov 03 10:44:54 2021 +0100
@@ -532,7 +532,8 @@
- sources of for the jEdit text editor and the Isabelle/jEdit
plugins (jedit_base and jedit_main) are included by default,
- more sources may be given on the command-line,
- - options -f and -D make the tool more convenient.
+ - options -f and -D make the tool more convenient,
+ - Gradle has been replaced by Maven (less ambitious and more robust).
* Remote provers from SystemOnTPTP (notably for Sledgehammer) are now
managed via Isabelle/Scala instead of perl; the dependency on
--- a/src/Doc/Main/Main_Doc.thy Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Doc/Main/Main_Doc.thy Wed Nov 03 10:44:54 2021 +0100
@@ -35,12 +35,12 @@
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
\<^term>\<open>\<not> (x = y)\<close> & @{term[source]"\<not> (x = y)"} & (\<^verbatim>\<open>~=\<close>)\\
@{term[source]"P \<longleftrightarrow> Q"} & \<^term>\<open>P \<longleftrightarrow> Q\<close> \\
\<^term>\<open>If x y z\<close> & @{term[source]"If x y z"}\\
\<^term>\<open>Let e\<^sub>1 (\<lambda>x. e\<^sub>2)\<close> & @{term[source]"Let e\<^sub>1 (\<lambda>x. e\<^sub>2)"}\\
-\end{supertabular}
+\end{tabular}
\section*{Orderings}
@@ -49,7 +49,7 @@
preorder, partial order, linear order, dense linear order and wellorder.
\<^smallskip>
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
\<^const>\<open>Orderings.less_eq\<close> & \<^typeof>\<open>Orderings.less_eq\<close> & (\<^verbatim>\<open><=\<close>)\\
\<^const>\<open>Orderings.less\<close> & \<^typeof>\<open>Orderings.less\<close>\\
\<^const>\<open>Orderings.Least\<close> & \<^typeof>\<open>Orderings.Least\<close>\\
@@ -60,11 +60,11 @@
@{const[source] bot} & \<^typeof>\<open>Orderings.bot\<close>\\
\<^const>\<open>Orderings.mono\<close> & \<^typeof>\<open>Orderings.mono\<close>\\
\<^const>\<open>Orderings.strict_mono\<close> & \<^typeof>\<open>Orderings.strict_mono\<close>\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
@{term[source]"x \<ge> y"} & \<^term>\<open>x \<ge> y\<close> & (\<^verbatim>\<open>>=\<close>)\\
@{term[source]"x > y"} & \<^term>\<open>x > y\<close>\\
\<^term>\<open>\<forall>x\<le>y. P\<close> & @{term[source]"\<forall>x. x \<le> y \<longrightarrow> P"}\\
@@ -72,7 +72,7 @@
\multicolumn{2}{@ {}l@ {}}{Similarly for $<$, $\ge$ and $>$}\\
\<^term>\<open>LEAST x. P\<close> & @{term[source]"Least (\<lambda>x. P)"}\\
\<^term>\<open>GREATEST x. P\<close> & @{term[source]"Greatest (\<lambda>x. P)"}\\
-\end{supertabular}
+\end{tabular}
\section*{Lattices}
@@ -91,7 +91,7 @@
Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>.
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
@{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\
@{text[source]"x \<sqsubset> y"} & \<^term>\<open>x < y\<close>\\
@{text[source]"x \<sqinter> y"} & \<^term>\<open>inf x y\<close>\\
@@ -100,12 +100,12 @@
@{text[source]"\<Squnion>A"} & \<^term>\<open>Sup A\<close>\\
@{text[source]"\<top>"} & @{term[source] top}\\
@{text[source]"\<bottom>"} & @{term[source] bot}\\
-\end{supertabular}
+\end{tabular}
\section*{Set}
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
\<^const>\<open>Set.empty\<close> & @{term_type_only "Set.empty" "'a set"}\\
\<^const>\<open>Set.insert\<close> & @{term_type_only insert "'a\<Rightarrow>'a set\<Rightarrow>'a set"}\\
\<^const>\<open>Collect\<close> & @{term_type_only Collect "('a\<Rightarrow>bool)\<Rightarrow>'a set"}\\
@@ -119,11 +119,11 @@
\<^const>\<open>image\<close> & @{term_type_only image "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set"}\\
\<^const>\<open>Ball\<close> & @{term_type_only Ball "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
\<^const>\<open>Bex\<close> & @{term_type_only Bex "'a set\<Rightarrow>('a\<Rightarrow>bool)\<Rightarrow>bool"}\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
\<open>{a\<^sub>1,\<dots>,a\<^sub>n}\<close> & \<open>insert a\<^sub>1 (\<dots> (insert a\<^sub>n {})\<dots>)\<close>\\
\<^term>\<open>a \<notin> A\<close> & @{term[source]"\<not>(x \<in> A)"}\\
\<^term>\<open>A \<subseteq> B\<close> & @{term[source]"A \<le> B"}\\
@@ -139,12 +139,12 @@
\<^term>\<open>\<forall>x\<in>A. P\<close> & @{term[source]"Ball A (\<lambda>x. P)"}\\
\<^term>\<open>\<exists>x\<in>A. P\<close> & @{term[source]"Bex A (\<lambda>x. P)"}\\
\<^term>\<open>range f\<close> & @{term[source]"f ` UNIV"}\\
-\end{supertabular}
+\end{tabular}
\section*{Fun}
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
\<^const>\<open>Fun.id\<close> & \<^typeof>\<open>Fun.id\<close>\\
\<^const>\<open>Fun.comp\<close> & \<^typeof>\<open>Fun.comp\<close> & (\texttt{o})\\
\<^const>\<open>Fun.inj_on\<close> & @{term_type_only Fun.inj_on "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>bool"}\\
@@ -153,7 +153,7 @@
\<^const>\<open>Fun.bij\<close> & \<^typeof>\<open>Fun.bij\<close>\\
\<^const>\<open>Fun.bij_betw\<close> & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
\<^const>\<open>Fun.fun_upd\<close> & \<^typeof>\<open>Fun.fun_upd\<close>\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
@@ -206,7 +206,7 @@
Types \<^typ>\<open>unit\<close> and \<open>\<times>\<close>.
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Product_Type.Unity\<close> & \<^typeof>\<open>Product_Type.Unity\<close>\\
\<^const>\<open>Pair\<close> & \<^typeof>\<open>Pair\<close>\\
\<^const>\<open>fst\<close> & \<^typeof>\<open>fst\<close>\\
@@ -214,7 +214,7 @@
\<^const>\<open>case_prod\<close> & \<^typeof>\<open>case_prod\<close>\\
\<^const>\<open>curry\<close> & \<^typeof>\<open>curry\<close>\\
\<^const>\<open>Product_Type.Sigma\<close> & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
@@ -264,13 +264,13 @@
\section*{Equiv\_Relations}
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Equiv_Relations.equiv\<close> & @{term_type_only Equiv_Relations.equiv "'a set \<Rightarrow> ('a*'a)set\<Rightarrow>bool"}\\
\<^const>\<open>Equiv_Relations.quotient\<close> & @{term_type_only Equiv_Relations.quotient "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set set"}\\
\<^const>\<open>Equiv_Relations.congruent\<close> & @{term_type_only Equiv_Relations.congruent "('a*'a)set\<Rightarrow>('a\<Rightarrow>'b)\<Rightarrow>bool"}\\
\<^const>\<open>Equiv_Relations.congruent2\<close> & @{term_type_only Equiv_Relations.congruent2 "('a*'a)set\<Rightarrow>('b*'b)set\<Rightarrow>('a\<Rightarrow>'b\<Rightarrow>'c)\<Rightarrow>bool"}\\
%@ {const Equiv_Relations.} & @ {term_type_only Equiv_Relations. ""}\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
@@ -305,7 +305,7 @@
structures from semigroups up to fields. Everything is done in terms of
overloaded operators:
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
\<open>0\<close> & \<^typeof>\<open>zero\<close>\\
\<open>1\<close> & \<^typeof>\<open>one\<close>\\
\<^const>\<open>plus\<close> & \<^typeof>\<open>plus\<close>\\
@@ -319,7 +319,7 @@
\<^const>\<open>Rings.dvd\<close> & \<^typeof>\<open>Rings.dvd\<close>\\
\<^const>\<open>divide\<close> & \<^typeof>\<open>divide\<close>\\
\<^const>\<open>modulo\<close> & \<^typeof>\<open>modulo\<close>\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
@@ -394,53 +394,53 @@
\section*{Finite\_Set}
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Finite_Set.finite\<close> & @{term_type_only Finite_Set.finite "'a set\<Rightarrow>bool"}\\
\<^const>\<open>Finite_Set.card\<close> & @{term_type_only Finite_Set.card "'a set \<Rightarrow> nat"}\\
\<^const>\<open>Finite_Set.fold\<close> & @{term_type_only Finite_Set.fold "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'b \<Rightarrow> 'a set \<Rightarrow> 'b"}\\
-\end{supertabular}
+\end{tabular}
\section*{Lattices\_Big}
-\begin{supertabular}{@ {} l @ {~::~} l l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l l @ {}}
\<^const>\<open>Lattices_Big.Min\<close> & \<^typeof>\<open>Lattices_Big.Min\<close>\\
\<^const>\<open>Lattices_Big.Max\<close> & \<^typeof>\<open>Lattices_Big.Max\<close>\\
\<^const>\<open>Lattices_Big.arg_min\<close> & \<^typeof>\<open>Lattices_Big.arg_min\<close>\\
\<^const>\<open>Lattices_Big.is_arg_min\<close> & \<^typeof>\<open>Lattices_Big.is_arg_min\<close>\\
\<^const>\<open>Lattices_Big.arg_max\<close> & \<^typeof>\<open>Lattices_Big.arg_max\<close>\\
\<^const>\<open>Lattices_Big.is_arg_max\<close> & \<^typeof>\<open>Lattices_Big.is_arg_max\<close>\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
\<^term>\<open>ARG_MIN f x. P\<close> & @{term[source]"arg_min f (\<lambda>x. P)"}\\
\<^term>\<open>ARG_MAX f x. P\<close> & @{term[source]"arg_max f (\<lambda>x. P)"}\\
-\end{supertabular}
+\end{tabular}
\section*{Groups\_Big}
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Groups_Big.sum\<close> & @{term_type_only Groups_Big.sum "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_add"}\\
\<^const>\<open>Groups_Big.prod\<close> & @{term_type_only Groups_Big.prod "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'b::comm_monoid_mult"}\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l l @ {}}
\<^term>\<open>sum (\<lambda>x. x) A\<close> & @{term[source]"sum (\<lambda>x. x) A"} & (\<^verbatim>\<open>SUM\<close>)\\
\<^term>\<open>sum (\<lambda>x. t) A\<close> & @{term[source]"sum (\<lambda>x. t) A"}\\
@{term[source] "\<Sum>x|P. t"} & \<^term>\<open>\<Sum>x|P. t\<close>\\
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>} & (\<^verbatim>\<open>PROD\<close>)\\
-\end{supertabular}
+\end{tabular}
\section*{Wellfounded}
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Wellfounded.wf\<close> & @{term_type_only Wellfounded.wf "('a*'a)set\<Rightarrow>bool"}\\
\<^const>\<open>Wellfounded.acc\<close> & @{term_type_only Wellfounded.acc "('a*'a)set\<Rightarrow>'a set"}\\
\<^const>\<open>Wellfounded.measure\<close> & @{term_type_only Wellfounded.measure "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set"}\\
@@ -448,12 +448,12 @@
\<^const>\<open>Wellfounded.mlex_prod\<close> & @{term_type_only Wellfounded.mlex_prod "('a\<Rightarrow>nat)\<Rightarrow>('a*'a)set\<Rightarrow>('a*'a)set"}\\
\<^const>\<open>Wellfounded.less_than\<close> & @{term_type_only Wellfounded.less_than "(nat*nat)set"}\\
\<^const>\<open>Wellfounded.pred_nat\<close> & @{term_type_only Wellfounded.pred_nat "(nat*nat)set"}\\
-\end{supertabular}
+\end{tabular}
\section*{Set\_Interval} % \<^theory>\<open>HOL.Set_Interval\<close>
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>lessThan\<close> & @{term_type_only lessThan "'a::ord \<Rightarrow> 'a set"}\\
\<^const>\<open>atMost\<close> & @{term_type_only atMost "'a::ord \<Rightarrow> 'a set"}\\
\<^const>\<open>greaterThan\<close> & @{term_type_only greaterThan "'a::ord \<Rightarrow> 'a set"}\\
@@ -462,11 +462,11 @@
\<^const>\<open>atLeastLessThan\<close> & @{term_type_only atLeastLessThan "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
\<^const>\<open>greaterThanAtMost\<close> & @{term_type_only greaterThanAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
\<^const>\<open>atLeastAtMost\<close> & @{term_type_only atLeastAtMost "'a::ord \<Rightarrow> 'a \<Rightarrow> 'a set"}\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
\<^term>\<open>lessThan y\<close> & @{term[source] "lessThan y"}\\
\<^term>\<open>atMost y\<close> & @{term[source] "atMost y"}\\
\<^term>\<open>greaterThan x\<close> & @{term[source] "greaterThan x"}\\
@@ -483,7 +483,7 @@
\<^term>\<open>sum (\<lambda>x. t) {..b}\<close> & @{term[source] "sum (\<lambda>x. t) {..b}"}\\
\<^term>\<open>sum (\<lambda>x. t) {..<b}\<close> & @{term[source] "sum (\<lambda>x. t) {..<b}"}\\
\multicolumn{2}{@ {}l@ {}}{Similarly for \<open>\<Prod>\<close> instead of \<open>\<Sum>\<close>}\\
-\end{supertabular}
+\end{tabular}
\section*{Power}
@@ -564,13 +564,13 @@
\subsubsection*{Syntax}
-\begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
+\begin{tabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
\<open>[x\<^sub>1,\<dots>,x\<^sub>n]\<close> & \<open>x\<^sub>1 # \<dots> # x\<^sub>n # []\<close>\\
\<^term>\<open>[m..<n]\<close> & @{term[source]"upt m n"}\\
\<^term>\<open>[i..j]\<close> & @{term[source]"upto i j"}\\
\<^term>\<open>xs[n := x]\<close> & @{term[source]"list_update xs n x"}\\
\<^term>\<open>\<Sum>x\<leftarrow>xs. e\<close> & @{term[source]"listsum (map (\<lambda>x. e) xs)"}\\
-\end{supertabular}
+\end{tabular}
\<^medskip>
Filter input syntax \<open>[pat \<leftarrow> e. b]\<close>, where
@@ -585,7 +585,7 @@
Maps model partial functions and are often used as finite tables. However,
the domain of a map may be infinite.
-\begin{supertabular}{@ {} l @ {~::~} l @ {}}
+\begin{tabular}{@ {} l @ {~::~} l @ {}}
\<^const>\<open>Map.empty\<close> & \<^typeof>\<open>Map.empty\<close>\\
\<^const>\<open>Map.map_add\<close> & \<^typeof>\<open>Map.map_add\<close>\\
\<^const>\<open>Map.map_comp\<close> & \<^typeof>\<open>Map.map_comp\<close>\\
@@ -595,7 +595,7 @@
\<^const>\<open>Map.map_le\<close> & \<^typeof>\<open>Map.map_le\<close>\\
\<^const>\<open>Map.map_of\<close> & \<^typeof>\<open>Map.map_of\<close>\\
\<^const>\<open>Map.map_upds\<close> & \<^typeof>\<open>Map.map_upds\<close>\\
-\end{supertabular}
+\end{tabular}
\subsubsection*{Syntax}
--- a/src/Doc/System/Scala.thy Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Doc/System/Scala.thy Wed Nov 03 10:44:54 2021 +0100
@@ -278,11 +278,11 @@
-L make symlinks to original source files
-f force update of existing directory
- Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
+ Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
such as IntelliJ IDEA.\<close>}
- The generated configuration is for Gradle\<^footnote>\<open>\<^url>\<open>https://gradle.org\<close>\<close>, but the
- main purpose is to import it into common Scala IDEs, such as IntelliJ
+ The generated configuration is for Maven\<^footnote>\<open>\<^url>\<open>https://maven.apache.org\<close>\<close>, but
+ the main purpose is to import it into common IDEs, such as IntelliJ
IDEA\<^footnote>\<open>\<^url>\<open>https://www.jetbrains.com/idea\<close>\<close>. This allows to explore the
sources with static analysis and other hints in real-time.
@@ -292,12 +292,9 @@
\<^medskip>
Option \<^verbatim>\<open>-L\<close> produces \<^emph>\<open>symlinks\<close> to the original files: this allows to
- develop Isabelle/Scala/jEdit modules within an external IDE. Note that the
- result cannot be built within the IDE: it requires implicit or explicit
- \<^verbatim>\<open>isabelle scala_build\<close> (\secref{sec:tool-scala-build}) instead.
-
- The default is to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has
- no permanent effect on the originals.
+ develop Isabelle/Scala/jEdit modules within an external IDE. The default is
+ to \<^emph>\<open>copy\<close> source files, so editing them within the IDE has no permanent
+ effect on the originals.
\<^medskip>
Option \<^verbatim>\<open>-D\<close> specifies an explicit project directory, instead of the default
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala Wed Nov 03 10:44:54 2021 +0100
@@ -85,7 +85,7 @@
}
using(store.open_database_context())(db_context =>
{
- for (export <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
+ for (`export` <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
val prefix = args.name.split('/') match {
case Array("mirabelle", action, "finalize") =>
s"${action} finalize "
--- a/src/Pure/Admin/build_jedit.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/Admin/build_jedit.scala Wed Nov 03 10:44:54 2021 +0100
@@ -161,6 +161,7 @@
Isabelle_System.copy_dir(jedit_dir, jedit_patched_dir)
val source_dir = jedit_patched_dir + Path.basic("jEdit")
+ val org_source_dir = source_dir + Path.basic("org")
val tmp_source_dir = tmp_dir + Path.basic("jEdit")
progress.echo("Patching jEdit sources ...")
@@ -187,7 +188,7 @@
val java_sources =
for {
- file <- File.find_files(source_dir.file, file => file.getName.endsWith(".java"))
+ file <- File.find_files(org_source_dir.file, file => file.getName.endsWith(".java"))
package_name <- Scala_Project.package_name(File.path(file))
if !exclude_package(package_name)
} yield File.path(component_dir.java_path.relativize(file.toPath).toFile)
--- a/src/Pure/PIDE/session.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/PIDE/session.scala Wed Nov 03 10:44:54 2021 +0100
@@ -507,7 +507,7 @@
case Protocol.Export(args)
if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined =>
val id = Value.Long.unapply(args.id.get).get
- val export = Export.make_entry("", args, msg.chunk, cache)
+ val `export` = Export.make_entry("", args, msg.chunk, cache)
change_command(_.add_export(id, (args.serial, export)))
case Protocol.Loading_Theory(node_name, id) =>
--- a/src/Pure/Thy/export_theory.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/Thy/export_theory.scala Wed Nov 03 10:44:54 2021 +0100
@@ -183,7 +183,7 @@
val DOCUMENT_TEXT = "document_text"
val PROOF_TEXT = "proof_text"
- def export(kind: String): String =
+ def `export`(kind: String): String =
kind match {
case Markup.TYPE_NAME => TYPE
case Markup.CONSTANT => CONST
--- a/src/Pure/Thy/html.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/Thy/html.scala Wed Nov 03 10:44:54 2021 +0100
@@ -56,7 +56,7 @@
val code = new Operator("code")
val item = new Operator("li")
val list = new Operator("ul")
- val enum = new Operator("ol")
+ val `enum` = new Operator("ol")
val descr = new Operator("dl")
val dt = new Operator("dt")
val dd = new Operator("dd")
@@ -70,7 +70,7 @@
val subparagraph = new Heading("h6")
def itemize(items: List[XML.Body]): XML.Elem = list(items.map(item(_)))
- def enumerate(items: List[XML.Body]): XML.Elem = enum(items.map(item(_)))
+ def enumerate(items: List[XML.Body]): XML.Elem = `enum`(items.map(item(_)))
def description(items: List[(XML.Body, XML.Body)]): XML.Elem =
descr(items.flatMap({ case (x, y) => List(dt(x), dd(y)) }))
--- a/src/Pure/Tools/build_job.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Wed Nov 03 10:44:54 2021 +0100
@@ -325,7 +325,7 @@
case _ => false
}
- private def export(msg: Prover.Protocol_Output): Boolean =
+ private def `export`(msg: Prover.Protocol_Output): Boolean =
msg.properties match {
case Protocol.Export(args) =>
export_consumer(session_name, args, msg.chunk)
@@ -364,7 +364,7 @@
if (!progress.stopped) {
val rendering = new Rendering(snapshot, options, session)
- def export(name: String, xml: XML.Body, compress: Boolean = true): Unit =
+ def `export`(name: String, xml: XML.Body, compress: Boolean = true): Unit =
{
if (!progress.stopped) {
val theory_name = snapshot.node_name.theory
--- a/src/Pure/Tools/scala_project.scala Tue Nov 02 13:51:29 2021 +0100
+++ b/src/Pure/Tools/scala_project.scala Wed Nov 03 10:44:54 2021 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/Tools/scala_project.scala
Author: Makarius
-Manage Isabelle/Scala/Java project sources, with output to Gradle for
+Manage Isabelle/Scala/Java project sources, with output to Maven for
IntelliJ IDEA.
*/
@@ -10,15 +10,56 @@
object Scala_Project
{
- /* groovy syntax */
+ /* Maven project */
- def groovy_string(s: String): String =
+ def java_version: String = "11"
+ def scala_version: String = scala.util.Properties.versionNumberString
+
+ def maven_project(jars: List[Path]): String =
{
- s.map(c =>
- c match {
- case '\t' | '\b' | '\n' | '\r' | '\f' | '\\' | '\'' | '"' => "\\" + c
- case _ => c.toString
- }).mkString("'", "", "'")
+ def dependency(jar: Path): String =
+ {
+ val name = jar.expand.drop_ext.base.implode
+ val system_path = File.platform_path(jar.absolute)
+ """ <dependency>
+ <groupId>classpath</groupId>
+ <artifactId>""" + XML.text(name) + """</artifactId>
+ <version>0</version>
+ <scope>system</scope>
+ <systemPath>""" + XML.text(system_path) + """</systemPath>
+ </dependency>"""
+ }
+
+ """<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+ <modelVersion>4.0.0</modelVersion>
+
+ <groupId>isabelle</groupId>
+ <artifactId>isabelle</artifactId>
+ <version>0</version>
+
+ <properties>
+ <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
+ <maven.compiler.source>""" + java_version + """</maven.compiler.source>
+ <maven.compiler.target>""" + java_version + """</maven.compiler.target>
+ </properties>
+
+ <build>
+ <plugins>
+ <plugin>
+ <groupId>net.alchim31.maven</groupId>
+ <artifactId>scala-maven-plugin</artifactId>
+ <version>4.5.3</version>
+ <configuration>
+ <scalaVersion>""" + scala_version + """</scalaVersion>
+ </configuration>
+ </plugin>
+ </plugins>
+ </build>
+
+ <dependencies>""" + jars.map(dependency).mkString("\n", "\n", "\n") + """</dependencies>
+</project>"""
}
@@ -127,7 +168,7 @@
if (project_dir.file.exists) {
val detect =
project_dir.is_dir &&
- (project_dir + Path.explode("build.gradle")).is_file &&
+ (project_dir + Path.explode("pom.xml")).is_file &&
(project_dir + Path.explode("src/main/scala")).is_dir
if (force && detect) {
@@ -146,6 +187,8 @@
val (jars, sources) = isabelle_files
isabelle_scala_files
+ File.write(project_dir + Path.explode("pom.xml"), maven_project(jars))
+
for (source <- sources ::: more_sources) {
val dir = (if (source.is_java) java_src_dir else scala_src_dir) + the_package_dir(source)
val target_dir = project_dir + dir
@@ -156,31 +199,13 @@
if (symlinks) Isabelle_System.symlink(source.absolute, target_dir, native = true)
else Isabelle_System.copy_file(source, target_dir)
}
-
- File.write(project_dir + Path.explode("settings.gradle"), "rootProject.name = 'Isabelle'\n")
- File.write(project_dir + Path.explode("build.gradle"),
-"""plugins {
- id 'scala'
-}
-
-repositories {
- mavenCentral()
-}
-
-dependencies {
- implementation 'org.scala-lang:scala-library:""" + scala.util.Properties.versionNumberString + """'
- compileOnly files(
- """ + jars.map(jar => groovy_string(File.platform_path(jar))).mkString("", ",\n ", ")") +
-"""
-}
-""")
}
/* Isabelle tool wrapper */
val isabelle_tool =
- Isabelle_Tool("scala_project", "setup Gradle project for Isabelle/Scala/jEdit",
+ Isabelle_Tool("scala_project", "setup Maven project for Isabelle/Scala/jEdit",
Scala_Project.here, args =>
{
var project_dir = default_project_dir
@@ -195,7 +220,7 @@
-L make symlinks to original source files
-f force update of existing directory
- Setup Gradle project for Isabelle/Scala/jEdit --- to support Scala IDEs
+ Setup Maven project for Isabelle/Scala/jEdit --- to support common IDEs
such as IntelliJ IDEA.
""",
"D:" -> (arg => project_dir = Path.explode(arg)),