src/Tools/jEdit/src/document_view.scala
changeset 54441 3d37b2957a3e
parent 54325 2c4155003352
child 54461 6c360a6ade0e
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 14 17:17:57 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu Nov 14 17:39:32 2013 +0100
     1.3 @@ -10,21 +10,15 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.collection.mutable
     1.8 -import scala.collection.immutable.SortedMap
     1.9  import scala.actors.Actor._
    1.10  
    1.11 -import java.lang.System
    1.12 -import java.text.BreakIterator
    1.13 -import java.awt.{Color, Graphics2D, Point}
    1.14 +import java.awt.Graphics2D
    1.15  import java.awt.event.KeyEvent
    1.16  import javax.swing.event.{CaretListener, CaretEvent}
    1.17  
    1.18 -import org.gjt.sp.jedit.{jEdit, Debug}
    1.19 -import org.gjt.sp.jedit.gui.RolloverButton
    1.20 +import org.gjt.sp.jedit.jEdit
    1.21  import org.gjt.sp.jedit.options.GutterOptionPane
    1.22 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    1.23 -import org.gjt.sp.jedit.syntax.SyntaxStyle
    1.24 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
    1.25  
    1.26  
    1.27  object Document_View
    1.28 @@ -244,7 +238,8 @@
    1.29              }
    1.30            }
    1.31  
    1.32 -        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
    1.33 +        case bad =>
    1.34 +          java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
    1.35        }
    1.36      }
    1.37    }