proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
authorwenzelm
Tue, 07 Apr 2020 21:07:28 +0200
changeset 71941 c255ed582095
parent 71940 522994a6c10e
child 71942 a5fda30edae2
proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Apr 07 20:36:09 2020 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Apr 07 21:07:28 2020 +0200
@@ -291,8 +291,8 @@
 
   private def init_editor(view: View)
   {
+    Keymap_Merge.check_dialog(view)
     Session_Build.check_dialog(view)
-    Keymap_Merge.check_dialog(view)
   }
 
   private def init_title(view: View)
--- a/src/Tools/jEdit/src/session_build.scala	Tue Apr 07 20:36:09 2020 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Tue Apr 07 21:07:28 2020 +0200
@@ -23,18 +23,18 @@
 {
   def check_dialog(view: View)
   {
-    GUI_Thread.require {}
-
     val options = PIDE.options.value
-    try {
-      if (JEdit_Sessions.session_no_build ||
+    Isabelle_Thread.fork() {
+      try {
+        if (JEdit_Sessions.session_no_build ||
           JEdit_Sessions.session_build(options, no_build = true) == 0)
-            JEdit_Sessions.session_start(options)
-      else new Dialog(view)
-    }
-    catch {
-      case exn: Throwable =>
-        GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+          JEdit_Sessions.session_start(options)
+        else GUI_Thread.later { new Dialog(view) }
+      }
+      catch {
+        case exn: Throwable =>
+          GUI.dialog(view, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
+      }
     }
   }