author  wenzelm 
Tue, 08 Jan 2013 18:24:52 +0100  
changeset 50775  8c1cda8ad833 
parent 50433  9131dadb2bf7 
child 51533  3f6280aedbcc 
permissions  rwrr 
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.increasefontsize and isabelle.decreasefontsize;
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("isabelletheories") 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("isabelleoutput") 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("isabellerawoutput") 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("isabelleprotocol") match { 

43 
case dockable: Protocol_Dockable => Some(dockable) 

44 
case _ => None 

45 
} 

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("isabellemonitor") 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  53 

50198
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

54 
/* font size */ 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

55 

0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

56 
def change_font_size(view: View, change: Int => Int) 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

57 
{ 
50775  58 
val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250 
50206  59 
jEdit.setIntegerProperty("view.fontsize", size) 
50198
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

60 
jEdit.propertiesChanged() 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

61 
jEdit.saveSettings() 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

62 
view.getStatus.setMessageAndClear("Text font size: " + size) 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

63 
} 
0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

64 

0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
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.increasefontsize and isabelle.decreasefontsize;
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.increasefontsize and isabelle.decreasefontsize;
wenzelm
parents:
50187
diff
changeset

67 

0c7b351a6871
added convenience actions isabelle.increasefontsize and isabelle.decreasefontsize;
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  90 
/* control styles */ 
91 

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  94 

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  97 

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  100 

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  103 

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  106 

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  109 

110 

111 
/* block styles */ 

112 

113 
private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) 

114 
{ 

115 
s1.foreach(text_area.userInput(_)) 

116 
s2.foreach(text_area.userInput(_)) 

117 
s2.foreach(_ => text_area.goToPrevCharacter(false)) 

118 
} 

119 

120 
def input_bsub(text_area: JEditTextArea) 

121 
{ enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) } 

122 

123 
def input_bsup(text_area: JEditTextArea) 

124 
{ enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) } 

125 
} 

126 