more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
authorwenzelm
Fri May 08 10:19:44 2015 +0200 (2015-05-08)
changeset 60274c2837a39da01
parent 60273 83de10e27007
child 60275 d8a4fe35da00
more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
clarified Isabelle.buffer_token_marker;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Thu May 07 22:12:05 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri May 08 10:19:44 2015 +0200
     1.3 @@ -50,18 +50,19 @@
     1.4    {
     1.5      GUI_Thread.require {}
     1.6  
     1.7 -    old_model match {
     1.8 -      case Some(old)
     1.9 -      if old.node_name == node_name && Isabelle.buffer_token_marker(buffer).isEmpty => old
    1.10 -
    1.11 -      case _ =>
    1.12 -        apply(buffer).map(_.deactivate)
    1.13 -        val model = new Document_Model(session, buffer, node_name)
    1.14 -        buffer.setProperty(key, model)
    1.15 -        model.activate()
    1.16 -        buffer.propertiesChanged
    1.17 -        model
    1.18 -    }
    1.19 +    val model =
    1.20 +      old_model match {
    1.21 +        case Some(old) if old.node_name == node_name => old
    1.22 +        case _ =>
    1.23 +          apply(buffer).map(_.deactivate)
    1.24 +          val model = new Document_Model(session, buffer, node_name)
    1.25 +          buffer.setProperty(key, model)
    1.26 +          model.activate()
    1.27 +          buffer.propertiesChanged
    1.28 +          model
    1.29 +      }
    1.30 +    model.init_token_marker
    1.31 +    model
    1.32    }
    1.33  }
    1.34  
     2.1 --- a/src/Tools/jEdit/src/isabelle.scala	Thu May 07 22:12:05 2015 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri May 08 10:19:44 2015 +0200
     2.3 @@ -78,10 +78,8 @@
     2.4    def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
     2.5    {
     2.6      val mode = JEdit_Lib.buffer_mode(buffer)
     2.7 -    val new_token_marker =
     2.8 -      if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
     2.9 -      else mode_token_marker(mode)
    2.10 -    if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker
    2.11 +    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
    2.12 +    else mode_token_marker(mode)
    2.13    }
    2.14  
    2.15