# HG changeset patch
# User wenzelm
# Date 1346705407 -7200
# Node ID 21c8d2070be9a8afed67e5022fd01b9b7ecf8d4d
# Parent  e7aecf2a5fc4c5a2a4a9372454f67a89cc8ad1e0
continue with more robust dummy session after failed startup;

diff -r e7aecf2a5fc4 -r 21c8d2070be9 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 22:31:27 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 22:50:07 2012 +0200
@@ -34,19 +34,20 @@
 {
   /* plugin instance */
 
-  @volatile var plugin: Plugin = null
-  @volatile var session: Session = null
   @volatile var startup_failure: Option[Throwable] = None
   @volatile var startup_notified = false
 
+  @volatile var plugin: Plugin = null
+  @volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty))
+
   def thy_load(): JEdit_Thy_Load =
     session.thy_load.asInstanceOf[JEdit_Thy_Load]
 
   def get_recent_syntax(): Option[Outer_Syntax] =
   {
     val current_session = session
-    if (current_session != null) Some(current_session.recent_syntax)
-    else None
+    if (current_session.recent_syntax == Outer_Syntax.empty) None
+    else Some(current_session.recent_syntax)
   }
 
 
@@ -508,8 +509,6 @@
     }
     catch {
       case exn: Throwable =>
-        stop()
-        Isabelle.session = null
         Isabelle.startup_failure = Some(exn)
         Isabelle.startup_notified = false
     }
@@ -517,10 +516,8 @@
 
   override def stop()
   {
-    if (Isabelle.session != null) {
-      Isabelle.session.phase_changed -= session_manager
-      Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
-      Isabelle.session.stop()
-    }
+    Isabelle.session.phase_changed -= session_manager
+    Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+    Isabelle.session.stop()
   }
 }