--- 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)
}
-
--- 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)
})
}
--- 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)
--- 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
}
--- 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)
--- 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): _*)
--- 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
}
--- 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 =
--- 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)
}
--- 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
--- 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)
--- 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(", ",", ")")
}
}
-
--- 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(_)): _*)
}
}
-
--- 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))
--- 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
{
--- 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)
}
--- 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"
}
--- 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
}
-
--- 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 ++= "<br/>"
- case c => result += c
+ case _ => result += c
}
def encode_chars(s: String) = s.iterator.foreach(encode_char(_))
--- 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 }) ~
--- 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)))
--- 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)
}
}
-
--- 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)) =>
--- 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)
--- 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
+}
--- 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)
}
--- 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><b>" + HTML.encode(kind) + "</b>" +
(if (name == "") "" else " " + HTML.encode(name)) + "</html>"
- 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
}
--- 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
}
}
--- 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
}
}
-
--- 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
--- 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
--- 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)
}
}
-