--- a/Admin/components/components.sha1 Fri Apr 01 11:30:28 2022 +0200
+++ b/Admin/components/components.sha1 Fri Apr 01 12:26:45 2022 +0200
@@ -398,6 +398,7 @@
201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz
a0622fe75c3482ba7dc3ce74d58583b648a1ff0d scala-2.13.4-1.tar.gz
ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz
+caedd48ae65db9d116a0e1712eec3a66fe95c712 scala-2.13.5-1.tar.gz
f51981baf34c020ad103b262f81796c37abcaa4a scala-2.13.5.tar.gz
0a7cab09dec357dab7819273f2542ff1c3ea0968 scala-2.13.6.tar.gz
1f8532dba290c6b2ef364632f3f92e71da93baba scala-2.13.7.tar.gz
--- a/Admin/components/main Fri Apr 01 11:30:28 2022 +0200
+++ b/Admin/components/main Fri Apr 01 12:26:45 2022 +0200
@@ -21,7 +21,7 @@
pdfjs-2.12.313
polyml-test-15c840d48c9a
postgresql-42.2.24
-scala-2.13.5
+scala-2.13.5-1
smbc-0.4.1
spass-3.8ds-2
sqlite-jdbc-3.36.0.3
--- a/CONTRIBUTORS Fri Apr 01 11:30:28 2022 +0200
+++ b/CONTRIBUTORS Fri Apr 01 12:26:45 2022 +0200
@@ -10,7 +10,7 @@
Various improvements to Isabelle/VSCode.
* March 2021: Florian Haftmann, TU München
- More ambitious minimazation of case expressions in generated code.
+ More ambitious minimization of case expressions in generated code.
Contributions to Isabelle2021-1
--- a/NEWS Fri Apr 01 11:30:28 2022 +0200
+++ b/NEWS Fri Apr 01 12:26:45 2022 +0200
@@ -95,7 +95,7 @@
* (Co)datatype package:
- Lemma map_ident_strong is now generated for all BNFs.
-* More ambitious minimazation of case expressions in generated code.
+* More ambitious minimization of case expressions in generated code.
*** System ***
--- a/etc/build.props Fri Apr 01 11:30:28 2022 +0200
+++ b/etc/build.props Fri Apr 01 12:26:45 2022 +0200
@@ -25,6 +25,7 @@
src/Pure/Admin/build_pdfjs.scala \
src/Pure/Admin/build_polyml.scala \
src/Pure/Admin/build_release.scala \
+ src/Pure/Admin/build_scala.scala \
src/Pure/Admin/build_spass.scala \
src/Pure/Admin/build_sqlite.scala \
src/Pure/Admin/build_status.scala \
--- a/lib/scripts/getsettings Fri Apr 01 11:30:28 2022 +0200
+++ b/lib/scripts/getsettings Fri Apr 01 12:26:45 2022 +0200
@@ -130,7 +130,7 @@
fi
if [ -e "$ISABELLE_SETUP_JAR" ]; then
- ISABELLE_SETUP_CLASSPATH="$(isabelle_java java -jar "$(platform_path "$ISABELLE_SETUP_JAR")" classpath)"
+ ISABELLE_SETUP_CLASSPATH="$(isabelle_jdk java -classpath "$(platform_path "$ISABELLE_SETUP_JAR")" isabelle.setup.Setup classpath)"
fi
set +o allexport
--- a/src/Doc/Sledgehammer/document/root.tex Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Apr 01 12:26:45 2022 +0200
@@ -1167,6 +1167,10 @@
Sledgehammer emits an error if the actual outcome differs from the expected outcome. This option is
useful for regression testing.
+The expected outcomes are not mutually exclusive. More specifically, \textit{some} is accepted
+whenever \textit{some\_preplayed} is accepted as the former has strictly fewer requirements
+than the later.
+
\nopagebreak
{\small See also \textit{timeout} (\S\ref{timeouts}).}
\end{enum}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Admin/build_scala.scala Fri Apr 01 12:26:45 2022 +0200
@@ -0,0 +1,166 @@
+/* Title: Pure/Admin/build_scala.scala
+ Author: Makarius
+
+Build Isabelle Scala component from official downloads.
+*/
+
+package isabelle
+
+
+object Build_Scala
+{
+ /* downloads */
+
+ sealed case class Download(
+ name: String,
+ version: String,
+ url: String,
+ physical_url: String = "",
+ base_version: String = "3")
+ {
+ def make_url(template: String): String =
+ template.replace("{V}", version).replace("{B}", base_version)
+
+ def proper_url: String = make_url(proper_string(physical_url).getOrElse(url))
+
+ def artifact: String =
+ Library.take_suffix[Char](_ != '/', proper_url.toList)._2.mkString
+
+ 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 "") +
+ ":\n " + make_url(url)
+ }
+
+ val main_download: Download =
+ Download("scala", "3.0.2", base_version = "",
+ url = "https://github.com/lampepfl/dotty/releases/download/{V}/scala3-{V}.tar.gz")
+
+ val lib_downloads: List[Download] = List(
+ Download("scala-parallel-collections", "1.0.4",
+ "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parallel-collections_{B}/{V}",
+ physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parallel-collections_{B}/{V}/scala-parallel-collections_{B}-{V}.jar"),
+ Download("scala-parser-combinators", "2.1.0",
+ "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-parser-combinators_{B}/{V}",
+ physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-parser-combinators_{B}/{V}/scala-parser-combinators_{B}-{V}.jar"),
+ Download("scala-swing", "3.0.0",
+ "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-swing_{B}/{V}",
+ physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-swing_{B}/{V}/scala-swing_{B}-{V}.jar"),
+ Download("scala-xml", "2.0.1",
+ "https://mvnrepository.com/artifact/org.scala-lang.modules/scala-xml_{B}/{V}",
+ physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_3/2.0.1/scala-xml_{B}-{V}.jar")
+ )
+
+
+ /* build Scala component */
+
+ def build_scala(
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress): Unit =
+ {
+ /* component */
+
+ val component_name = main_download.name + "-" + main_download.version
+ val component_dir = Isabelle_System.new_directory(target_dir + Path.basic(component_name))
+ progress.echo("Component " + component_dir)
+
+
+ /* download */
+
+ main_download.get_unpacked(component_dir, strip = 1, progress = progress)
+
+ val lib_dir = component_dir + Path.explode("lib")
+ lib_downloads.foreach(download =>
+ download.get(lib_dir + Path.basic(download.artifact), progress = progress))
+
+ File.write(component_dir + Path.basic("LICENSE"),
+ Url.read(Url("https://www.apache.org/licenses/LICENSE-2.0.txt")))
+
+
+ /* classpath */
+
+ val classpath: List[String] =
+ {
+ def no_function(name: String): String = "function " + name + "() {\n:\n}"
+ val script =
+ cat_lines(List(
+ no_function("stty"),
+ no_function("tput"),
+ "PROG_HOME=" + File.bash_path(component_dir),
+ File.read(component_dir + Path.explode("bin/common"))
+ .replace("scala_exit_status=127", "scala_exit_status=0"),
+ "compilerJavaClasspathArgs",
+ "echo \"$jvm_cp_args\""))
+
+ val main_classpath = Path.split(Isabelle_System.bash(script).check.out).map(_.file_name)
+ val lib_classpath = lib_downloads.map(_.artifact)
+
+ main_classpath ::: lib_classpath
+ }
+
+ val interfaces =
+ classpath.find(_.startsWith("scala3-interfaces"))
+ .getOrElse(error("Missing jar for scala3-interfaces"))
+
+
+ /* settings */
+
+ val etc_dir = Isabelle_System.make_directory(component_dir + Path.basic("etc"))
+ File.write(etc_dir + Path.basic("settings"),
+ """# -*- shell-script -*- :mode=shellscript:
+
+SCALA_HOME="$COMPONENT"
+SCALA_INTERFACES="$SCALA_HOME/lib/""" + interfaces + """"
+""" + terminate_lines(classpath.map(jar => "classpath \"$SCALA_HOME/lib/" + jar + "\"")))
+
+
+ /* README */
+
+ File.write(component_dir + Path.basic("README"),
+ "This distribution of Scala integrates the following parts:\n\n" +
+ (main_download :: lib_downloads).map(_.print).mkString("\n\n") + """
+
+
+ Makarius
+ """ + Date.Format.date(Date.now()) + "\n")
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("build_scala", "build Isabelle Scala component from official downloads",
+ Scala_Project.here, args =>
+ {
+ var target_dir = Path.current
+
+ val getopts = Getopts("""
+Usage: isabelle build_scala [OPTIONS]
+
+ Options are:
+ -D DIR target directory (default ".")
+
+ Build Isabelle Scala component from official downloads.
+""",
+ "D:" -> (arg => target_dir = Path.explode(arg)))
+
+ val more_args = getopts(args)
+ if (more_args.nonEmpty) getopts.usage()
+
+ val progress = new Console_Progress()
+
+ build_scala(target_dir = target_dir, progress = progress)
+ })
+}
--- a/src/Pure/Concurrent/delay.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Concurrent/delay.scala Fri Apr 01 12:26:45 2022 +0200
@@ -33,8 +33,7 @@
}
}
- def invoke(): Unit = synchronized
- {
+ def invoke(): Unit = synchronized {
val new_run =
running match {
case Some(request) => if (first) false else { request.cancel(); true }
@@ -44,16 +43,14 @@
running = Some(Event_Timer.request(Time.now() + delay)(run))
}
- def revoke(): Unit = synchronized
- {
+ def revoke(): Unit = synchronized {
running match {
case Some(request) => request.cancel(); running = None
case None =>
}
}
- def postpone(alt_delay: Time): Unit = synchronized
- {
+ def postpone(alt_delay: Time): Unit = synchronized {
running match {
case Some(request) =>
val alt_time = Time.now() + alt_delay
--- a/src/Pure/Concurrent/isabelle_thread.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Concurrent/isabelle_thread.scala Fri Apr 01 12:26:45 2022 +0200
@@ -148,22 +148,19 @@
// synchronized, with concurrent changes
private var interrupt_postponed: Boolean = false
- def clear_interrupt: Boolean = synchronized
- {
+ def clear_interrupt: Boolean = synchronized {
val was_interrupted = isInterrupted || interrupt_postponed
Exn.Interrupt.dispose()
interrupt_postponed = false
was_interrupted
}
- def raise_interrupt: Unit = synchronized
- {
+ def raise_interrupt: Unit = synchronized {
interrupt_postponed = false
super.interrupt()
}
- def postpone_interrupt: Unit = synchronized
- {
+ def postpone_interrupt: Unit = synchronized {
interrupt_postponed = true
Exn.Interrupt.dispose()
}
--- a/src/Pure/GUI/wrap_panel.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/GUI/wrap_panel.scala Fri Apr 01 12:26:45 2022 +0200
@@ -35,8 +35,7 @@
private def layout_size(target: Container, preferred: Boolean): Dimension =
{
- target.getTreeLock.synchronized
- {
+ target.getTreeLock.synchronized {
val target_width =
if (target.getSize.width == 0) Integer.MAX_VALUE
else target.getSize.width
--- a/src/Pure/General/bytes.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/General/bytes.scala Fri Apr 01 12:26:45 2022 +0200
@@ -75,10 +75,12 @@
val buf = new Array[Byte](8192)
var m = 0
- do {
+ var cont = true
+ while (cont) {
m = stream.read(buf, 0, buf.length min (limit - out.size))
if (m != -1) out.write(buf, 0, m)
- } while (m != -1 && limit > out.size)
+ cont = (m != -1 && limit > out.size)
+ }
new Bytes(out.toByteArray, 0, out.size)
}
--- a/src/Pure/General/sha1.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/General/sha1.scala Fri Apr 01 12:26:45 2022 +0200
@@ -40,10 +40,12 @@
{
val buf = new Array[Byte](65536)
var m = 0
- do {
+ var cont = true
+ while (cont) {
m = stream.read(buf, 0, buf.length)
if (m != -1) sha.update(buf, 0, m)
- } while (m != -1)
+ cont = (m != -1)
+ }
}))
def digest(path: Path): Digest = digest(path.file)
--- a/src/Pure/Isar/token.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Isar/token.scala Fri Apr 01 12:26:45 2022 +0200
@@ -89,8 +89,8 @@
(x => Token(Token.Kind.SYM_IDENT, x))
val keyword =
- literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) |||
- literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x))
+ literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x)) |||
+ literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x))
val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x))
@@ -102,8 +102,8 @@
val bad = one(_ => true) ^^ (x => Token(Token.Kind.ERROR, x))
space | (recover_delimited |
- (((ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident)))))) |||
- keyword) | bad))
+ ((keyword |||
+ (ident | (var_ | (type_ident | (type_var | (float | (nat_ | sym_ident))))))) | bad))
}
def token(keywords: Keyword.Keywords): Parser[Token] =
--- a/src/Pure/ML/ml_lex.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala Fri Apr 01 12:26:45 2022 +0200
@@ -249,7 +249,7 @@
(x => Token(Kind.ERROR, x))
space | (ml_control | (recover | (ml_antiq |
- (((word | (real | (int | (long_ident | (ident | type_var))))) ||| keyword) | bad))))
+ ((keyword ||| (word | (real | (int | (long_ident | (ident | type_var)))))) | bad))))
}
def token: Parser[Token] =
--- a/src/Pure/ML/ml_statistics.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/ML/ml_statistics.scala Fri Apr 01 12:26:45 2022 +0200
@@ -80,27 +80,23 @@
private var session: Session = null
private var monitoring: Future[Unit] = Future.value(())
- override def init(session: Session): Unit = synchronized
- {
+ override def init(session: Session): Unit = synchronized {
this.session = session
}
- override def exit(): Unit = synchronized
- {
+ override def exit(): Unit = synchronized {
session = null
monitoring.cancel()
}
- private def consume(props: Properties.T): Unit = synchronized
- {
+ private def consume(props: Properties.T): Unit = synchronized {
if (session != null) {
val props1 = (session.cache.props(props ::: Java_Statistics.jvm_statistics()))
session.runtime_statistics.post(Session.Runtime_Statistics(props1))
}
}
- private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized
- {
+ private def ml_statistics(msg: Prover.Protocol_Output): Boolean = synchronized {
msg.properties match {
case Markup.ML_Statistics(pid, stats_dir) =>
monitoring =
--- a/src/Pure/System/isabelle_tool.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/System/isabelle_tool.scala Fri Apr 01 12:26:45 2022 +0200
@@ -227,6 +227,7 @@
Build_PolyML.isabelle_tool2,
Build_SPASS.isabelle_tool,
Build_SQLite.isabelle_tool,
+ Build_Scala.isabelle_tool,
Build_Status.isabelle_tool,
Build_Vampire.isabelle_tool,
Build_VeriT.isabelle_tool,
--- a/src/Pure/System/scala.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/System/scala.scala Fri Apr 01 12:26:45 2022 +0200
@@ -202,15 +202,13 @@
override def init(session: Session): Unit =
synchronized { this.session = session }
- override def exit(): Unit = synchronized
- {
+ override def exit(): Unit = synchronized {
for ((id, future) <- futures) cancel(id, future)
futures = Map.empty
}
private def result(id: String, tag: Scala.Tag.Value, res: List[Bytes]): Unit =
- synchronized
- {
+ synchronized {
if (futures.isDefinedAt(id)) {
session.protocol_command_raw("Scala.result", Bytes(id) :: Bytes(tag.id.toString) :: res)
futures -= id
@@ -223,8 +221,7 @@
result(id, Scala.Tag.INTERRUPT, Nil)
}
- private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
- {
+ private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
msg.properties match {
case Markup.Invoke_Scala(name, id) =>
def body: Unit =
@@ -243,8 +240,7 @@
}
}
- private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
- {
+ private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
msg.properties match {
case Markup.Cancel_Scala(id) =>
futures.get(id) match {
--- a/src/Pure/Thy/presentation.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Thy/presentation.scala Fri Apr 01 12:26:45 2022 +0200
@@ -210,7 +210,7 @@
/* HTML output */
private val div_elements =
- Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name,
+ Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.`enum`.name,
HTML.descr.name)
def make_html(
@@ -261,7 +261,7 @@
(Nil, end_offset - XML.symbol_length(text))
case XML.Elem(Markup.Markdown_List(kind), body) =>
val (body1, offset) = html_body(body, end_offset)
- if (kind == Markup.ENUMERATE) (List(HTML.enum(body1)), offset)
+ if (kind == Markup.ENUMERATE) (List(HTML.`enum`(body1)), offset)
else (List(HTML.list(body1)), offset)
case XML.Elem(markup, body) =>
val name = markup.name
--- a/src/Pure/Thy/sessions.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Thy/sessions.scala Fri Apr 01 12:26:45 2022 +0200
@@ -1150,11 +1150,12 @@
val buf = ByteBuffer.allocate(n)
var i = 0
var m = 0
- do {
+ var cont = true
+ while (cont) {
m = file.read(buf)
if (m != -1) i += m
+ cont = (m != -1 && n > i)
}
- while (m != -1 && n > i)
if (i == n) {
val prefix = new String(buf.array(), 0, sha1_prefix.length, UTF8.charset)
--- a/src/Pure/Tools/phabricator.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/Tools/phabricator.scala Fri Apr 01 12:26:45 2022 +0200
@@ -951,12 +951,14 @@
val results = new mutable.ListBuffer[A]
var after = ""
- do {
+ var cont = true
+ while (cont) {
val result =
execute(method, params = params ++ JSON.optional("after" -> proper_string(after)))
results ++= result.get_value(JSON.list(_, "data", unapply))
after = result.get_value(JSON.value(_, "cursor", JSON.string0(_, "after")))
- } while (after.nonEmpty)
+ cont = after.nonEmpty
+ }
results.toList
}
--- a/src/Pure/library.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Pure/library.scala Fri Apr 01 12:26:45 2022 +0200
@@ -75,7 +75,12 @@
private def next_chunk(i: Int): Option[(CharSequence, Int)] =
{
if (i < end) {
- var j = i; do j += 1 while (j < end && !sep(source.charAt(j)))
+ var j = i
+ var cont = true
+ while (cont) {
+ j += 1
+ cont = (j < end && !sep(source.charAt(j)))
+ }
Some((source.subSequence(i + 1, j), j))
}
else None
--- a/src/Tools/jEdit/src/document_model.scala Fri Apr 01 11:30:28 2022 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Fri Apr 01 12:26:45 2022 +0200
@@ -606,8 +606,7 @@
else Nil
}
- def edit(edits: List[Text.Edit]): Unit = synchronized
- {
+ def edit(edits: List[Text.Edit]): Unit = synchronized {
GUI_Thread.require {}
reset_blob()