src/Tools/jEdit/src/plugin.scala
changeset 44238 36120feb70ed
parent 44225 a8f921e6484f
child 44379 1079ab6b342b
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 15:14:48 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 17 16:01:27 2011 +0200
     1.3 @@ -316,6 +316,24 @@
     1.4      }
     1.5      session.start(timeout, modes ::: List(logic))
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* convenience actions */
    1.10 +
    1.11 +  private def user_input(text_area: JEditTextArea, s1: String, s2: String = "")
    1.12 +  {
    1.13 +    s1.foreach(text_area.userInput(_))
    1.14 +    s2.foreach(text_area.userInput(_))
    1.15 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
    1.16 +  }
    1.17 +
    1.18 +  def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded)
    1.19 +  def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded)
    1.20 +  def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded)
    1.21 +  def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded)
    1.22 +  def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
    1.23 +  def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
    1.24 +  def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
    1.25  }
    1.26  
    1.27