src/Tools/jEdit/src/document_view.scala
changeset 62985 4be23c432491
parent 62092 9ace5f5bae69
child 62986 9d2fae6b31cc
equal deleted inserted replaced
62984:61b32a6d87e9 62985:4be23c432491
   192   }
   192   }
   193 
   193 
   194 
   194 
   195   /* text status overview left of scrollbar */
   195   /* text status overview left of scrollbar */
   196 
   196 
   197   private val overview = new Text_Overview(this)
   197   private val text_overview = new Text_Overview(this)
   198 
   198 
   199 
   199 
   200   /* main */
   200   /* main */
   201 
   201 
   202   private val main =
   202   private val main =
   203     Session.Consumer[Any](getClass.getName) {
   203     Session.Consumer[Any](getClass.getName) {
   204       case _: Session.Raw_Edits =>
   204       case _: Session.Raw_Edits =>
   205         overview.invoke()
   205         text_overview.invoke()
   206 
   206 
   207       case changed: Session.Commands_Changed =>
   207       case changed: Session.Commands_Changed =>
   208         val buffer = model.buffer
   208         val buffer = model.buffer
   209         GUI_Thread.later {
   209         GUI_Thread.later {
   210           JEdit_Lib.buffer_lock(buffer) {
   210           JEdit_Lib.buffer_lock(buffer) {
   215                 snapshot.load_commands.exists(changed.commands.contains)
   215                 snapshot.load_commands.exists(changed.commands.contains)
   216 
   216 
   217               if (changed.assignment || load_changed ||
   217               if (changed.assignment || load_changed ||
   218                   (changed.nodes.contains(model.node_name) &&
   218                   (changed.nodes.contains(model.node_name) &&
   219                    changed.commands.exists(snapshot.node.commands.contains)))
   219                    changed.commands.exists(snapshot.node.commands.contains)))
   220                 overview.invoke()
   220                 text_overview.invoke()
   221 
   221 
   222               val visible_lines = text_area.getVisibleLines
   222               val visible_lines = text_area.getVisibleLines
   223               if (visible_lines > 0) {
   223               if (visible_lines > 0) {
   224                 if (changed.assignment || load_changed)
   224                 if (changed.assignment || load_changed)
   225                   text_area.invalidateScreenLineRange(0, visible_lines)
   225                   text_area.invalidateScreenLineRange(0, visible_lines)
   254     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
   254     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_view)
   255     rich_text_area.activate()
   255     rich_text_area.activate()
   256     text_area.getGutter.addExtension(gutter_painter)
   256     text_area.getGutter.addExtension(gutter_painter)
   257     text_area.addKeyListener(key_listener)
   257     text_area.addKeyListener(key_listener)
   258     text_area.addCaretListener(caret_listener)
   258     text_area.addCaretListener(caret_listener)
   259     text_area.addLeftOfScrollBar(overview); text_area.revalidate(); text_area.repaint()
   259     text_area.addLeftOfScrollBar(text_overview); text_area.revalidate(); text_area.repaint()
   260     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   260     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   261       foreach(text_area.addStructureMatcher(_))
   261       foreach(text_area.addStructureMatcher(_))
   262     session.raw_edits += main
   262     session.raw_edits += main
   263     session.commands_changed += main
   263     session.commands_changed += main
   264   }
   264   }
   269 
   269 
   270     session.raw_edits -= main
   270     session.raw_edits -= main
   271     session.commands_changed -= main
   271     session.commands_changed -= main
   272     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   272     Isabelle.structure_matchers(JEdit_Lib.buffer_mode(text_area.getBuffer)).
   273       foreach(text_area.removeStructureMatcher(_))
   273       foreach(text_area.removeStructureMatcher(_))
   274     overview.revoke(); text_area.removeLeftOfScrollBar(overview)
   274     text_overview.revoke(); text_area.removeLeftOfScrollBar(text_overview)
   275     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   275     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
   276     text_area.removeKeyListener(key_listener)
   276     text_area.removeKeyListener(key_listener)
   277     text_area.getGutter.removeExtension(gutter_painter)
   277     text_area.getGutter.removeExtension(gutter_painter)
   278     rich_text_area.deactivate()
   278     rich_text_area.deactivate()
   279     painter.removeExtension(update_view)
   279     painter.removeExtension(update_view)