src/Tools/jEdit/src/plugin.scala
changeset 43510 17d431c92575
parent 43487 98cd7e83fc5b
child 43513 06951ddfc812
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:21:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:25:35 2011 +0200
     1.3 @@ -191,6 +191,54 @@
     1.4    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     1.5    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
     1.6  
     1.7 +  def init_model(buffer: Buffer)
     1.8 +  {
     1.9 +    swing_buffer_lock(buffer) {
    1.10 +      val opt_model =
    1.11 +        document_model(buffer) match {
    1.12 +          case Some(model) => Some(model)
    1.13 +          case None =>
    1.14 +            // FIXME strip protocol prefix of URL
    1.15 +            Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
    1.16 +              case Some((dir, thy_name)) =>
    1.17 +                Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
    1.18 +              case None => None
    1.19 +            }
    1.20 +        }
    1.21 +      if (opt_model.isDefined) {
    1.22 +        for (text_area <- jedit_text_areas(buffer)) {
    1.23 +          if (document_view(text_area).map(_.model) != opt_model)
    1.24 +            Document_View.init(opt_model.get, text_area)
    1.25 +        }
    1.26 +      }
    1.27 +    }
    1.28 +  }
    1.29 +
    1.30 +  def exit_model(buffer: Buffer)
    1.31 +  {
    1.32 +    swing_buffer_lock(buffer) {
    1.33 +      jedit_text_areas(buffer).foreach(Document_View.exit)
    1.34 +      Document_Model.exit(buffer)
    1.35 +    }
    1.36 +  }
    1.37 +
    1.38 +  def init_view(buffer: Buffer, text_area: JEditTextArea)
    1.39 +  {
    1.40 +    swing_buffer_lock(buffer) {
    1.41 +      document_model(buffer) match {
    1.42 +        case Some(model) => Document_View.init(model, text_area)
    1.43 +        case None =>
    1.44 +      }
    1.45 +    }
    1.46 +  }
    1.47 +
    1.48 +  def exit_view(buffer: Buffer, text_area: JEditTextArea)
    1.49 +  {
    1.50 +    swing_buffer_lock(buffer) {
    1.51 +      Document_View.exit(text_area)
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55  
    1.56    /* dockable windows */
    1.57  
    1.58 @@ -267,47 +315,13 @@
    1.59  {
    1.60    /* session management */
    1.61  
    1.62 -  private def init_model(buffer: Buffer)
    1.63 -  {
    1.64 -    Isabelle.swing_buffer_lock(buffer) {
    1.65 -      val opt_model =
    1.66 -        Document_Model(buffer) match {
    1.67 -          case Some(model) => Some(model)
    1.68 -          case None =>
    1.69 -            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
    1.70 -              case Some((dir, thy_name)) =>
    1.71 -                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
    1.72 -              case None => None
    1.73 -            }
    1.74 -        }
    1.75 -      if (opt_model.isDefined) {
    1.76 -        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    1.77 -          if (Document_View(text_area).map(_.model) != opt_model)
    1.78 -            Document_View.init(opt_model.get, text_area)
    1.79 -        }
    1.80 -      }
    1.81 -    }
    1.82 -  }
    1.83 -
    1.84 -  private def exit_model(buffer: Buffer)
    1.85 -  {
    1.86 -    Isabelle.swing_buffer_lock(buffer) {
    1.87 -      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
    1.88 -      Document_Model.exit(buffer)
    1.89 -    }
    1.90 -  }
    1.91 -
    1.92 -  private case class Init_Model(buffer: Buffer)
    1.93 -  private case class Exit_Model(buffer: Buffer)
    1.94 -  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
    1.95 -  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
    1.96 +  @volatile private var session_ready = false
    1.97  
    1.98    private val session_manager = actor {
    1.99 -    var ready = false
   1.100      loop {
   1.101        react {
   1.102          case phase: Session.Phase =>
   1.103 -          ready = phase == Session.Ready
   1.104 +          session_ready = phase == Session.Ready
   1.105            phase match {
   1.106              case Session.Failed =>
   1.107                Swing_Thread.now {
   1.108 @@ -316,32 +330,11 @@
   1.109                  Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
   1.110                }
   1.111  
   1.112 -            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
   1.113 -            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
   1.114 +            case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
   1.115 +            case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   1.116              case _ =>
   1.117            }
   1.118  
   1.119 -        case Init_Model(buffer) =>
   1.120 -          if (ready) init_model(buffer)
   1.121 -
   1.122 -        case Exit_Model(buffer) =>
   1.123 -          exit_model(buffer)
   1.124 -
   1.125 -        case Init_View(buffer, text_area) =>
   1.126 -          if (ready) {
   1.127 -            Isabelle.swing_buffer_lock(buffer) {
   1.128 -              Document_Model(buffer) match {
   1.129 -                case Some(model) => Document_View.init(model, text_area)
   1.130 -                case None =>
   1.131 -              }
   1.132 -            }
   1.133 -          }
   1.134 -
   1.135 -        case Exit_View(buffer, text_area) =>
   1.136 -          Isabelle.swing_buffer_lock(buffer) {
   1.137 -            Document_View.exit(text_area)
   1.138 -          }
   1.139 -
   1.140          case bad => System.err.println("session_manager: ignoring bad message " + bad)
   1.141        }
   1.142      }
   1.143 @@ -352,16 +345,19 @@
   1.144  
   1.145    override def handleMessage(message: EBMessage)
   1.146    {
   1.147 +    Swing_Thread.assert()
   1.148      message match {
   1.149        case msg: EditorStarted =>
   1.150 -      Isabelle.check_jvm()
   1.151 -      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
   1.152 +        Isabelle.check_jvm()
   1.153 +        if (Isabelle.Boolean_Property("auto-start"))
   1.154 +          Isabelle.start_session()
   1.155  
   1.156        case msg: BufferUpdate
   1.157        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   1.158  
   1.159          val buffer = msg.getBuffer
   1.160 -        if (buffer != null) session_manager ! Init_Model(buffer)
   1.161 +        if (buffer != null && session_ready)
   1.162 +          Isabelle.init_model(buffer)
   1.163  
   1.164        case msg: EditPaneUpdate
   1.165        if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   1.166 @@ -375,10 +371,11 @@
   1.167  
   1.168          if (buffer != null && text_area != null) {
   1.169            if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   1.170 -              msg.getWhat == EditPaneUpdate.CREATED)
   1.171 -            session_manager ! Init_View(buffer, text_area)
   1.172 -          else
   1.173 -            session_manager ! Exit_View(buffer, text_area)
   1.174 +              msg.getWhat == EditPaneUpdate.CREATED) {
   1.175 +            if (session_ready)
   1.176 +              Isabelle.init_view(buffer, text_area)
   1.177 +          }
   1.178 +          else Isabelle.exit_view(buffer, text_area)
   1.179          }
   1.180  
   1.181        case msg: PropertiesChanged =>