# HG changeset patch
# User wenzelm
# Date 1260310559 -3600
# Node ID b63a88e2d75ab23160adcfbe48a665aab3e29361
# Parent  0c630c52fc7498822365b9392d1839086e4ae3a5
misc tuning;

diff -r 0c630c52fc74 -r b63a88e2d75a src/Tools/jEdit/src/jedit/results_dockable.scala
--- a/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 22:38:32 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/results_dockable.scala	Tue Dec 08 23:15:59 2009 +0100
@@ -9,7 +9,6 @@
 
 import isabelle.proofdocument.{Command, HTML_Panel}
 
-import scala.io.Source
 import scala.actors.Actor._
 
 import javax.swing.JPanel
@@ -22,14 +21,15 @@
 
 class Results_Dockable(view: View, position: String) extends JPanel
 {
-  // outer panel
+  /* outer panel */
 
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
+
   setLayout(new BorderLayout)
 
 
-  // HTML panel
+  /* HTML panel */
 
   private val html_panel = new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"))
   add(html_panel, BorderLayout.CENTER)
@@ -56,7 +56,7 @@
     loop {
       react {
         case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
-        case bad => System.err.println("properties: ignoring bad message " + bad)
+        case bad => System.err.println("properties_actor: ignoring bad message " + bad)
       }
     }
   }