isabelle: src/Tools/jEdit/src/jedit/isabelle_options.scala@09270033330e (annotated)

36760 b82a698ef6c9 tuned headers; wenzelm parents: 34782 diff changeset	1	/* Title: Tools/jEdit/src/jedit/isabelle_options.scala
b82a698ef6c9 tuned headers; wenzelm parents: 34782 diff changeset	2	Author: Johannes Hölzl, TU Munich
b82a698ef6c9 tuned headers; wenzelm parents: 34782 diff changeset	3
b82a698ef6c9 tuned headers; wenzelm parents: 34782 diff changeset	4	Editor pane for plugin options.
b82a698ef6c9 tuned headers; wenzelm parents: 34782 diff changeset	5	*/
34407 aad6834ba380 added some headers and comments; wenzelm parents: 34318 diff changeset	6
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	7	package isabelle.jedit
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	8
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	9
39518 96180281c3b2 tuned; wenzelm parents: 39517 diff changeset	10	import javax.swing.JSpinner
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	11
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	12	import scala.swing.CheckBox
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	13
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	14	import org.gjt.sp.jedit.AbstractOptionPane
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	15
34468 9d4b4f290676 maintain Isabelle properties via object Isabelle.Property with apply/update methods; wenzelm parents: 34441 diff changeset	16
34760 dc7f5e0d9d27 misc modernization of names; wenzelm parents: 34759 diff changeset	17	class Isabelle_Options extends AbstractOptionPane("isabelle")
34617 8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	18	{
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 38854 diff changeset	19	private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	20	private val auto_start = new CheckBox()
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	21	private val relative_font_size = new JSpinner()
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 36817 diff changeset	22	private val tooltip_font_size = new JSpinner()
40339 088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	23	private val tooltip_margin = new JSpinner()
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 37203 diff changeset	24	private val tooltip_dismiss_delay = new JSpinner()
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	25
34617 8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	26	override def _init()
8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	27	{
39517 e036c67448e6 separate Isabelle.logic_selector; wenzelm parents: 38854 diff changeset	28	addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
34782 fcd6a41326a6 refined treatment of default logic concerning property and GUI; wenzelm parents: 34781 diff changeset	29
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	30	addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	31	auto_start.selected = Isabelle.Boolean_Property("auto-start")
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	32
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	33	relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	34	addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 36817 diff changeset	35
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	36	tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	37	addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 37203 diff changeset	38
40339 088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	39	tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	40	addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	41
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40339 diff changeset	42	tooltip_dismiss_delay.setValue(
09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40339 diff changeset	43	(Isabelle.Double_Property("tooltip-dismiss-delay", 8.0) * 1000) round)
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	44	addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	45	}
34617 8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	46
8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	47	override def _save()
8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	48	{
39734 47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	49	Isabelle.Property("logic") = logic_selector.selection.item.name
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	50
47f5a8c92666 moved "auto-start" to options panel; wenzelm parents: 39518 diff changeset	51	Isabelle.Boolean_Property("auto-start") = auto_start.selected
34617 8d2c49605685 simplified option pane: proper logic title, hardwired font path; wenzelm parents: 34506 diff changeset	52
36814 dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	53	Isabelle.Int_Property("relative-font-size") =
dc85664dbf6d support Isabelle plugin properties with defaults; wenzelm parents: 36760 diff changeset	54	relative_font_size.getValue().asInstanceOf[Int]
37201 8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 36817 diff changeset	55
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 36817 diff changeset	56	Isabelle.Int_Property("tooltip-font-size") =
8517a650cfdc control tooltip font via Swing HTML, with tooltip-font-size property; wenzelm parents: 36817 diff changeset	57	tooltip_font_size.getValue().asInstanceOf[Int]
38854 eb6a35be18ca Isabelle/jEdit property for global tooltip dismiss delay; wenzelm parents: 37203 diff changeset	58
40339 088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	59	Isabelle.Int_Property("tooltip-margin") =
088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	60	tooltip_margin.getValue().asInstanceOf[Int]
088e5adca5ad added property "tooltip-margin"; wenzelm parents: 39734 diff changeset	61
40849 09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40339 diff changeset	62	Isabelle.Double_Property("tooltip-dismiss-delay") =
09270033330e store tooltip-dismiss-delay as Double(seconds); wenzelm parents: 40339 diff changeset	63	tooltip_dismiss_delay.getValue().asInstanceOf[Int].toDouble / 1000
34318 c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	64	}
c13e168a8ae6 original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout; wenzelm parents: diff changeset	65	}

author	wenzelm
	Wed, 01 Dec 2010 21:07:50 +0100
changeset 40849	09270033330e
parent 40339	088e5adca5ad
child 40850	d804de9ac970
permissions	-rw-r--r--