tuned signature;
authorwenzelm
Sat Jul 09 12:56:51 2011 +0200 (2011-07-09 ago)
changeset 437143749d1e6dde9
parent 43713 1ba5331b4623
child 43715 518e44a0ee15
tuned signature;
src/Pure/General/pretty.scala
src/Pure/General/sha1.scala
src/Pure/General/symbol.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/text.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Pure/General/pretty.scala	Fri Jul 08 22:00:53 2011 +0200
     1.2 +++ b/src/Pure/General/pretty.scala	Sat Jul 09 12:56:51 2011 +0200
     1.3 @@ -53,7 +53,7 @@
     1.4            Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     1.5      }
     1.6  
     1.7 -  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
     1.8 +  sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
     1.9    {
    1.10      def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
    1.11      def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
     2.1 --- a/src/Pure/General/sha1.scala	Fri Jul 08 22:00:53 2011 +0200
     2.2 +++ b/src/Pure/General/sha1.scala	Sat Jul 09 12:56:51 2011 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  
     2.5  object SHA1
     2.6  {
     2.7 -  case class Digest(rep: String)
     2.8 +  sealed case class Digest(rep: String)
     2.9    {
    2.10      override def toString: String = rep
    2.11    }
     3.1 --- a/src/Pure/General/symbol.scala	Fri Jul 08 22:00:53 2011 +0200
     3.2 +++ b/src/Pure/General/symbol.scala	Sat Jul 09 12:56:51 2011 +0200
     3.3 @@ -120,7 +120,7 @@
     3.4  
     3.5    class Index(text: CharSequence)
     3.6    {
     3.7 -    case class Entry(chr: Int, sym: Int)
     3.8 +    sealed case class Entry(chr: Int, sym: Int)
     3.9      val index: Array[Entry] =
    3.10      {
    3.11        val matcher = new Matcher(text)
     4.1 --- a/src/Pure/PIDE/command.scala	Fri Jul 08 22:00:53 2011 +0200
     4.2 +++ b/src/Pure/PIDE/command.scala	Sat Jul 09 12:56:51 2011 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4  {
     4.5    /** accumulated results from prover **/
     4.6  
     4.7 -  case class State(
     4.8 +  sealed case class State(
     4.9      val command: Command,
    4.10      val status: List[Markup] = Nil,
    4.11      val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
     5.1 --- a/src/Pure/PIDE/markup_tree.scala	Fri Jul 08 22:00:53 2011 +0200
     5.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 09 12:56:51 2011 +0200
     5.3 @@ -48,7 +48,7 @@
     5.4  }
     5.5  
     5.6  
     5.7 -case class Markup_Tree(val branches: Markup_Tree.Branches.T)
     5.8 +sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
     5.9  {
    5.10    import Markup_Tree._
    5.11  
     6.1 --- a/src/Pure/PIDE/text.scala	Fri Jul 08 22:00:53 2011 +0200
     6.2 +++ b/src/Pure/PIDE/text.scala	Sat Jul 09 12:56:51 2011 +0200
     6.3 @@ -52,7 +52,7 @@
     6.4  
     6.5    /* information associated with text range */
     6.6  
     6.7 -  case class Info[A](val range: Text.Range, val info: A)
     6.8 +  sealed case class Info[A](val range: Text.Range, val info: A)
     6.9    {
    6.10      def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
    6.11      def try_restrict(r: Text.Range): Option[Info[A]] =
     7.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Jul 08 22:00:53 2011 +0200
     7.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 09 12:56:51 2011 +0200
     7.3 @@ -105,7 +105,7 @@
     7.4  
     7.5    /* text area ranges */
     7.6  
     7.7 -  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
     7.8 +  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
     7.9  
    7.10    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    7.11    {