author | wenzelm |
Sun, 25 Nov 2012 21:10:29 +0100 | |
changeset 50206 | 6626bc5ed053 |
parent 50205 | 788c8263e634 |
permissions | -rw-r--r-- |
50183 | 1 |
/* Title: Tools/jEdit/src/plugin.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Convenience actions for Isabelle/jEdit. |
|
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 |
14 |
||
15 |
||
16 |
object Isabelle_Actions |
|
17 |
{ |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
18 |
/* font size */ |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
19 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
20 |
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
|
21 |
{ |
50206 | 22 |
val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 |
23 |
jEdit.setIntegerProperty("view.fontsize", size) |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
24 |
jEdit.propertiesChanged() |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
25 |
jEdit.saveSettings() |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
26 |
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
|
27 |
} |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
28 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
29 |
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
|
30 |
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
|
31 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
32 |
|
50183 | 33 |
/* full checking */ |
34 |
||
35 |
def check_buffer(buffer: Buffer) |
|
36 |
{ |
|
50205 | 37 |
PIDE.document_model(buffer) match { |
50183 | 38 |
case None => |
39 |
case Some(model) => model.full_perspective() |
|
40 |
} |
|
41 |
} |
|
42 |
||
50205 | 43 |
def cancel_execution() { PIDE.session.cancel_execution() } |
50183 | 44 |
|
45 |
||
46 |
/* control styles */ |
|
47 |
||
48 |
def control_sub(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
49 |
{ Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) } |
50183 | 50 |
|
51 |
def control_sup(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
52 |
{ Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) } |
50183 | 53 |
|
54 |
def control_isub(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
55 |
{ Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) } |
50183 | 56 |
|
57 |
def control_isup(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
58 |
{ Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) } |
50183 | 59 |
|
60 |
def control_bold(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
61 |
{ Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) } |
50183 | 62 |
|
63 |
def control_reset(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
64 |
{ Token_Markup.edit_control_style(text_area, "") } |
50183 | 65 |
|
66 |
||
67 |
/* block styles */ |
|
68 |
||
69 |
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) |
|
70 |
{ |
|
71 |
s1.foreach(text_area.userInput(_)) |
|
72 |
s2.foreach(text_area.userInput(_)) |
|
73 |
s2.foreach(_ => text_area.goToPrevCharacter(false)) |
|
74 |
} |
|
75 |
||
76 |
def input_bsub(text_area: JEditTextArea) |
|
77 |
{ enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) } |
|
78 |
||
79 |
def input_bsup(text_area: JEditTextArea) |
|
80 |
{ enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } |
|
81 |
} |
|
82 |