equal
deleted
inserted
replaced
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.awt.BorderLayout |
12 import java.awt.BorderLayout |
13 import java.awt.event.{ComponentEvent, ComponentAdapter} |
13 import java.awt.event.{ComponentEvent, ComponentAdapter} |
14 |
|
15 import scala.swing.Button |
|
16 import scala.swing.event.ButtonClicked |
|
17 |
14 |
18 import org.gjt.sp.jedit.{jEdit, View} |
15 import org.gjt.sp.jedit.{jEdit, View} |
19 |
16 |
20 |
17 |
21 class Document_Dockable(view: View, position: String) extends Dockable(view, position) { |
18 class Document_Dockable(view: View, position: String) extends Dockable(view, position) { |
54 private val document_session = |
51 private val document_session = |
55 new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) { |
52 new GUI.Selector(JEdit_Sessions.sessions_structure().build_topological_order.sorted) { |
56 val title = "Session" |
53 val title = "Session" |
57 } |
54 } |
58 |
55 |
59 private val build_button = new Button("<html><b>Build</b></html>") { |
56 private val build_button = |
|
57 new GUI.Button("<html><b>Build</b></html>") { |
60 tooltip = "Build document" |
58 tooltip = "Build document" |
61 reactions += { case ButtonClicked(_) => |
59 override def clicked(): Unit = { |
62 pretty_text_area.update( |
60 pretty_text_area.update( |
63 Document.Snapshot.init, Command.Results.empty, |
61 Document.Snapshot.init, Command.Results.empty, |
64 List(XML.Text(Date.now().toString))) // FIXME |
62 List(XML.Text(Date.now().toString))) // FIXME |
65 } |
63 } |
66 } |
64 } |