# HG changeset patch # User wenzelm # Date 1579114490 -3600 # Node ID 8313dca6dee938ec1a573f14f8ff6ea21d8ca83a # Parent 6316debd3a9f422f3a32f3f43ceecdd9bda90b30 misc tuning, following hint by IntelliJ; diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/linear_set.scala --- 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 = diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/mercurial.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/path.scala --- 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()) diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/scan.scala --- 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 { diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/ssh.scala --- 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)) diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/General/symbol.scala --- 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 */ diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/ML/ml_console.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/ML/ml_process.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/PIDE/markup_tree.scala --- 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 } } diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/PIDE/prover.scala --- 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 } diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/System/getopts.scala --- 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) diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/System/isabelle_tool.scala --- 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) => diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/System/platform.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/System/tty_loop.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/Tools/server.scala --- 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 = { diff -r 6316debd3a9f -r 8313dca6dee9 src/Pure/Tools/spell_checker.scala --- 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 */ diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/Graphview/graph_panel.scala --- 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) diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/Graphview/layout.scala --- 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) diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/Graphview/metrics.scala --- 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 } } diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/Graphview/mutator_dialog.scala --- 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 diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/VSCode/src/dynamic_output.scala --- 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) } diff -r 6316debd3a9f -r 8313dca6dee9 src/Tools/jEdit/src/completion_popup.scala --- 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) } }