--- a/etc/settings Sat Apr 09 11:40:42 2022 +0200
+++ b/etc/settings Sat Apr 09 12:10: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/Pure/Admin/build_scala.scala Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Admin/build_scala.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/General/antiquote.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/General/json.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/Isar/token.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/ML/ml_lex.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/PIDE/rendering.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala Sat Apr 09 12:10: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/System/scala.scala Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/System/scala.scala Sat Apr 09 12:10:17 2022 +0200
@@ -112,15 +112,11 @@
}
}
- def toplevel(interpret: Boolean, source: String): List[String] = {
+ def toplevel(source: String): List[String] = {
val out = new StringWriter
val interp = interpreter(new PrintWriter(out))
val marker = '\u000b'
- val ok =
- interp.withLabel(marker.toString) {
- if (interpret) interp.interpret(source) == Results.Success
- else (new interp.ReadEvalPrint).compile(source)
- }
+ val ok = interp.withLabel(marker.toString) { (new interp.ReadEvalPrint).compile(source) }
out.close()
val Error = """(?s)^\S* error: (.*)$""".r
@@ -135,15 +131,9 @@
object Toplevel extends Fun_String("scala_toplevel") {
val here = Scala_Project.here
- def apply(arg: String): String = {
- val (interpret, source) =
- YXML.parse_body(arg) match {
- case Nil => (false, "")
- case List(XML.Text(source)) => (false, source)
- case body => import XML.Decode._; pair(bool, string)(body)
- }
+ def apply(source: String): String = {
val errors =
- try { Compiler.context().toplevel(interpret, source) }
+ try { Compiler.context().toplevel(source) }
catch { case ERROR(msg) => List(msg) }
locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
}
--- a/src/Pure/System/scala_compiler.ML Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/System/scala_compiler.ML Sat Apr 09 12:10:17 2022 +0200
@@ -6,7 +6,7 @@
signature SCALA_COMPILER =
sig
- val toplevel: bool -> string -> unit
+ val toplevel: string -> unit
val static_check: string * Position.T -> unit
end;
@@ -15,18 +15,15 @@
(* check declaration *)
-fun toplevel interpret source =
+fun toplevel source =
let val errors =
- (interpret, source)
- |> let open XML.Encode in pair bool string end
- |> YXML.string_of_body
- |> \<^scala>\<open>scala_toplevel\<close>
+ \<^scala>\<open>scala_toplevel\<close> source
|> YXML.parse_body
|> let open XML.Decode in list string end
in if null errors then () else error (cat_lines errors) end;
fun static_check (source, pos) =
- toplevel false ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
+ toplevel ("package test\nclass __Dummy__ { __dummy__ => " ^ source ^ " }")
handle ERROR msg => error (msg ^ Position.here pos);
--- a/src/Pure/Thy/bibtex.scala Sat Apr 09 11:40:42 2022 +0200
+++ b/src/Pure/Thy/bibtex.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/Tools/scala_project.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/Tools/server.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Pure/term_xml.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/layout.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/popups.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Sat Apr 09 12:10: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 11:40:42 2022 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala Sat Apr 09 12:10: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 =