# HG changeset patch # User wenzelm # Date 1438177977 -7200 # Node ID 1cdc63224ed3fa5b0e15d04afaa49deba534657e # Parent 5b99a334fd4cf91b63f1c8d7c041a41ace5426f2 more GUI components; diff -r 5b99a334fd4c -r 1cdc63224ed3 src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Wed Jul 29 14:04:19 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Wed Jul 29 15:52:57 2015 +0200 @@ -10,7 +10,10 @@ import isabelle._ import java.awt.BorderLayout -import java.awt.event.{ComponentEvent, ComponentAdapter} +import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} + +import scala.swing.{Button, Label, Component} +import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.View @@ -26,6 +29,48 @@ private var current_output: List[XML.Tree] = Nil + /* common GUI components */ + + private val context_label = new Label("Context:") { tooltip = "Isabelle/ML context (optional)" } + private val context_field = + new Completion_Popup.History_Text_Field("isabelle-debugger-context") + { + setColumns(20) + setToolTipText(context_label.tooltip) + setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2)) + } + + private val expression_label = new Label("ML:") { tooltip = "Isabelle/ML expression" } + private val expression_field = + new Completion_Popup.History_Text_Field("isabelle-debugger-expression") + { + override def processKeyEvent(evt: KeyEvent) + { + if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) + eval_expression() + super.processKeyEvent(evt) + } + { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) } + setColumns(40) + setToolTipText(expression_label.tooltip) + setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2)) + } + + private val eval_button = new Button("Eval") { + tooltip = "Evaluate Isabelle/ML expression within optional context" + reactions += { case ButtonClicked(_) => eval_expression() } + } + + private def eval_expression() + { + // FIXME + Output.writeln("eval context = " + quote(context_field.getText) + " expression = " + + quote(expression_field.getText)) + } + + private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } + + /* pretty text area */ val pretty_text_area = new Pretty_Text_Area(view) @@ -34,8 +79,6 @@ override def detach_operation = pretty_text_area.detach_operation - private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() } - private def handle_resize() { GUI_Thread.require {} @@ -100,6 +143,8 @@ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)( + context_label, Component.wrap(context_field), + expression_label, Component.wrap(expression_field), eval_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom) add(controls.peer, BorderLayout.NORTH) }