equal
deleted
inserted
replaced
95 |
95 |
96 action = |
96 action = |
97 Action(Symbol.decode(symbol)) { |
97 Action(Symbol.decode(symbol)) { |
98 val text_area = view.getTextArea |
98 val text_area = view.getTextArea |
99 if (is_control && HTML.control.isDefinedAt(symbol)) |
99 if (is_control && HTML.control.isDefinedAt(symbol)) |
100 Token_Markup.edit_control_style(text_area, symbol) |
100 Syntax_Style.edit_control_style(text_area, symbol) |
101 else |
101 else |
102 text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol)) |
102 text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol)) |
103 text_area.requestFocus |
103 text_area.requestFocus |
104 } |
104 } |
105 tooltip = |
105 tooltip = |
109 |
109 |
110 private class Reset_Component extends Button |
110 private class Reset_Component extends Button |
111 { |
111 { |
112 action = Action("Reset") { |
112 action = Action("Reset") { |
113 val text_area = view.getTextArea |
113 val text_area = view.getTextArea |
114 Token_Markup.edit_control_style(text_area, "") |
114 Syntax_Style.edit_control_style(text_area, "") |
115 text_area.requestFocus |
115 text_area.requestFocus |
116 } |
116 } |
117 tooltip = "Reset control symbols within text" |
117 tooltip = "Reset control symbols within text" |
118 } |
118 } |
119 |
119 |