src/Tools/jEdit/src/document_view.scala
changeset 58748 8f92f17d8781
parent 57612 990ffb84489b
child 59129 6959ceb53ac8
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Tue Oct 21 13:56:42 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Tue Oct 21 15:21:44 2014 +0200
     1.3 @@ -251,6 +251,8 @@
     1.4      text_area.addKeyListener(key_listener)
     1.5      text_area.addCaretListener(caret_listener)
     1.6      text_area.addLeftOfScrollBar(overview)
     1.7 +    Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
     1.8 +      foreach(text_area.addStructureMatcher(_))
     1.9      session.raw_edits += main
    1.10      session.commands_changed += main
    1.11    }
    1.12 @@ -261,6 +263,8 @@
    1.13  
    1.14      session.raw_edits -= main
    1.15      session.commands_changed -= main
    1.16 +    Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
    1.17 +      foreach(text_area.removeStructureMatcher(_))
    1.18      text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
    1.19      text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
    1.20      text_area.removeKeyListener(key_listener)