author  wenzelm 
Thu, 22 Nov 2012 17:01:20 +0100  
changeset 50168  4a575ef46466 
parent 50166  2585c81d840a 
child 50195  863b1dfc396c 
permissions  rwrr 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

1 
/* Title: Tools/jEdit/src/pretty_text_area.scala 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

3 

50160  4 
GUI component for prettyprinted text with markup, rendered like jEdit 
5 
text area. 

49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

6 
*/ 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

7 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

8 
package isabelle.jedit 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

9 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

10 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

11 
import isabelle._ 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

12 

49422
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

13 
import java.awt.{Font, FontMetrics, Toolkit} 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

14 
import java.awt.event.{ActionListener, ActionEvent, KeyEvent} 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

15 
import javax.swing.{KeyStroke, JComponent} 
49412  16 

49422
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

17 
import org.gjt.sp.jedit.{jEdit, View, Registers} 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

18 
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea} 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

19 
import org.gjt.sp.util.SyntaxUtilities 
49412  20 

49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

21 

49412  22 
object Pretty_Text_Area 
23 
{ 

49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

24 
private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body): 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

25 
(String, Isabelle_Rendering) = 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

26 
{ 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

27 
val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body) 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

28 
val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value) 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

29 
(text, rendering) 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

30 
} 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

31 

97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

32 
private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body) 
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

33 
: (String, Document.State) = 
49412  34 
{ 
49414  35 
val command = Command.rich_text(Document.new_id(), formatted_body) 
49412  36 
val node_name = command.node_name 
37 
val edits: List[Document.Edit_Text] = 

49414  38 
List(node_name > Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) 
49412  39 

49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

40 
val state0 = base_snapshot.state.define_command(command) 
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

41 
val version0 = base_snapshot.version 
49412  42 
val nodes0 = version0.nodes 
43 

44 
val nodes1 = nodes0 + (node_name > nodes0(node_name).update_commands(Linear_Set(command))) 

45 
val version1 = Document.Version.make(version0.syntax, nodes1) 

46 
val state1 = 

47 
state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 

48 
.define_version(version1, state0.the_assignment(version0)) 

49414  49 
.assign(version1.id, List(command.id > Some(Document.new_id())))._2 
49412  50 

49416
1053a564dd25
some actual rich text markup via XML.content_markup;
wenzelm
parents:
49414
diff
changeset

51 
(command.source, state1) 
49412  52 
} 
53 
} 

54 

49446  55 
class Pretty_Text_Area(view: View) extends JEditEmbeddedTextArea 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

56 
{ 
49446  57 
text_area => 
58 

49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

59 
Swing_Thread.require() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

60 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

61 
private var current_font_family = "Dialog" 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

62 
private var current_font_size: Int = 12 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

63 
private var current_body: XML.Body = Nil 
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

64 
private var current_base_snapshot = Document.State.init.snapshot() 
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

65 
private var current_rendering: Isabelle_Rendering = 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

66 
Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2 
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

67 
private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

68 

49492  69 
private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering, true) 
49416
1053a564dd25
some actual rich text markup via XML.content_markup;
wenzelm
parents:
49414
diff
changeset

70 

49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

71 
def refresh() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

72 
{ 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

73 
Swing_Thread.require() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

74 

50168
4a575ef46466
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
wenzelm
parents:
50166
diff
changeset

75 
val font = new Font(current_font_family, Font.PLAIN, current_font_size) 
4a575ef46466
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
wenzelm
parents:
50166
diff
changeset

76 
getPainter.setFont(font) 
4a575ef46466
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
wenzelm
parents:
50166
diff
changeset

77 
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias"))) 
4a575ef46466
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
wenzelm
parents:
50166
diff
changeset

78 
getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size)) 
4a575ef46466
always refresh font metrics, to help window size calculation (amending 2585c81d840a);
wenzelm
parents:
50166
diff
changeset

79 

50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

80 
if (getWidth > 0) { 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

81 
val font_metrics = getPainter.getFontMetrics(font) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

82 
val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1)  2) max 20 
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

83 

50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

84 
val base_snapshot = current_base_snapshot 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

85 
val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics)) 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

86 

50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

87 
future_rendering.map(_.cancel(true)) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

88 
future_rendering = Some(default_thread_pool.submit(() => 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

89 
{ 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

90 
val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

91 
Simple_Thread.interrupted_exception() 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

92 

50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

93 
Swing_Thread.later { 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

94 
current_rendering = rendering 
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

95 

50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

96 
try { 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

97 
getBuffer.beginCompoundEdit 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

98 
getBuffer.setReadOnly(false) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

99 
setText(text) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

100 
setCaretPosition(0) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

101 
getBuffer.setReadOnly(true) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

102 
} 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

103 
finally { 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

104 
getBuffer.endCompoundEdit 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

105 
} 
49471
97964515a676
text_rendering as managed task, with cancellation;
wenzelm
parents:
49446
diff
changeset

106 
} 
50166
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

107 
})) 
2585c81d840a
take component width as indication if it is already visible/layedout, to avoid multiple formatting with minimal margin;
wenzelm
parents:
50160
diff
changeset

108 
} 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

109 
} 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

110 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

111 
def resize(font_family: String, font_size: Int) 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

112 
{ 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

113 
Swing_Thread.require() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

114 

0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

115 
current_font_family = font_family 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

116 
current_font_size = font_size 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

117 
refresh() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

118 
} 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

119 

49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

120 
def update(base_snapshot: Document.Snapshot, body: XML.Body) 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

121 
{ 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

122 
Swing_Thread.require() 
49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

123 
require(!base_snapshot.is_outdated) 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

124 

49419
e2726211f834
pass base_snapshot to enable hyperlinks into other nodes;
wenzelm
parents:
49416
diff
changeset

125 
current_base_snapshot = base_snapshot 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

126 
current_body = body 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

127 
refresh() 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

128 
} 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

129 

49422
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

130 

21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

131 
/* keyboard actions */ 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

132 

21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

133 
private val action_listener = new ActionListener { 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

134 
def actionPerformed(e: ActionEvent) { 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

135 
e.getActionCommand match { 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

136 
case "copy" => Registers.copy(text_area, '$') 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

137 
case _ => 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

138 
} 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

139 
} 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

140 
} 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

141 

49446  142 
registerKeyboardAction(action_listener, "copy", 
49422
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

143 
KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED) 
49446  144 
registerKeyboardAction(action_listener, "copy", 
49422
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

145 
KeyStroke.getKeyStroke(KeyEvent.VK_C, 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

146 
Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED) 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

147 

21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

148 

21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

149 
/* init */ 
21f77309d93a
minimal clipboard support (similar to org.lobobrowser.html.gui.HtmlBlockPanel);
wenzelm
parents:
49421
diff
changeset

150 

49472  151 
override def isCaretVisible: Boolean = false 
152 

153 
getPainter.setStructureHighlightEnabled(false) 

49475  154 
getPainter.setLineHighlightEnabled(false) 
155 

49446  156 
getBuffer.setTokenMarker(new Token_Markup.Marker(true, None)) 
157 
getBuffer.setReadOnly(true) 

49475  158 

49412  159 
rich_text_area.activate() 
49398
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

160 
} 
0fa4389c04f9
alternative output panel, based on Pretty_Text_Area, based on JEditEmbeddedTextArea;
wenzelm
parents:
diff
changeset

161 