maintain Isabelle properties via object Isabelle.Property with apply/update methods;
--- 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
}
}
--- 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 =>
--- 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