# HG changeset patch
# User wenzelm
# Date 1590148399 -7200
# Node ID e95ea6956df39d30eafdfd0c20d14f5680245b9c
# Parent  8bbadb065ebe7ea2fdbaac94862da9687fdd903f
unused;

diff -r 8bbadb065ebe -r e95ea6956df3 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri May 22 12:18:09 2020 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri May 22 13:53:19 2020 +0200
@@ -10,15 +10,9 @@
 import isabelle._
 
 import console.{Console, ConsolePane, Shell, Output}
-
-import org.gjt.sp.jedit.{jEdit, JARClassLoader}
-import org.gjt.sp.jedit.MiscUtilities
-
-import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
-
-import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
+import org.gjt.sp.jedit.JARClassLoader
+import java.io.{OutputStream, Writer, PrintWriter}
 import scala.tools.nsc.interpreter.IMain
-import scala.collection.mutable
 
 
 class Scala_Console extends Shell("Scala")