--- a/src/Tools/jEdit/src/raw_output_dockable.scala Mon Sep 24 21:16:33 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Tue Sep 25 12:17:58 2012 +0200
@@ -17,8 +17,7 @@
import org.gjt.sp.jedit.View
-class Raw_Output_Dockable(view: View, position: String)
- extends Dockable(view: View, position: String)
+class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val text_area = new TextArea
set_content(new ScrollPane(text_area))
--- a/src/Tools/jEdit/src/readme_dockable.scala Mon Sep 24 21:16:33 2012 +0200
+++ b/src/Tools/jEdit/src/readme_dockable.scala Tue Sep 25 12:17:58 2012 +0200
@@ -12,7 +12,7 @@
import org.gjt.sp.jedit.View
-class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class README_Dockable(view: View, position: String) extends Dockable(view, position)
{
private val readme = new HTML_Panel("SansSerif", 14)
private val readme_path = Path.explode("$JEDIT_HOME/README.html")
--- a/src/Tools/jEdit/src/session_dockable.scala Mon Sep 24 21:16:33 2012 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala Tue Sep 25 12:17:58 2012 +0200
@@ -21,7 +21,7 @@
import org.gjt.sp.jedit.{View, jEdit}
-class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class Session_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* status */
--- a/src/Tools/jEdit/src/syslog_dockable.scala Mon Sep 24 21:16:33 2012 +0200
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Tue Sep 25 12:17:58 2012 +0200
@@ -12,12 +12,10 @@
import scala.actors.Actor._
import scala.swing.TextArea
-import java.lang.System
-
import org.gjt.sp.jedit.View
-class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
+class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* GUI components */
@@ -42,7 +40,7 @@
case output: Isabelle_Process.Output =>
if (output.is_syslog) update_syslog()
- case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
+ case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
}
}
}