# HG changeset patch
# User wenzelm
# Date 1348568278 -7200
# Node ID c3a6e110679b15bb41abdb84eae1ae9c71c3d650
# Parent  af7b652180d50aa4bd5e27c085f360f9a65a288c
tuned;

diff -r af7b652180d5 -r c3a6e110679b src/Tools/jEdit/src/raw_output_dockable.scala
--- 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))
diff -r af7b652180d5 -r c3a6e110679b src/Tools/jEdit/src/readme_dockable.scala
--- 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")
diff -r af7b652180d5 -r c3a6e110679b src/Tools/jEdit/src/session_dockable.scala
--- 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 */
 
diff -r af7b652180d5 -r c3a6e110679b src/Tools/jEdit/src/syslog_dockable.scala
--- 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)
       }
     }
   }