src/Tools/jEdit/src/isabelle_actions.scala
changeset 50183 2b3e24e1c9e7
child 50187 b5a09812abc4
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sat Nov 24 14:50:19 2012 +0100
     1.3 @@ -0,0 +1,67 @@
     1.4 +/*  Title:      Tools/jEdit/src/plugin.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Convenience actions for Isabelle/jEdit.
     1.8 +*/
     1.9 +
    1.10 +package isabelle.jedit
    1.11 +
    1.12 +
    1.13 +import isabelle._
    1.14 +
    1.15 +import org.gjt.sp.jedit.Buffer
    1.16 +import org.gjt.sp.jedit.textarea.JEditTextArea
    1.17 +
    1.18 +
    1.19 +object Isabelle_Actions
    1.20 +{
    1.21 +  /* full checking */
    1.22 +
    1.23 +  def check_buffer(buffer: Buffer)
    1.24 +  {
    1.25 +    Isabelle.document_model(buffer) match {
    1.26 +      case None =>
    1.27 +      case Some(model) => model.full_perspective()
    1.28 +    }
    1.29 +  }
    1.30 +
    1.31 +
    1.32 +  def cancel_execution() { Isabelle.session.cancel_execution() }
    1.33 +
    1.34 +  /* control styles */
    1.35 +
    1.36 +  def control_sub(text_area: JEditTextArea)
    1.37 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.sub_decoded) }
    1.38 +
    1.39 +  def control_sup(text_area: JEditTextArea)
    1.40 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.sup_decoded) }
    1.41 +
    1.42 +  def control_isub(text_area: JEditTextArea)
    1.43 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.isub_decoded) }
    1.44 +
    1.45 +  def control_isup(text_area: JEditTextArea)
    1.46 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.isup_decoded) }
    1.47 +
    1.48 +  def control_bold(text_area: JEditTextArea)
    1.49 +  { Token_Markup.edit_ctrl_style(text_area, Symbol.bold_decoded) }
    1.50 +
    1.51 +  def control_reset(text_area: JEditTextArea)
    1.52 +  { Token_Markup.edit_ctrl_style(text_area, "") }
    1.53 +
    1.54 +
    1.55 +  /* block styles */
    1.56 +
    1.57 +  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    1.58 +  {
    1.59 +    s1.foreach(text_area.userInput(_))
    1.60 +    s2.foreach(text_area.userInput(_))
    1.61 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
    1.62 +  }
    1.63 +
    1.64 +  def input_bsub(text_area: JEditTextArea)
    1.65 +  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    1.66 +
    1.67 +  def input_bsup(text_area: JEditTextArea)
    1.68 +  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    1.69 +}
    1.70 +