# HG changeset patch # User wenzelm # Date 1347289997 -7200 # Node ID 248e66e8321f271c35ea5173aaed2d5c3de92cdf # Parent cb70157293c0d600268c9c0504a483e5ecd1a1a4 more systematic JEdit_Options.make_component; separate module Isabelle_Logic; diff -r cb70157293c0 -r 248e66e8321f src/Pure/System/options.scala --- a/src/Pure/System/options.scala Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Pure/System/options.scala Mon Sep 10 17:13:17 2012 +0200 @@ -24,11 +24,11 @@ { def print: String = toString.toLowerCase(Locale.ENGLISH) } - private case object Bool extends Type - private case object Int extends Type - private case object Real extends Type - private case object String extends Type - private case object Unknown extends Type + case object Bool extends Type + case object Int extends Type + case object Real extends Type + case object String extends Type + case object Unknown extends Type case class Opt(typ: Type, value: String, description: String) { @@ -147,7 +147,7 @@ /* check */ - private def check_name(name: String): Options.Opt = + def check_name(name: String): Options.Opt = options.get(name) match { case Some(opt) if !opt.unknown => opt case _ => error("Unknown option " + quote(name)) diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Mon Sep 10 17:13:17 2012 +0200 @@ -14,6 +14,7 @@ "src/html_panel.scala" "src/hyperlink.scala" "src/isabelle_encoding.scala" + "src/isabelle_logic.scala" "src/isabelle_options.scala" "src/isabelle_rendering.scala" "src/isabelle_sidekick.scala" diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/src/isabelle_logic.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_logic.scala Mon Sep 10 17:13:17 2012 +0200 @@ -0,0 +1,76 @@ +/* Title: Tools/jEdit/src/isabelle_logic.scala + Author: Makarius + +Isabellel logic session. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.swing.ComboBox +import scala.swing.event.SelectionChanged + + +object Isabelle_Logic +{ + private def default_logic(): String = + { + val logic = Isabelle_System.getenv("JEDIT_LOGIC") + if (logic != "") logic + else Isabelle_System.getenv_strict("ISABELLE_LOGIC") + } + + private class Logic_Entry(val name: String, val description: String) + { + override def toString = description + } + + def logic_selector(autosave: Boolean): Option_Component = + { + Swing_Thread.require() + + val entries = + new Logic_Entry("", "default (" + default_logic() + ")") :: + Isabelle_System.find_logics().map(name => new Logic_Entry(name, name)) + + val component = new ComboBox(entries) with Option_Component { + val title = Isabelle.options.title("jedit_logic") + def save = Isabelle.options.string("jedit_logic") = selection.item.name + } + + if (autosave) { + component.listenTo(component.selection) + component.reactions += { case SelectionChanged(_) => component.save() } + } + + val logic = Isabelle.options.string("jedit_logic") + entries.find(_.name == logic) match { + case Some(entry) => component.selection.item = entry + case None => + } + + component.tooltip = Isabelle.options.value.check_name("jedit_logic").description + component + } + + def session_args(): List[String] = + { + val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) + val logic = + Isabelle.options.string("jedit_logic") match { + case "" => default_logic() + case logic => logic + } + modes ::: List(logic) + } + + def session_content(inlined_files: Boolean): Build.Session_Content = + { + val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) + val name = Path.explode(session_args().last).base.implode // FIXME more robust + Build.session_content(inlined_files, dirs, name).check_errors + } +} + diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Mon Sep 10 17:13:17 2012 +0200 @@ -1,5 +1,5 @@ /* Title: Tools/jEdit/src/isabelle_options.scala - Author: Johannes Hölzl, TU Munich + Author: Makarius Editor pane for plugin options. */ @@ -9,59 +9,26 @@ import isabelle._ -import javax.swing.{JSpinner, JTextField} - -import scala.swing.CheckBox - import org.gjt.sp.jedit.AbstractOptionPane class Isabelle_Options extends AbstractOptionPane("isabelle") { - private val logic_selector = Isabelle.logic_selector(Isabelle.options.string("jedit_logic")) - private val auto_start = new CheckBox() - private val relative_font_size = new JSpinner() - private val tooltip_font_size = new JSpinner() - private val tooltip_margin = new JSpinner() - private val tooltip_dismiss_delay = new JTextField() + private val components = List( + Isabelle_Logic.logic_selector(false), + Isabelle.options.make_component("jedit_auto_start"), + Isabelle.options.make_component("jedit_relative_font_size"), + Isabelle.options.make_component("jedit_tooltip_font_size"), + Isabelle.options.make_component("jedit_tooltip_margin"), + Isabelle.options.make_component("jedit_tooltip_dismiss_delay")) override def _init() { - addComponent(Isabelle.options.title("jedit_logic"), - logic_selector.peer.asInstanceOf[java.awt.Component]) - - addComponent(Isabelle.options.title("jedit_auto_start"), auto_start.peer) - auto_start.selected = Isabelle.options.bool("jedit_auto_start") - - addComponent(Isabelle.options.title("jedit_relative_font_size"), relative_font_size) - relative_font_size.setValue(Isabelle.options.int("jedit_relative_font_size")) - - tooltip_font_size.setValue(Isabelle.options.int("jedit_tooltip_font_size")) - addComponent(Isabelle.options.title("jedit_tooltip_font_size"), tooltip_font_size) - - tooltip_margin.setValue(Isabelle.options.int("jedit_tooltip_margin")) - addComponent(Isabelle.options.title("jedit_tooltip_margin"), tooltip_margin) - - // FIXME InputVerifier for Double - tooltip_dismiss_delay.setText(Isabelle.options.real("jedit_tooltip_dismiss_delay").toString) - addComponent(Isabelle.options.title("jedit_tooltip_dismiss_delay"), tooltip_dismiss_delay) + for (c <- components) addComponent(c.title, c.peer) } override def _save() { - Isabelle.options.string("jedit_logic") = logic_selector.selection.item.name - - Isabelle.options.bool("jedit_auto_start") = auto_start.selected - - Isabelle.options.int("jedit_relative_font_size") = - relative_font_size.getValue().asInstanceOf[Int] - - Isabelle.options.int("jedit_tooltip_font_size") = - tooltip_font_size.getValue().asInstanceOf[Int] - - Isabelle.options.int("jedit_tooltip_margin") = - tooltip_margin.getValue().asInstanceOf[Int] - - Isabelle.options + ("jedit_tooltip_dismiss_delay", tooltip_dismiss_delay.getText) + for (c <- components) c.save() } } diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Tools/jEdit/src/jedit_options.scala Mon Sep 10 17:13:17 2012 +0200 @@ -9,10 +9,55 @@ import isabelle._ +import javax.swing.{InputVerifier, JComponent} +import javax.swing.text.JTextComponent +import scala.swing.{Component, CheckBox, TextArea} + + +trait Option_Component extends Component +{ + val title: String + def save(): Unit +} class JEdit_Options extends Options_Variable { - def title(name: String): String = value.title("jedit", name) - def description(name: String): String = value.description(name) + def title(opt_name: String): String = value.title("jedit", opt_name) + + def make_component(opt_name: String): Option_Component = + { + Swing_Thread.require() + + val opt = value.check_name(opt_name) + val opt_title = title(opt_name) + + val component = + if (opt.typ == Options.Bool) + new CheckBox with Option_Component { + val title = opt_title + def save = bool(opt_name) = selected + selected = bool(opt_name) + } + else { + val text_area = + new TextArea with Option_Component { + val title = opt_title + def save = update(value + (opt_name, text)) + text = opt.value + } + text_area.peer.setInputVerifier(new InputVerifier { + def verify(jcomponent: JComponent): Boolean = + jcomponent match { + case text: JTextComponent => + try { value + (opt_name, text.getText); true } + catch { case ERROR(_) => false } + case _ => true + } + }) + text_area + } + component.tooltip = opt.description + component + } } diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Mon Sep 10 17:13:17 2012 +0200 @@ -14,7 +14,7 @@ import javax.swing.JOptionPane import scala.collection.mutable -import scala.swing.{ComboBox, ListView, ScrollPane} +import scala.swing.{ListView, ScrollPane} import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View} @@ -227,53 +227,6 @@ } - /* logic image */ - - def default_logic(): String = - { - val logic = Isabelle_System.getenv("JEDIT_LOGIC") - if (logic != "") logic - else Isabelle_System.getenv_strict("ISABELLE_LOGIC") - } - - class Logic_Entry(val name: String, val description: String) - { - override def toString = description - } - - def logic_selector(logic: String): ComboBox[Logic_Entry] = - { - val entries = - new Logic_Entry("", "default (" + default_logic() + ")") :: - Isabelle_System.find_logics().map(name => new Logic_Entry(name, name)) - val component = new ComboBox(entries) - entries.find(_.name == logic) match { - case None => - case Some(entry) => component.selection.item = entry - } - component.tooltip = "Isabelle logic image" - component - } - - def session_args(): List[String] = - { - val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) - val logic = - Isabelle.options.string("jedit_logic") match { - case "" => Isabelle.default_logic() - case logic => logic - } - modes ::: List(logic) - } - - def session_content(inlined_files: Boolean): Build.Session_Content = - { - val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) - val name = Path.explode(session_args().last).base.implode // FIXME more robust - Build.session_content(inlined_files, dirs, name).check_errors - } - - /* convenience actions */ private def user_input(text_area: JEditTextArea, s1: String, s2: String = "") @@ -398,7 +351,7 @@ message match { case msg: EditorStarted => if (Isabelle.options.bool("jedit_auto_start")) - Isabelle.session.start(Isabelle.session_args()) + Isabelle.session.start(Isabelle_Logic.session_args()) case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => @@ -452,7 +405,7 @@ if (ModeProvider.instance.isInstanceOf[ModeProvider]) ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) - val content = Isabelle.session_content(false) + val content = Isabelle_Logic.session_content(false) val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) Isabelle.session = new Session(thy_load) diff -r cb70157293c0 -r 248e66e8321f src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Mon Sep 10 15:20:50 2012 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Mon Sep 10 17:13:17 2012 +0200 @@ -11,7 +11,7 @@ import scala.actors.Actor._ import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component} -import scala.swing.event.{ButtonClicked, MouseClicked, SelectionChanged} +import scala.swing.event.{ButtonClicked, MouseClicked} import java.lang.System import java.awt.{BorderLayout, Graphics2D, Insets} @@ -60,12 +60,7 @@ } check.tooltip = jEdit.getProperty("isabelle.check-buffer.label") - private val logic = Isabelle.logic_selector(Isabelle.options.string("jedit_logic")) - logic.listenTo(logic.selection) - logic.reactions += { - case SelectionChanged(_) => - Isabelle.options.string("jedit_logic") = logic.selection.item.name - } + private val logic = Isabelle_Logic.logic_selector(true) private val controls = new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)