# HG changeset patch # User wenzelm # Date 1430604070 -7200 # Node ID 5fb4990dfc736da4b7c73ffb3f9b2be42dfecedc # Parent 0b7656c5f0e9bf6e4062e860e09cf986acdb2a0a misc tuning, based on warnings by IntelliJ IDEA; diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Concurrent/future.scala Sun May 03 00:01:10 2015 +0200 @@ -26,7 +26,7 @@ new Pending_Future(Scala_Future[A](body)(execution_context)) def promise[A]: Promise[A] = - new Promise_Future[A](Scala_Promise[A]) + new Promise_Future[A](Scala_Promise[A]()) } trait Future[A] @@ -90,4 +90,3 @@ } def fulfill(x: A): Unit = promise.success(x) } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/General/completion.scala Sun May 03 00:01:10 2015 +0200 @@ -432,7 +432,7 @@ if ok completion <- words_map.get_list(complete_word) } yield (complete_word, completion) - ((full_word, completions)) + (full_word, completions) }) } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/graph.scala --- a/src/Pure/General/graph.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/General/graph.scala Sun May 03 00:01:10 2015 +0200 @@ -39,17 +39,17 @@ /* XML data representation */ def encode[Key, A](key: XML.Encode.T[Key], info: XML.Encode.T[A]): XML.Encode.T[Graph[Key, A]] = - ((graph: Graph[Key, A]) => { + (graph: Graph[Key, A]) => { import XML.Encode._ list(pair(pair(key, info), list(key)))(graph.dest) - }) + } def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])( implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] = - ((body: XML.Body) => { + (body: XML.Body) => { import XML.Decode._ make(list(pair(pair(key, info), list(key)))(body))(ord) - }) + } } @@ -209,7 +209,7 @@ xs0 match { case Nil => xs1 case x :: xs => - if (!(x_set(x)) || x == z || path.contains(x) || + if (!x_set(x) || x == z || path.contains(x) || xs.exists(red(x)) || xs1.exists(red(x))) irreds(xs, xs1) else irreds(xs, x :: xs1) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/path.scala --- a/src/Pure/General/path.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/General/path.scala Sun May 03 00:01:10 2015 +0200 @@ -18,9 +18,9 @@ /* path elements */ sealed abstract class Elem - private case class Root(val name: String) extends Elem - private case class Basic(val name: String) extends Elem - private case class Variable(val name: String) extends Elem + private case class Root(name: String) extends Elem + private case class Basic(name: String) extends Elem + private case class Variable(name: String) extends Elem private case object Parent extends Elem private def err_elem(msg: String, s: String): Nothing = @@ -30,7 +30,7 @@ if (s == "" || s == "~" || s == "~~") err_elem("Illegal", s) else { "/\\$:\"'".iterator.foreach(c => - if (s.iterator.exists(_ == c)) + if (s.iterator.contains(c)) err_elem("Illegal character " + quote(c.toString) + " in", s)) s } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/General/scan.scala Sun May 03 00:01:10 2015 +0200 @@ -91,7 +91,7 @@ private def quoted_body(quote: Symbol.Symbol): Parser[String] = { rep(many1(sym => sym != quote && sym != "\\") | "\\" + quote | "\\\\" | - (("""\\\d\d\d""".r) ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) + ("""\\\d\d\d""".r ^? { case x if x.substring(1, 4).toInt <= 255 => x })) ^^ (_.mkString) } def quoted(quote: Symbol.Symbol): Parser[String] = @@ -307,7 +307,7 @@ { /* representation */ - private sealed case class Tree(val branches: Map[Char, (String, Tree)]) + private sealed case class Tree(branches: Map[Char, (String, Tree)]) private val empty_tree = Tree(Map()) val empty: Lexicon = new Lexicon(empty_tree) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/General/symbol.scala Sun May 03 00:01:10 2015 +0200 @@ -318,7 +318,7 @@ val names: Map[Symbol, String] = { val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""") - Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*) + Map((for ((sym @ name(a), _) <- symbols) yield sym -> a): _*) } val groups: List[(String, List[Symbol])] = @@ -334,7 +334,7 @@ for { (sym, props) <- symbols ("abbrev", a) <- props.reverse - } yield (sym -> a)): _*) + } yield sym -> a): _*) /* recoding */ @@ -381,7 +381,7 @@ private val Font = new Properties.String("font") val fonts: Map[Symbol, String] = - recode_map((for ((sym, Font(font)) <- symbols) yield (sym -> font)): _*) + 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): _*) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Isar/outer_syntax.scala Sun May 03 00:01:10 2015 +0200 @@ -33,7 +33,7 @@ result += '\\' if (c < 10) result += '0' if (c < 100) result += '0' - result ++= (c.asInstanceOf[Int].toString) + result ++= c.asInstanceOf[Int].toString } else result += c } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Isar/token.scala Sun May 03 00:01:10 2015 +0200 @@ -144,7 +144,7 @@ var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.token_line(keywords, ctxt), in) match { - case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } + 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) } @@ -158,7 +158,7 @@ def implode(toks: List[Token]): String = toks match { case List(tok) => tok.source - case toks => toks.map(_.source).mkString + case _ => toks.map(_.source).mkString } @@ -222,7 +222,7 @@ } -sealed case class Token(val kind: Token.Kind.Value, val source: String) +sealed case class Token(kind: Token.Kind.Value, source: String) { def is_command: Boolean = kind == Token.Kind.COMMAND def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean = diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/ML/ml_lex.scala Sun May 03 00:01:10 2015 +0200 @@ -62,7 +62,7 @@ val ERROR = Value("bad input") } - sealed case class Token(val kind: Kind.Value, val source: String) + sealed case class Token(kind: Kind.Value, source: String) { def is_keyword: Boolean = kind == Kind.KEYWORD def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source) @@ -282,7 +282,7 @@ var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.token_line(SML, ctxt), in) match { - case Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } + 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) } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/command.scala Sun May 03 00:01:10 2015 +0200 @@ -427,7 +427,7 @@ val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] = ((Symbol.Text_Chunk.Default -> chunk) :: (for (Exn.Res((name, Some((_, file)))) <- blobs) - yield (Symbol.Text_Chunk.File(name.node) -> file))).toMap + yield Symbol.Text_Chunk.File(name.node) -> file)).toMap def length: Int = source.length def range: Text.Range = chunk.range diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/document.scala Sun May 03 00:01:10 2015 +0200 @@ -502,21 +502,21 @@ final case class State private( /*reachable versions*/ - val versions: Map[Document_ID.Version, Version] = Map.empty, + versions: Map[Document_ID.Version, Version] = Map.empty, /*inlined auxiliary files*/ - val blobs: Set[SHA1.Digest] = Set.empty, + blobs: Set[SHA1.Digest] = Set.empty, /*static markup from define_command*/ - val commands: Map[Document_ID.Command, Command.State] = Map.empty, + commands: Map[Document_ID.Command, Command.State] = Map.empty, /*dynamic markup from execution*/ - val execs: Map[Document_ID.Exec, Command.State] = Map.empty, + execs: Map[Document_ID.Exec, Command.State] = Map.empty, /*command-exec assignment for each version*/ - val assignments: Map[Document_ID.Version, State.Assignment] = Map.empty, + assignments: Map[Document_ID.Version, State.Assignment] = Map.empty, /*commands with markup produced by other commands (imm_succs)*/ - val commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long, + commands_redirection: Graph[Document_ID.Command, Unit] = Graph.long, /*explicit (linear) history*/ - val history: History = History.init, + history: History = History.init, /*intermediate state between remove_versions/removed_versions*/ - val removing_versions: Boolean = false) + removing_versions: Boolean = false) { private def fail[A]: A = throw new State.Fail(this) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Sun May 03 00:01:10 2015 +0200 @@ -57,7 +57,7 @@ def filter_markup(elements: Markup.Elements): List[XML.Elem] = { var result: List[XML.Elem] = Nil - for { elem <- rev_markup; if (elements(elem.name)) } + for (elem <- rev_markup if elements(elem.name)) result ::= elem result.toList } @@ -267,4 +267,3 @@ case list => list.mkString("Tree(", ",", ")") } } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/prover.scala Sun May 03 00:01:10 2015 +0200 @@ -293,7 +293,7 @@ { val n = read_int() val buf = - if (n <= default_buffer.size) default_buffer + if (n <= default_buffer.length) default_buffer else new Array[Byte](n) var i = 0 @@ -367,4 +367,3 @@ protocol_command_bytes(name, args.map(Bytes(_)): _*) } } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/text.scala Sun May 03 00:01:10 2015 +0200 @@ -34,7 +34,7 @@ } } - sealed case class Range(val start: Offset, val stop: Offset) + sealed case class Range(start: Offset, stop: Offset) { // denotation: {start} Un {i. start < i & i < stop} if (start > stop) @@ -124,7 +124,7 @@ /* information associated with text range */ - sealed case class Info[A](val range: Text.Range, val info: A) + sealed case class Info[A](range: Text.Range, info: A) { def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info) def try_restrict(r: Text.Range): Option[Info[A]] = range.try_restrict(r).map(Info(_, info)) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/PIDE/xml.scala Sun May 03 00:01:10 2015 +0200 @@ -36,9 +36,9 @@ /* wrapped elements */ - val XML_ELEM = "xml_elem"; - val XML_NAME = "xml_name"; - val XML_BODY = "xml_body"; + val XML_ELEM = "xml_elem" + val XML_NAME = "xml_name" + val XML_BODY = "xml_body" object Wrapped_Elem { diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/System/isabelle_process.scala Sun May 03 00:01:10 2015 +0200 @@ -25,7 +25,7 @@ process.stdin.close process } - catch { case exn @ ERROR(_) => system_channel.accepted(); throw(exn) } + catch { case exn @ ERROR(_) => system_channel.accepted(); throw exn } new Isabelle_Process(receiver, system_channel, system_process) } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/System/isabelle_system.scala Sun May 03 00:01:10 2015 +0200 @@ -93,9 +93,9 @@ default( default( default(sys.env + ("ISABELLE_JDK_HOME" -> posix_path(jdk_home())), - ("TEMP_WINDOWS" -> temp_windows)), - ("HOME" -> user_home)), - ("ISABELLE_APP" -> "true")) + "TEMP_WINDOWS" -> temp_windows), + "HOME" -> user_home), + "ISABELLE_APP" -> "true") } val system_home = @@ -125,8 +125,8 @@ val entries = (for (entry <- File.read(dump) split "\u0000" if entry != "") yield { val i = entry.indexOf('=') - if (i <= 0) (entry -> "") - else (entry.substring(0, i) -> entry.substring(i + 1)) + if (i <= 0) entry -> "" + else entry.substring(0, i) -> entry.substring(i + 1) }).toMap entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM" } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/System/options.scala Sun May 03 00:01:10 2015 +0200 @@ -368,7 +368,7 @@ (for { (name, opt2) <- options.iterator opt1 = defaults.options.get(name) - if (opt1.isEmpty || opt1.get.value != opt2.value) + if opt1.isEmpty || opt1.get.value != opt2.value } yield (name, opt2.value, if (opt1.isEmpty) " (* unknown *)" else "")).toList val prefs = @@ -429,4 +429,3 @@ } val seconds = new Seconds_Access } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Thy/html.scala Sun May 03 00:01:10 2015 +0200 @@ -28,7 +28,7 @@ case '"' => result ++= """ case '\'' => result ++= "'" case '\n' => result ++= "
" - case c => result += c + case _ => result += c } def encode_chars(s: String) = s.iterator.foreach(encode_char(_)) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Thy/thy_header.scala Sun May 03 00:01:10 2015 +0200 @@ -100,7 +100,7 @@ val args = position(theory_name) ~ - (opt($$$(IMPORTS) ~! (rep1(position(theory_xname)))) ^^ + (opt($$$(IMPORTS) ~! rep1(position(theory_xname))) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ (opt($$$(KEYWORDS) ~! keyword_decls) ^^ { case None => Nil case Some(_ ~ xs) => xs }) ~ diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Sun May 03 00:01:10 2015 +0200 @@ -339,7 +339,7 @@ node2, (name, node2.edit_perspective)) else node2 - if (!(node.same_perspective(node3.text_perspective, node3.perspective))) + if (!node.same_perspective(node3.text_perspective, node3.perspective)) doc_edits += (name -> node3.perspective) doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands))) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Tools/bibtex.scala Sun May 03 00:01:10 2015 +0200 @@ -133,7 +133,7 @@ } } - sealed case class Token(kind: Token.Kind.Value, val source: String) + sealed case class Token(kind: Token.Kind.Value, source: String) { def is_kind: Boolean = kind == Token.Kind.COMMAND || @@ -398,7 +398,7 @@ var ctxt = context while (!in.atEnd) { Parsers.parse(Parsers.chunk_line(ctxt), in) match { - case Parsers.Success((x, c), rest) => { chunks += x; ctxt = c; in = rest } + 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) } @@ -406,4 +406,3 @@ (chunks.toList, ctxt) } } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/Tools/build.scala Sun May 03 00:01:10 2015 +0200 @@ -908,7 +908,7 @@ loop(pending - name, running - name, results + (name -> Result(false, heap, res.rc))) //}}} - case None if (running.size < (max_jobs max 1)) => + case None if running.size < (max_jobs max 1) => //{{{ check/start next job pending.dequeue(running.isDefinedAt(_)) match { case Some((name, info)) => diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Pure/library.scala --- a/src/Pure/library.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Pure/library.scala Sun May 03 00:01:10 2015 +0200 @@ -107,7 +107,7 @@ def hasNext(): Boolean = state.isDefined def next(): CharSequence = state match { - case Some((s, i)) => { state = next_chunk(i); s } + case Some((s, i)) => state = next_chunk(i); s case None => Iterator.empty.next() } } @@ -207,7 +207,7 @@ /* canonical list operations */ - def member[A, B](xs: List[A])(x: B): Boolean = xs.exists(_ == x) + def member[A, B](xs: List[A])(x: B): Boolean = xs.contains(x) def insert[A](x: A)(xs: List[A]): List[A] = if (xs.contains(x)) xs else x :: xs def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs) diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/Graphview/shapes.scala --- a/src/Tools/Graphview/shapes.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/Graphview/shapes.scala Sun May 03 00:01:10 2015 +0200 @@ -163,7 +163,7 @@ val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0) var p1 = (0.0, 0.0) var p2 = (0.0, 0.0) - while (!i.isDone()) { + while (!i.isDone) { i.currentSegment(seg) match { case PathIterator.SEG_MOVETO => p2 = (seg(0), seg(1)) case PathIterator.SEG_LINETO => @@ -223,4 +223,4 @@ } } } -} \ No newline at end of file +} diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/active.scala --- a/src/Tools/jEdit/src/active.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/active.scala Sun May 03 00:01:10 2015 +0200 @@ -61,9 +61,9 @@ props match { case Position.Id(id) => Isabelle.edit_command(snapshot, buffer, - props.exists(_ == Markup.PADDING_COMMAND), id, text) + props.contains(Markup.PADDING_COMMAND), id, text) case _ => - if (props.exists(_ == Markup.PADDING_LINE)) + if (props.contains(Markup.PADDING_LINE)) Isabelle.insert_line_padding(text_area, text) else text_area.setSelectedText(text) } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sun May 03 00:01:10 2015 +0200 @@ -252,11 +252,11 @@ val label_html = "" + HTML.encode(kind) + "" + (if (name == "") "" else " " + HTML.encode(name)) + "" - val range = Text.Range(offset, offset + source.size) + val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) data.root.add(new DefaultMutableTreeNode(asset)) } - offset += source.size + offset += source.length } data } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/graphview_dockable.scala --- a/src/Tools/jEdit/src/graphview_dockable.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun May 03 00:01:10 2015 +0200 @@ -117,13 +117,13 @@ override def init() { - GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener)) + GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener)) PIDE.session.global_options += main } override def exit() { - GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener)) + GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener)) PIDE.session.global_options -= main } } diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sun May 03 00:01:10 2015 +0200 @@ -230,7 +230,7 @@ /* graphics range */ - case class Gfx_Range(val x: Int, val y: Int, val length: Int) + case class Gfx_Range(x: Int, y: Int, length: Int) // NB: jEdit always normalizes \r\n and \r to \n // NB: last line lacks \n @@ -274,7 +274,7 @@ if (offset >= 0) { val range = point_range(text_area.getBuffer, offset) gfx_range(text_area, range) match { - case Some(g) if (g.x <= x && x < g.x + g.length) => Some(range) + case Some(g) if g.x <= x && x < g.x + g.length => Some(range) case _ => None } } @@ -371,4 +371,3 @@ (mod & InputEvent.META_MASK) != 0 } } - diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sun May 03 00:01:10 2015 +0200 @@ -332,10 +332,10 @@ } case msg: EditPaneUpdate - if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || + if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || msg.getWhat == EditPaneUpdate.CREATED || - msg.getWhat == EditPaneUpdate.DESTROYED) => + msg.getWhat == EditPaneUpdate.DESTROYED => val edit_pane = msg.getEditPane val buffer = edit_pane.getBuffer val text_area = edit_pane.getTextArea diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Sun May 03 00:01:10 2015 +0200 @@ -407,7 +407,7 @@ PIDE.editor.hyperlink_command_id(snapshot, id, offset) case _ => None } - opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) + opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => val opt_link = @@ -419,14 +419,14 @@ PIDE.editor.hyperlink_command_id(snapshot, id, offset) case _ => None } - opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) + opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => val opt_link = Bibtex_JEdit.entries_iterator.collectFirst( { case (a, buffer, offset) if a == name => PIDE.editor.hyperlink_buffer(buffer, offset) }) - opt_link.map(link => (links :+ Text.Info(snapshot.convert(info_range), link))) + opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case _ => None }) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None } @@ -472,7 +472,7 @@ case (msgs, Text.Info(info_range, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) => val entry: Command.Results.Entry = - (serial -> XML.Elem(Markup(Markup.message(name), props), body)) + serial -> XML.Elem(Markup(Markup.message(name), props), body) Some(Text.Info(snapshot.convert(info_range), entry) :: msgs) case _ => None diff -r 0b7656c5f0e9 -r 5fb4990dfc73 src/Tools/jEdit/src/rich_text_area.scala --- a/src/Tools/jEdit/src/rich_text_area.scala Fri May 01 15:33:43 2015 +0200 +++ b/src/Tools/jEdit/src/rich_text_area.scala Sun May 03 00:01:10 2015 +0200 @@ -284,7 +284,7 @@ for { (color, separator) <- rendering.line_background(line_range) } { gfx.setColor(color) - val sep = if (separator) (2 min (line_height / 2)) else 0 + val sep = if (separator) 2 min (line_height / 2) else 0 gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep) } @@ -659,4 +659,3 @@ painter.removeExtension(set_state) } } -