more robust types (for scala3);
authorwenzelm
Mon, 04 Apr 2022 22:42:12 +0200
changeset 75404 a1363da718aa
parent 75403 0f80086c000e
child 75405 b13ab7d11b90
more robust types (for scala3);
src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala	Mon Apr 04 22:06:40 2022 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Mon Apr 04 22:42:12 2022 +0200
@@ -93,7 +93,8 @@
           "Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
     }
 
-    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
+    val query: Completion_Popup.History_Text_Field =
+      make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
 
 
     /* GUI page */
@@ -146,17 +147,18 @@
         (snapshot, results, body) =>
           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
 
+    private val query_label = new Label("Find:") {
+      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
+    }
+
+    val query: Completion_Popup.History_Text_Field =
+      make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
+
     private def apply_query(): Unit = {
       query.addCurrentToHistory()
       query_operation.apply_query(List(query.getText))
     }
 
-    private val query_label = new Label("Find:") {
-      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
-    }
-
-    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
-
 
     /* GUI page */