proper asynchronous GUI interaction for somewhat heavy JEdit_Sessions.session_build check;
--- 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)))
+ }
}
}