src/Tools/jEdit/src/plugin.scala
changeset 49099 10e899bb6530
parent 49098 673e0ed547af
child 49100 e7aecf2a5fc4
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 21:30:34 2012 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 03 22:22:38 2012 +0200
     1.3 @@ -21,7 +21,8 @@
     1.4  import org.gjt.sp.jedit.buffer.JEditBuffer
     1.5  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     1.6  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
     1.7 -import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     1.8 +import org.gjt.sp.jedit.msg.{EditorStarted, ViewUpdate,
     1.9 +  BufferUpdate, EditPaneUpdate, PropertiesChanged}
    1.10  import org.gjt.sp.jedit.gui.DockableWindowManager
    1.11  
    1.12  import org.gjt.sp.util.SyntaxUtilities
    1.13 @@ -34,8 +35,10 @@
    1.14  {
    1.15    /* plugin instance */
    1.16  
    1.17 -  var plugin: Plugin = null
    1.18 -  var session: Session = null
    1.19 +  @volatile var plugin: Plugin = null
    1.20 +  @volatile var session: Session = null
    1.21 +  @volatile var startup_failure: Option[Throwable] = None
    1.22 +  @volatile var startup_notified = false
    1.23  
    1.24    def thy_load(): JEdit_Thy_Load =
    1.25      session.thy_load.asInstanceOf[JEdit_Thy_Load]
    1.26 @@ -432,66 +435,93 @@
    1.27    override def handleMessage(message: EBMessage)
    1.28    {
    1.29      Swing_Thread.assert()
    1.30 -    message match {
    1.31 -      case msg: EditorStarted =>
    1.32 -        if (Isabelle.Boolean_Property("auto-start"))
    1.33 -          Isabelle.session.start(Isabelle.session_args())
    1.34  
    1.35 -      case msg: BufferUpdate
    1.36 -      if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    1.37 -        if (Isabelle.session.is_ready) {
    1.38 -          val buffer = msg.getBuffer
    1.39 -          if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
    1.40 -          delay_load(true)
    1.41 -        }
    1.42 +    if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) {
    1.43 +      message match {
    1.44 +        case msg: ViewUpdate =>
    1.45 +          Library.error_dialog(msg.getView, "Isabelle plugin startup failure",
    1.46 +            Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)),
    1.47 +            "Prover IDE inactive!")
    1.48 +          Isabelle.startup_notified = true
    1.49 +        case _ =>
    1.50 +      }
    1.51 +    }
    1.52 +
    1.53 +    if (Isabelle.startup_failure.isEmpty) {
    1.54 +      message match {
    1.55 +        case msg: EditorStarted =>
    1.56 +          if (Isabelle.Boolean_Property("auto-start"))
    1.57 +            Isabelle.session.start(Isabelle.session_args())
    1.58  
    1.59 -      case msg: EditPaneUpdate
    1.60 -      if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    1.61 -          msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.62 -          msg.getWhat == EditPaneUpdate.CREATED ||
    1.63 -          msg.getWhat == EditPaneUpdate.DESTROYED) =>
    1.64 -        val edit_pane = msg.getEditPane
    1.65 -        val buffer = edit_pane.getBuffer
    1.66 -        val text_area = edit_pane.getTextArea
    1.67 +        case msg: BufferUpdate
    1.68 +        if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    1.69 +          if (Isabelle.session.is_ready) {
    1.70 +            val buffer = msg.getBuffer
    1.71 +            if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
    1.72 +            delay_load(true)
    1.73 +          }
    1.74  
    1.75 -        if (buffer != null && text_area != null) {
    1.76 -          if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.77 -              msg.getWhat == EditPaneUpdate.CREATED) {
    1.78 -            if (Isabelle.session.is_ready)
    1.79 -              Isabelle.init_view(buffer, text_area)
    1.80 +        case msg: EditPaneUpdate
    1.81 +        if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    1.82 +            msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.83 +            msg.getWhat == EditPaneUpdate.CREATED ||
    1.84 +            msg.getWhat == EditPaneUpdate.DESTROYED) =>
    1.85 +          val edit_pane = msg.getEditPane
    1.86 +          val buffer = edit_pane.getBuffer
    1.87 +          val text_area = edit_pane.getTextArea
    1.88 +
    1.89 +          if (buffer != null && text_area != null) {
    1.90 +            if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.91 +                msg.getWhat == EditPaneUpdate.CREATED) {
    1.92 +              if (Isabelle.session.is_ready)
    1.93 +                Isabelle.init_view(buffer, text_area)
    1.94 +            }
    1.95 +            else Isabelle.exit_view(buffer, text_area)
    1.96            }
    1.97 -          else Isabelle.exit_view(buffer, text_area)
    1.98 -        }
    1.99  
   1.100 -      case msg: PropertiesChanged =>
   1.101 -        Isabelle.setup_tooltips()
   1.102 -        Isabelle.session.global_settings.event(Session.Global_Settings)
   1.103 +        case msg: PropertiesChanged =>
   1.104 +          Isabelle.setup_tooltips()
   1.105 +          Isabelle.session.global_settings.event(Session.Global_Settings)
   1.106  
   1.107 -      case _ =>
   1.108 +        case _ =>
   1.109 +      }
   1.110      }
   1.111    }
   1.112  
   1.113    override def start()
   1.114 -  { // FIXME more robust error handling
   1.115 -    Isabelle.plugin = this
   1.116 -    Isabelle.setup_tooltips()
   1.117 -    Isabelle_System.init()
   1.118 -    Isabelle_System.install_fonts()
   1.119 +  {
   1.120 +    try {
   1.121 +      Isabelle.plugin = this
   1.122 +      Isabelle.setup_tooltips()
   1.123 +      Isabelle_System.init()
   1.124 +      Isabelle_System.install_fonts()
   1.125 +
   1.126 +      SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   1.127 +      if (ModeProvider.instance.isInstanceOf[ModeProvider])
   1.128 +        ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   1.129  
   1.130 -    val content = Isabelle.session_content(false)
   1.131 -    val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   1.132 -    Isabelle.session = new Session(thy_load)
   1.133 +      val content = Isabelle.session_content(false)
   1.134 +      val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
   1.135 +      Isabelle.session = new Session(thy_load)
   1.136  
   1.137 -    SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   1.138 -    if (ModeProvider.instance.isInstanceOf[ModeProvider])
   1.139 -      ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   1.140 -    Isabelle.session.phase_changed += session_manager
   1.141 +      Isabelle.session.phase_changed += session_manager
   1.142 +      Isabelle.startup_failure = None
   1.143 +    }
   1.144 +    catch {
   1.145 +      case exn: Throwable =>
   1.146 +        stop()
   1.147 +        Isabelle.session = null
   1.148 +        Isabelle.startup_failure = Some(exn)
   1.149 +        Isabelle.startup_notified = false
   1.150 +    }
   1.151    }
   1.152  
   1.153    override def stop()
   1.154    {
   1.155 -    Isabelle.session.phase_changed -= session_manager
   1.156 -    Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   1.157 -    Isabelle.session.stop()
   1.158 +    if (Isabelle.session != null) {
   1.159 +      Isabelle.session.phase_changed -= session_manager
   1.160 +      Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   1.161 +      Isabelle.session.stop()
   1.162 +    }
   1.163    }
   1.164  }