# HG changeset patch
# User wenzelm
# Date 1384447172 -3600
# Node ID 3d37b2957a3ea80dbee796518c4ede0e2fe7c5dd
# Parent  2c4940d2edf7aebbac9dbdb269d541fc3dab64bf
tuned imports;

diff -r 2c4940d2edf7 -r 3d37b2957a3e src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Nov 14 17:17:57 2013 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Nov 14 17:39:32 2013 +0100
@@ -14,9 +14,6 @@
 
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.textarea.TextArea
-
-import java.awt.font.TextAttribute
 
 
 object Document_Model
diff -r 2c4940d2edf7 -r 3d37b2957a3e src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Nov 14 17:17:57 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Nov 14 17:39:32 2013 +0100
@@ -10,21 +10,15 @@
 
 import isabelle._
 
-import scala.collection.mutable
-import scala.collection.immutable.SortedMap
 import scala.actors.Actor._
 
-import java.lang.System
-import java.text.BreakIterator
-import java.awt.{Color, Graphics2D, Point}
+import java.awt.Graphics2D
 import java.awt.event.KeyEvent
 import javax.swing.event.{CaretListener, CaretEvent}
 
-import org.gjt.sp.jedit.{jEdit, Debug}
-import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
-import org.gjt.sp.jedit.syntax.SyntaxStyle
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
 
 
 object Document_View
@@ -244,7 +238,8 @@
             }
           }
 
-        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
+        case bad =>
+          java.lang.System.err.println("command_change_actor: ignoring bad message " + bad)
       }
     }
   }