tuned;
authorwenzelm
Tue Sep 25 12:17:58 2012 +0200 (2012-09-25)
changeset 49559c3a6e110679b
parent 49558 af7b652180d5
child 49560 11430dd89e35
tuned;
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/readme_dockable.scala
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Mon Sep 24 21:16:33 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Tue Sep 25 12:17:58 2012 +0200
     1.3 @@ -17,8 +17,7 @@
     1.4  import org.gjt.sp.jedit.View
     1.5  
     1.6  
     1.7 -class Raw_Output_Dockable(view: View, position: String)
     1.8 -  extends Dockable(view: View, position: String)
     1.9 +class Raw_Output_Dockable(view: View, position: String) extends Dockable(view, position)
    1.10  {
    1.11    private val text_area = new TextArea
    1.12    set_content(new ScrollPane(text_area))
     2.1 --- a/src/Tools/jEdit/src/readme_dockable.scala	Mon Sep 24 21:16:33 2012 +0200
     2.2 +++ b/src/Tools/jEdit/src/readme_dockable.scala	Tue Sep 25 12:17:58 2012 +0200
     2.3 @@ -12,7 +12,7 @@
     2.4  import org.gjt.sp.jedit.View
     2.5  
     2.6  
     2.7 -class README_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
     2.8 +class README_Dockable(view: View, position: String) extends Dockable(view, position)
     2.9  {
    2.10    private val readme = new HTML_Panel("SansSerif", 14)
    2.11    private val readme_path = Path.explode("$JEDIT_HOME/README.html")
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Mon Sep 24 21:16:33 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 25 12:17:58 2012 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4  import org.gjt.sp.jedit.{View, jEdit}
     3.5  
     3.6  
     3.7 -class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
     3.8 +class Session_Dockable(view: View, position: String) extends Dockable(view, position)
     3.9  {
    3.10    /* status */
    3.11  
     4.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Mon Sep 24 21:16:33 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Tue Sep 25 12:17:58 2012 +0200
     4.3 @@ -12,12 +12,10 @@
     4.4  import scala.actors.Actor._
     4.5  import scala.swing.TextArea
     4.6  
     4.7 -import java.lang.System
     4.8 -
     4.9  import org.gjt.sp.jedit.View
    4.10  
    4.11  
    4.12 -class Syslog_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
    4.13 +class Syslog_Dockable(view: View, position: String) extends Dockable(view, position)
    4.14  {
    4.15    /* GUI components */
    4.16  
    4.17 @@ -42,7 +40,7 @@
    4.18          case output: Isabelle_Process.Output =>
    4.19            if (output.is_syslog) update_syslog()
    4.20  
    4.21 -        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    4.22 +        case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    4.23        }
    4.24      }
    4.25    }