42 } |
42 } |
43 |
43 |
44 |
44 |
45 /* jEdit text area operations */ |
45 /* jEdit text area operations */ |
46 |
46 |
47 private def complete_text_area(text_area: JEditTextArea, item: Item) |
47 object Text_Area |
48 { |
48 { |
49 Swing_Thread.require() |
49 private def insert(text_area: JEditTextArea, item: Item) |
50 |
50 { |
51 val buffer = text_area.getBuffer |
51 Swing_Thread.require() |
52 val len = item.original.length |
52 |
53 if (buffer.isEditable && len > 0) { |
53 val buffer = text_area.getBuffer |
54 JEdit_Lib.buffer_edit(buffer) { |
54 val len = item.original.length |
55 val caret = text_area.getCaretPosition |
55 if (buffer.isEditable && len > 0) { |
56 JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match { |
56 JEdit_Lib.buffer_edit(buffer) { |
57 case Some(text) if text == item.original => |
57 val caret = text_area.getCaretPosition |
58 buffer.remove(caret - len, len) |
58 JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match { |
59 buffer.insert(caret - len, item.replacement) |
59 case Some(text) if text == item.original => |
60 case _ => |
60 buffer.remove(caret - len, len) |
|
61 buffer.insert(caret - len, item.replacement) |
|
62 case _ => |
|
63 } |
61 } |
64 } |
62 } |
65 } |
63 } |
66 } |
64 } |
67 |
65 |
68 def input(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent) |
66 def input_text_area(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent) |
69 { |
67 { |
70 Swing_Thread.require() |
68 Swing_Thread.require() |
71 |
69 |
72 val view = text_area.getView |
70 val view = text_area.getView |
73 val root = view.getRootPane |
71 val root = view.getRootPane |
74 val buffer = text_area.getBuffer |
72 val buffer = text_area.getBuffer |
75 val painter = text_area.getPainter |
73 val painter = text_area.getPainter |
76 |
74 |
77 register(root, null) |
75 register(root, null) |
78 |
76 |
79 if (buffer.isEditable) { |
77 if (buffer.isEditable) { |
80 get_syntax match { |
78 get_syntax match { |
81 case Some(syntax) => |
79 case Some(syntax) => |
82 val caret = text_area.getCaretPosition |
80 val caret = text_area.getCaretPosition |
83 val result = |
81 val result = |
84 { |
82 { |
85 val line = buffer.getLineOfOffset(caret) |
83 val line = buffer.getLineOfOffset(caret) |
86 val start = buffer.getLineStartOffset(line) |
84 val start = buffer.getLineStartOffset(line) |
87 val text = buffer.getSegment(start, caret - start) |
85 val text = buffer.getSegment(start, caret - start) |
88 |
86 |
89 syntax.completion.complete(text) match { |
87 syntax.completion.complete(text) match { |
90 case Some((word, cs)) => |
88 case Some((word, cs)) => |
91 val ds = |
89 val ds = |
92 (if (Isabelle_Encoding.is_active(buffer)) |
90 (if (Isabelle_Encoding.is_active(buffer)) |
93 cs.map(Symbol.decode(_)).sorted |
91 cs.map(Symbol.decode(_)).sorted |
94 else cs).filter(_ != word) |
92 else cs).filter(_ != word) |
95 if (ds.isEmpty) None |
93 if (ds.isEmpty) None |
96 else Some((word, ds.map(s => Item(word, s, s)))) |
94 else Some((word, ds.map(s => Item(word, s, s)))) |
97 case None => None |
95 case None => None |
98 } |
96 } |
99 } |
97 } |
100 result match { |
98 result match { |
101 case Some((original, items)) => |
99 case Some((original, items)) => |
102 val popup_font = |
100 val popup_font = |
103 painter.getFont.deriveFont( |
101 painter.getFont.deriveFont( |
104 (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat |
102 (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat |
105 max 10.0f) |
103 max 10.0f) |
106 |
104 |
107 val location = text_area.offsetToXY(caret - original.length) |
105 val location = text_area.offsetToXY(caret - original.length) |
108 if (location != null) { |
106 if (location != null) { |
109 location.y = location.y + painter.getFontMetrics.getHeight |
107 location.y = location.y + painter.getFontMetrics.getHeight |
110 SwingUtilities.convertPointToScreen(location, painter) |
108 SwingUtilities.convertPointToScreen(location, painter) |
111 |
109 |
112 val completion = |
110 val completion = |
113 new Completion_Popup(root, popup_font, location, items) { |
111 new Completion_Popup(root, popup_font, location, items) { |
114 override def complete(item: Item) { insert(text_area, item) } |
112 override def complete(item: Item) { complete_text_area(text_area, item) } |
115 override def propagate(e: KeyEvent) { |
113 override def propagate(e: KeyEvent) { |
116 JEdit_Lib.propagate_key(view, e) |
114 JEdit_Lib.propagate_key(view, e) |
117 if (!e.isConsumed) input(text_area, get_syntax, e) |
115 if (!e.isConsumed) input_text_area(text_area, get_syntax, e) |
118 } |
|
119 override def refocus() { text_area.requestFocus } |
116 } |
120 } |
117 override def refocus() { text_area.requestFocus } |
121 register(root, completion) |
118 } |
122 } |
119 register(root, completion) |
123 case None => |
120 } |
124 } |
121 case None => |
125 case None => |
122 } |
126 } |
123 case None => |
|
124 } |
127 } |
125 } |
128 } |
126 } |
129 } |
127 } |
130 } |
128 |
131 |