--- 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)
--- 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()
}
}
--- 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 _ =>
}
--- 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)
--- 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
--- 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]