25 |
25 |
26 object Token_Markup |
26 object Token_Markup |
27 { |
27 { |
28 /* editing support for control symbols */ |
28 /* editing support for control symbols */ |
29 |
29 |
30 private val is_ctrl_style = |
30 val is_control_style = |
31 Set(Symbol.sub_decoded, Symbol.sup_decoded, |
31 Set(Symbol.sub_decoded, Symbol.sup_decoded, |
32 Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded) |
32 Symbol.isub_decoded, Symbol.isup_decoded, Symbol.bold_decoded) |
33 |
33 |
34 def update_ctrl_style(ctrl: String, text: String): String = |
34 def update_control_style(control: String, text: String): String = |
35 { |
35 { |
36 val result = new StringBuilder |
36 val result = new StringBuilder |
37 for (sym <- Symbol.iterator(text) if !is_ctrl_style(sym)) { |
37 for (sym <- Symbol.iterator(text) if !is_control_style(sym)) { |
38 if (Symbol.is_controllable(sym)) result ++= ctrl |
38 if (Symbol.is_controllable(sym)) result ++= control |
39 result ++= sym |
39 result ++= sym |
40 } |
40 } |
41 result.toString |
41 result.toString |
42 } |
42 } |
43 |
43 |
44 def edit_ctrl_style(text_area: TextArea, ctrl: String) |
44 def edit_control_style(text_area: TextArea, control: String) |
45 { |
45 { |
46 Swing_Thread.assert() |
46 Swing_Thread.assert() |
47 |
47 |
48 val buffer = text_area.getBuffer |
48 val buffer = text_area.getBuffer |
49 |
49 |
50 text_area.getSelection.toList match { |
50 text_area.getSelection.toList match { |
51 case Nil if ctrl == "" => |
51 case Nil if control == "" => |
52 try { |
52 try { |
53 buffer.beginCompoundEdit() |
53 buffer.beginCompoundEdit() |
54 val caret = text_area.getCaretPosition |
54 val caret = text_area.getCaretPosition |
55 if (caret > 0 && is_ctrl_style(buffer.getText(caret - 1, 1))) |
55 if (caret > 0 && is_control_style(buffer.getText(caret - 1, 1))) |
56 text_area.backspace() |
56 text_area.backspace() |
57 } |
57 } |
58 finally { |
58 finally { |
59 buffer.endCompoundEdit() |
59 buffer.endCompoundEdit() |
60 } |
60 } |
61 case Nil if ctrl != "" => |
61 case Nil if control != "" => |
62 text_area.setSelectedText(ctrl) |
62 text_area.setSelectedText(control) |
63 case sels => |
63 case sels => |
64 try { |
64 try { |
65 buffer.beginCompoundEdit() |
65 buffer.beginCompoundEdit() |
66 sels.foreach(sel => |
66 sels.foreach(sel => |
67 text_area.setSelectedText(sel, |
67 text_area.setSelectedText(sel, |
68 update_ctrl_style(ctrl, text_area.getSelectedText(sel)))) |
68 update_control_style(control, text_area.getSelectedText(sel)))) |
69 } |
69 } |
70 finally { |
70 finally { |
71 buffer.endCompoundEdit() |
71 buffer.endCompoundEdit() |
72 } |
72 } |
73 } |
73 } |
163 } |
163 } |
164 |
164 |
165 def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = |
165 def extended_styles(text: CharSequence): Map[Text.Offset, Byte => Byte] = |
166 { |
166 { |
167 // FIXME Symbol.bsub_decoded etc. |
167 // FIXME Symbol.bsub_decoded etc. |
168 def ctrl_style(sym: String): Option[Byte => Byte] = |
168 def control_style(sym: String): Option[Byte => Byte] = |
169 if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_)) |
169 if (sym == Symbol.sub_decoded || sym == Symbol.isub_decoded) Some(subscript(_)) |
170 else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_)) |
170 else if (sym == Symbol.sup_decoded || sym == Symbol.isup_decoded) Some(superscript(_)) |
171 else if (sym == Symbol.bold_decoded) Some(bold(_)) |
171 else if (sym == Symbol.bold_decoded) Some(bold(_)) |
172 else None |
172 else None |
173 |
173 |
175 def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) |
175 def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte) |
176 { |
176 { |
177 for (i <- start until stop) result += (i -> style) |
177 for (i <- start until stop) result += (i -> style) |
178 } |
178 } |
179 var offset = 0 |
179 var offset = 0 |
180 var ctrl = "" |
180 var control = "" |
181 for (sym <- Symbol.iterator(text)) { |
181 for (sym <- Symbol.iterator(text)) { |
182 if (ctrl_style(sym).isDefined) ctrl = sym |
182 if (control_style(sym).isDefined) control = sym |
183 else if (ctrl != "") { |
183 else if (control != "") { |
184 if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { |
184 if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) { |
185 mark(offset - ctrl.length, offset, _ => hidden) |
185 mark(offset - control.length, offset, _ => hidden) |
186 mark(offset, offset + sym.length, ctrl_style(ctrl).get) |
186 mark(offset, offset + sym.length, control_style(control).get) |
187 } |
187 } |
188 ctrl = "" |
188 control = "" |
189 } |
189 } |
190 Symbol.lookup_font(sym) match { |
190 Symbol.lookup_font(sym) match { |
191 case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) |
191 case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _)) |
192 case _ => |
192 case _ => |
193 } |
193 } |