# HG changeset patch # User blanchet # Date 1648808805 -7200 # Node ID 38663b1de300c4eb826d9d1bd353d7039e5bbb23 # Parent 840256534f34b1cd03350249136bdfed7e74154a# Parent b3ca4a6ed74b3ba1dd776f89d7f9b386d789b229 merge diff -r 840256534f34 -r 38663b1de300 Admin/components/components.sha1 --- 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 diff -r 840256534f34 -r 38663b1de300 Admin/components/main --- 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 diff -r 840256534f34 -r 38663b1de300 CONTRIBUTORS --- 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 diff -r 840256534f34 -r 38663b1de300 NEWS --- 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 *** diff -r 840256534f34 -r 38663b1de300 etc/build.props --- 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 \ diff -r 840256534f34 -r 38663b1de300 lib/scripts/getsettings --- 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 diff -r 840256534f34 -r 38663b1de300 src/Doc/Sledgehammer/document/root.tex --- 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} diff -r 840256534f34 -r 38663b1de300 src/Pure/Admin/build_scala.scala --- /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) + }) +} diff -r 840256534f34 -r 38663b1de300 src/Pure/Concurrent/delay.scala --- 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 diff -r 840256534f34 -r 38663b1de300 src/Pure/Concurrent/isabelle_thread.scala --- 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() } diff -r 840256534f34 -r 38663b1de300 src/Pure/GUI/wrap_panel.scala --- 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 diff -r 840256534f34 -r 38663b1de300 src/Pure/General/bytes.scala --- 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) } diff -r 840256534f34 -r 38663b1de300 src/Pure/General/sha1.scala --- 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) diff -r 840256534f34 -r 38663b1de300 src/Pure/Isar/token.scala --- 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] = diff -r 840256534f34 -r 38663b1de300 src/Pure/ML/ml_lex.scala --- 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] = diff -r 840256534f34 -r 38663b1de300 src/Pure/ML/ml_statistics.scala --- 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 = diff -r 840256534f34 -r 38663b1de300 src/Pure/System/isabelle_tool.scala --- 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, diff -r 840256534f34 -r 38663b1de300 src/Pure/System/scala.scala --- 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 { diff -r 840256534f34 -r 38663b1de300 src/Pure/Thy/presentation.scala --- 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 diff -r 840256534f34 -r 38663b1de300 src/Pure/Thy/sessions.scala --- 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) diff -r 840256534f34 -r 38663b1de300 src/Pure/Tools/phabricator.scala --- 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 } diff -r 840256534f34 -r 38663b1de300 src/Pure/library.scala --- 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 diff -r 840256534f34 -r 38663b1de300 src/Tools/jEdit/src/document_model.scala --- 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()