equal
deleted
inserted
replaced
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import scala.swing.{Button, CheckBox} |
12 import scala.swing.Button |
13 import scala.swing.event.ButtonClicked |
13 import scala.swing.event.ButtonClicked |
14 |
14 |
15 import java.awt.BorderLayout |
15 import java.awt.BorderLayout |
16 import java.awt.event.{ComponentEvent, ComponentAdapter} |
16 import java.awt.event.{ComponentEvent, ComponentAdapter} |
17 |
17 |
76 GUI_Thread.require { if (auto_update_enabled) update() } |
76 GUI_Thread.require { if (auto_update_enabled) update() } |
77 |
77 |
78 |
78 |
79 /* controls */ |
79 /* controls */ |
80 |
80 |
81 private val auto_update_button = new CheckBox("Auto update") { |
81 private val auto_update_button = new GUI.Bool("Auto update", init = auto_update_enabled) { |
82 tooltip = "Indicate automatic update following cursor movement" |
82 tooltip = "Indicate automatic update following cursor movement" |
83 reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() } |
83 override def clicked(state: Boolean): Unit = { |
84 selected = auto_update_enabled |
84 auto_update_enabled = state |
|
85 auto_update() |
|
86 } |
85 } |
87 } |
86 |
88 |
87 private val update_button = new Button("<html><b>Update</b></html>") { |
89 private val update_button = new Button("<html><b>Update</b></html>") { |
88 tooltip = "Update display according to the command at cursor position" |
90 tooltip = "Update display according to the command at cursor position" |
89 reactions += { case ButtonClicked(_) => update_request() } |
91 reactions += { case ButtonClicked(_) => update_request() } |