# HG changeset patch # User wenzelm # Date 1407851180 -7200 # Node ID dd9550f8410651520faf919c50a46b849b6c0e83 # Parent dcb758188aa6e5d2e86e859a2f7c4872634dac06 tuned; diff -r dcb758188aa6 -r dd9550f84106 src/Pure/Concurrent/future.scala --- a/src/Pure/Concurrent/future.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/Concurrent/future.scala Tue Aug 12 15:46:20 2014 +0200 @@ -37,7 +37,7 @@ def join: A def map[B](f: A => B): Future[B] = Future.fork { f(join) } - override def toString = + override def toString: String = peek match { case None => "" case Some(Exn.Exn(_)) => "" diff -r dcb758188aa6 -r dd9550f84106 src/Pure/General/time.scala --- a/src/Pure/General/time.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/General/time.scala Tue Aug 12 15:46:20 2014 +0200 @@ -40,7 +40,7 @@ def is_zero: Boolean = ms == 0 def is_relevant: Boolean = ms >= 1 - override def toString = Time.print_seconds(seconds) + override def toString: String = Time.print_seconds(seconds) def message: String = toString + "s" } diff -r dcb758188aa6 -r dd9550f84106 src/Pure/General/timing.scala --- a/src/Pure/General/timing.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/General/timing.scala Tue Aug 12 15:46:20 2014 +0200 @@ -38,6 +38,6 @@ def message: String = elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time" - override def toString = message + override def toString: String = message } diff -r dcb758188aa6 -r dd9550f84106 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/command.scala Tue Aug 12 15:46:20 2014 +0200 @@ -325,7 +325,7 @@ def position: Position.T = span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none } - override def toString = id + "/" + span.kind.toString + override def toString: String = id + "/" + span.kind.toString /* classification */ diff -r dcb758188aa6 -r dd9550f84106 src/Pure/PIDE/markup_tree.scala --- a/src/Pure/PIDE/markup_tree.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/markup_tree.scala Tue Aug 12 15:46:20 2014 +0200 @@ -261,7 +261,7 @@ make_body(root_range, Nil, overlapping(root_range)) } - override def toString = + override def toString: String = branches.toList.map(_._2) match { case Nil => "Empty" case list => list.mkString("Tree(", ",", ")") diff -r dcb758188aa6 -r dd9550f84106 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/text.scala Tue Aug 12 15:46:20 2014 +0200 @@ -40,7 +40,7 @@ if (start > stop) error("Bad range: [" + start.toString + ":" + stop.toString + "]") - override def toString = "[" + start.toString + ":" + stop.toString + "]" + override def toString: String = "[" + start.toString + ":" + stop.toString + "]" def length: Int = stop - start @@ -116,7 +116,7 @@ case other: Perspective => ranges == other.ranges case _ => false } - override def toString = ranges.toString + override def toString: String = ranges.toString } @@ -141,7 +141,7 @@ final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) { - override def toString = + override def toString: String = (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")" diff -r dcb758188aa6 -r dd9550f84106 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Pure/PIDE/xml.scala Tue Aug 12 15:46:20 2014 +0200 @@ -21,7 +21,7 @@ type Attributes = Properties.T - sealed abstract class Tree { override def toString = string_of_tree(this) } + sealed abstract class Tree { override def toString: String = string_of_tree(this) } case class Elem(markup: Markup, body: List[Tree]) extends Tree { def name: String = markup.name diff -r dcb758188aa6 -r dd9550f84106 src/Tools/jEdit/src/documentation_dockable.scala --- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Aug 12 15:46:20 2014 +0200 @@ -24,13 +24,13 @@ private case class Documentation(name: String, title: String, path: Path) { - override def toString = + override def toString: String = "" + HTML.encode(name) + ": " + HTML.encode(title) + "" } private case class Text_File(name: String, path: Path) { - override def toString = name + override def toString: String = name } private val root = new DefaultMutableTreeNode diff -r dcb758188aa6 -r dd9550f84106 src/Tools/jEdit/src/isabelle_logic.scala --- a/src/Tools/jEdit/src/isabelle_logic.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Tue Aug 12 15:46:20 2014 +0200 @@ -24,7 +24,7 @@ private class Logic_Entry(val name: String, val description: String) { - override def toString = description + override def toString: String = description } def logic_selector(autosave: Boolean): Option_Component = diff -r dcb758188aa6 -r dd9550f84106 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 12 15:31:24 2014 +0200 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Tue Aug 12 15:46:20 2014 +0200 @@ -21,7 +21,7 @@ object Isabelle_Sidekick { def int_to_pos(offset: Text.Offset): Position = - new Position { def getOffset = offset; override def toString = offset.toString } + new Position { def getOffset = offset; override def toString: String = offset.toString } class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset { @@ -39,7 +39,7 @@ override def setStart(start: Position) = _start = start override def getEnd: Position = _end override def setEnd(end: Position) = _end = end - override def toString = _name + override def toString: String = _name } def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode, @@ -173,7 +173,7 @@ new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { override def getShortString: String = content override def getLongString: String = info_text - override def toString = quote(content) + " " + range.toString + override def toString: String = quote(content) + " " + range.toString }) }) }