tuned;
authorwenzelm
Tue Aug 12 15:46:20 2014 +0200 (2014-08-12)
changeset 57912dd9550f84106
parent 57911 dcb758188aa6
child 57913 8544ef75d1d8
tuned;
src/Pure/Concurrent/future.scala
src/Pure/General/time.scala
src/Pure/General/timing.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/xml.scala
src/Tools/jEdit/src/documentation_dockable.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
     1.1 --- a/src/Pure/Concurrent/future.scala	Tue Aug 12 15:31:24 2014 +0200
     1.2 +++ b/src/Pure/Concurrent/future.scala	Tue Aug 12 15:46:20 2014 +0200
     1.3 @@ -37,7 +37,7 @@
     1.4    def join: A
     1.5    def map[B](f: A => B): Future[B] = Future.fork { f(join) }
     1.6  
     1.7 -  override def toString =
     1.8 +  override def toString: String =
     1.9      peek match {
    1.10        case None => "<future>"
    1.11        case Some(Exn.Exn(_)) => "<failed>"
     2.1 --- a/src/Pure/General/time.scala	Tue Aug 12 15:31:24 2014 +0200
     2.2 +++ b/src/Pure/General/time.scala	Tue Aug 12 15:46:20 2014 +0200
     2.3 @@ -40,7 +40,7 @@
     2.4    def is_zero: Boolean = ms == 0
     2.5    def is_relevant: Boolean = ms >= 1
     2.6  
     2.7 -  override def toString = Time.print_seconds(seconds)
     2.8 +  override def toString: String = Time.print_seconds(seconds)
     2.9  
    2.10    def message: String = toString + "s"
    2.11  }
     3.1 --- a/src/Pure/General/timing.scala	Tue Aug 12 15:31:24 2014 +0200
     3.2 +++ b/src/Pure/General/timing.scala	Tue Aug 12 15:46:20 2014 +0200
     3.3 @@ -38,6 +38,6 @@
     3.4    def message: String =
     3.5      elapsed.message + " elapsed time, " + cpu.message + " cpu time, " + gc.message + " GC time"
     3.6  
     3.7 -  override def toString = message
     3.8 +  override def toString: String = message
     3.9  }
    3.10  
     4.1 --- a/src/Pure/PIDE/command.scala	Tue Aug 12 15:31:24 2014 +0200
     4.2 +++ b/src/Pure/PIDE/command.scala	Tue Aug 12 15:46:20 2014 +0200
     4.3 @@ -325,7 +325,7 @@
     4.4    def position: Position.T =
     4.5      span.kind match { case Command_Span.Command_Span(_, pos) => pos case _ => Position.none }
     4.6  
     4.7 -  override def toString = id + "/" + span.kind.toString
     4.8 +  override def toString: String = id + "/" + span.kind.toString
     4.9  
    4.10  
    4.11    /* classification */
     5.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Aug 12 15:31:24 2014 +0200
     5.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Aug 12 15:46:20 2014 +0200
     5.3 @@ -261,7 +261,7 @@
     5.4     make_body(root_range, Nil, overlapping(root_range))
     5.5    }
     5.6  
     5.7 -  override def toString =
     5.8 +  override def toString: String =
     5.9      branches.toList.map(_._2) match {
    5.10        case Nil => "Empty"
    5.11        case list => list.mkString("Tree(", ",", ")")
     6.1 --- a/src/Pure/PIDE/text.scala	Tue Aug 12 15:31:24 2014 +0200
     6.2 +++ b/src/Pure/PIDE/text.scala	Tue Aug 12 15:46:20 2014 +0200
     6.3 @@ -40,7 +40,7 @@
     6.4      if (start > stop)
     6.5        error("Bad range: [" + start.toString + ":" + stop.toString + "]")
     6.6  
     6.7 -    override def toString = "[" + start.toString + ":" + stop.toString + "]"
     6.8 +    override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
     6.9  
    6.10      def length: Int = stop - start
    6.11  
    6.12 @@ -116,7 +116,7 @@
    6.13          case other: Perspective => ranges == other.ranges
    6.14          case _ => false
    6.15        }
    6.16 -    override def toString = ranges.toString
    6.17 +    override def toString: String = ranges.toString
    6.18    }
    6.19  
    6.20  
    6.21 @@ -141,7 +141,7 @@
    6.22  
    6.23    final class Edit private(val is_insert: Boolean, val start: Offset, val text: String)
    6.24    {
    6.25 -    override def toString =
    6.26 +    override def toString: String =
    6.27        (if (is_insert) "Insert(" else "Remove(") + (start, text).toString + ")"
    6.28  
    6.29  
     7.1 --- a/src/Pure/PIDE/xml.scala	Tue Aug 12 15:31:24 2014 +0200
     7.2 +++ b/src/Pure/PIDE/xml.scala	Tue Aug 12 15:46:20 2014 +0200
     7.3 @@ -21,7 +21,7 @@
     7.4  
     7.5    type Attributes = Properties.T
     7.6  
     7.7 -  sealed abstract class Tree { override def toString = string_of_tree(this) }
     7.8 +  sealed abstract class Tree { override def toString: String = string_of_tree(this) }
     7.9    case class Elem(markup: Markup, body: List[Tree]) extends Tree
    7.10    {
    7.11      def name: String = markup.name
     8.1 --- a/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 15:31:24 2014 +0200
     8.2 +++ b/src/Tools/jEdit/src/documentation_dockable.scala	Tue Aug 12 15:46:20 2014 +0200
     8.3 @@ -24,13 +24,13 @@
     8.4  
     8.5    private case class Documentation(name: String, title: String, path: Path)
     8.6    {
     8.7 -    override def toString =
     8.8 +    override def toString: String =
     8.9        "<html><b>" + HTML.encode(name) + "</b>:  " + HTML.encode(title) + "</html>"
    8.10    }
    8.11  
    8.12    private case class Text_File(name: String, path: Path)
    8.13    {
    8.14 -    override def toString = name
    8.15 +    override def toString: String = name
    8.16    }
    8.17  
    8.18    private val root = new DefaultMutableTreeNode
     9.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Tue Aug 12 15:31:24 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Tue Aug 12 15:46:20 2014 +0200
     9.3 @@ -24,7 +24,7 @@
     9.4  
     9.5    private class Logic_Entry(val name: String, val description: String)
     9.6    {
     9.7 -    override def toString = description
     9.8 +    override def toString: String = description
     9.9    }
    9.10  
    9.11    def logic_selector(autosave: Boolean): Option_Component =
    10.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 12 15:31:24 2014 +0200
    10.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Tue Aug 12 15:46:20 2014 +0200
    10.3 @@ -21,7 +21,7 @@
    10.4  object Isabelle_Sidekick
    10.5  {
    10.6    def int_to_pos(offset: Text.Offset): Position =
    10.7 -    new Position { def getOffset = offset; override def toString = offset.toString }
    10.8 +    new Position { def getOffset = offset; override def toString: String = offset.toString }
    10.9  
   10.10    class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
   10.11    {
   10.12 @@ -39,7 +39,7 @@
   10.13      override def setStart(start: Position) = _start = start
   10.14      override def getEnd: Position = _end
   10.15      override def setEnd(end: Position) = _end = end
   10.16 -    override def toString = _name
   10.17 +    override def toString: String = _name
   10.18    }
   10.19  
   10.20    def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
   10.21 @@ -173,7 +173,7 @@
   10.22                    new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
   10.23                      override def getShortString: String = content
   10.24                      override def getLongString: String = info_text
   10.25 -                    override def toString = quote(content) + " " + range.toString
   10.26 +                    override def toString: String = quote(content) + " " + range.toString
   10.27                    })
   10.28                })
   10.29          }