--- 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"
--- 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"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def (HOL) "code_monad"} & : & \<open>theory \<rightarrow> theory\<close> \\
@{command_def (HOL) "code_reflect"} & : & \<open>theory \<rightarrow> theory\<close> \\
- @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close>
+ @{command_def (HOL) "code_pred"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
+ @{attribute_def (HOL) code_timing} & : & \<open>attribute\<close> \\
+ @{attribute_def (HOL) code_simp_trace} & : & \<open>attribute\<close> \\
+ @{attribute_def (HOL) code_runtime_trace} & : & \<open>attribute\<close>
\end{matharray}
\<^rail>\<open>
@@ -2436,9 +2439,8 @@
Variants \<open>code drop:\<close> and \<open>code abort:\<close> take a list of constants as arguments
and drop all code equations declared for them. In the case of \<open>abort\<close>,
- 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.
\<close>
end
--- 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,
--- 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")
)
--- 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" +
--- 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)
}
--- 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)
--- 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)
--- 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]
--- 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 _ => ??? }
}
--- 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)
--- 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 _ => ??? }))
}
--- 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))
--- 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
--- 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 }
}
--- 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
}
--- 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) =>
--- 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
--- 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
--- 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] = {
--- 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 _))
--- 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 =