# HG changeset patch
# User wenzelm
# Date 1498556987 -7200
# Node ID d8f2c745f572d401e6c8f331ce84907c85a45c40
# Parent  02c66b71c01372303496256a003a83d6fbde1a24
GUI controls similar to Tools/jEdit/src/state_dockable.scala;

diff -r 02c66b71c013 -r d8f2c745f572 src/Tools/VSCode/src/state_panel.scala
--- a/src/Tools/VSCode/src/state_panel.scala	Tue Jun 27 11:47:14 2017 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala	Tue Jun 27 11:49:47 2017 +0200
@@ -62,9 +62,7 @@
             HTML.output_document(
               List(HTML.style(HTML.fonts_css()),
                 HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
-              List(
-                HTML.chapter("Proof state"),
-                HTML.source(text)),
+              List(controls, HTML.source(text)),
               css = "")
           output(content)
         })
@@ -93,6 +91,36 @@
   def auto_update() { if (auto_update_enabled.value) update() }
 
 
+  /* controls */
+
+  private def id_parameter: XML.Elem =
+    HTML.GUI.parameter(id.toString, name = "id")
+
+  private def auto_update_button: XML.Elem =
+    HTML.GUI.checkbox(HTML.text("Auto update"),
+      name = "auto_update",
+      tooltip = "Indicate automatic update following cursor movement",
+      submit = true,
+      selected = auto_update_enabled.value)
+
+  private def update_button: XML.Elem =
+    HTML.GUI.button(List(HTML.bold(HTML.text("Update"))),
+      name = "update",
+      tooltip = "Update display according to the command at cursor position",
+      submit = true)
+
+  private def locate_button: XML.Elem =
+    HTML.GUI.button(HTML.text("Locate"),
+      name = "locate",
+      tooltip = "Locate printed command within source text",
+      submit = true)
+
+  private val controls: XML.Elem =
+    HTML.Wrap_Panel(
+      contents = List(id_parameter, auto_update_button, update_button, locate_button),
+      alignment = HTML.Wrap_Panel.Alignment.right)
+
+
   /* main */
 
   private val main =