equal
deleted
inserted
replaced
6 |
6 |
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
|
12 import scala.swing.Button |
|
13 import scala.swing.event.ButtonClicked |
|
14 |
11 |
15 import java.awt.BorderLayout |
12 import java.awt.BorderLayout |
16 import java.awt.event.{ComponentEvent, ComponentAdapter} |
13 import java.awt.event.{ComponentEvent, ComponentAdapter} |
17 |
14 |
18 import org.gjt.sp.jedit.View |
15 import org.gjt.sp.jedit.View |
84 auto_update_enabled = state |
81 auto_update_enabled = state |
85 auto_update() |
82 auto_update() |
86 } |
83 } |
87 } |
84 } |
88 |
85 |
89 private val update_button = new Button("<html><b>Update</b></html>") { |
86 private val update_button = new GUI.Button("<html><b>Update</b></html>") { |
90 tooltip = "Update display according to the command at cursor position" |
87 tooltip = "Update display according to the command at cursor position" |
91 reactions += { case ButtonClicked(_) => update_request() } |
88 override def clicked(): Unit = update_request() |
92 } |
89 } |
93 |
90 |
94 private val locate_button = new Button("Locate") { |
91 private val locate_button = new GUI.Button("Locate") { |
95 tooltip = "Locate printed command within source text" |
92 tooltip = "Locate printed command within source text" |
96 reactions += { case ButtonClicked(_) => print_state.locate_query() } |
93 override def clicked(): Unit = print_state.locate_query() |
97 } |
94 } |
98 |
95 |
99 private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } |
96 private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } |
100 |
97 |
101 private val controls = |
98 private val controls = |