# HG changeset patch # User wenzelm # Date 1660328453 -7200 # Node ID b054f22efd0d976754dcfd4e224fc87697b0b0f4 # Parent b8a4f9b1eed622d82a3f5d43b07d63cd370372eb more GUI elements; diff -r b8a4f9b1eed6 -r b054f22efd0d src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Fri Aug 12 20:14:20 2022 +0200 +++ b/src/Tools/jEdit/src/document_dockable.scala Fri Aug 12 20:20:53 2022 +0200 @@ -12,8 +12,8 @@ import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter} -import scala.swing.Button -import scala.swing.event.ButtonClicked +import scala.swing.{ComboBox, Button} +import scala.swing.event.{SelectionChanged, ButtonClicked} import org.gjt.sp.jedit.{jEdit, View} @@ -51,6 +51,14 @@ /* controls */ + private val document_session: ComboBox[String] = { + new ComboBox(JEdit_Sessions.sessions_structure().build_topological_order.sorted) { + val title = "Session" + listenTo(selection) + reactions += { case SelectionChanged(_) => } // FIXME + } + } + private val build_button = new Button("Build") { tooltip = "Build document" reactions += { case ButtonClicked(_) => @@ -63,7 +71,7 @@ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() } private val controls = - Wrap_Panel(List(process_indicator.component, build_button, + Wrap_Panel(List(document_session, process_indicator.component, build_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom)) add(controls.peer, BorderLayout.NORTH)