# HG changeset patch
# User wenzelm
# Date 1245957328 -7200
# Node ID e45052ff72334aaf0408a46a07353df70d178f45
# Parent  8d2c4960568559e1f746f0835109ca3055787564
added Boolean_Property, Int_Property;
simplified font handling -- hardwired path;
tuned comments;
tuned;

diff -r 8d2c49605685 -r e45052ff7233 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Jun 25 21:14:10 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Jun 25 21:15:28 2009 +0200
@@ -23,62 +23,86 @@
 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
 
 
-object Isabelle {
-  // name
+object Isabelle
+{
+  /* name */
+
   val NAME = "Isabelle"
   val VFS_PREFIX = "isabelle:"
 
-  // properties
-  object Property {
-    private val OPTION_PREFIX = "options.isabelle."
-    def apply(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
+
+  /* properties */
+
+  val OPTION_PREFIX = "options.isabelle."
+
+  object Property
+  {
+    def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
   }
 
-  // Isabelle system instance
+  object Boolean_Property
+  {
+    def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
+    def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
+  }
+
+  object Int_Property
+  {
+    def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
+    def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
+  }
+
+
+  /* Isabelle system instance */
+
   var system: Isabelle_System = null
   def symbols = system.symbols
   lazy val completion = new Completion + symbols
 
-  // settings
-  def default_logic = {
+
+  /* settings */
+
+  def default_logic =
+  {
     val logic = Isabelle.Property("logic")
     if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
   }
 
-  // plugin instance
+
+  /* plugin instance */
+
   var plugin: Plugin = null
 
-  // running provers
+
+  /* running provers */
+
   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
 }
 
 
-class Plugin extends EBPlugin {
-
-  // Isabelle font
+class Plugin extends EBPlugin
+{
+  /* Isabelle font */
 
   var font: Font = null
   val font_changed = new EventBus[Font]
 
-  def set_font(path: String, size: Float) {
-    font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
-      deriveFont(Font.PLAIN, size)
+  def set_font(size: Int)
+  {
+    font = Font.createFont(Font.TRUETYPE_FONT,
+        new FileInputStream(Isabelle.system.platform_path("~~/lib/fonts/IsabelleMono.ttf"))).
+      deriveFont(Font.PLAIN, size max 1)
     font_changed.event(font)
   }
 
 
-  /* unique ids */  // FIXME specific to "session" (!??)
-
-  private var id_count: BigInt = 0
-  def id() : String = synchronized { id_count += 1; "editor:" + id_count }
-
-
-  // mapping buffer <-> prover
+  /* mapping buffer <-> prover */
 
   private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
 
-  private def install(view: View) {
+  private def install(view: View)
+  {
     val buffer = view.getBuffer
     val prover_setup = new ProverSetup(buffer)
     mapping.update(buffer, prover_setup)
@@ -88,62 +112,63 @@
   private def uninstall(view: View) =
     mapping.removeKey(view.getBuffer).get.deactivate
 
-  def switch_active (view : View) =
+  def switch_active (view: View) =
     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
     else install(view)
 
-  def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
-  def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
-  
-  
-  // main plugin plumbing
+  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
+  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 EditPaneUpdate.BUFFER_CHANGED =>
-        mapping get epu.getEditPane.getBuffer match {
-          //only activate 'isabelle'-buffers!
-          case None =>
-          case Some(prover_setup) => 
-            prover_setup.theory_view.activate
-            val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
-            if (dockable != null) {
-              val output_dockable = dockable.asInstanceOf[OutputDockable]
-              if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
-                output_dockable.asInstanceOf[OutputDockable].removeAll
-                output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
-                output_dockable.revalidate
+  override def handleMessage(msg: EBMessage)
+  {
+    msg match {
+      case epu: EditPaneUpdate => epu.getWhat match {
+        case EditPaneUpdate.BUFFER_CHANGED =>
+          mapping get epu.getEditPane.getBuffer match {
+            // only activate 'isabelle' buffers
+            case None =>
+            case Some(prover_setup) =>
+              prover_setup.theory_view.activate
+              val dockable =
+                epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
+              if (dockable != null) {
+                val output_dockable = dockable.asInstanceOf[OutputDockable]
+                if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
+                  output_dockable.asInstanceOf[OutputDockable].removeAll
+                  output_dockable.asInstanceOf[OutputDockable].
+                    add(new JScrollPane(prover_setup.output_text_view))
+                  output_dockable.revalidate
+                }
               }
-            }
-        }
-      case EditPaneUpdate.BUFFER_CHANGING =>
-        val buffer = epu.getEditPane.getBuffer
-        if (buffer != null) mapping get buffer match {
-          //only deactivate 'isabelle'-buffers!
-          case None =>
-          case Some(prover_setup) => prover_setup.theory_view.deactivate
-        }
+          }
+        case EditPaneUpdate.BUFFER_CHANGING =>
+          val buffer = epu.getEditPane.getBuffer
+          if (buffer != null) mapping get buffer match {
+            // only deactivate 'isabelle' buffers
+            case None =>
+            case Some(prover_setup) => prover_setup.theory_view.deactivate
+          }
+        case _ =>
+      }
       case _ =>
     }
-    case _ =>
   }
 
-  override def start() {
+  override def start()
+  {
     Isabelle.system = new Isabelle_System
     Isabelle.plugin = this
-    
-    if (Isabelle.Property("font-path") != null && Isabelle.Property("font-size") != null)
-      try {
-        set_font(Isabelle.Property("font-path"), Isabelle.Property("font-size").toFloat)
-      }
-      catch {
-        case e: NumberFormatException =>
-      }
+    set_font(Isabelle.Int_Property("font-size"))
   }
-  
-  override def stop() {
+
+  override def stop()
+  {
     // TODO: proper cleanup
     Isabelle.system = null
     Isabelle.plugin = null
   }
+
 }