# HG changeset patch
# User wenzelm
# Date 1245957250 -7200
# Node ID 8d2c4960568559e1f746f0835109ca3055787564
# Parent  bc923168c880608cff152b51bc708d81180a9aee
simplified option pane: proper logic title, hardwired font path;
tuned;

diff -r bc923168c880 -r 8d2c49605685 src/Tools/jEdit/plugin/Isabelle.props
--- a/src/Tools/jEdit/plugin/Isabelle.props	Thu Jun 25 14:19:14 2009 +0200
+++ b/src/Tools/jEdit/plugin/Isabelle.props	Thu Jun 25 21:14:10 2009 +0200
@@ -29,7 +29,7 @@
 plugin.isabelle.jedit.Plugin.option-pane=isabelle
 options.isabelle.label=Isabelle
 options.isabelle.code=new isabelle.jedit.OptionPane();
-options.isabelle.font-path.title=Font Path
+options.isabelle.logic.title=Logic
 options.isabelle.font-size.title=Font Size
 options.isabelle.font-size=18
 
diff -r bc923168c880 -r 8d2c49605685 src/Tools/jEdit/src/jedit/OptionPane.scala
--- a/src/Tools/jEdit/src/jedit/OptionPane.scala	Thu Jun 25 14:19:14 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/OptionPane.scala	Thu Jun 25 21:14:10 2009 +0200
@@ -6,75 +6,42 @@
 
 package isabelle.jedit
 
-import java.lang.Integer
-
-import java.awt.BorderLayout
-import java.awt.GridBagConstraints.HORIZONTAL
-import java.awt.BorderLayout.{WEST, CENTER, EAST}
-import java.awt.event.{ActionListener, ActionEvent}
-import javax.swing.{JTextField, JButton, JPanel, JLabel, JFileChooser, JSpinner, JComboBox}
+import javax.swing.{JComboBox, JSpinner}
 
 import org.gjt.sp.jedit.AbstractOptionPane
 
 
-class OptionPane extends AbstractOptionPane("isabelle") {
-  var pathName = new JTextField()
-  var fontSize = new JSpinner()
-  var logicName = new JComboBox()
-    
-  override def _init() {
-    addComponent(Isabelle.Property("font-path.title"), {
-      val pickPath = new JButton("...")
-      pickPath.addActionListener(new ActionListener() {
-        override def actionPerformed(e : ActionEvent) {
-          val chooser = new JFileChooser(pathName.getText())
-          if (chooser.showOpenDialog(OptionPane.this) == JFileChooser.APPROVE_OPTION)
-            pathName.setText(chooser.getSelectedFile().getAbsolutePath())
-        } 
-      })
+class OptionPane extends AbstractOptionPane("isabelle")
+{
+  private val logic_name = new JComboBox()
+  private val font_size = new JSpinner()
 
-      pathName.setText(Isabelle.Property("font-path"))
-      
-      val pathPanel = new JPanel(new BorderLayout())
-      pathPanel.add(pathName, CENTER)
-      pathPanel.add(pickPath, EAST)
-      pathPanel
-    }, HORIZONTAL)
-
-    addComponent(Isabelle.Property("font-size.title"), {
-      try {
-        if (Isabelle.Property("font-size") != null)
-          fontSize.setValue(Isabelle.Property("font-size").toInt)
-      }
-      catch {
-        case e : NumberFormatException => 
-          fontSize.setValue(14)
-      }
-      
-      fontSize
-    })
-
+  override def _init()
+  {
     addComponent(Isabelle.Property("logic.title"), {
       for (name <- Isabelle.system.find_logics()) {
-        logicName.addItem(name)
+        logic_name.addItem(name)
         if (name == Isabelle.Property("logic"))
-          logicName.setSelectedItem(name)
+          logic_name.setSelectedItem(name)
       }
-
-      logicName
+      logic_name
+    })
+    addComponent(Isabelle.Property("font-size.title"), {
+      font_size.setValue(Isabelle.Int_Property("font-size"))
+      font_size
     })
   }
-    
-  override def _save() {
-    val size = fontSize.getValue()
-    val name = pathName.getText()
-    if (Isabelle.Property("font-path") != name || Isabelle.Property("font-size") != size.toString) {
-      Isabelle.Property("font-path") = name
-      Isabelle.Property("font-size") = size.toString
-      Swing.later { Isabelle.plugin.set_font(name, size.asInstanceOf[Integer].intValue) }
+
+  override def _save()
+  {
+    val logic = logic_name.getSelectedItem.asInstanceOf[String]
+    Isabelle.Property("logic") = logic
+
+    val size = font_size.getValue().asInstanceOf[Int]
+    if (Isabelle.Int_Property("font-size") != size)
+    {
+      Isabelle.Int_Property("font-size") = size
+      Swing.later { Isabelle.plugin.set_font(size) }
     }
-    
-    val logic = logicName.getSelectedItem.asInstanceOf[String]
-    Isabelle.Property("logic") = logic
   }
 }