src/Tools/jEdit/src/isabelle.scala
author wenzelm
Tue, 08 Jan 2013 18:24:52 +0100
changeset 50775 8c1cda8ad833
parent 50433 9131dadb2bf7
child 51533 3f6280aedbcc
permissions -rw-r--r--
upper bound for font size;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     3
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
     4
Convenience operations for Isabelle/jEdit.
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     5
*/
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     6
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     8
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     9
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    10
import isabelle._
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    11
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    12
import org.gjt.sp.jedit.{jEdit, View, Buffer}
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    14
import org.gjt.sp.jedit.gui.DockableWindowManager
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    15
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    16
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    17
object Isabelle
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    18
{
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    19
  /* dockable windows */
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    20
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    21
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    22
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    23
  def docked_theories(view: View): Option[Theories_Dockable] =
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    24
    wm(view).getDockableWindow("isabelle-theories") match {
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    25
      case dockable: Theories_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    26
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    27
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    28
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    29
  def docked_output(view: View): Option[Output_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    30
    wm(view).getDockableWindow("isabelle-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    31
      case dockable: Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    32
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    33
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    34
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    35
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    36
    wm(view).getDockableWindow("isabelle-raw-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    37
      case dockable: Raw_Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    38
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    39
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    40
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    41
  def docked_protocol(view: View): Option[Protocol_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    42
    wm(view).getDockableWindow("isabelle-protocol") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    43
      case dockable: Protocol_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    44
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    45
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    46
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    47
  def docked_monitor(view: View): Option[Monitor_Dockable] =
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    48
    wm(view).getDockableWindow("isabelle-monitor") match {
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    49
      case dockable: Monitor_Dockable => Some(dockable)
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    50
      case _ => None
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    51
    }
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    52
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    53
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    54
  /* font size */
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    55
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    56
  def change_font_size(view: View, change: Int => Int)
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    57
  {
50775
8c1cda8ad833 upper bound for font size;
wenzelm
parents: 50433
diff changeset
    58
    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
50206
6626bc5ed053 tuned signature;
wenzelm
parents: 50205
diff changeset
    59
    jEdit.setIntegerProperty("view.fontsize", size)
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    60
    jEdit.propertiesChanged()
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    61
    jEdit.saveSettings()
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    62
    view.getStatus.setMessageAndClear("Text font size: " + size)
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    63
  }
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    64
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    65
  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    66
  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    67
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    68
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    69
  /* structured insert */
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    70
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    71
  def insert_line_padding(text_area: JEditTextArea, text: String)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    72
  {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    73
    val buffer = text_area.getBuffer
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    74
    JEdit_Lib.buffer_edit(buffer) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    75
      val text1 =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    76
        if (text_area.getSelectionCount == 0) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    77
          def pad(range: Text.Range): String =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    78
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    79
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    80
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    81
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    82
          pad(before_caret) + text + pad(caret)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    83
        }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    84
        else text
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    85
      text_area.setSelectedText(text1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    86
    }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    87
  }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    88
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
    89
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    90
  /* control styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    91
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    92
  def control_sub(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    93
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    94
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    95
  def control_sup(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    96
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    97
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    98
  def control_isub(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
    99
  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   100
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   101
  def control_isup(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   102
  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   103
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   104
  def control_bold(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   105
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   106
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   107
  def control_reset(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   108
  { Token_Markup.edit_control_style(text_area, "") }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   109
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   110
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   111
  /* block styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   112
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   113
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   114
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   115
    s1.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   116
    s2.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   117
    s2.foreach(_ => text_area.goToPrevCharacter(false))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   118
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   119
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   120
  def input_bsub(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   121
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   122
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   123
  def input_bsup(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   124
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   125
}
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   126