--- a/src/Tools/jEdit/src/isabelle.scala Wed Mar 15 13:35:14 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Mar 15 13:49:39 2017 +0100
@@ -379,19 +379,19 @@
/* control styles */
def control_sub(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.sub) }
+ { Syntax_Style.edit_control_style(text_area, Symbol.sub) }
def control_sup(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.sup) }
+ { Syntax_Style.edit_control_style(text_area, Symbol.sup) }
def control_bold(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.bold) }
+ { Syntax_Style.edit_control_style(text_area, Symbol.bold) }
def control_emph(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, Symbol.emph) }
+ { Syntax_Style.edit_control_style(text_area, Symbol.emph) }
def control_reset(text_area: JEditTextArea)
- { Token_Markup.edit_control_style(text_area, "") }
+ { Syntax_Style.edit_control_style(text_area, "") }
/* block styles */