# HG changeset patch
# User wenzelm
# Date 1260994264 -3600
# Node ID b97d5b38dea43180acb31b02d31a78368b452398
# Parent  643c48774b1766cb75786c1ed5f8367d745d1a0a
explicit object Session.Global_Settings;
misc tuning;

diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -6,19 +6,13 @@
 
 package isabelle.jedit
 
+import isabelle.proofdocument.Command
 
 import java.io.File
 
-import gatchan.jedit.hyperlinks.Hyperlink
-import gatchan.jedit.hyperlinks.HyperlinkSource
-import gatchan.jedit.hyperlinks.AbstractHyperlink
+import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
 
-import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.jEdit
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.TextUtilities
-
-import isabelle.proofdocument.Command
+import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
 
 
 private class Internal_Hyperlink(start: Int, end: Int, line: Int, ref_offset: Int)
diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -7,7 +7,7 @@
 package isabelle.jedit
 
 
-import isabelle.proofdocument.{Command, HTML_Panel}
+import isabelle.proofdocument.{Command, HTML_Panel, Session}
 
 import scala.actors.Actor._
 
@@ -19,18 +19,11 @@
 
 
 
-class Output_Dockable(view: View, position: String) extends JPanel
+class Output_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
 {
-  /* outer panel */
-
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  setLayout(new BorderLayout)
-
-
-  /* HTML panel */
-
   private val html_panel =
     new HTML_Panel(Isabelle.system, Isabelle.Int_Property("font-size"), null)
   add(html_panel, BorderLayout.CENTER)
@@ -50,32 +43,26 @@
                 else cmd.results(model.current_document)
               html_panel.render(body)
           }
+
+        case Session.Global_Settings =>
+          html_panel.init(Isabelle.Int_Property("font-size"))
           
         case bad => System.err.println("output_actor: ignoring bad message " + bad)
       }
     }
   }
 
-  private val properties_actor = actor {
-    loop {
-      react {
-        case _: Unit => html_panel.init(Isabelle.Int_Property("font-size"))
-        case bad => System.err.println("properties_actor: ignoring bad message " + bad)
-      }
-    }
-  }
-
   override def addNotify()
   {
     super.addNotify()
     Isabelle.session.results += output_actor
-    Isabelle.session.global_settings += properties_actor
+    Isabelle.session.global_settings += output_actor
   }
 
   override def removeNotify()
   {
     Isabelle.session.results -= output_actor
-    Isabelle.session.global_settings -= properties_actor
+    Isabelle.session.global_settings -= output_actor
     super.removeNotify()
   }
 }
diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/jedit/plugin.scala
--- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -163,7 +163,7 @@
         }
 
       case msg: PropertiesChanged =>
-        Isabelle.session.global_settings.event(())
+        Isabelle.session.global_settings.event(Session.Global_Settings)
 
       case _ =>
     }
diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/jedit/protocol_dockable.scala
--- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -16,18 +16,11 @@
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
 
-class Protocol_Dockable(view: View, position: String) extends JPanel
+class Protocol_Dockable(view: View, position: String) extends JPanel(new BorderLayout)
 {
-  // outer panel
-
   if (position == DockableWindowManager.FLOATING)
     setPreferredSize(new Dimension(500, 250))
 
-  setLayout(new BorderLayout)
-
-
-  // text area
-
   private val text_area = new JTextArea
   add(new JScrollPane(text_area), BorderLayout.CENTER)
 
diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/proofdocument/html_panel.scala
--- a/src/Tools/jEdit/src/proofdocument/html_panel.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -101,7 +101,7 @@
   private case class Render(body: List[XML.Tree])
 
   private val main_actor = actor {
-    // double buffering
+    // crude double buffering
     var doc1: Document = null
     var doc2: Document = null
 
diff -r 643c48774b17 -r b97d5b38dea4 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 16 14:40:31 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 16 21:11:04 2009 +0100
@@ -9,6 +9,11 @@
 
 import scala.actors.Actor._
 
+object Session
+{
+  case object Global_Settings
+}
+
 
 class Session(system: Isabelle_System)
 {
@@ -59,7 +64,7 @@
 
   /* pervasive event buses */
 
-  val global_settings = new Event_Bus[Unit]
+  val global_settings = new Event_Bus[Session.Global_Settings.type]
   val raw_results = new Event_Bus[Isabelle_Process.Result]
   val results = new Event_Bus[Command]