misc tuning, based on warnings by IntelliJ IDEA;
authorwenzelm
Sun May 03 00:01:10 2015 +0200 (2015-05-03)
changeset 602155fb4990dfc73
parent 60214 0b7656c5f0e9
child 60216 ef4f0b5b925e
misc tuning, based on warnings by IntelliJ IDEA;
src/Pure/Concurrent/future.scala
src/Pure/General/completion.scala
src/Pure/General/graph.scala
src/Pure/General/path.scala
src/Pure/General/scan.scala
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
src/Pure/ML/ml_lex.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/xml.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/options.scala
src/Pure/Thy/html.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/bibtex.scala
src/Pure/Tools/build.scala
src/Pure/library.scala
src/Tools/Graphview/shapes.scala
src/Tools/jEdit/src/active.scala
src/Tools/jEdit/src/bibtex_jedit.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/jedit_lib.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Pure/Concurrent/future.scala	Fri May 01 15:33:43 2015 +0200
     1.2 +++ b/src/Pure/Concurrent/future.scala	Sun May 03 00:01:10 2015 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4      new Pending_Future(Scala_Future[A](body)(execution_context))
     1.5  
     1.6    def promise[A]: Promise[A] =
     1.7 -    new Promise_Future[A](Scala_Promise[A])
     1.8 +    new Promise_Future[A](Scala_Promise[A]())
     1.9  }
    1.10  
    1.11  trait Future[A]
    1.12 @@ -90,4 +90,3 @@
    1.13      }
    1.14    def fulfill(x: A): Unit = promise.success(x)
    1.15  }
    1.16 -
     2.1 --- a/src/Pure/General/completion.scala	Fri May 01 15:33:43 2015 +0200
     2.2 +++ b/src/Pure/General/completion.scala	Sun May 03 00:01:10 2015 +0200
     2.3 @@ -432,7 +432,7 @@
     2.4                      if ok
     2.5                      completion <- words_map.get_list(complete_word)
     2.6                    } yield (complete_word, completion)
     2.7 -              ((full_word, completions))
     2.8 +              (full_word, completions)
     2.9            })
    2.10        }
    2.11  
     3.1 --- a/src/Pure/General/graph.scala	Fri May 01 15:33:43 2015 +0200
     3.2 +++ b/src/Pure/General/graph.scala	Sun May 03 00:01:10 2015 +0200
     3.3 @@ -39,17 +39,17 @@
     3.4    /* XML data representation */
     3.5  
     3.6    def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] =
     3.7 -    ((graph: Graph[Key, A]) => {
     3.8 +    (graph: Graph[Key, A]) => {
     3.9        import XML.Encode._
    3.10        list(pair(pair(key, info), list(key)))(graph.dest)
    3.11 -    })
    3.12 +    }
    3.13  
    3.14    def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
    3.15      implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
    3.16 -    ((body: XML.Body) => {
    3.17 +    (body: XML.Body) => {
    3.18        import XML.Decode._
    3.19        make(list(pair(pair(key, info), list(key)))(body))(ord)
    3.20 -    })
    3.21 +    }
    3.22  }
    3.23  
    3.24  
    3.25 @@ -209,7 +209,7 @@
    3.26        xs0 match {
    3.27          case Nil => xs1
    3.28          case x :: xs =>
    3.29 -          if (!(x_set(x)) || x == z || path.contains(x) ||
    3.30 +          if (!x_set(x) || x == z || path.contains(x) ||
    3.31                xs.exists(red(x)) || xs1.exists(red(x)))
    3.32              irreds(xs, xs1)
    3.33            else irreds(xs, x :: xs1)
     4.1 --- a/src/Pure/General/path.scala	Fri May 01 15:33:43 2015 +0200
     4.2 +++ b/src/Pure/General/path.scala	Sun May 03 00:01:10 2015 +0200
     4.3 @@ -18,9 +18,9 @@
     4.4    /* path elements */
     4.5  
     4.6    sealed abstract class Elem
     4.7 -  private case class Root(val name: String) extends Elem
     4.8 -  private case class Basic(val name: String) extends Elem
     4.9 -  private case class Variable(val name: String) extends Elem
    4.10 +  private case class Root(name: String) extends Elem
    4.11 +  private case class Basic(name: String) extends Elem
    4.12 +  private case class Variable(name: String) extends Elem
    4.13    private case object Parent extends Elem
    4.14  
    4.15    private def err_elem(msg: String, s: String): Nothing =
    4.16 @@ -30,7 +30,7 @@
    4.17      if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s)
    4.18      else {
    4.19        "/\\$:\"'".iterator.foreach(c =>
    4.20 -        if (s.iterator.exists(_ == c))
    4.21 +        if (s.iterator.contains(c))
    4.22            err_elem("Illegal character " + quote(c.toString) + " in", s))
    4.23        s
    4.24      }
     5.1 --- a/src/Pure/General/scan.scala	Fri May 01 15:33:43 2015 +0200
     5.2 +++ b/src/Pure/General/scan.scala	Sun May 03 00:01:10 2015 +0200
     5.3 @@ -91,7 +91,7 @@
     5.4      private def quoted_body(quote: Symbol.Symbol): Parser[String] =
     5.5      {
     5.6        rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" |
     5.7 -        (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
     5.8 +        ("""\\\d\d\d""".r ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString)
     5.9      }
    5.10  
    5.11      def quoted(quote: Symbol.Symbol): Parser[String] =
    5.12 @@ -307,7 +307,7 @@
    5.13    {
    5.14      /* representation */
    5.15  
    5.16 -    private sealed case class Tree(val branches: Map[Char, (String, Tree)])
    5.17 +    private sealed case class Tree(branches: Map[Char, (String, Tree)])
    5.18      private val empty_tree = Tree(Map())
    5.19  
    5.20      val empty: Lexicon = new Lexicon(empty_tree)
     6.1 --- a/src/Pure/General/symbol.scala	Fri May 01 15:33:43 2015 +0200
     6.2 +++ b/src/Pure/General/symbol.scala	Sun May 03 00:01:10 2015 +0200
     6.3 @@ -318,7 +318,7 @@
     6.4      val names: Map[Symbol, String] =
     6.5      {
     6.6        val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
     6.7 -      Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     6.8 +      Map((for ((sym @ name(a), _) <- symbols) yield sym -> a): _*)
     6.9      }
    6.10  
    6.11      val groups: List[(String, List[Symbol])] =
    6.12 @@ -334,7 +334,7 @@
    6.13          for {
    6.14            (sym, props) <- symbols
    6.15            ("abbrev", a) <- props.reverse
    6.16 -        } yield (sym -> a)): _*)
    6.17 +        } yield sym -> a): _*)
    6.18  
    6.19  
    6.20      /* recoding */
    6.21 @@ -381,7 +381,7 @@
    6.22  
    6.23      private val Font = new Properties.String("font")
    6.24      val fonts: Map[Symbol, String] =
    6.25 -      recode_map((for ((sym, Font(font)) <- symbols) yield (sym -> font)): _*)
    6.26 +      recode_map((for ((sym, Font(font)) <- symbols) yield sym -> font): _*)
    6.27  
    6.28      val font_names: List[String] = Set(fonts.toList.map(_._2): _*).toList
    6.29      val font_index: Map[String, Int] = Map((font_names zip (0 until font_names.length).toList): _*)
     7.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri May 01 15:33:43 2015 +0200
     7.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun May 03 00:01:10 2015 +0200
     7.3 @@ -33,7 +33,7 @@
     7.4            result += '\\'
     7.5            if (c < 10) result += '0'
     7.6            if (c < 100) result += '0'
     7.7 -          result ++= (c.asInstanceOf[Int].toString)
     7.8 +          result ++= c.asInstanceOf[Int].toString
     7.9          }
    7.10          else result += c
    7.11        }
     8.1 --- a/src/Pure/Isar/token.scala	Fri May 01 15:33:43 2015 +0200
     8.2 +++ b/src/Pure/Isar/token.scala	Sun May 03 00:01:10 2015 +0200
     8.3 @@ -144,7 +144,7 @@
     8.4      var ctxt = context
     8.5      while (!in.atEnd) {
     8.6        Parsers.parse(Parsers.token_line(keywords, ctxt), in) match {
     8.7 -        case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
     8.8 +        case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
     8.9          case Parsers.NoSuccess(_, rest) =>
    8.10            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    8.11        }
    8.12 @@ -158,7 +158,7 @@
    8.13    def implode(toks: List[Token]): String =
    8.14      toks match {
    8.15        case List(tok) => tok.source
    8.16 -      case toks => toks.map(_.source).mkString
    8.17 +      case _ => toks.map(_.source).mkString
    8.18      }
    8.19  
    8.20  
    8.21 @@ -222,7 +222,7 @@
    8.22  }
    8.23  
    8.24  
    8.25 -sealed case class Token(val kind: Token.Kind.Value, val source: String)
    8.26 +sealed case class Token(kind: Token.Kind.Value, source: String)
    8.27  {
    8.28    def is_command: Boolean = kind == Token.Kind.COMMAND
    8.29    def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
     9.1 --- a/src/Pure/ML/ml_lex.scala	Fri May 01 15:33:43 2015 +0200
     9.2 +++ b/src/Pure/ML/ml_lex.scala	Sun May 03 00:01:10 2015 +0200
     9.3 @@ -62,7 +62,7 @@
     9.4      val ERROR = Value("bad input")
     9.5    }
     9.6  
     9.7 -  sealed case class Token(val kind: Kind.Value, val source: String)
     9.8 +  sealed case class Token(kind: Kind.Value, source: String)
     9.9    {
    9.10      def is_keyword: Boolean = kind == Kind.KEYWORD
    9.11      def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
    9.12 @@ -282,7 +282,7 @@
    9.13      var ctxt = context
    9.14      while (!in.atEnd) {
    9.15        Parsers.parse(Parsers.token_line(SML, ctxt), in) match {
    9.16 -        case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest }
    9.17 +        case Parsers.Success((x, c), rest) => toks += x; ctxt = c; in = rest
    9.18          case Parsers.NoSuccess(_, rest) =>
    9.19            error("Unexpected failure of tokenizing input:\n" + rest.source.toString)
    9.20        }
    10.1 --- a/src/Pure/PIDE/command.scala	Fri May 01 15:33:43 2015 +0200
    10.2 +++ b/src/Pure/PIDE/command.scala	Sun May 03 00:01:10 2015 +0200
    10.3 @@ -427,7 +427,7 @@
    10.4    val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
    10.5      ((Symbol.Text_Chunk.Default -> chunk) ::
    10.6        (for (Exn.Res((name, Some((_, file)))) <- blobs)
    10.7 -        yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap
    10.8 +        yield Symbol.Text_Chunk.File(name.node) -> file)).toMap
    10.9  
   10.10    def length: Int = source.length
   10.11    def range: Text.Range = chunk.range
    11.1 --- a/src/Pure/PIDE/document.scala	Fri May 01 15:33:43 2015 +0200
    11.2 +++ b/src/Pure/PIDE/document.scala	Sun May 03 00:01:10 2015 +0200
    11.3 @@ -502,21 +502,21 @@
    11.4  
    11.5    final case class State private(
    11.6      /*reachable versions*/
    11.7 -    val versions: Map[Document_ID.Version, Version] = Map.empty,
    11.8 +    versions: Map[Document_ID.Version, Version] = Map.empty,
    11.9      /*inlined auxiliary files*/
   11.10 -    val blobs: Set[SHA1.Digest] = Set.empty,
   11.11 +    blobs: Set[SHA1.Digest] = Set.empty,
   11.12      /*static markup from define_command*/
   11.13 -    val commands: Map[Document_ID.Command, Command.State] = Map.empty,
   11.14 +    commands: Map[Document_ID.Command, Command.State] = Map.empty,
   11.15      /*dynamic markup from execution*/
   11.16 -    val execs: Map[Document_ID.Exec, Command.State] = Map.empty,
   11.17 +    execs: Map[Document_ID.Exec, Command.State] = Map.empty,
   11.18      /*command-exec assignment for each version*/
   11.19 -    val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
   11.20 +    assignments: Map[Document_ID.Version, State.Assignment] = Map.empty,
   11.21      /*commands with markup produced by other commands (imm_succs)*/
   11.22 -    val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
   11.23 +    commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long,
   11.24      /*explicit (linear) history*/
   11.25 -    val history: History = History.init,
   11.26 +    history: History = History.init,
   11.27      /*intermediate state between remove_versions/removed_versions*/
   11.28 -    val removing_versions: Boolean = false)
   11.29 +    removing_versions: Boolean = false)
   11.30    {
   11.31      private def fail[A]: A = throw new State.Fail(this)
   11.32  
    12.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri May 01 15:33:43 2015 +0200
    12.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sun May 03 00:01:10 2015 +0200
    12.3 @@ -57,7 +57,7 @@
    12.4      def filter_markup(elements: Markup.Elements): List[XML.Elem] =
    12.5      {
    12.6        var result: List[XML.Elem] = Nil
    12.7 -      for { elem <- rev_markup; if (elements(elem.name)) }
    12.8 +      for (elem <- rev_markup if elements(elem.name))
    12.9          result ::= elem
   12.10        result.toList
   12.11      }
   12.12 @@ -267,4 +267,3 @@
   12.13        case list => list.mkString("Tree(", ",", ")")
   12.14      }
   12.15  }
   12.16 -
    13.1 --- a/src/Pure/PIDE/prover.scala	Fri May 01 15:33:43 2015 +0200
    13.2 +++ b/src/Pure/PIDE/prover.scala	Sun May 03 00:01:10 2015 +0200
    13.3 @@ -293,7 +293,7 @@
    13.4        {
    13.5          val n = read_int()
    13.6          val buf =
    13.7 -          if (n <= default_buffer.size) default_buffer
    13.8 +          if (n <= default_buffer.length) default_buffer
    13.9            else new Array[Byte](n)
   13.10  
   13.11          var i = 0
   13.12 @@ -367,4 +367,3 @@
   13.13      protocol_command_bytes(name, args.map(Bytes(_)): _*)
   13.14    }
   13.15  }
   13.16 -
    14.1 --- a/src/Pure/PIDE/text.scala	Fri May 01 15:33:43 2015 +0200
    14.2 +++ b/src/Pure/PIDE/text.scala	Sun May 03 00:01:10 2015 +0200
    14.3 @@ -34,7 +34,7 @@
    14.4      }
    14.5    }
    14.6  
    14.7 -  sealed case class Range(val start: Offset, val stop: Offset)
    14.8 +  sealed case class Range(start: Offset, stop: Offset)
    14.9    {
   14.10      // denotation: {start} Un {i. start < i & i < stop}
   14.11      if (start > stop)
   14.12 @@ -124,7 +124,7 @@
   14.13  
   14.14    /* information associated with text range */
   14.15  
   14.16 -  sealed case class Info[A](val range: Text.Range, val info: A)
   14.17 +  sealed case class Info[A](range: Text.Range, info: A)
   14.18    {
   14.19      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
   14.20      def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info))
    15.1 --- a/src/Pure/PIDE/xml.scala	Fri May 01 15:33:43 2015 +0200
    15.2 +++ b/src/Pure/PIDE/xml.scala	Sun May 03 00:01:10 2015 +0200
    15.3 @@ -36,9 +36,9 @@
    15.4  
    15.5    /* wrapped elements */
    15.6  
    15.7 -  val XML_ELEM = "xml_elem";
    15.8 -  val XML_NAME = "xml_name";
    15.9 -  val XML_BODY = "xml_body";
   15.10 +  val XML_ELEM = "xml_elem"
   15.11 +  val XML_NAME = "xml_name"
   15.12 +  val XML_BODY = "xml_body"
   15.13  
   15.14    object Wrapped_Elem
   15.15    {
    16.1 --- a/src/Pure/System/isabelle_process.scala	Fri May 01 15:33:43 2015 +0200
    16.2 +++ b/src/Pure/System/isabelle_process.scala	Sun May 03 00:01:10 2015 +0200
    16.3 @@ -25,7 +25,7 @@
    16.4          process.stdin.close
    16.5          process
    16.6        }
    16.7 -      catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) }
    16.8 +      catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn }
    16.9  
   16.10      new Isabelle_Process(receiver, system_channel, system_process)
   16.11    }
    17.1 --- a/src/Pure/System/isabelle_system.scala	Fri May 01 15:33:43 2015 +0200
    17.2 +++ b/src/Pure/System/isabelle_system.scala	Sun May 03 00:01:10 2015 +0200
    17.3 @@ -93,9 +93,9 @@
    17.4          default(
    17.5            default(
    17.6              default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())),
    17.7 -              ("TEMP_WINDOWS" -> temp_windows)),
    17.8 -            ("HOME" -> user_home)),
    17.9 -          ("ISABELLE_APP" -> "true"))
   17.10 +              "TEMP_WINDOWS" -> temp_windows),
   17.11 +            "HOME" -> user_home),
   17.12 +          "ISABELLE_APP" -> "true")
   17.13        }
   17.14  
   17.15        val system_home =
   17.16 @@ -125,8 +125,8 @@
   17.17            val entries =
   17.18              (for (entry <- File.read(dump) split "\u0000" if entry != "") yield {
   17.19                val i = entry.indexOf('=')
   17.20 -              if (i <= 0) (entry -> "")
   17.21 -              else (entry.substring(0, i) -> entry.substring(i + 1))
   17.22 +              if (i <= 0) entry -> ""
   17.23 +              else entry.substring(0, i) -> entry.substring(i + 1)
   17.24              }).toMap
   17.25            entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
   17.26          }
    18.1 --- a/src/Pure/System/options.scala	Fri May 01 15:33:43 2015 +0200
    18.2 +++ b/src/Pure/System/options.scala	Sun May 03 00:01:10 2015 +0200
    18.3 @@ -368,7 +368,7 @@
    18.4        (for {
    18.5          (name, opt2) <- options.iterator
    18.6          opt1 = defaults.options.get(name)
    18.7 -        if (opt1.isEmpty || opt1.get.value != opt2.value)
    18.8 +        if opt1.isEmpty || opt1.get.value != opt2.value
    18.9        } yield (name, opt2.value, if (opt1.isEmpty) "  (* unknown *)" else "")).toList
   18.10  
   18.11      val prefs =
   18.12 @@ -429,4 +429,3 @@
   18.13    }
   18.14    val seconds = new Seconds_Access
   18.15  }
   18.16 -
    19.1 --- a/src/Pure/Thy/html.scala	Fri May 01 15:33:43 2015 +0200
    19.2 +++ b/src/Pure/Thy/html.scala	Sun May 03 00:01:10 2015 +0200
    19.3 @@ -28,7 +28,7 @@
    19.4          case '"' => result ++= "&quot;"
    19.5          case '\'' => result ++= "&#39;"
    19.6          case '\n' => result ++= "<br/>"
    19.7 -        case c => result += c
    19.8 +        case _ => result += c
    19.9        }
   19.10      def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
   19.11  
    20.1 --- a/src/Pure/Thy/thy_header.scala	Fri May 01 15:33:43 2015 +0200
    20.2 +++ b/src/Pure/Thy/thy_header.scala	Sun May 03 00:01:10 2015 +0200
    20.3 @@ -100,7 +100,7 @@
    20.4  
    20.5      val args =
    20.6        position(theory_name) ~
    20.7 -      (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^
    20.8 +      (opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^
    20.9          { case None => Nil case Some(_ ~ xs) => xs }) ~
   20.10        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   20.11          { case None => Nil case Some(_ ~ xs) => xs }) ~
    21.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri May 01 15:33:43 2015 +0200
    21.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sun May 03 00:01:10 2015 +0200
    21.3 @@ -339,7 +339,7 @@
    21.4                    node2, (name, node2.edit_perspective))
    21.5                else node2
    21.6  
    21.7 -            if (!(node.same_perspective(node3.text_perspective, node3.perspective)))
    21.8 +            if (!node.same_perspective(node3.text_perspective, node3.perspective))
    21.9                doc_edits += (name -> node3.perspective)
   21.10  
   21.11              doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
    22.1 --- a/src/Pure/Tools/bibtex.scala	Fri May 01 15:33:43 2015 +0200
    22.2 +++ b/src/Pure/Tools/bibtex.scala	Sun May 03 00:01:10 2015 +0200
    22.3 @@ -133,7 +133,7 @@
    22.4      }
    22.5    }
    22.6  
    22.7 -  sealed case class Token(kind: Token.Kind.Value, val source: String)
    22.8 +  sealed case class Token(kind: Token.Kind.Value, source: String)
    22.9    {
   22.10      def is_kind: Boolean =
   22.11        kind == Token.Kind.COMMAND ||
   22.12 @@ -398,7 +398,7 @@
   22.13      var ctxt = context
   22.14      while (!in.atEnd) {
   22.15        Parsers.parse(Parsers.chunk_line(ctxt), in) match {
   22.16 -        case Parsers.Success((x, c), rest) => { chunks += x; ctxt = c; in = rest }
   22.17 +        case Parsers.Success((x, c), rest) => chunks += x; ctxt = c; in = rest
   22.18          case Parsers.NoSuccess(_, rest) =>
   22.19            error("Unepected failure to parse input:\n" + rest.source.toString)
   22.20        }
   22.21 @@ -406,4 +406,3 @@
   22.22      (chunks.toList, ctxt)
   22.23    }
   22.24  }
   22.25 -
    23.1 --- a/src/Pure/Tools/build.scala	Fri May 01 15:33:43 2015 +0200
    23.2 +++ b/src/Pure/Tools/build.scala	Sun May 03 00:01:10 2015 +0200
    23.3 @@ -908,7 +908,7 @@
    23.4              loop(pending - name, running - name,
    23.5                results + (name -> Result(false, heap, res.rc)))
    23.6              //}}}
    23.7 -          case None if (running.size < (max_jobs max 1)) =>
    23.8 +          case None if running.size < (max_jobs max 1) =>
    23.9              //{{{ check/start next job
   23.10              pending.dequeue(running.isDefinedAt(_)) match {
   23.11                case Some((name, info)) =>
    24.1 --- a/src/Pure/library.scala	Fri May 01 15:33:43 2015 +0200
    24.2 +++ b/src/Pure/library.scala	Sun May 03 00:01:10 2015 +0200
    24.3 @@ -107,7 +107,7 @@
    24.4        def hasNext(): Boolean = state.isDefined
    24.5        def next(): CharSequence =
    24.6          state match {
    24.7 -          case Some((s, i)) => { state = next_chunk(i); s }
    24.8 +          case Some((s, i)) => state = next_chunk(i); s
    24.9            case None => Iterator.empty.next()
   24.10          }
   24.11      }
   24.12 @@ -207,7 +207,7 @@
   24.13  
   24.14    /* canonical list operations */
   24.15  
   24.16 -  def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x)
   24.17 +  def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x)
   24.18    def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs
   24.19    def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
   24.20    def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
    25.1 --- a/src/Tools/Graphview/shapes.scala	Fri May 01 15:33:43 2015 +0200
    25.2 +++ b/src/Tools/Graphview/shapes.scala	Sun May 03 00:01:10 2015 +0200
    25.3 @@ -163,7 +163,7 @@
    25.4          val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0)
    25.5          var p1 = (0.0, 0.0)
    25.6          var p2 = (0.0, 0.0)
    25.7 -        while (!i.isDone()) {
    25.8 +        while (!i.isDone) {
    25.9            i.currentSegment(seg) match {
   25.10              case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1))
   25.11              case PathIterator.SEG_LINETO =>
   25.12 @@ -223,4 +223,4 @@
   25.13        }
   25.14      }
   25.15    }
   25.16 -}
   25.17 \ No newline at end of file
   25.18 +}
    26.1 --- a/src/Tools/jEdit/src/active.scala	Fri May 01 15:33:43 2015 +0200
    26.2 +++ b/src/Tools/jEdit/src/active.scala	Sun May 03 00:01:10 2015 +0200
    26.3 @@ -61,9 +61,9 @@
    26.4                    props match {
    26.5                      case Position.Id(id) =>
    26.6                        Isabelle.edit_command(snapshot, buffer,
    26.7 -                        props.exists(_ == Markup.PADDING_COMMAND), id, text)
    26.8 +                        props.contains(Markup.PADDING_COMMAND), id, text)
    26.9                      case _ =>
   26.10 -                      if (props.exists(_ == Markup.PADDING_LINE))
   26.11 +                      if (props.contains(Markup.PADDING_LINE))
   26.12                          Isabelle.insert_line_padding(text_area, text)
   26.13                        else text_area.setSelectedText(text)
   26.14                    }
    27.1 --- a/src/Tools/jEdit/src/bibtex_jedit.scala	Fri May 01 15:33:43 2015 +0200
    27.2 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala	Sun May 03 00:01:10 2015 +0200
    27.3 @@ -252,11 +252,11 @@
    27.4              val label_html =
    27.5                "<html><b>" + HTML.encode(kind) + "</b>" +
    27.6                (if (name == "") "" else " " + HTML.encode(name)) + "</html>"
    27.7 -            val range = Text.Range(offset, offset + source.size)
    27.8 +            val range = Text.Range(offset, offset + source.length)
    27.9              val asset = new Asset(label, label_html, range, source)
   27.10              data.root.add(new DefaultMutableTreeNode(asset))
   27.11            }
   27.12 -          offset += source.size
   27.13 +          offset += source.length
   27.14          }
   27.15          data
   27.16        }
    28.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Fri May 01 15:33:43 2015 +0200
    28.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun May 03 00:01:10 2015 +0200
    28.3 @@ -117,13 +117,13 @@
    28.4  
    28.5    override def init()
    28.6    {
    28.7 -    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
    28.8 +    GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
    28.9      PIDE.session.global_options += main
   28.10    }
   28.11  
   28.12    override def exit()
   28.13    {
   28.14 -    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
   28.15 +    GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
   28.16      PIDE.session.global_options -= main
   28.17    }
   28.18  }
    29.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Fri May 01 15:33:43 2015 +0200
    29.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun May 03 00:01:10 2015 +0200
    29.3 @@ -230,7 +230,7 @@
    29.4  
    29.5    /* graphics range */
    29.6  
    29.7 -  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    29.8 +  case class Gfx_Range(x: Int, y: Int, length: Int)
    29.9  
   29.10    // NB: jEdit always normalizes \r\n and \r to \n
   29.11    // NB: last line lacks \n
   29.12 @@ -274,7 +274,7 @@
   29.13        if (offset >= 0) {
   29.14          val range = point_range(text_area.getBuffer, offset)
   29.15          gfx_range(text_area, range) match {
   29.16 -          case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range)
   29.17 +          case Some(g) if g.x <= x && x < g.x + g.length => Some(range)
   29.18            case _ => None
   29.19          }
   29.20        }
   29.21 @@ -371,4 +371,3 @@
   29.22      (mod & InputEvent.META_MASK) != 0
   29.23    }
   29.24  }
   29.25 -
    30.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri May 01 15:33:43 2015 +0200
    30.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun May 03 00:01:10 2015 +0200
    30.3 @@ -332,10 +332,10 @@
    30.4            }
    30.5  
    30.6          case msg: EditPaneUpdate
    30.7 -        if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    30.8 +        if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    30.9              msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   30.10              msg.getWhat == EditPaneUpdate.CREATED ||
   30.11 -            msg.getWhat == EditPaneUpdate.DESTROYED) =>
   30.12 +            msg.getWhat == EditPaneUpdate.DESTROYED =>
   30.13            val edit_pane = msg.getEditPane
   30.14            val buffer = edit_pane.getBuffer
   30.15            val text_area = edit_pane.getTextArea
    31.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri May 01 15:33:43 2015 +0200
    31.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun May 03 00:01:10 2015 +0200
    31.3 @@ -407,7 +407,7 @@
    31.4                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
    31.5                  case _ => None
    31.6                }
    31.7 -            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
    31.8 +            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
    31.9  
   31.10            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
   31.11              val opt_link =
   31.12 @@ -419,14 +419,14 @@
   31.13                    PIDE.editor.hyperlink_command_id(snapshot, id, offset)
   31.14                  case _ => None
   31.15                }
   31.16 -            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   31.17 +            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
   31.18  
   31.19            case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
   31.20              val opt_link =
   31.21                Bibtex_JEdit.entries_iterator.collectFirst(
   31.22                  { case (a, buffer, offset) if a == name =>
   31.23                      PIDE.editor.hyperlink_buffer(buffer, offset) })
   31.24 -            opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link)))
   31.25 +            opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
   31.26  
   31.27            case _ => None
   31.28          }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
   31.29 @@ -472,7 +472,7 @@
   31.30            case (msgs, Text.Info(info_range,
   31.31              XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
   31.32              val entry: Command.Results.Entry =
   31.33 -              (serial -> XML.Elem(Markup(Markup.message(name), props), body))
   31.34 +              serial -> XML.Elem(Markup(Markup.message(name), props), body)
   31.35              Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
   31.36  
   31.37            case _ => None
    32.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Fri May 01 15:33:43 2015 +0200
    32.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun May 03 00:01:10 2015 +0200
    32.3 @@ -284,7 +284,7 @@
    32.4              for { (color, separator) <- rendering.line_background(line_range) }
    32.5              {
    32.6                gfx.setColor(color)
    32.7 -              val sep = if (separator) (2 min (line_height / 2)) else 0
    32.8 +              val sep = if (separator) 2 min (line_height / 2) else 0
    32.9                gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
   32.10              }
   32.11  
   32.12 @@ -659,4 +659,3 @@
   32.13      painter.removeExtension(set_state)
   32.14    }
   32.15  }
   32.16 -