--- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Fri Dec 11 23:38:14 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_options.scala Tue Dec 15 00:21:21 2009 +0100
@@ -17,17 +17,25 @@
private val logic_name = new JComboBox()
private val font_size = new JSpinner()
+ private class List_Item(val name: String, val descr: String) {
+ def this(name: String) = this(name, name)
+ override def toString = descr
+ }
+
override def _init()
{
val logic = Isabelle.Property("logic")
addComponent(Isabelle.Property("logic.title"), {
- for (name <- "default" :: Isabelle.system.find_logics()) {
- logic_name.addItem(name)
+ logic_name.addItem(new List_Item("", "default (" + Isabelle.default_logic() + ")"))
+ for (name <- Isabelle.system.find_logics()) {
+ val item = new List_Item(name)
+ logic_name.addItem(item)
if (name == logic)
- logic_name.setSelectedItem(name)
+ logic_name.setSelectedItem(item)
}
logic_name
})
+
addComponent(Isabelle.Property("font-size.title"), {
font_size.setValue(Isabelle.Int_Property("font-size"))
font_size
@@ -36,7 +44,7 @@
override def _save()
{
- val logic = logic_name.getSelectedItem.asInstanceOf[String]
+ val logic = logic_name.getSelectedItem.asInstanceOf[List_Item].name
Isabelle.Property("logic") = logic
val size = font_size.getValue().asInstanceOf[Int]
--- a/src/Tools/jEdit/src/jedit/plugin.scala Fri Dec 11 23:38:14 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Tue Dec 15 00:21:21 2009 +0100
@@ -55,17 +55,20 @@
/* settings */
- def cmd_args(): List[String] =
+ def default_logic(): String =
+ {
+ val logic = system.getenv("JEDIT_LOGIC")
+ if (logic != "") logic
+ else system.getenv_strict("ISABELLE_LOGIC")
+ }
+
+ def isabelle_args(): List[String] =
{
val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
val logic = {
- val logic1 = Isabelle.Property("logic")
- if (logic1 != null && logic1 != "" && logic1 != "default") logic1
- else {
- val logic2 = system.getenv("JEDIT_LOGIC")
- if (logic2 != "") logic2
- else system.getenv_strict("ISABELLE_LOGIC")
- }
+ val logic = Isabelle.Property("logic")
+ if (logic != null && logic != "") logic
+ else default_logic()
}
modes ++ List(logic)
}
@@ -94,7 +97,7 @@
val theory_view = new Theory_View(Isabelle.session, text_area) // FIXME multiple text areas!?
mapping += (buffer -> theory_view)
- Isabelle.session.start(Isabelle.cmd_args())
+ Isabelle.session.start(Isabelle.isabelle_args())
theory_view.activate()
Isabelle.session.begin_document(buffer.getName)
}