# HG changeset patch
# User wenzelm
# Date 1231698746 -3600
# Node ID 9d4b4f2906767293c3acef6425e4b5cb23a14692
# Parent  c7d7a92fe3d55f465d89cefa54960d940e4fb235
maintain Isabelle properties via object Isabelle.Property with apply/update methods;

diff -r c7d7a92fe3d5 -r 9d4b4f290676 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Jan 11 17:35:56 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Sun Jan 11 19:32:26 2009 +0100
@@ -17,15 +17,14 @@
 
 import org.gjt.sp.jedit.AbstractOptionPane
 
+
 class OptionPane extends AbstractOptionPane("isabelle") {
-  import Isabelle.property
-  
   var pathName = new JTextField()
   var fontSize = new JSpinner()
   var logicName = new JComboBox()
     
   override def _init() {
-    addComponent(property("font-path.title"), {
+    addComponent(Isabelle.Property("font-path.title"), {
       val pickPath = new JButton("...")
       pickPath.addActionListener(new ActionListener() {
         override def actionPerformed(e : ActionEvent) {
@@ -35,7 +34,7 @@
         } 
       })
 
-      pathName.setText(property("font-path"))
+      pathName.setText(Isabelle.Property("font-path"))
       
       val pathPanel = new JPanel(new BorderLayout())
       pathPanel.add(pathName, CENTER)
@@ -43,10 +42,10 @@
       pathPanel
     }, HORIZONTAL)
 
-    addComponent(property("font-size.title"), {
+    addComponent(Isabelle.Property("font-size.title"), {
       try {
-        if (property("font-size") != null)
-          fontSize.setValue(Integer.valueOf(property("font-size")))
+        if (Isabelle.Property("font-size") != null)
+          fontSize.setValue(Integer.valueOf(Isabelle.Property("font-size")))
       }
       catch {
         case e : NumberFormatException => 
@@ -56,10 +55,10 @@
       fontSize
     })
 
-    addComponent(property("logic.title"), {
+    addComponent(Isabelle.Property("logic.title"), {
       for (name <- Isabelle.system.find_logics()) {
         logicName.addItem(name)
-        if (name == property("logic"))
+        if (name == Isabelle.Property("logic"))
           logicName.setSelectedItem(name)
       }
 
@@ -70,9 +69,9 @@
   override def _save() {
     val size = fontSize.getValue()
     val name = pathName.getText()
-    if (property("font-path") != name || property("font-size") != size.toString) {
-      property("font-path", name)
-      property("font-size", size.toString)
+    if (Isabelle.Property("font-path") != name || Isabelle.Property("font-size") != size.toString) {
+      Isabelle.Property("font-path") = name
+      Isabelle.Property("font-size") = size.toString
       SwingUtilities invokeLater new Runnable() {
         override def run() = 
           Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue)
@@ -80,6 +79,6 @@
     }
     
     val logic = logicName.getSelectedItem.asInstanceOf[String]
-    property("logic", logic) 
+    Isabelle.Property("logic") = logic
   }
 }
diff -r c7d7a92fe3d5 -r 9d4b4f290676 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Jan 11 17:35:56 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sun Jan 11 19:32:26 2009 +0100
@@ -26,13 +26,14 @@
 object Isabelle {
   // 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)
+  object Property {
+    private val OPTION_PREFIX = "options.isabelle."
+    def apply(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
+    def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
+  }
 
 
   // Isabelle system
@@ -128,9 +129,9 @@
     Isabelle.symbols = new Symbol.Interpretation(Isabelle.system)
     Isabelle.plugin = this
     
-    if (Isabelle.property("font-path") != null && Isabelle.property("font-size") != null)
+    if (Isabelle.Property("font-path") != null && Isabelle.Property("font-size") != null)
       try {
-        set_font(Isabelle.property("font-path"), Isabelle.property("font-size").toFloat)
+        set_font(Isabelle.Property("font-path"), Isabelle.Property("font-size").toFloat)
       }
       catch {
         case e: NumberFormatException =>
diff -r c7d7a92fe3d5 -r 9d4b4f290676 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Jan 11 17:35:56 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sun Jan 11 19:32:26 2009 +0100
@@ -34,7 +34,7 @@
   val output_text_view = new JTextArea
 
   def activate(view: View) {
-    prover.start(Isabelle.property("logic"))
+    prover.start(Isabelle.Property("logic"))
     val buffer = view.getBuffer
     val dir = buffer.getDirectory