src/Tools/jEdit/src/isabelle.scala
author wenzelm
Sun Nov 25 21:40:34 2012 +0100 (2012-11-25)
changeset 50209 907373a080b9
parent 50208 1382ad6d4774
child 50299 f70b3712040f
permissions -rw-r--r--
tuned signature;
wenzelm@50208
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
wenzelm@50183
     2
    Author:     Makarius
wenzelm@50183
     3
wenzelm@50208
     4
Convenience operations 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@50198
    12
import org.gjt.sp.jedit.{jEdit, View, Buffer}
wenzelm@50183
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@50208
    14
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@50183
    15
wenzelm@50183
    16
wenzelm@50208
    17
object Isabelle
wenzelm@50183
    18
{
wenzelm@50208
    19
  /* dockable windows */
wenzelm@50208
    20
wenzelm@50208
    21
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    22
wenzelm@50208
    23
  def docked_session(view: View): Option[Session_Dockable] =
wenzelm@50208
    24
    wm(view).getDockableWindow("isabelle-session") match {
wenzelm@50208
    25
      case dockable: Session_Dockable => Some(dockable)
wenzelm@50208
    26
      case _ => None
wenzelm@50208
    27
    }
wenzelm@50208
    28
wenzelm@50208
    29
  def docked_output(view: View): Option[Output_Dockable] =
wenzelm@50208
    30
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    31
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    32
      case _ => None
wenzelm@50208
    33
    }
wenzelm@50208
    34
wenzelm@50208
    35
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
    36
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
    37
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
    38
      case _ => None
wenzelm@50208
    39
    }
wenzelm@50208
    40
wenzelm@50208
    41
  def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@50208
    42
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@50208
    43
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@50208
    44
      case _ => None
wenzelm@50208
    45
    }
wenzelm@50208
    46
wenzelm@50208
    47
wenzelm@50198
    48
  /* font size */
wenzelm@50198
    49
wenzelm@50198
    50
  def change_font_size(view: View, change: Int => Int)
wenzelm@50198
    51
  {
wenzelm@50206
    52
    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
wenzelm@50206
    53
    jEdit.setIntegerProperty("view.fontsize", size)
wenzelm@50198
    54
    jEdit.propertiesChanged()
wenzelm@50198
    55
    jEdit.saveSettings()
wenzelm@50198
    56
    view.getStatus.setMessageAndClear("Text font size: " + size)
wenzelm@50198
    57
  }
wenzelm@50198
    58
wenzelm@50198
    59
  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
wenzelm@50198
    60
  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
wenzelm@50198
    61
wenzelm@50198
    62
wenzelm@50183
    63
  /* control styles */
wenzelm@50183
    64
wenzelm@50183
    65
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
    66
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
    67
wenzelm@50183
    68
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
    69
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
    70
wenzelm@50183
    71
  def control_isub(text_area: JEditTextArea)
wenzelm@50187
    72
  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
wenzelm@50183
    73
wenzelm@50183
    74
  def control_isup(text_area: JEditTextArea)
wenzelm@50187
    75
  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
wenzelm@50183
    76
wenzelm@50183
    77
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
    78
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
    79
wenzelm@50183
    80
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
    81
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
    82
wenzelm@50183
    83
wenzelm@50183
    84
  /* block styles */
wenzelm@50183
    85
wenzelm@50183
    86
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
    87
  {
wenzelm@50183
    88
    s1.foreach(text_area.userInput(_))
wenzelm@50183
    89
    s2.foreach(text_area.userInput(_))
wenzelm@50183
    90
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
    91
  }
wenzelm@50183
    92
wenzelm@50183
    93
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
    94
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
    95
wenzelm@50183
    96
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
    97
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
    98
}
wenzelm@50183
    99