377 |
377 |
378 |
378 |
379 /* control styles */ |
379 /* control styles */ |
380 |
380 |
381 def control_sub(text_area: JEditTextArea) |
381 def control_sub(text_area: JEditTextArea) |
382 { Token_Markup.edit_control_style(text_area, Symbol.sub) } |
382 { Syntax_Style.edit_control_style(text_area, Symbol.sub) } |
383 |
383 |
384 def control_sup(text_area: JEditTextArea) |
384 def control_sup(text_area: JEditTextArea) |
385 { Token_Markup.edit_control_style(text_area, Symbol.sup) } |
385 { Syntax_Style.edit_control_style(text_area, Symbol.sup) } |
386 |
386 |
387 def control_bold(text_area: JEditTextArea) |
387 def control_bold(text_area: JEditTextArea) |
388 { Token_Markup.edit_control_style(text_area, Symbol.bold) } |
388 { Syntax_Style.edit_control_style(text_area, Symbol.bold) } |
389 |
389 |
390 def control_emph(text_area: JEditTextArea) |
390 def control_emph(text_area: JEditTextArea) |
391 { Token_Markup.edit_control_style(text_area, Symbol.emph) } |
391 { Syntax_Style.edit_control_style(text_area, Symbol.emph) } |
392 |
392 |
393 def control_reset(text_area: JEditTextArea) |
393 def control_reset(text_area: JEditTextArea) |
394 { Token_Markup.edit_control_style(text_area, "") } |
394 { Syntax_Style.edit_control_style(text_area, "") } |
395 |
395 |
396 |
396 |
397 /* block styles */ |
397 /* block styles */ |
398 |
398 |
399 private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) |
399 private def enclose_input(text_area: JEditTextArea, s1: String, s2: String) |