--- a/src/Pure/General/linear_set.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/linear_set.scala Wed Jan 15 19:54:50 2020 +0100
@@ -117,7 +117,7 @@
override def stringPrefix = "Linear_Set"
- override def isEmpty: Boolean = !start.isDefined
+ override def isEmpty: Boolean = start.isEmpty
override def size: Int = if (isEmpty) 0 else nexts.size + 1
def contains(elem: A): Boolean =
--- a/src/Pure/General/mercurial.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/mercurial.scala Wed Jan 15 19:54:50 2020 +0100
@@ -200,7 +200,7 @@
val edited =
hgrc.is_file && {
val lines = split_lines(File.read(hgrc))
- lines.filter(header).length == 1 && {
+ lines.count(header) == 1 && {
if (local_hg.paths(options = "-q").contains(path_name)) {
val old_source = local_hg.paths(args = path_name).head
val old_entry = path_name + ".old = " + old_source
--- a/src/Pure/General/path.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/path.scala Wed Jan 15 19:54:50 2020 +0100
@@ -233,7 +233,7 @@
case x => List(x)
}
- new Path(Path.norm_elems(elems.map(eval).flatten))
+ new Path(Path.norm_elems(elems.flatMap(eval)))
}
def expand: Path = expand_env(Isabelle_System.settings())
--- a/src/Pure/General/scan.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/scan.scala Wed Jan 15 19:54:50 2020 +0100
@@ -412,7 +412,7 @@
val offset = in.offset
val len = source.length - offset
- def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
+ @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
{
if (i < len) {
tree.branches.get(source.charAt(offset + i)) match {
--- a/src/Pure/General/ssh.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/ssh.scala Wed Jan 15 19:54:50 2020 +0100
@@ -90,7 +90,7 @@
host_key_alias: String = "",
on_close: () => Unit = () => ()): Session =
{
- val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
+ val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
session.setUserInfo(No_User_Info)
session.setServerAliveInterval(alive_interval(options))
--- a/src/Pure/General/symbol.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/General/symbol.scala Wed Jan 15 19:54:50 2020 +0100
@@ -379,11 +379,10 @@
}
val groups: List[(String, List[Symbol])] =
- symbols.map({ case (sym, props) =>
+ symbols.flatMap({ case (sym, props) =>
val gs = for (("group", g) <- props) yield g
if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _)
- }).flatten
- .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
+ }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
.sortBy(_._1)
val abbrevs: Multi_Map[Symbol, String] =
@@ -444,7 +443,7 @@
recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
- val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
+ val font_index: Map[String, Int] = Map((font_names zip font_names.indices.toList): _*)
/* classification */
--- a/src/Pure/ML/ml_console.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/ML/ml_console.scala Wed Jan 15 19:54:50 2020 +0100
@@ -47,7 +47,7 @@
"r" -> (_ => raw_ml_system = true))
val more_args = getopts(args)
- if (!more_args.isEmpty) getopts.usage()
+ if (more_args.nonEmpty) getopts.usage()
// build logic
--- a/src/Pure/ML/ml_process.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/ML/ml_process.scala Wed Jan 15 19:54:50 2020 +0100
@@ -128,8 +128,8 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
- map(eval => List("--eval", eval)).flatten ::: args
+ (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
+ .flatMap(eval => List("--eval", eval)) ::: args
Bash.process(
"exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
@@ -180,7 +180,7 @@
"o:" -> (arg => options = options + arg))
val more_args = getopts(args)
- if (args.isEmpty || !more_args.isEmpty) getopts.usage()
+ if (args.isEmpty || more_args.nonEmpty) getopts.usage()
val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
result().print_stdout.rc
--- a/src/Pure/PIDE/markup_tree.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Wed Jan 15 19:54:50 2020 +0100
@@ -153,7 +153,7 @@
new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
else {
Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
- body.filter(e => !new_range.contains(e._1)).map(_._2).mkString("\n"))
+ body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
this
}
}
--- a/src/Pure/PIDE/prover.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/PIDE/prover.scala Wed Jan 15 19:54:50 2020 +0100
@@ -22,8 +22,8 @@
{
override def toString: String =
XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
- args.map(s =>
- List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
+ args.flatMap(s =>
+ List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
}
class Output(val message: XML.Elem) extends Message
@@ -224,12 +224,12 @@
//{{{
var c = -1
var done = false
- while (!done && (result.length == 0 || reader.ready)) {
+ while (!done && (result.isEmpty || reader.ready)) {
c = reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
- if (result.length > 0) {
+ if (result.nonEmpty) {
output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
result.clear
}
--- a/src/Pure/System/getopts.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/System/getopts.scala Wed Jan 15 19:54:50 2020 +0100
@@ -47,11 +47,11 @@
private def getopts(args: List[List[Char]]): List[List[Char]] =
args match {
case List('-', '-') :: rest_args => rest_args
- case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && !rest_opts.isEmpty =>
+ case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
case List('-', opt) :: rest_args if is_option0(opt) =>
option(opt, Nil); getopts(rest_args)
- case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && !opt_arg.isEmpty =>
+ case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
option(opt, opt_arg); getopts(rest_args)
case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
option(opt, opt_arg); getopts(rest_args)
--- a/src/Pure/System/isabelle_tool.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/System/isabelle_tool.scala Wed Jan 15 19:54:50 2020 +0100
@@ -82,7 +82,7 @@
}
private def find_external(name: String): Option[List[String] => Unit] =
- dirs.collectFirst({
+ dirs().collectFirst({
case dir if is_external(dir, name + ".scala") =>
compile(dir + Path.explode(name + ".scala"))
case dir if is_external(dir, name) =>
--- a/src/Pure/System/platform.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/System/platform.scala Wed Jan 15 19:54:50 2020 +0100
@@ -11,9 +11,9 @@
{
/* platform family */
- val is_linux = System.getProperty("os.name", "") == "Linux"
- val is_macos = System.getProperty("os.name", "") == "Mac OS X"
- val is_windows = System.getProperty("os.name", "").startsWith("Windows")
+ val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
+ val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
+ val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
def family: Family.Value =
if (is_linux) Family.linux
@@ -58,7 +58,7 @@
/* JVM version */
private val Version = """1\.(\d+)\.0_(\d+)""".r
- lazy val jvm_version =
+ lazy val jvm_version: String =
System.getProperty("java.version") match {
case Version(a, b) => a + "u" + b
case a => a
--- a/src/Pure/System/tty_loop.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/System/tty_loop.scala Wed Jan 15 19:54:50 2020 +0100
@@ -21,12 +21,12 @@
while (!finished) {
var c = -1
var done = false
- while (!done && (result.length == 0 || reader.ready)) {
+ while (!done && (result.isEmpty || reader.ready)) {
c = reader.read
if (c >= 0) result.append(c.asInstanceOf[Char])
else done = true
}
- if (result.length > 0) {
+ if (result.nonEmpty) {
System.out.print(result.toString)
System.out.flush()
result.clear
--- a/src/Pure/Tools/server.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/Tools/server.scala Wed Jan 15 19:54:50 2020 +0100
@@ -520,7 +520,7 @@
private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
- def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
+ def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
def remove_session(id: UUID.T): Headless.Session =
{
--- a/src/Pure/Tools/spell_checker.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala Wed Jan 15 19:54:50 2020 +0100
@@ -198,7 +198,7 @@
}
def reset_enabled(): Int =
- updates.valuesIterator.filter(upd => !upd.permanent).length
+ updates.valuesIterator.count(upd => !upd.permanent)
/* check known words */
--- a/src/Tools/Graphview/graph_panel.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/Graphview/graph_panel.scala Wed Jan 15 19:54:50 2020 +0100
@@ -148,7 +148,7 @@
(scale * font_height).floor / font_height
}
- def apply() =
+ def apply(): AffineTransform =
{
val box = graphview.bounding_box()
val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
--- a/src/Tools/Graphview/layout.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/Graphview/layout.scala Wed Jan 15 19:54:50 2020 +0100
@@ -232,8 +232,8 @@
case (outer_parent, outer_parent_index) =>
graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
(0 until outer_parent_index).iterator.map(inner_parent =>
- graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)).
- filter(inner_child => outer_child < inner_child).size).sum).sum
+ graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
+ .count(inner_child => outer_child < inner_child)).sum).sum
}.sum
case _ => 0
}.sum
@@ -289,7 +289,7 @@
def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
{
- ((graph, false) /: (0 until level.length)) {
+ ((graph, false) /: level.indices) {
case ((graph, moved), i) =>
val r = level(i)
val d = r.deflection(graph, top_down)
--- a/src/Tools/Graphview/metrics.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/Graphview/metrics.scala Wed Jan 15 19:54:50 2020 +0100
@@ -36,7 +36,7 @@
{
def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
private val mix = string_bounds("mix")
- val space_width = string_bounds(" ").getWidth
+ val space_width: Double = string_bounds(" ").getWidth
def char_width: Double = mix.getWidth / 3
def height: Double = mix.getHeight
def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
@@ -56,7 +56,7 @@
object Pretty_Metric extends Pretty.Metric
{
- val unit = space_width max 1.0
+ val unit: Double = space_width max 1.0
def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
}
}
--- a/src/Tools/Graphview/mutator_dialog.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala Wed Jan 15 19:54:50 2020 +0100
@@ -179,7 +179,7 @@
contents += enabledBox
contents += Swing.RigidBox(new Dimension(5, 0))
focusList = enabledBox.peer :: focusList
- inputs.map(_ match {
+ inputs.map({
case (n, c) =>
contents += Swing.RigidBox(new Dimension(10, 0))
if (n != "") {
@@ -189,7 +189,6 @@
contents += c.asInstanceOf[Component]
focusList = c.asInstanceOf[Component].peer :: focusList
- case _ =>
})
{
@@ -371,12 +370,12 @@
}
def getFirstComponent(root: java.awt.Container): java.awt.Component =
- if (items.length > 0) items(0) else null
+ if (items.nonEmpty) items(0) else null
def getDefaultComponent(root: java.awt.Container): java.awt.Component =
getFirstComponent(root)
def getLastComponent(root: java.awt.Container): java.awt.Component =
- if (items.length > 0) items.last else null
+ if (items.nonEmpty) items.last else null
}
}
\ No newline at end of file
--- a/src/Tools/VSCode/src/dynamic_output.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala Wed Jan 15 19:54:50 2020 +0100
@@ -28,7 +28,7 @@
case None => copy(output = Nil)
case Some(command) =>
copy(output =
- if (!restriction.isDefined || restriction.get.contains(command))
+ if (restriction.isEmpty || restriction.get.contains(command))
Rendering.output_messages(snapshot.command_results(command))
else output)
}
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Jan 15 19:49:13 2020 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Wed Jan 15 19:54:50 2020 +0100
@@ -368,7 +368,7 @@
}
val selection = text_area.getSelection()
- if (!special && (selection == null || selection.length == 0))
+ if (!special && (selection == null || selection.isEmpty))
Isabelle.indent_input(text_area)
}
}