slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
authorwenzelm
Fri Sep 24 14:14:21 2010 +0200 (2010-09-24)
changeset 39637cc3452317b5f
parent 39636 610dc743932c
child 39638 4293ce5b07fb
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
src/Tools/jEdit/src/jedit/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 24 14:12:33 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Fri Sep 24 14:14:21 2010 +0200
     1.3 @@ -226,10 +226,14 @@
     1.4  
     1.5    private def init_model(buffer: Buffer): Option[Document_Model] =
     1.6    {
     1.7 -    Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
     1.8 -      case Some((_, thy_name)) if Document_Model(buffer).isEmpty =>
     1.9 -        Some(Document_Model.init(Isabelle.session, buffer, thy_name))
    1.10 -      case _ => Document_Model(buffer)
    1.11 +    Document_Model(buffer) match {
    1.12 +      case Some(model) => model.refresh; Some(model)
    1.13 +      case None =>
    1.14 +        Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
    1.15 +          case Some((_, thy_name)) =>
    1.16 +            Some(Document_Model.init(Isabelle.session, buffer, thy_name))
    1.17 +          case None => None
    1.18 +        }
    1.19      }
    1.20    }
    1.21  
    1.22 @@ -240,7 +244,7 @@
    1.23          case None =>
    1.24          case Some(model) =>
    1.25            for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    1.26 -            if (Document_View(text_area).isEmpty)
    1.27 +            if (Document_View(text_area).map(_.model) != Some(model))
    1.28                Document_View.init(model, text_area)
    1.29            }
    1.30        }
    1.31 @@ -250,12 +254,8 @@
    1.32    private def deactivate_buffer(buffer: Buffer)
    1.33    {
    1.34      Isabelle.swing_buffer_lock(buffer) {
    1.35 -      for (text_area <- Isabelle.jedit_text_areas(buffer)) {
    1.36 -        if (Document_View(text_area).isDefined)
    1.37 -          Document_View.exit(text_area)
    1.38 -      }
    1.39 -      if (Document_Model(buffer).isDefined)
    1.40 -        Document_Model.exit(buffer)
    1.41 +      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
    1.42 +      Document_Model.exit(buffer)
    1.43      }
    1.44    }
    1.45  
    1.46 @@ -288,16 +288,12 @@
    1.47          msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    1.48  
    1.49          val buffer = msg.getBuffer
    1.50 -        Isabelle.swing_buffer_lock(buffer) {
    1.51 -          init_model(buffer) match {
    1.52 -            case Some(model) => model.refresh()
    1.53 -            case None =>
    1.54 -          }
    1.55 -        }
    1.56 +        if (buffer != null) activate_buffer(buffer)
    1.57  
    1.58        case msg: EditPaneUpdate
    1.59        if Isabelle.session.phase == Session.Ready &&
    1.60 -        (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.61 +        (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
    1.62 +          msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.63            msg.getWhat == EditPaneUpdate.CREATED ||
    1.64            msg.getWhat == EditPaneUpdate.DESTROYED) =>
    1.65  
    1.66 @@ -305,25 +301,18 @@
    1.67          val buffer = edit_pane.getBuffer
    1.68          val text_area = edit_pane.getTextArea
    1.69  
    1.70 -        def init_view()
    1.71 -        {
    1.72 -          Document_Model(buffer) match {
    1.73 -            case Some(model) => Document_View.init(model, text_area)
    1.74 -            case None =>
    1.75 -          }
    1.76 -        }
    1.77 -        def exit_view()
    1.78 -        {
    1.79 -          if (Document_View(text_area).isDefined)
    1.80 -            Document_View.exit(text_area)
    1.81 -        }
    1.82 -
    1.83 -        Isabelle.swing_buffer_lock(buffer) {
    1.84 -          msg.getWhat match {
    1.85 -            case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
    1.86 -            case EditPaneUpdate.CREATED => init_view()
    1.87 -            case EditPaneUpdate.DESTROYED => exit_view()
    1.88 -            case _ =>
    1.89 +        if (buffer != null && text_area != null) {
    1.90 +          Isabelle.swing_buffer_lock(buffer) {
    1.91 +            msg.getWhat match {
    1.92 +              case EditPaneUpdate.BUFFER_CHANGING | EditPaneUpdate.DESTROYED =>
    1.93 +                Document_View.exit(text_area)
    1.94 +              case EditPaneUpdate.BUFFER_CHANGED | EditPaneUpdate.CREATED =>
    1.95 +                Document_Model(buffer) match {
    1.96 +                  case Some(model) => Document_View.init(model, text_area)
    1.97 +                  case None =>
    1.98 +                }
    1.99 +              case _ =>
   1.100 +            }
   1.101            }
   1.102          }
   1.103