# HG changeset patch
# User wenzelm
# Date 1310209011 -7200
# Node ID 3749d1e6dde9be213a81f4fb89f93873738aad7f
# Parent  1ba5331b462384d38771d7fe964bcc5fd56c7f06
tuned signature;

diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/General/pretty.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -53,7 +53,7 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
+  sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/General/sha1.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -12,7 +12,7 @@
 
 object SHA1
 {
-  case class Digest(rep: String)
+  sealed case class Digest(rep: String)
   {
     override def toString: String = rep
   }
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/General/symbol.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -120,7 +120,7 @@
 
   class Index(text: CharSequence)
   {
-    case class Entry(chr: Int, sym: Int)
+    sealed case class Entry(chr: Int, sym: Int)
     val index: Array[Entry] =
     {
       val matcher = new Matcher(text)
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -16,7 +16,7 @@
 {
   /** accumulated results from prover **/
 
-  case class State(
+  sealed case class State(
     val command: Command,
     val status: List[Markup] = Nil,
     val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -48,7 +48,7 @@
 }
 
 
-case class Markup_Tree(val branches: Markup_Tree.Branches.T)
+sealed case class Markup_Tree(val branches: Markup_Tree.Branches.T)
 {
   import Markup_Tree._
 
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -52,7 +52,7 @@
 
   /* information associated with text range */
 
-  case class Info[A](val range: Text.Range, val info: A)
+  sealed case class Info[A](val range: Text.Range, val info: A)
   {
     def restrict(r: Text.Range): Info[A] = Info(range.restrict(r), info)
     def try_restrict(r: Text.Range): Option[Info[A]] =
diff -r 1ba5331b4623 -r 3749d1e6dde9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Jul 08 22:00:53 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 09 12:56:51 2011 +0200
@@ -105,7 +105,7 @@
 
   /* text area ranges */
 
-  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
+  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
 
   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
   {