author | wenzelm |
Thu, 29 Aug 2013 13:14:00 +0200 | |
changeset 53276 | cbed0aa0b0db |
parent 53274 | 1760c01f1c78 |
child 53277 | 6aa348237973 |
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 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
19 |
/* editor modes */ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
20 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
21 |
val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news") |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
22 |
|
53276 | 23 |
private lazy val news_syntax = Outer_Syntax.init() |
24 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
25 |
def mode_syntax(name: String): Option[Outer_Syntax] = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
26 |
name match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
27 |
case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
28 |
case "isabelle-options" => Some(Options.options_syntax) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
29 |
case "isabelle-root" => Some(Build.root_syntax) |
53276 | 30 |
case "isabelle-news" => Some(news_syntax) |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
31 |
case _ => None |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
32 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
33 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
34 |
|
50208 | 35 |
/* dockable windows */ |
36 |
||
37 |
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
38 |
||
50299 | 39 |
def docked_theories(view: View): Option[Theories_Dockable] = |
40 |
wm(view).getDockableWindow("isabelle-theories") match { |
|
41 |
case dockable: Theories_Dockable => Some(dockable) |
|
50208 | 42 |
case _ => None |
43 |
} |
|
44 |
||
51533 | 45 |
def docked_timing(view: View): Option[Timing_Dockable] = |
46 |
wm(view).getDockableWindow("isabelle-timing") match { |
|
47 |
case dockable: Timing_Dockable => Some(dockable) |
|
48 |
case _ => None |
|
49 |
} |
|
50 |
||
50208 | 51 |
def docked_output(view: View): Option[Output_Dockable] = |
52 |
wm(view).getDockableWindow("isabelle-output") match { |
|
53 |
case dockable: Output_Dockable => Some(dockable) |
|
54 |
case _ => None |
|
55 |
} |
|
56 |
||
57 |
def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
58 |
wm(view).getDockableWindow("isabelle-raw-output") match { |
|
59 |
case dockable: Raw_Output_Dockable => Some(dockable) |
|
60 |
case _ => None |
|
61 |
} |
|
62 |
||
63 |
def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
64 |
wm(view).getDockableWindow("isabelle-protocol") match { |
|
65 |
case dockable: Protocol_Dockable => Some(dockable) |
|
66 |
case _ => None |
|
67 |
} |
|
68 |
||
50433
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
69 |
def docked_monitor(view: View): Option[Monitor_Dockable] = |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
70 |
wm(view).getDockableWindow("isabelle-monitor") match { |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
71 |
case dockable: Monitor_Dockable => Some(dockable) |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
72 |
case _ => None |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
73 |
} |
9131dadb2bf7
basic monitor panel, using the powerful jfreechart library;
wenzelm
parents:
50341
diff
changeset
|
74 |
|
50208 | 75 |
|
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
76 |
/* continuous checking */ |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
77 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
78 |
private val CONTINUOUS_CHECKING = "editor_continuous_checking" |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
79 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
80 |
def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING) |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
81 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
82 |
def continuous_checking_=(b: Boolean) |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
83 |
{ |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
84 |
Swing_Thread.require() |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
85 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
86 |
if (continuous_checking != b) { |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
87 |
PIDE.options.bool(CONTINUOUS_CHECKING) = b |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
88 |
PIDE.options_changed() |
52974 | 89 |
PIDE.editor.flush() |
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
90 |
} |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
91 |
} |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
92 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
93 |
def set_continuous_checking() { continuous_checking = true } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
94 |
def reset_continuous_checking() { continuous_checking = false } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
95 |
def toggle_continuous_checking() { continuous_checking = !continuous_checking } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
96 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
97 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
98 |
/* required document nodes */ |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
99 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
100 |
private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false) |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
101 |
{ |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
102 |
Swing_Thread.require() |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
103 |
PIDE.document_model(view.getBuffer) match { |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
104 |
case Some(model) => |
52816
c608e0ade554
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents:
52815
diff
changeset
|
105 |
model.node_required = (if (toggle) !model.node_required else set) |
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
106 |
case None => |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
107 |
} |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
108 |
} |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
109 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
110 |
def set_node_required(view: View) { node_required_update(view, set = true) } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
111 |
def reset_node_required(view: View) { node_required_update(view, set = false) } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
112 |
def toggle_node_required(view: View) { node_required_update(view, toggle = true) } |
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
113 |
|
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
51533
diff
changeset
|
114 |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
115 |
/* font size */ |
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
116 |
|
53272 | 117 |
def reset_font_size(view: View): Unit = |
118 |
Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size")) |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
119 |
|
53272 | 120 |
def increase_font_size(view: View): Unit = |
121 |
Rendering.font_size_change(view, i => i + ((i / 10) max 1)) |
|
122 |
||
123 |
def decrease_font_size(view: View): Unit = |
|
124 |
Rendering.font_size_change(view, i => i - ((i / 10) max 1)) |
|
50198
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
125 |
|
0c7b351a6871
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents:
50187
diff
changeset
|
126 |
|
50341
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
127 |
/* structured insert */ |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
128 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
129 |
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
|
130 |
{ |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
131 |
val buffer = text_area.getBuffer |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
132 |
JEdit_Lib.buffer_edit(buffer) { |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
133 |
val text1 = |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
134 |
if (text_area.getSelectionCount == 0) { |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
138 |
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
|
139 |
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
|
140 |
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
|
141 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
142 |
else text |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
143 |
text_area.setSelectedText(text1) |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
144 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
145 |
} |
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
146 |
|
0c65a7cfc0f3
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents:
50299
diff
changeset
|
147 |
|
50183 | 148 |
/* control styles */ |
149 |
||
150 |
def control_sub(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
151 |
{ Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) } |
50183 | 152 |
|
153 |
def control_sup(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
154 |
{ Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) } |
50183 | 155 |
|
156 |
def control_bold(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
157 |
{ Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) } |
50183 | 158 |
|
159 |
def control_reset(text_area: JEditTextArea) |
|
50187
b5a09812abc4
special handling of control symbols in Symbols dockable;
wenzelm
parents:
50183
diff
changeset
|
160 |
{ Token_Markup.edit_control_style(text_area, "") } |
50183 | 161 |
|
162 |
||
163 |
/* block styles */ |
|
164 |
||
165 |
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) |
|
166 |
{ |
|
167 |
s1.foreach(text_area.userInput(_)) |
|
168 |
s2.foreach(text_area.userInput(_)) |
|
169 |
s2.foreach(_ => text_area.goToPrevCharacter(false)) |
|
170 |
} |
|
171 |
||
172 |
def input_bsub(text_area: JEditTextArea) |
|
173 |
{ enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) } |
|
174 |
||
175 |
def input_bsup(text_area: JEditTextArea) |
|
176 |
{ enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } |
|
177 |
} |
|
178 |