src/Tools/jEdit/src/plugin.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56770 e160ae47db94
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Fri Apr 25 12:51:08 2014 +0200
     1.3 @@ -22,8 +22,6 @@
     1.4  
     1.5  import org.gjt.sp.util.SyntaxUtilities
     1.6  
     1.7 -import scala.actors.Actor._
     1.8 -
     1.9  
    1.10  object PIDE
    1.11  {
    1.12 @@ -174,7 +172,7 @@
    1.13  
    1.14    def options_changed()
    1.15    {
    1.16 -    PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
    1.17 +    PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value))
    1.18      Swing_Thread.later { delay_load.invoke() }
    1.19    }
    1.20  
    1.21 @@ -244,34 +242,27 @@
    1.22      }
    1.23  
    1.24  
    1.25 -  /* session manager */
    1.26 +  /* session phase */
    1.27  
    1.28 -  private val session_manager = actor {
    1.29 -    loop {
    1.30 -      react {
    1.31 -        case phase: Session.Phase =>
    1.32 -          phase match {
    1.33 -            case Session.Inactive | Session.Failed =>
    1.34 -              Swing_Thread.later {
    1.35 -                GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
    1.36 -                    "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
    1.37 -              }
    1.38 +  private val session_phase =
    1.39 +    Session.Consumer[Session.Phase](getClass.getName) {
    1.40 +      case Session.Inactive | Session.Failed =>
    1.41 +        Swing_Thread.later {
    1.42 +          GUI.error_dialog(jEdit.getActiveView, "Prover process terminated",
    1.43 +              "Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog()))
    1.44 +        }
    1.45  
    1.46 -            case Session.Ready =>
    1.47 -              PIDE.session.update_options(PIDE.options.value)
    1.48 -              PIDE.init_models()
    1.49 -              Swing_Thread.later { delay_load.invoke() }
    1.50 +      case Session.Ready =>
    1.51 +        PIDE.session.update_options(PIDE.options.value)
    1.52 +        PIDE.init_models()
    1.53 +        Swing_Thread.later { delay_load.invoke() }
    1.54  
    1.55 -            case Session.Shutdown =>
    1.56 -              PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    1.57 -              Swing_Thread.later { delay_load.revoke() }
    1.58 +      case Session.Shutdown =>
    1.59 +        PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    1.60 +        Swing_Thread.later { delay_load.revoke() }
    1.61  
    1.62 -            case _ =>
    1.63 -          }
    1.64 -        case bad => System.err.println("session_manager: ignoring bad message " + bad)
    1.65 -      }
    1.66 +      case _ =>
    1.67      }
    1.68 -  }
    1.69  
    1.70  
    1.71    /* main plugin plumbing */
    1.72 @@ -366,7 +357,7 @@
    1.73          override def reparse_limit = PIDE.options.int("editor_reparse_limit")
    1.74        }
    1.75  
    1.76 -      PIDE.session.phase_changed += session_manager
    1.77 +      PIDE.session.phase_changed += session_phase
    1.78        PIDE.startup_failure = None
    1.79      }
    1.80      catch {
    1.81 @@ -385,7 +376,7 @@
    1.82        PIDE.completion_history.value.save()
    1.83      }
    1.84  
    1.85 -    PIDE.session.phase_changed -= session_manager
    1.86 +    PIDE.session.phase_changed -= session_phase
    1.87      PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
    1.88      PIDE.session.stop()
    1.89    }