init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
authorwenzelm
Wed Jun 22 20:25:35 2011 +0200 (2011-06-22)
changeset 4351017d431c92575
parent 43509 4414c8b02bf9
child 43511 d138e7482a1b
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 22 20:21:22 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 22 20:25:35 2011 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4        Swing_Thread.require()
     1.5        if (model.buffer == text_area.getBuffer) body
     1.6        else {
     1.7 -        // FIXME Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
     1.8 +        Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
     1.9          default
    1.10        }
    1.11      }
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:21:22 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:25:35 2011 +0200
     2.3 @@ -191,6 +191,54 @@
     2.4    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     2.5    def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
     2.6  
     2.7 +  def init_model(buffer: Buffer)
     2.8 +  {
     2.9 +    swing_buffer_lock(buffer) {
    2.10 +      val opt_model =
    2.11 +        document_model(buffer) match {
    2.12 +          case Some(model) => Some(model)
    2.13 +          case None =>
    2.14 +            // FIXME strip protocol prefix of URL
    2.15 +            Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
    2.16 +              case Some((dir, thy_name)) =>
    2.17 +                Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
    2.18 +              case None => None
    2.19 +            }
    2.20 +        }
    2.21 +      if (opt_model.isDefined) {
    2.22 +        for (text_area <- jedit_text_areas(buffer)) {
    2.23 +          if (document_view(text_area).map(_.model) != opt_model)
    2.24 +            Document_View.init(opt_model.get, text_area)
    2.25 +        }
    2.26 +      }
    2.27 +    }
    2.28 +  }
    2.29 +
    2.30 +  def exit_model(buffer: Buffer)
    2.31 +  {
    2.32 +    swing_buffer_lock(buffer) {
    2.33 +      jedit_text_areas(buffer).foreach(Document_View.exit)
    2.34 +      Document_Model.exit(buffer)
    2.35 +    }
    2.36 +  }
    2.37 +
    2.38 +  def init_view(buffer: Buffer, text_area: JEditTextArea)
    2.39 +  {
    2.40 +    swing_buffer_lock(buffer) {
    2.41 +      document_model(buffer) match {
    2.42 +        case Some(model) => Document_View.init(model, text_area)
    2.43 +        case None =>
    2.44 +      }
    2.45 +    }
    2.46 +  }
    2.47 +
    2.48 +  def exit_view(buffer: Buffer, text_area: JEditTextArea)
    2.49 +  {
    2.50 +    swing_buffer_lock(buffer) {
    2.51 +      Document_View.exit(text_area)
    2.52 +    }
    2.53 +  }
    2.54 +
    2.55  
    2.56    /* dockable windows */
    2.57  
    2.58 @@ -267,47 +315,13 @@
    2.59  {
    2.60    /* session management */
    2.61  
    2.62 -  private def init_model(buffer: Buffer)
    2.63 -  {
    2.64 -    Isabelle.swing_buffer_lock(buffer) {
    2.65 -      val opt_model =
    2.66 -        Document_Model(buffer) match {
    2.67 -          case Some(model) => Some(model)
    2.68 -          case None =>
    2.69 -            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
    2.70 -              case Some((dir, thy_name)) =>
    2.71 -                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
    2.72 -              case None => None
    2.73 -            }
    2.74 -        }
    2.75 -      if (opt_model.isDefined) {
    2.76 -        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    2.77 -          if (Document_View(text_area).map(_.model) != opt_model)
    2.78 -            Document_View.init(opt_model.get, text_area)
    2.79 -        }
    2.80 -      }
    2.81 -    }
    2.82 -  }
    2.83 -
    2.84 -  private def exit_model(buffer: Buffer)
    2.85 -  {
    2.86 -    Isabelle.swing_buffer_lock(buffer) {
    2.87 -      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
    2.88 -      Document_Model.exit(buffer)
    2.89 -    }
    2.90 -  }
    2.91 -
    2.92 -  private case class Init_Model(buffer: Buffer)
    2.93 -  private case class Exit_Model(buffer: Buffer)
    2.94 -  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
    2.95 -  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
    2.96 +  @volatile private var session_ready = false
    2.97  
    2.98    private val session_manager = actor {
    2.99 -    var ready = false
   2.100      loop {
   2.101        react {
   2.102          case phase: Session.Phase =>
   2.103 -          ready = phase == Session.Ready
   2.104 +          session_ready = phase == Session.Ready
   2.105            phase match {
   2.106              case Session.Failed =>
   2.107                Swing_Thread.now {
   2.108 @@ -316,32 +330,11 @@
   2.109                  Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
   2.110                }
   2.111  
   2.112 -            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
   2.113 -            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
   2.114 +            case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
   2.115 +            case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
   2.116              case _ =>
   2.117            }
   2.118  
   2.119 -        case Init_Model(buffer) =>
   2.120 -          if (ready) init_model(buffer)
   2.121 -
   2.122 -        case Exit_Model(buffer) =>
   2.123 -          exit_model(buffer)
   2.124 -
   2.125 -        case Init_View(buffer, text_area) =>
   2.126 -          if (ready) {
   2.127 -            Isabelle.swing_buffer_lock(buffer) {
   2.128 -              Document_Model(buffer) match {
   2.129 -                case Some(model) => Document_View.init(model, text_area)
   2.130 -                case None =>
   2.131 -              }
   2.132 -            }
   2.133 -          }
   2.134 -
   2.135 -        case Exit_View(buffer, text_area) =>
   2.136 -          Isabelle.swing_buffer_lock(buffer) {
   2.137 -            Document_View.exit(text_area)
   2.138 -          }
   2.139 -
   2.140          case bad => System.err.println("session_manager: ignoring bad message " + bad)
   2.141        }
   2.142      }
   2.143 @@ -352,16 +345,19 @@
   2.144  
   2.145    override def handleMessage(message: EBMessage)
   2.146    {
   2.147 +    Swing_Thread.assert()
   2.148      message match {
   2.149        case msg: EditorStarted =>
   2.150 -      Isabelle.check_jvm()
   2.151 -      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
   2.152 +        Isabelle.check_jvm()
   2.153 +        if (Isabelle.Boolean_Property("auto-start"))
   2.154 +          Isabelle.start_session()
   2.155  
   2.156        case msg: BufferUpdate
   2.157        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   2.158  
   2.159          val buffer = msg.getBuffer
   2.160 -        if (buffer != null) session_manager ! Init_Model(buffer)
   2.161 +        if (buffer != null && session_ready)
   2.162 +          Isabelle.init_model(buffer)
   2.163  
   2.164        case msg: EditPaneUpdate
   2.165        if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
   2.166 @@ -375,10 +371,11 @@
   2.167  
   2.168          if (buffer != null && text_area != null) {
   2.169            if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   2.170 -              msg.getWhat == EditPaneUpdate.CREATED)
   2.171 -            session_manager ! Init_View(buffer, text_area)
   2.172 -          else
   2.173 -            session_manager ! Exit_View(buffer, text_area)
   2.174 +              msg.getWhat == EditPaneUpdate.CREATED) {
   2.175 +            if (session_ready)
   2.176 +              Isabelle.init_view(buffer, text_area)
   2.177 +          }
   2.178 +          else Isabelle.exit_view(buffer, text_area)
   2.179          }
   2.180  
   2.181        case msg: PropertiesChanged =>