misc tuning, following hint by IntelliJ;
authorwenzelm
Wed Jan 15 19:54:50 2020 +0100 (6 days ago)
changeset 713838313dca6dee9
parent 71382 6316debd3a9f
child 71384 0243bf758e79
misc tuning, following hint by IntelliJ;
src/Pure/General/linear_set.scala
src/Pure/General/mercurial.scala
src/Pure/General/path.scala
src/Pure/General/scan.scala
src/Pure/General/ssh.scala
src/Pure/General/symbol.scala
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_process.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/prover.scala
src/Pure/System/getopts.scala
src/Pure/System/isabelle_tool.scala
src/Pure/System/platform.scala
src/Pure/System/tty_loop.scala
src/Pure/Tools/server.scala
src/Pure/Tools/spell_checker.scala
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/layout.scala
src/Tools/Graphview/metrics.scala
src/Tools/Graphview/mutator_dialog.scala
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/linear_set.scala	Wed Jan 15 19:49:13 2020 +0100
     1.2 +++ b/src/Pure/General/linear_set.scala	Wed Jan 15 19:54:50 2020 +0100
     1.3 @@ -117,7 +117,7 @@
     1.4  
     1.5    override def stringPrefix = "Linear_Set"
     1.6  
     1.7 -  override def isEmpty: Boolean = !start.isDefined
     1.8 +  override def isEmpty: Boolean = start.isEmpty
     1.9    override def size: Int = if (isEmpty) 0 else nexts.size + 1
    1.10  
    1.11    def contains(elem: A): Boolean =
     2.1 --- a/src/Pure/General/mercurial.scala	Wed Jan 15 19:49:13 2020 +0100
     2.2 +++ b/src/Pure/General/mercurial.scala	Wed Jan 15 19:54:50 2020 +0100
     2.3 @@ -200,7 +200,7 @@
     2.4      val edited =
     2.5        hgrc.is_file && {
     2.6          val lines = split_lines(File.read(hgrc))
     2.7 -        lines.filter(header).length == 1 && {
     2.8 +        lines.count(header) == 1 && {
     2.9            if (local_hg.paths(options = "-q").contains(path_name)) {
    2.10              val old_source = local_hg.paths(args = path_name).head
    2.11              val old_entry = path_name + ".old = " + old_source
     3.1 --- a/src/Pure/General/path.scala	Wed Jan 15 19:49:13 2020 +0100
     3.2 +++ b/src/Pure/General/path.scala	Wed Jan 15 19:54:50 2020 +0100
     3.3 @@ -233,7 +233,7 @@
     3.4          case x => List(x)
     3.5        }
     3.6  
     3.7 -    new Path(Path.norm_elems(elems.map(eval).flatten))
     3.8 +    new Path(Path.norm_elems(elems.flatMap(eval)))
     3.9    }
    3.10  
    3.11    def expand: Path = expand_env(Isabelle_System.settings())
     4.1 --- a/src/Pure/General/scan.scala	Wed Jan 15 19:49:13 2020 +0100
     4.2 +++ b/src/Pure/General/scan.scala	Wed Jan 15 19:54:50 2020 +0100
     4.3 @@ -412,7 +412,7 @@
     4.4        val offset = in.offset
     4.5        val len = source.length - offset
     4.6  
     4.7 -      def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
     4.8 +      @tailrec def scan_tree(tree: Lexicon.Tree, result: String, i: Int): String =
     4.9        {
    4.10          if (i < len) {
    4.11            tree.branches.get(source.charAt(offset + i)) match {
     5.1 --- a/src/Pure/General/ssh.scala	Wed Jan 15 19:49:13 2020 +0100
     5.2 +++ b/src/Pure/General/ssh.scala	Wed Jan 15 19:54:50 2020 +0100
     5.3 @@ -90,7 +90,7 @@
     5.4        host_key_alias: String = "",
     5.5        on_close: () => Unit = () => ()): Session =
     5.6      {
     5.7 -      val session = jsch.getSession(proper_string(user) getOrElse null, host, make_port(port))
     5.8 +      val session = jsch.getSession(proper_string(user).orNull, host, make_port(port))
     5.9  
    5.10        session.setUserInfo(No_User_Info)
    5.11        session.setServerAliveInterval(alive_interval(options))
     6.1 --- a/src/Pure/General/symbol.scala	Wed Jan 15 19:49:13 2020 +0100
     6.2 +++ b/src/Pure/General/symbol.scala	Wed Jan 15 19:54:50 2020 +0100
     6.3 @@ -379,11 +379,10 @@
     6.4      }
     6.5  
     6.6      val groups: List[(String, List[Symbol])] =
     6.7 -      symbols.map({ case (sym, props) =>
     6.8 +      symbols.flatMap({ case (sym, props) =>
     6.9          val gs = for (("group", g) <- props) yield g
    6.10          if (gs.isEmpty) List(sym -> "unsorted") else gs.map(sym -> _)
    6.11 -      }).flatten
    6.12 -        .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
    6.13 +      }).groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
    6.14          .sortBy(_._1)
    6.15  
    6.16      val abbrevs: Multi_Map[Symbol, String] =
    6.17 @@ -444,7 +443,7 @@
    6.18        recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
    6.19  
    6.20      val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    6.21 -    val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
    6.22 +    val font_index: Map[String, Int] = Map((font_names zip font_names.indices.toList): _*)
    6.23  
    6.24  
    6.25      /* classification */
     7.1 --- a/src/Pure/ML/ml_console.scala	Wed Jan 15 19:49:13 2020 +0100
     7.2 +++ b/src/Pure/ML/ml_console.scala	Wed Jan 15 19:54:50 2020 +0100
     7.3 @@ -47,7 +47,7 @@
     7.4          "r" -> (_ => raw_ml_system = true))
     7.5  
     7.6        val more_args = getopts(args)
     7.7 -      if (!more_args.isEmpty) getopts.usage()
     7.8 +      if (more_args.nonEmpty) getopts.usage()
     7.9  
    7.10  
    7.11        // build logic
     8.1 --- a/src/Pure/ML/ml_process.scala	Wed Jan 15 19:49:13 2020 +0100
     8.2 +++ b/src/Pure/ML/ml_process.scala	Wed Jan 15 19:54:50 2020 +0100
     8.3 @@ -128,8 +128,8 @@
     8.4      // bash
     8.5      val bash_args =
     8.6        ml_runtime_options :::
     8.7 -      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
     8.8 -        map(eval => List("--eval", eval)).flatten ::: args
     8.9 +      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
    8.10 +        .flatMap(eval => List("--eval", eval)) ::: args
    8.11  
    8.12      Bash.process(
    8.13        "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ +
    8.14 @@ -180,7 +180,7 @@
    8.15        "o:" -> (arg => options = options + arg))
    8.16  
    8.17      val more_args = getopts(args)
    8.18 -    if (args.isEmpty || !more_args.isEmpty) getopts.usage()
    8.19 +    if (args.isEmpty || more_args.nonEmpty) getopts.usage()
    8.20  
    8.21      val rc = ML_Process(options, logic = logic, args = eval_args, dirs = dirs, modes = modes).
    8.22        result().print_stdout.rc
     9.1 --- a/src/Pure/PIDE/markup_tree.scala	Wed Jan 15 19:49:13 2020 +0100
     9.2 +++ b/src/Pure/PIDE/markup_tree.scala	Wed Jan 15 19:54:50 2020 +0100
     9.3 @@ -153,7 +153,7 @@
     9.4              new Markup_Tree(branches -- body.keys, Entry(new_markup, new Markup_Tree(body)))
     9.5            else {
     9.6              Output.warning("Ignored overlapping markup information: " + new_markup + "\n" +
     9.7 -              body.filter(e => !new_range.contains(e._1)).map(_._2).mkString("\n"))
     9.8 +              body.filter(e => !new_range.contains(e._1)).values.mkString("\n"))
     9.9              this
    9.10            }
    9.11          }
    10.1 --- a/src/Pure/PIDE/prover.scala	Wed Jan 15 19:49:13 2020 +0100
    10.2 +++ b/src/Pure/PIDE/prover.scala	Wed Jan 15 19:54:50 2020 +0100
    10.3 @@ -22,8 +22,8 @@
    10.4    {
    10.5      override def toString: String =
    10.6        XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
    10.7 -        args.map(s =>
    10.8 -          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
    10.9 +        args.flatMap(s =>
   10.10 +          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s))))).toString
   10.11    }
   10.12  
   10.13    class Output(val message: XML.Elem) extends Message
   10.14 @@ -224,12 +224,12 @@
   10.15            //{{{
   10.16            var c = -1
   10.17            var done = false
   10.18 -          while (!done && (result.length == 0 || reader.ready)) {
   10.19 +          while (!done && (result.isEmpty || reader.ready)) {
   10.20              c = reader.read
   10.21              if (c >= 0) result.append(c.asInstanceOf[Char])
   10.22              else done = true
   10.23            }
   10.24 -          if (result.length > 0) {
   10.25 +          if (result.nonEmpty) {
   10.26              output(markup, Nil, List(XML.Text(Symbol.decode(result.toString))))
   10.27              result.clear
   10.28            }
    11.1 --- a/src/Pure/System/getopts.scala	Wed Jan 15 19:49:13 2020 +0100
    11.2 +++ b/src/Pure/System/getopts.scala	Wed Jan 15 19:54:50 2020 +0100
    11.3 @@ -47,11 +47,11 @@
    11.4    private def getopts(args: List[List[Char]]): List[List[Char]] =
    11.5      args match {
    11.6        case List('-', '-') :: rest_args => rest_args
    11.7 -      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && !rest_opts.isEmpty =>
    11.8 +      case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
    11.9          option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
   11.10        case List('-', opt) :: rest_args if is_option0(opt) =>
   11.11          option(opt, Nil); getopts(rest_args)
   11.12 -      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && !opt_arg.isEmpty =>
   11.13 +      case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
   11.14          option(opt, opt_arg); getopts(rest_args)
   11.15        case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
   11.16          option(opt, opt_arg); getopts(rest_args)
    12.1 --- a/src/Pure/System/isabelle_tool.scala	Wed Jan 15 19:49:13 2020 +0100
    12.2 +++ b/src/Pure/System/isabelle_tool.scala	Wed Jan 15 19:54:50 2020 +0100
    12.3 @@ -82,7 +82,7 @@
    12.4    }
    12.5  
    12.6    private def find_external(name: String): Option[List[String] => Unit] =
    12.7 -    dirs.collectFirst({
    12.8 +    dirs().collectFirst({
    12.9        case dir if is_external(dir, name + ".scala") =>
   12.10          compile(dir + Path.explode(name + ".scala"))
   12.11        case dir if is_external(dir, name) =>
    13.1 --- a/src/Pure/System/platform.scala	Wed Jan 15 19:49:13 2020 +0100
    13.2 +++ b/src/Pure/System/platform.scala	Wed Jan 15 19:54:50 2020 +0100
    13.3 @@ -11,9 +11,9 @@
    13.4  {
    13.5    /* platform family */
    13.6  
    13.7 -  val is_linux = System.getProperty("os.name", "") == "Linux"
    13.8 -  val is_macos = System.getProperty("os.name", "") == "Mac OS X"
    13.9 -  val is_windows = System.getProperty("os.name", "").startsWith("Windows")
   13.10 +  val is_linux: Boolean = System.getProperty("os.name", "") == "Linux"
   13.11 +  val is_macos: Boolean = System.getProperty("os.name", "") == "Mac OS X"
   13.12 +  val is_windows: Boolean = System.getProperty("os.name", "").startsWith("Windows")
   13.13  
   13.14    def family: Family.Value =
   13.15      if (is_linux) Family.linux
   13.16 @@ -58,7 +58,7 @@
   13.17    /* JVM version */
   13.18  
   13.19    private val Version = """1\.(\d+)\.0_(\d+)""".r
   13.20 -  lazy val jvm_version =
   13.21 +  lazy val jvm_version: String =
   13.22      System.getProperty("java.version") match {
   13.23        case Version(a, b) => a + "u" + b
   13.24        case a => a
    14.1 --- a/src/Pure/System/tty_loop.scala	Wed Jan 15 19:49:13 2020 +0100
    14.2 +++ b/src/Pure/System/tty_loop.scala	Wed Jan 15 19:54:50 2020 +0100
    14.3 @@ -21,12 +21,12 @@
    14.4        while (!finished) {
    14.5          var c = -1
    14.6          var done = false
    14.7 -        while (!done && (result.length == 0 || reader.ready)) {
    14.8 +        while (!done && (result.isEmpty || reader.ready)) {
    14.9            c = reader.read
   14.10            if (c >= 0) result.append(c.asInstanceOf[Char])
   14.11            else done = true
   14.12          }
   14.13 -        if (result.length > 0) {
   14.14 +        if (result.nonEmpty) {
   14.15            System.out.print(result.toString)
   14.16            System.out.flush()
   14.17            result.clear
    15.1 --- a/src/Pure/Tools/server.scala	Wed Jan 15 19:49:13 2020 +0100
    15.2 +++ b/src/Pure/Tools/server.scala	Wed Jan 15 19:54:50 2020 +0100
    15.3 @@ -520,7 +520,7 @@
    15.4  
    15.5    private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session])
    15.6    def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString))
    15.7 -  def the_session(id: UUID.T): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
    15.8 +  def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id))
    15.9    def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
   15.10    def remove_session(id: UUID.T): Headless.Session =
   15.11    {
    16.1 --- a/src/Pure/Tools/spell_checker.scala	Wed Jan 15 19:49:13 2020 +0100
    16.2 +++ b/src/Pure/Tools/spell_checker.scala	Wed Jan 15 19:54:50 2020 +0100
    16.3 @@ -198,7 +198,7 @@
    16.4    }
    16.5  
    16.6    def reset_enabled(): Int =
    16.7 -    updates.valuesIterator.filter(upd => !upd.permanent).length
    16.8 +    updates.valuesIterator.count(upd => !upd.permanent)
    16.9  
   16.10  
   16.11    /* check known words */
    17.1 --- a/src/Tools/Graphview/graph_panel.scala	Wed Jan 15 19:49:13 2020 +0100
    17.2 +++ b/src/Tools/Graphview/graph_panel.scala	Wed Jan 15 19:54:50 2020 +0100
    17.3 @@ -148,7 +148,7 @@
    17.4        (scale * font_height).floor / font_height
    17.5      }
    17.6  
    17.7 -    def apply() =
    17.8 +    def apply(): AffineTransform =
    17.9      {
   17.10        val box = graphview.bounding_box()
   17.11        val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
    18.1 --- a/src/Tools/Graphview/layout.scala	Wed Jan 15 19:49:13 2020 +0100
    18.2 +++ b/src/Tools/Graphview/layout.scala	Wed Jan 15 19:54:50 2020 +0100
    18.3 @@ -232,8 +232,8 @@
    18.4            case (outer_parent, outer_parent_index) =>
    18.5              graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
    18.6                (0 until outer_parent_index).iterator.map(inner_parent =>
    18.7 -                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_)).
    18.8 -                  filter(inner_child => outer_child < inner_child).size).sum).sum
    18.9 +                graph.imm_succs(top(inner_parent)).iterator.map(bot.indexOf(_))
   18.10 +                  .count(inner_child => outer_child < inner_child)).sum).sum
   18.11          }.sum
   18.12        case _ => 0
   18.13      }.sum
   18.14 @@ -289,7 +289,7 @@
   18.15  
   18.16      def deflect(level: List[Region], top_down: Boolean, graph: Graph): (Graph, Boolean) =
   18.17      {
   18.18 -      ((graph, false) /: (0 until level.length)) {
   18.19 +      ((graph, false) /: level.indices) {
   18.20          case ((graph, moved), i) =>
   18.21            val r = level(i)
   18.22            val d = r.deflection(graph, top_down)
    19.1 --- a/src/Tools/Graphview/metrics.scala	Wed Jan 15 19:49:13 2020 +0100
    19.2 +++ b/src/Tools/Graphview/metrics.scala	Wed Jan 15 19:54:50 2020 +0100
    19.3 @@ -36,7 +36,7 @@
    19.4  {
    19.5    def string_bounds(s: String): Rectangle2D = font.getStringBounds(s, Metrics.font_render_context)
    19.6    private val mix = string_bounds("mix")
    19.7 -  val space_width = string_bounds(" ").getWidth
    19.8 +  val space_width: Double = string_bounds(" ").getWidth
    19.9    def char_width: Double = mix.getWidth / 3
   19.10    def height: Double = mix.getHeight
   19.11    def ascent: Double = font.getLineMetrics("", Metrics.font_render_context).getAscent
   19.12 @@ -56,7 +56,7 @@
   19.13  
   19.14    object Pretty_Metric extends Pretty.Metric
   19.15    {
   19.16 -    val unit = space_width max 1.0
   19.17 +    val unit: Double = space_width max 1.0
   19.18      def apply(s: String): Double = if (s == "\n") 1.0 else string_bounds(s).getWidth / unit
   19.19    }
   19.20  }
    20.1 --- a/src/Tools/Graphview/mutator_dialog.scala	Wed Jan 15 19:49:13 2020 +0100
    20.2 +++ b/src/Tools/Graphview/mutator_dialog.scala	Wed Jan 15 19:54:50 2020 +0100
    20.3 @@ -179,7 +179,7 @@
    20.4      contents += enabledBox
    20.5      contents += Swing.RigidBox(new Dimension(5, 0))
    20.6      focusList = enabledBox.peer :: focusList
    20.7 -    inputs.map(_ match {
    20.8 +    inputs.map({
    20.9        case (n, c) =>
   20.10          contents += Swing.RigidBox(new Dimension(10, 0))
   20.11          if (n != "") {
   20.12 @@ -189,7 +189,6 @@
   20.13          contents += c.asInstanceOf[Component]
   20.14  
   20.15          focusList = c.asInstanceOf[Component].peer :: focusList
   20.16 -      case _ =>
   20.17      })
   20.18  
   20.19      {
   20.20 @@ -371,12 +370,12 @@
   20.21      }
   20.22  
   20.23      def getFirstComponent(root: java.awt.Container): java.awt.Component =
   20.24 -      if (items.length > 0) items(0) else null
   20.25 +      if (items.nonEmpty) items(0) else null
   20.26  
   20.27      def getDefaultComponent(root: java.awt.Container): java.awt.Component =
   20.28        getFirstComponent(root)
   20.29  
   20.30      def getLastComponent(root: java.awt.Container): java.awt.Component =
   20.31 -      if (items.length > 0) items.last else null
   20.32 +      if (items.nonEmpty) items.last else null
   20.33    }
   20.34  }
   20.35 \ No newline at end of file
    21.1 --- a/src/Tools/VSCode/src/dynamic_output.scala	Wed Jan 15 19:49:13 2020 +0100
    21.2 +++ b/src/Tools/VSCode/src/dynamic_output.scala	Wed Jan 15 19:54:50 2020 +0100
    21.3 @@ -28,7 +28,7 @@
    21.4                  case None => copy(output = Nil)
    21.5                  case Some(command) =>
    21.6                    copy(output =
    21.7 -                    if (!restriction.isDefined || restriction.get.contains(command))
    21.8 +                    if (restriction.isEmpty || restriction.get.contains(command))
    21.9                        Rendering.output_messages(snapshot.command_results(command))
   21.10                      else output)
   21.11                }
    22.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 15 19:49:13 2020 +0100
    22.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jan 15 19:54:50 2020 +0100
    22.3 @@ -368,7 +368,7 @@
    22.4          }
    22.5  
    22.6          val selection = text_area.getSelection()
    22.7 -        if (!special && (selection == null || selection.length == 0))
    22.8 +        if (!special && (selection == null || selection.isEmpty))
    22.9            Isabelle.indent_input(text_area)
   22.10        }
   22.11      }