maintain history more often;

--- a/src/Tools/jEdit/src/debugger_dockable.scala	Thu Aug 06 23:20:15 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Fri Aug 07 11:44:11 2015 +0200
@@ -212,6 +212,8 @@
 
   private def eval_expression()
   {
+    context_field.addCurrentToHistory()
+    expression_field.addCurrentToHistory()
     tree_selection() match {
       case Some((t, opt_index)) if t.debug_states.nonEmpty =>
         Debugger.eval(t.thread_name, opt_index getOrElse 0,

--- a/src/Tools/jEdit/src/query_dockable.scala	Thu Aug 06 23:20:15 2015 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Fri Aug 07 11:44:11 2015 +0200
@@ -37,7 +37,8 @@
 
   private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
 
-  private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
+  private def make_query(property: String, tooltip: String, apply_query: () => Unit)
+      : Completion_Popup.History_Text_Field =
     new Completion_Popup.History_Text_Field(property)
     {
       override def processKeyEvent(evt: KeyEvent)
@@ -83,6 +84,7 @@
 
     private def apply_query()
     {
+      query.addCurrentToHistory()
       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
     }
 
@@ -148,6 +150,7 @@
 
     private def apply_query()
     {
+      query.addCurrentToHistory()
       query_operation.apply_query(List(query.getText))
     }
 

--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala	Thu Aug 06 23:20:15 2015 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala	Fri Aug 07 11:44:11 2015 +0200
@@ -73,6 +73,7 @@
   /* controls */
 
   private def clicked {
+    provers.addCurrentToHistory()
     PIDE.options.string("sledgehammer_provers") = provers.getText
     sledgehammer.apply_query(
       List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))