src/Tools/jEdit/src/plugin.scala
changeset 43714 3749d1e6dde9
parent 43697 77ce24aa1770
child 44160 8848867501fb
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Jul 08 22:00:53 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 09 12:56:51 2011 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4  
     1.5    /* text area ranges */
     1.6  
     1.7 -  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
     1.8 +  sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int)
     1.9  
    1.10    def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    1.11    {