# HG changeset patch # User desharna # Date 1649678477 -7200 # Node ID 6b38054241b84fa9e012d5deed14030d021d5ab1 # Parent 9c2a0b67eb68d5c1f7e2b3b4278b61354330c005# Parent 320f413fe4b9917a9204c0832bad665af3ae4a35 merged diff -r 9c2a0b67eb68 -r 6b38054241b8 etc/settings --- a/etc/settings Sat Apr 09 08:53:15 2022 +0200 +++ b/etc/settings Mon Apr 11 14:01:17 2022 +0200 @@ -17,7 +17,7 @@ ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" ISABELLE_JAVAC_OPTIONS="-encoding UTF-8 -Xlint:-options -deprecation -source 11 -target 11" -ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -Wconf:cat=other-match-analysis:silent -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m" +ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -feature -deprecation -target:11 -Xsource:3 -J-Xms512m -J-Xmx4g -J-Xss16m" ISABELLE_SCALA_JAR="$ISABELLE_HOME/lib/classes/isabelle.jar" diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Doc/Isar_Ref/HOL_Specific.thy --- a/src/Doc/Isar_Ref/HOL_Specific.thy Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Doc/Isar_Ref/HOL_Specific.thy Mon Apr 11 14:01:17 2022 +0200 @@ -2282,7 +2282,10 @@ @{command_def (HOL) "code_identifier"} & : & \theory \ theory\ \\ @{command_def (HOL) "code_monad"} & : & \theory \ theory\ \\ @{command_def (HOL) "code_reflect"} & : & \theory \ theory\ \\ - @{command_def (HOL) "code_pred"} & : & \theory \ proof(prove)\ + @{command_def (HOL) "code_pred"} & : & \theory \ proof(prove)\ \\ + @{attribute_def (HOL) code_timing} & : & \attribute\ \\ + @{attribute_def (HOL) code_simp_trace} & : & \attribute\ \\ + @{attribute_def (HOL) code_runtime_trace} & : & \attribute\ \end{matharray} \<^rail>\ @@ -2436,9 +2439,8 @@ Variants \code drop:\ and \code abort:\ take a list of constants as arguments and drop all code equations declared for them. In the case of \abort\, - these constants then do not require to a specification by means of - code equations; if needed these are implemented by program abort (exception) - instead. + these constants if needed are implemented by program abort + (exception). Packages declaring code equations usually provide a reasonable default setup. @@ -2502,6 +2504,15 @@ a set of introduction rules. Optional mode annotations determine which arguments are supposed to be input or output. If alternative introduction rules are declared, one must prove a corresponding elimination rule. + + \<^descr> @{attribute (HOL) "code_timing"} scrapes timing samples from different + stages of the code generator. + + \<^descr> @{attribute (HOL) "code_simp_trace"} traces the simplifier when it is + used with code equations. + + \<^descr> @{attribute (HOL) "code_runtime_trace"} traces ML code generated + dynamically for execution. \ end diff -r 9c2a0b67eb68 -r 6b38054241b8 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Sat Apr 09 08:53:15 2022 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Mon Apr 11 14:01:17 2022 +0200 @@ -171,8 +171,9 @@ val e_config : atp_config = {exec = (["E_HOME"], ["eprover-ho", "eprover"]), arguments = fn _ => fn _ => fn extra_options => fn timeout => fn problem => - ["--tstp-in --tstp-out --silent " ^ extra_options ^ " --cpu-limit=" ^ - string_of_int (to_secs 2 timeout) ^ " --proof-object=1 " ^ File.bash_path problem], + ["--tstp-in --tstp-out --silent " ^ extra_options ^ + " --demod-under-lambda=true --cpu-limit=" ^ string_of_int (to_secs 2 timeout) ^ + " --proof-object=1 " ^ File.bash_path problem], proof_delims = [("# SZS output start CNFRefutation", "# SZS output end CNFRefutation")] @ tstp_proof_delims, diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Admin/build_scala.scala --- a/src/Pure/Admin/build_scala.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Admin/build_scala.scala Mon Apr 11 14:01:17 2022 +0200 @@ -43,22 +43,22 @@ } val main_download: Download = - Download("scala", "3.0.2", base_version = "", + Download("scala", "3.1.1", 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", + Download("scala-parser-combinators", "2.1.1", "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", + Download("scala-xml", "2.1.0", "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") + physical_url = "https://repo1.maven.org/maven2/org/scala-lang/modules/scala-xml_{B}/{V}/scala-xml_{B}-{V}.jar") ) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/General/antiquote.scala Mon Apr 11 14:01:17 2022 +0200 @@ -44,7 +44,8 @@ /* read */ def read(input: CharSequence): List[Antiquote] = { - Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match { + val result = Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) + (result : @unchecked) match { case Parsers.Success(xs, _) => xs case Parsers.NoSuccess(_, next) => error("Malformed quotation/antiquotation source" + diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/General/json.scala --- a/src/Pure/General/json.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/General/json.scala Mon Apr 11 14:01:17 2022 +0200 @@ -145,7 +145,8 @@ def parse(input: CharSequence, strict: Boolean): T = { val scanner = new Lexer.Scanner(Scan.char_reader(input)) - phrase(if (strict) json_object | json_array else json_value)(scanner) match { + val result = phrase(if (strict) json_object | json_array else json_value)(scanner) + (result : @unchecked) match { case Success(json, _) => json case NoSuccess(_, next) => error("Malformed JSON input at " + next.pos) } diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Isar/token.scala Mon Apr 11 14:01:17 2022 +0200 @@ -140,7 +140,8 @@ val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { - Parsers.parse(Parsers.token_line(keywords, ctxt), in) match { + val result = Parsers.parse(Parsers.token_line(keywords, ctxt), in) + (result : @unchecked) match { case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/ML/ml_lex.scala Mon Apr 11 14:01:17 2022 +0200 @@ -281,7 +281,8 @@ val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { - Parsers.parse(Parsers.token_line(SML, ctxt), in) match { + val result = Parsers.parse(Parsers.token_line(SML, ctxt), in) + (result : @unchecked) match { case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/PIDE/rendering.scala Mon Apr 11 14:01:17 2022 +0200 @@ -563,7 +563,6 @@ case (res, Text.Info(_, elem)) => Command.State.get_result_proper(command_states, elem.markup.properties) .map(res :+ _) - case _ => None }) var seen_serials = Set.empty[Long] diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/System/isabelle_system.scala Mon Apr 11 14:01:17 2022 +0200 @@ -149,13 +149,13 @@ } private def apply_paths1(args: List[String], fun: Path => Unit): List[String] = - apply_paths(args, { case List(path) => fun(path) }) + apply_paths(args, { case List(path) => fun(path) case _ => ??? }) private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] = - apply_paths(args, { case List(path1, path2) => fun(path1, path2) }) + apply_paths(args, { case List(path1, path2) => fun(path1, path2) case _ => ??? }) private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] = - apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) }) + apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) case _ => ??? }) /* permissions */ @@ -481,7 +481,7 @@ object Download extends Scala.Fun("download", thread = true) { val here = Scala_Project.here override def invoke(args: List[Bytes]): List[Bytes] = - args match { case List(url) => List(download(url.text).bytes) } + args match { case List(url) => List(download(url.text).bytes) case _ => ??? } } diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/System/scala.scala diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/System/scala_compiler.ML diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Thy/bibtex.scala --- a/src/Pure/Thy/bibtex.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Thy/bibtex.scala Mon Apr 11 14:01:17 2022 +0200 @@ -599,7 +599,8 @@ val chunks = new mutable.ListBuffer[Chunk] var ctxt = context while (!in.atEnd) { - Parsers.parse(Parsers.chunk_line(ctxt), in) match { + val result = Parsers.parse(Parsers.chunk_line(ctxt), in) + (result : @unchecked) match { case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest case Parsers.NoSuccess(_, rest) => error("Unepected failure to parse input:\n" + rest.source.toString) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Thy/export_theory.scala Mon Apr 11 14:01:17 2022 +0200 @@ -264,12 +264,13 @@ def decode_syntax: XML.Decode.T[Syntax] = XML.Decode.variant(List( - { case (Nil, Nil) => No_Syntax }, - { case (List(delim), Nil) => Prefix(delim) }, + { case (Nil, Nil) => No_Syntax case _ => ??? }, + { case (List(delim), Nil) => Prefix(delim) case _ => ??? }, { case (Nil, body) => import XML.Decode._ val (ass, delim, pri) = triple(int, string, int)(body) - Infix(Assoc(ass), delim, pri) })) + Infix(Assoc(ass), delim, pri) + case _ => ??? })) /* types */ @@ -684,11 +685,11 @@ val decode_recursion: XML.Decode.T[Recursion] = { import XML.Decode._ variant(List( - { case (Nil, a) => Primrec(list(string)(a)) }, - { case (Nil, Nil) => Recdef }, - { case (Nil, a) => Primcorec(list(string)(a)) }, - { case (Nil, Nil) => Corec }, - { case (Nil, Nil) => Unknown_Recursion })) + { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? }, + { case (Nil, Nil) => Recdef case _ => ??? }, + { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? }, + { case (Nil, Nil) => Corec case _ => ??? }, + { case (Nil, Nil) => Unknown_Recursion case _ => ??? })) } @@ -713,10 +714,10 @@ val decode_rough_classification: XML.Decode.T[Rough_Classification] = { import XML.Decode._ variant(List( - { case (Nil, a) => Equational(decode_recursion(a)) }, - { case (Nil, Nil) => Inductive }, - { case (Nil, Nil) => Co_Inductive }, - { case (Nil, Nil) => Unknown })) + { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? }, + { case (Nil, Nil) => Inductive case _ => ??? }, + { case (Nil, Nil) => Co_Inductive case _ => ??? }, + { case (Nil, Nil) => Unknown case _ => ??? })) } diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Mon Apr 11 14:01:17 2022 +0200 @@ -463,7 +463,11 @@ val result = { val theory_timing = - theory_timings.iterator.map({ case props @ Markup.Name(name) => name -> props }).toMap + theory_timings.iterator.map( + { + case props @ Markup.Name(name) => name -> props + case _ => ??? + }).toMap val used_theory_timings = for { (name, _) <- deps(session_name).used_theories } yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Tools/scala_project.scala --- a/src/Pure/Tools/scala_project.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Tools/scala_project.scala Mon Apr 11 14:01:17 2022 +0200 @@ -11,8 +11,8 @@ object Scala_Project { /** build tools **/ - def java_version: String = "15" - def scala_version: String = scala.util.Properties.versionNumberString + val java_version: String = "17" + val scala_version: String = "2.13.5" abstract class Build_Tool { def project_root: Path diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/Tools/server.scala Mon Apr 11 14:01:17 2022 +0200 @@ -348,11 +348,7 @@ } } } - catch { - case _: IOException => false - case _: SocketException => false - case _: SocketTimeoutException => false - } + catch { case _: IOException => false } } diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Pure/term_xml.scala --- a/src/Pure/term_xml.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Pure/term_xml.scala Mon Apr 11 14:01:17 2022 +0200 @@ -48,20 +48,20 @@ def typ: T[Typ] = variant[Typ](List( - { case (List(a), b) => Type(a, list(typ)(b)) }, - { case (List(a), b) => TFree(a, sort(b)) }, + { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? }, + { case (List(a), b) => TFree(a, sort(b)) case _ => ??? }, { case (a, b) => TVar(indexname(a), sort(b)) })) val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) } def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) }, - { case (List(a), b) => Free(a, typ_body(b)) }, + { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, + { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) + { case (Nil, a) => Bound(int(a)) case _ => ??? }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) def term_env(env: Map[String, Typ]): T[Term] = { def env_type(x: String, t: Typ): Typ = @@ -69,12 +69,12 @@ def term: T[Term] = variant[Term](List( - { case (List(a), b) => Const(a, list(typ)(b)) }, - { case (List(a), b) => Free(a, env_type(a, typ_body(b))) }, + { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? }, + { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? }, { case (a, b) => Var(indexname(a), typ_body(b)) }, - { case (Nil, a) => Bound(int(a)) }, - { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) }, - { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) })) + { case (Nil, a) => Bound(int(a)) case _ => ??? }, + { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? }, + { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? })) term } @@ -82,17 +82,17 @@ val term = term_env(env) def proof: T[Proof] = variant[Proof](List( - { case (Nil, Nil) => MinProof }, - { case (Nil, a) => PBound(int(a)) }, - { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) }, - { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) }, - { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) }, - { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) }, - { case (Nil, a) => Hyp(term(a)) }, - { case (List(a), b) => PAxm(a, list(typ)(b)) }, - { case (List(a), b) => PClass(typ(b), a) }, - { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) }, - { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) })) + { case (Nil, Nil) => MinProof case _ => ??? }, + { case (Nil, a) => PBound(int(a)) case _ => ??? }, + { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? }, + { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? }, + { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? }, + { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? }, + { case (Nil, a) => Hyp(term(a)) case _ => ??? }, + { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? }, + { case (List(a), b) => PClass(typ(b), a) case _ => ??? }, + { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? }, + { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? })) proof } diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/Graphview/layout.scala --- a/src/Tools/Graphview/layout.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/Graphview/layout.scala Mon Apr 11 14:01:17 2022 +0200 @@ -137,9 +137,10 @@ val levels1 = dummies_levels.foldLeft(levels)(_ + _) val graph1 = - (v1 :: dummies ::: List(v2)).sliding(2). + (v1 :: dummies ::: List(v2)).sliding(2).map(_.toList). foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) { case (g, List(a, b)) => g.add_edge(a, b) + case _ => ??? } (graph1, levels1) } @@ -235,7 +236,7 @@ } private def count_crossings(graph: Graph, levels: List[Level]): Int = - levels.iterator.sliding(2).map { + levels.iterator.sliding(2).map(_.toList).map { case List(top, bot) => top.iterator.zipWithIndex.map { case (outer_parent, outer_parent_index) => diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/Graphview/popups.scala --- a/src/Tools/Graphview/popups.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/Graphview/popups.scala Mon Apr 11 14:01:17 2022 +0200 @@ -30,25 +30,25 @@ new Menu(caption) { contents += new MenuItem(new Action("This") { - def apply = + def apply(): Unit = add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, false))) }) contents += new MenuItem(new Action("Family") { - def apply = + def apply(): Unit = add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, true))) }) contents += new MenuItem(new Action("Parents") { - def apply = + def apply(): Unit = add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, false, true))) }) contents += new MenuItem(new Action("Children") { - def apply = + def apply(): Unit = add_mutator(Mutator.make(graphview, Mutator.Node_List(nodes, reverse, true, false))) }) @@ -77,7 +77,7 @@ contents += new MenuItem( new Action(quote(to.toString)) { - def apply = + def apply(): Unit = add_mutator( Mutator.make(graphview, Mutator.Edge_Endpoints((from, to)))) }) @@ -96,7 +96,7 @@ contents += new MenuItem( new Action(quote(from.toString)) { - def apply = + def apply(): Unit = add_mutator( Mutator.make(graphview, Mutator.Edge_Endpoints((from, to)))) }) @@ -113,7 +113,7 @@ popup.add( new MenuItem( - new Action("Remove all filters") { def apply = graphview.model.Mutators(Nil) }).peer) + new Action("Remove all filters") { def apply(): Unit = graphview.model.Mutators(Nil) }).peer) popup.add(new JPopupMenu.Separator) if (mouse_node.isDefined) { @@ -138,7 +138,7 @@ } popup.add(new MenuItem(new Action("Fit to window") { - def apply = graph_panel.fit_to_window() }).peer + def apply(): Unit = graph_panel.fit_to_window() }).peer ) popup diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/Graphview/shapes.scala Mon Apr 11 14:01:17 2022 +0200 @@ -116,7 +116,7 @@ val dy = coords(2).y - coords(0).y val (dx2, dy2) = - coords.sliding(3).foldLeft((dx, dy)) { + coords.sliding(3).map(_.toList).foldLeft((dx, dy)) { case ((dx, dy), List(l, m, r)) => val dx2 = r.x - l.x val dy2 = r.y - l.y @@ -125,6 +125,7 @@ m.x - slack * dx2, m.y - slack * dy2, m.x, m.y) (dx2, dy2) + case _ => ??? } val l = ds.last diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Apr 11 14:01:17 2022 +0200 @@ -143,8 +143,6 @@ case (res, Text.Info(_, msg)) => Command.State.get_result_proper(command_states, msg.markup.properties).map(res + _) - - case _ => None }).filterNot(info => info.info.is_empty) def diagnostics_output(results: List[Text.Info[Command.Results]]): List[LSP.Diagnostic] = { diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Mon Apr 11 14:01:17 2022 +0200 @@ -353,7 +353,6 @@ snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ => { case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem)) - case _ => None }).map(_.info) gutter_message_content.get(pris.foldLeft(0)(_ max _)) diff -r 9c2a0b67eb68 -r 6b38054241b8 src/Tools/jEdit/src/text_structure.scala --- a/src/Tools/jEdit/src/text_structure.scala Sat Apr 09 08:53:15 2022 +0200 +++ b/src/Tools/jEdit/src/text_structure.scala Mon Apr 11 14:01:17 2022 +0200 @@ -107,7 +107,7 @@ def indent_indent(tok: Token): Int = if (keywords.is_command(tok, keyword_open)) indent_size - else if (keywords.is_command(tok, keyword_close)) - indent_size + else if (keywords.is_command(tok, keyword_close)) { - indent_size } else 0 def indent_offset(tok: Token): Int =