src/Tools/jEdit/src/isabelle_actions.scala
author wenzelm
Sat Nov 24 14:50:19 2012 +0100 (2012-11-24 ago)
changeset 50183 2b3e24e1c9e7
child 50187 b5a09812abc4
permissions -rw-r--r--
improved editing support for control styles;
separate module for Isabelle actions;
wenzelm@50183
     1
/*  Title:      Tools/jEdit/src/plugin.scala
wenzelm@50183
     2
    Author:     Makarius
wenzelm@50183
     3
wenzelm@50183
     4
Convenience actions for Isabelle/jEdit.
wenzelm@50183
     5
*/
wenzelm@50183
     6
wenzelm@50183
     7
package isabelle.jedit
wenzelm@50183
     8
wenzelm@50183
     9
wenzelm@50183
    10
import isabelle._
wenzelm@50183
    11
wenzelm@50183
    12
import org.gjt.sp.jedit.Buffer
wenzelm@50183
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@50183
    14
wenzelm@50183
    15
wenzelm@50183
    16
object Isabelle_Actions
wenzelm@50183
    17
{
wenzelm@50183
    18
  /* full checking */
wenzelm@50183
    19
wenzelm@50183
    20
  def check_buffer(buffer: Buffer)
wenzelm@50183
    21
  {
wenzelm@50183
    22
    Isabelle.document_model(buffer) match {
wenzelm@50183
    23
      case None =>
wenzelm@50183
    24
      case Some(model) => model.full_perspective()
wenzelm@50183
    25
    }
wenzelm@50183
    26
  }
wenzelm@50183
    27
wenzelm@50183
    28
wenzelm@50183
    29
  def cancel_execution() { Isabelle.session.cancel_execution() }
wenzelm@50183
    30
wenzelm@50183
    31
  /* control styles */
wenzelm@50183
    32
wenzelm@50183
    33
  def control_sub(text_area: JEditTextArea)
wenzelm@50183
    34
  { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
    35
wenzelm@50183
    36
  def control_sup(text_area: JEditTextArea)
wenzelm@50183
    37
  { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
    38
wenzelm@50183
    39
  def control_isub(text_area: JEditTextArea)
wenzelm@50183
    40
  { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
wenzelm@50183
    41
wenzelm@50183
    42
  def control_isup(text_area: JEditTextArea)
wenzelm@50183
    43
  { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
wenzelm@50183
    44
wenzelm@50183
    45
  def control_bold(text_area: JEditTextArea)
wenzelm@50183
    46
  { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
    47
wenzelm@50183
    48
  def control_reset(text_area: JEditTextArea)
wenzelm@50183
    49
  { Token_Markup.edit_ctrl_style(text_area, "") }
wenzelm@50183
    50
wenzelm@50183
    51
wenzelm@50183
    52
  /* block styles */
wenzelm@50183
    53
wenzelm@50183
    54
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
    55
  {
wenzelm@50183
    56
    s1.foreach(text_area.userInput(_))
wenzelm@50183
    57
    s2.foreach(text_area.userInput(_))
wenzelm@50183
    58
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
    59
  }
wenzelm@50183
    60
wenzelm@50183
    61
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
    62
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
    63
wenzelm@50183
    64
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
    65
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
    66
}
wenzelm@50183
    67