# HG changeset patch
# User wenzelm
# Date 1489525559 -3600
# Node ID fef7b7a9e5b08287bf49569e2e997c4dd188ace1
# Parent  63d91d5de121fa6e95d2a0ac5f620d9d1c67814c
tuned;

diff -r 63d91d5de121 -r fef7b7a9e5b0 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:54:46 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 22:05:59 2017 +0100
@@ -13,12 +13,8 @@
 
 import java.io.{File => JFile}
 
-import scala.swing.{ListView, ScrollPane}
-
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager}
-import org.gjt.sp.jedit.gui.AboutDialog
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.syntax.ModeProvider
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.util.SyntaxUtilities
@@ -42,7 +38,7 @@
     session.resources.asInstanceOf[JEdit_Resources]
 
 
-  /* current document content */
+  /* semantic document content */
 
   def snapshot(view: View): Document.Snapshot = GUI_Thread.now
   {