# HG changeset patch
# User wenzelm
# Date 1229892221 -3600
# Node ID 3da749b53842045f1e37eefc3e58d79fe2a24667
# Parent  5a8b9fc98d8c2cdff8de4b63463afe28297421f6
renamed Plugin.plugin to Plugin.self;
added Symbol.Interpretation (formerly in VFS);
tuned Plugin.font handling;
tuned;

diff -r 5a8b9fc98d8c -r 3da749b53842 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Dec 21 21:43:40 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Dec 21 21:43:41 2008 +0100
@@ -16,7 +16,7 @@
 
 import isabelle.utils.EventSource
 import isabelle.prover.{Prover, Command}
-import isabelle.IsabelleSystem
+import isabelle.{IsabelleSystem, Symbol}
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
@@ -25,26 +25,51 @@
 
 
 object Plugin {
+  // name
   val NAME = "Isabelle"
   val OPTION_PREFIX = "options.isabelle."
   val VFS_PREFIX = "isabelle:"
-  
+
+  // properties
   def property(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
   def property(name: String, value: String) = 
     jEdit.setProperty(OPTION_PREFIX + name, value)
-  
-  var plugin: Plugin = null
-  def prover(buffer: JEditBuffer) = plugin.prover_setup(buffer).get.prover
-  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer).get
+
+  // dynamic instance
+  var self: Plugin = null
+
+  // provers
+  def prover(buffer: JEditBuffer) = self.prover_setup(buffer).get.prover
+  def prover_setup(buffer: JEditBuffer) = self.prover_setup(buffer).get
 }
 
 
 class Plugin extends EBPlugin {
-  
-  private val mapping = new HashMap[JEditBuffer, ProverSetup]
+
+  // Isabelle symbols
+  val symbols = new Symbol.Interpretation
+
+
+  // Isabelle font
+
+  var font: Font = null
+  val font_changed = new EventSource[Font]
 
-  var viewFont: Font = null
-  val viewFontChanged = new EventSource[Font]
+  def set_font(path: String, size: Float) {
+    try {
+      font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
+        deriveFont(Font.PLAIN, size)
+      font_changed.fire(font)
+    }
+    catch {
+      case e: IOException =>
+    }
+  }
+
+
+  // mapping buffer <-> prover
+
+  private val mapping = new HashMap[JEditBuffer, ProverSetup]
 
   def install(view: View) {
     val buffer = view.getBuffer
@@ -68,11 +93,13 @@
   }
 
   def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
-  def is_active(buffer: JEditBuffer) =
-    mapping.get(buffer) match { case None => false case _ => true }
+  def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
+
   
+  // main plugin plumbing
+
   override def handleMessage(msg: EBMessage) = msg match {
-    case epu: EditPaneUpdate => epu.getWhat() match {
+    case epu: EditPaneUpdate => epu.getWhat match {
       case EditPaneUpdate.BUFFER_CHANGED =>
         mapping get epu.getEditPane.getBuffer match {
           //only activate 'isabelle'-buffers!
@@ -101,25 +128,12 @@
     case _ =>
   }
 
-  def setFont(path: String, size: Float) {
-    try {
-      val fontStream = new FileInputStream(path)
-      val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
-      viewFont = font.deriveFont(Font.PLAIN, size)
-
-      viewFontChanged.fire(viewFont)
-    }
-    catch {
-      case e: IOException =>
-    }
-  }
-  
   override def start() {
-    Plugin.plugin = this
+    Plugin.self = this
     
     if (Plugin.property("font-path") != null && Plugin.property("font-size") != null)
       try {
-        setFont(Plugin.property("font-path"), Plugin.property("font-size").toFloat)
+        set_font(Plugin.property("font-path"), Plugin.property("font-size").toFloat)
       }
       catch {
         case e: NumberFormatException =>
@@ -128,6 +142,6 @@
   
   override def stop() {
     // TODO: proper cleanup
-    Plugin.plugin = null
+    Plugin.self = null
   }
 }