author | wenzelm |
Tue, 04 Dec 2012 11:06:51 +0100 | |
changeset 50341 | 0c65a7cfc0f3 |
parent 50299 | f70b3712040f |
child 50433 | 9131dadb2bf7 |
permissions | -rw-r--r-- |
50208 | 1 |
/* Title: Tools/jEdit/src/isabelle.scala |
50183 | 2 |
Author: Makarius |
3 |
||
50208 | 4 |
Convenience operations for Isabelle/jEdit. |
50183 | 5 |
*/ |
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
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 | 13 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
50208 | 14 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
50183 | 15 |
|
16 |
||
50208 | 17 |
object Isabelle |
50183 | 18 |
{ |
50208 | 19 |
/* dockable windows */ |
20 |
||
21 |
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
22 |
||
50299 | 23 |
def docked_theories(view: View): Option[Theories_Dockable] = |
24 |
wm(view).getDockableWindow("isabelle-theories") match { |
|
25 |
case dockable: Theories_Dockable => Some(dockable) |
|
50208 | 26 |
case _ => None |
27 |
} |
|
28 |
||
29 |
def docked_output(view: View): Option[Output_Dockable] = |
|
30 |
wm(view).getDockableWindow("isabelle-output") match { |
|
31 |
case dockable: Output_Dockable => Some(dockable) |
|
32 |
case _ => None |
|
33 |
} |
|
34 |
||
35 |
def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
36 |
wm(view).getDockableWindow("isabelle-raw-output") match { |
|
37 |
case dockable: Raw_Output_Dockable => Some(dockable) |
|
38 |
case _ => None |
|
39 |
} |
|
40 |
||
41 |
def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
42 |
wm(view).getDockableWindow("isabelle-protocol") match { |
|
43 |
case dockable: Protocol_Dockable => Some(dockable) |
|
44 |
case _ => None |
|
45 |
} |
|
46 |
||
47 |
||
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
48 |
/* font size */ |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
49 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
50 |
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
|
51 |
{ |
50206 | 52 |
val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 |
53 |
jEdit.setIntegerProperty("view.fontsize", size) |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
54 |
jEdit.propertiesChanged() |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
55 |
jEdit.saveSettings() |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
56 |
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
|
57 |
} |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
58 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
59 |
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
|
60 |
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
|
61 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
62 |
|
50341
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
63 |
/* structured insert */ |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
64 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
65 |
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
|
66 |
{ |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
67 |
val buffer = text_area.getBuffer |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
68 |
JEdit_Lib.buffer_edit(buffer) { |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
69 |
val text1 = |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
70 |
if (text_area.getSelectionCount == 0) { |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
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
|
77 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
78 |
else text |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
79 |
text_area.setSelectedText(text1) |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
80 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
81 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
82 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
83 |
|
50183 | 84 |
/* control styles */ |
85 |
||
86 |
def control_sub(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
87 |
{ Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) } |
50183 | 88 |
|
89 |
def control_sup(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
90 |
{ Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) } |
50183 | 91 |
|
92 |
def control_isub(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.isub_decoded) } |
50183 | 94 |
|
95 |
def control_isup(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.isup_decoded) } |
50183 | 97 |
|
98 |
def control_bold(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.bold_decoded) } |
50183 | 100 |
|
101 |
def control_reset(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, "") } |
50183 | 103 |
|
104 |
||
105 |
/* block styles */ |
|
106 |
||
107 |
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) |
|
108 |
{ |
|
109 |
s1.foreach(text_area.userInput(_)) |
|
110 |
s2.foreach(text_area.userInput(_)) |
|
111 |
s2.foreach(_ => text_area.goToPrevCharacter(false)) |
|
112 |
} |
|
113 |
||
114 |
def input_bsub(text_area: JEditTextArea) |
|
115 |
{ enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) } |
|
116 |
||
117 |
def input_bsup(text_area: JEditTextArea) |
|
118 |
{ enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } |
|
119 |
} |
|
120 |