src/Tools/jEdit/src/plugin.scala
changeset 44864 e50557cb0eb6
parent 44721 ba478c3f7255
child 44954 b536b1144eb3
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:28:07 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:48:06 2011 +0200
     1.3 @@ -343,6 +343,16 @@
     1.4    def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
     1.5    def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
     1.6    def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
     1.7 +
     1.8 +  def check_buffer(buffer: Buffer)
     1.9 +  {
    1.10 +    document_model(buffer) match {
    1.11 +      case None =>
    1.12 +      case Some(model) => model.full_perspective()
    1.13 +    }
    1.14 +  }
    1.15 +
    1.16 +  def cancel_execution() { session.cancel_execution() }
    1.17  }
    1.18  
    1.19