src/Tools/jEdit/src/isabelle.scala
changeset 50208 1382ad6d4774
parent 50206 6626bc5ed053
child 50209 907373a080b9
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Nov 25 21:35:29 2012 +0100
     1.3 @@ -0,0 +1,112 @@
     1.4 +/*  Title:      Tools/jEdit/src/isabelle.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Convenience operations 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.{jEdit, View, Buffer}
    1.16 +import org.gjt.sp.jedit.textarea.JEditTextArea
    1.17 +import org.gjt.sp.jedit.gui.DockableWindowManager
    1.18 +
    1.19 +
    1.20 +object Isabelle
    1.21 +{
    1.22 +  /* dockable windows */
    1.23 +
    1.24 +  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    1.25 +
    1.26 +  def docked_session(view: View): Option[Session_Dockable] =
    1.27 +    wm(view).getDockableWindow("isabelle-session") match {
    1.28 +      case dockable: Session_Dockable => Some(dockable)
    1.29 +      case _ => None
    1.30 +    }
    1.31 +
    1.32 +  def docked_output(view: View): Option[Output_Dockable] =
    1.33 +    wm(view).getDockableWindow("isabelle-output") match {
    1.34 +      case dockable: Output_Dockable => Some(dockable)
    1.35 +      case _ => None
    1.36 +    }
    1.37 +
    1.38 +  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    1.39 +    wm(view).getDockableWindow("isabelle-raw-output") match {
    1.40 +      case dockable: Raw_Output_Dockable => Some(dockable)
    1.41 +      case _ => None
    1.42 +    }
    1.43 +
    1.44 +  def docked_protocol(view: View): Option[Protocol_Dockable] =
    1.45 +    wm(view).getDockableWindow("isabelle-protocol") match {
    1.46 +      case dockable: Protocol_Dockable => Some(dockable)
    1.47 +      case _ => None
    1.48 +    }
    1.49 +
    1.50 +
    1.51 +  /* font size */
    1.52 +
    1.53 +  def change_font_size(view: View, change: Int => Int)
    1.54 +  {
    1.55 +    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    1.56 +    jEdit.setIntegerProperty("view.fontsize", size)
    1.57 +    jEdit.propertiesChanged()
    1.58 +    jEdit.saveSettings()
    1.59 +    view.getStatus.setMessageAndClear("Text font size: " + size)
    1.60 +  }
    1.61 +
    1.62 +  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    1.63 +  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    1.64 +
    1.65 +
    1.66 +  /* full checking */
    1.67 +
    1.68 +  def check_buffer(buffer: Buffer)
    1.69 +  {
    1.70 +    PIDE.document_model(buffer) match {
    1.71 +      case None =>
    1.72 +      case Some(model) => model.full_perspective()
    1.73 +    }
    1.74 +  }
    1.75 +
    1.76 +  def cancel_execution() { PIDE.session.cancel_execution() }
    1.77 +
    1.78 +
    1.79 +  /* control styles */
    1.80 +
    1.81 +  def control_sub(text_area: JEditTextArea)
    1.82 +  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    1.83 +
    1.84 +  def control_sup(text_area: JEditTextArea)
    1.85 +  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    1.86 +
    1.87 +  def control_isub(text_area: JEditTextArea)
    1.88 +  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    1.89 +
    1.90 +  def control_isup(text_area: JEditTextArea)
    1.91 +  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    1.92 +
    1.93 +  def control_bold(text_area: JEditTextArea)
    1.94 +  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    1.95 +
    1.96 +  def control_reset(text_area: JEditTextArea)
    1.97 +  { Token_Markup.edit_control_style(text_area, "") }
    1.98 +
    1.99 +
   1.100 +  /* block styles */
   1.101 +
   1.102 +  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   1.103 +  {
   1.104 +    s1.foreach(text_area.userInput(_))
   1.105 +    s2.foreach(text_area.userInput(_))
   1.106 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
   1.107 +  }
   1.108 +
   1.109 +  def input_bsub(text_area: JEditTextArea)
   1.110 +  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   1.111 +
   1.112 +  def input_bsup(text_area: JEditTextArea)
   1.113 +  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   1.114 +}
   1.115 +