s1520454056@5025
|
1 |
package isac.gui.mawen.editor
|
s1520454056@5025
|
2 |
|
s1520454056@5025
|
3 |
import javax.swing._
|
wneuper@5049
|
4 |
import isac.gui.mawen.syntax.Ast._
|
s1520454056@5025
|
5 |
import java.awt._
|
s1520454056@5025
|
6 |
import java.awt.geom._
|
s1520454056@5025
|
7 |
import java.awt.font._
|
s1520454056@5029
|
8 |
import edu.tum.cs.isabelle.api.Implementation
|
s1520454056@5029
|
9 |
import java.awt.event._
|
s1520454056@5029
|
10 |
import java.awt.font._
|
s1520454056@5029
|
11 |
import shapeless.Widen
|
s1520454056@5057
|
12 |
import org.drools.xml.ExtensibleXmlParser.Null
|
s1520454056@5093
|
13 |
import scala.collection.immutable.List
|
s1520454056@5025
|
14 |
|
s1520454056@5144
|
15 |
class AstComponent(var ast: Ast, editorPanel: EditorPanel) extends JComponent with AstContainer with MouseListener with MouseMotionListener with MouseWheelListener with ActionListener with KeyListener {
|
s1520454056@5057
|
16 |
|
s1520454056@5029
|
17 |
var isSelected = false
|
s1520454056@5057
|
18 |
addMouseListener(this)
|
s1520454056@5057
|
19 |
addMouseMotionListener(this)
|
s1520454056@5057
|
20 |
addMouseWheelListener(this)
|
s1520454056@5057
|
21 |
var pressedMousePoint : Point = null
|
s1520454056@5144
|
22 |
var marker : Rectangle = new Rectangle()
|
s1520454056@5144
|
23 |
var markedBoxes : List[Box] = List.empty[Box]
|
s1520454056@5057
|
24 |
|
s1520454056@5057
|
25 |
var mousePositionFunction : (Graphics, Int, Int, String, Box) => Unit = null
|
s1520454056@5093
|
26 |
|
s1520454056@5144
|
27 |
var box : Box = null
|
s1520454056@5093
|
28 |
|
s1520454056@5144
|
29 |
setFocusable(true)
|
s1520454056@5144
|
30 |
addKeyListener(EventUtil.CreateKeyEventHandler(this))
|
s1520454056@5101
|
31 |
|
s1520454056@5112
|
32 |
setSize(50,150)
|
s1520454056@5025
|
33 |
|
s1520454056@5091
|
34 |
def setAst(ast: Ast) = {
|
s1520454056@5091
|
35 |
this.ast = ast
|
s1520454056@5091
|
36 |
repaint()
|
s1520454056@5091
|
37 |
}
|
s1520454056@5129
|
38 |
def getAst() : Ast = this.ast
|
s1520454056@5057
|
39 |
|
s1520454056@5101
|
40 |
|
s1520454056@5101
|
41 |
|
s1520454056@5101
|
42 |
|
s1520454056@5057
|
43 |
override def paint(g: Graphics) = {
|
s1520454056@5057
|
44 |
val g2 = g.asInstanceOf[Graphics2D]
|
s1520454056@5057
|
45 |
|
s1520454056@5057
|
46 |
// enable antialiasing for Text
|
s1520454056@5057
|
47 |
val rh = new RenderingHints(
|
s1520454056@5057
|
48 |
RenderingHints.KEY_TEXT_ANTIALIASING,
|
s1520454056@5057
|
49 |
RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
|
s1520454056@5057
|
50 |
g2.setRenderingHints(rh);
|
s1520454056@5057
|
51 |
|
s1520454056@5057
|
52 |
// white background
|
s1520454056@5057
|
53 |
g.setColor(Color.WHITE)
|
s1520454056@5057
|
54 |
g.fillRect(0, 0, getWidth, getHeight)
|
s1520454056@5057
|
55 |
|
s1520454056@5057
|
56 |
|
s1520454056@5057
|
57 |
g.setColor(Color.BLACK)
|
s1520454056@5057
|
58 |
g.translate(Settings.translateX, Settings.translateY)
|
s1520454056@5057
|
59 |
g2.scale(Settings.zoom, Settings.zoom)
|
s1520454056@5101
|
60 |
|
s1520454056@5144
|
61 |
box = Util.assembleBoxes(g, ast, (g2: Graphics, x0: Int, y0: Int, str: String, box: Box) =>
|
s1520454056@5093
|
62 |
{
|
s1520454056@5093
|
63 |
|
s1520454056@5101
|
64 |
if (EventUtil.foreachBoxFunction != null) {
|
s1520454056@5101
|
65 |
EventUtil.foreachBoxFunction(g2, box)
|
s1520454056@5093
|
66 |
}
|
s1520454056@5057
|
67 |
}
|
s1520454056@5101
|
68 |
)
|
s1520454056@5131
|
69 |
|
s1520454056@5112
|
70 |
BoxUtil.Draw(box , g, editorPanel.field)
|
s1520454056@5108
|
71 |
setSize((box.width * Settings.zoom).round + 50 + Settings.translateX, Math.max((box.height * Settings.zoom).round, 50) + Settings.translateY)
|
s1520454056@5108
|
72 |
setPreferredSize(getSize)
|
s1520454056@5108
|
73 |
|
s1520454056@5112
|
74 |
|
s1520454056@5108
|
75 |
|
s1520454056@5101
|
76 |
EventUtil.foreachBoxFunction = null
|
s1520454056@5025
|
77 |
|
s1520454056@5144
|
78 |
g.drawRect(marker.x, marker.y, marker.width, marker.height)
|
s1520454056@5025
|
79 |
|
s1520454056@5057
|
80 |
}
|
s1520454056@5057
|
81 |
|
s1520454056@5057
|
82 |
|
s1520454056@5029
|
83 |
def mouseEntered(e: MouseEvent) {
|
s1520454056@5029
|
84 |
isSelected = true
|
s1520454056@5029
|
85 |
|
s1520454056@5029
|
86 |
}
|
s1520454056@5029
|
87 |
def mouseExited(e: MouseEvent ) {
|
s1520454056@5029
|
88 |
isSelected = false
|
s1520454056@5029
|
89 |
|
s1520454056@5029
|
90 |
}
|
s1520454056@5029
|
91 |
def mousePressed(e: MouseEvent ) {
|
s1520454056@5144
|
92 |
val boxAst : Ast = AstInfoUtil.FindBox(ast)
|
s1520454056@5144
|
93 |
if (boxAst != null) {
|
s1520454056@5144
|
94 |
ast =TransformAstUtil.Update(ast, boxAst, TransformAstUtil.UnBox)
|
s1520454056@5144
|
95 |
}
|
s1520454056@5144
|
96 |
|
s1520454056@5144
|
97 |
|
s1520454056@5057
|
98 |
pressedMousePoint = new Point ( Settings.translateX - e.getX , Settings.translateY - e.getY)
|
s1520454056@5144
|
99 |
marker.setLocation((e.getX / Settings.zoom ).round - (Settings.translateX / Settings.zoom).round,
|
s1520454056@5144
|
100 |
(e.getY / Settings.zoom ).round - (Settings.translateY / Settings.zoom).round)
|
s1520454056@5029
|
101 |
}
|
s1520454056@5029
|
102 |
def mouseReleased(e: MouseEvent ) {
|
s1520454056@5057
|
103 |
pressedMousePoint = null
|
s1520454056@5144
|
104 |
marker.setSize(0, 0)
|
s1520454056@5144
|
105 |
var highest : Box = findHighesBoxOf(box, markedBoxes)
|
s1520454056@5144
|
106 |
ast = TransformAstUtil.Update(ast, highest.ast, TransformAstUtil.Box)
|
s1520454056@5029
|
107 |
|
s1520454056@5144
|
108 |
markedBoxes = List.empty[Box]
|
s1520454056@5144
|
109 |
repaint()
|
s1520454056@5029
|
110 |
}
|
s1520454056@5029
|
111 |
def mouseClicked(e: MouseEvent ) {
|
s1520454056@5057
|
112 |
if (e.isControlDown()) {
|
s1520454056@5093
|
113 |
|
s1520454056@5101
|
114 |
EventUtil.foreachBoxFunction = EventUtil.doInBox(e.getPoint,
|
s1520454056@5093
|
115 |
(g, box) => {
|
s1520454056@5129
|
116 |
println(isac.gui.mawen.syntax.Ast.raw_string_of(ast))
|
s1520454056@5093
|
117 |
ast = TransformAstUtil.Update(ast, box.ast, TransformAstUtil.AstToCursor)
|
s1520454056@5129
|
118 |
println(isac.gui.mawen.syntax.Ast.raw_string_of(ast))
|
s1520454056@5101
|
119 |
|
s1520454056@5093
|
120 |
repaint()
|
s1520454056@5093
|
121 |
}
|
s1520454056@5093
|
122 |
);
|
s1520454056@5057
|
123 |
}else {
|
s1520454056@5057
|
124 |
mousePositionFunction = null
|
s1520454056@5057
|
125 |
}
|
s1520454056@5057
|
126 |
repaint()
|
s1520454056@5029
|
127 |
}
|
s1520454056@5093
|
128 |
|
s1520454056@5101
|
129 |
|
s1520454056@5057
|
130 |
|
s1520454056@5057
|
131 |
def mouseDragged(e:MouseEvent) {
|
s1520454056@5144
|
132 |
if (e.isControlDown() && Settings.isdraggingAllowed) {
|
s1520454056@5108
|
133 |
if (pressedMousePoint != null) {
|
s1520454056@5108
|
134 |
Settings.translateX = e.getX + pressedMousePoint.x
|
s1520454056@5108
|
135 |
Settings.translateY = e.getY + pressedMousePoint.y
|
s1520454056@5108
|
136 |
|
s1520454056@5108
|
137 |
repaint()
|
s1520454056@5108
|
138 |
}
|
s1520454056@5108
|
139 |
}
|
s1520454056@5144
|
140 |
else {
|
s1520454056@5144
|
141 |
marker.setSize(((e.getX / Settings.zoom).round - marker.x ) - (Settings.translateX / Settings.zoom).round,
|
s1520454056@5144
|
142 |
((e.getY / Settings.zoom).round - marker.y ) - (Settings.translateY / Settings.zoom).round)
|
s1520454056@5144
|
143 |
EventUtil.foreachBoxFunction = (g, b) => {
|
s1520454056@5144
|
144 |
if (b.BoxIn(marker) && b.isLeaf()) {
|
s1520454056@5144
|
145 |
b.draw(g, false)
|
s1520454056@5144
|
146 |
if (!markedBoxes.contains(b))
|
s1520454056@5144
|
147 |
markedBoxes = b :: markedBoxes
|
s1520454056@5144
|
148 |
}
|
s1520454056@5144
|
149 |
}
|
s1520454056@5144
|
150 |
repaint()
|
s1520454056@5144
|
151 |
|
s1520454056@5144
|
152 |
}
|
s1520454056@5057
|
153 |
}
|
s1520454056@5057
|
154 |
|
s1520454056@5057
|
155 |
def mouseMoved(e: MouseEvent ) {
|
s1520454056@5101
|
156 |
EventUtil.drawBoxAt(e.getPoint())
|
s1520454056@5144
|
157 |
|
s1520454056@5093
|
158 |
repaint()
|
s1520454056@5057
|
159 |
}
|
s1520454056@5057
|
160 |
|
s1520454056@5057
|
161 |
def mouseWheelMoved(e: MouseWheelEvent): Unit = {
|
s1520454056@5108
|
162 |
if (Settings.isZoomAllowed) {
|
s1520454056@5108
|
163 |
if (e.getPreciseWheelRotation() < 0) {
|
s1520454056@5108
|
164 |
Settings.zoom -= 0.1f;
|
s1520454056@5108
|
165 |
} else {
|
s1520454056@5108
|
166 |
Settings.zoom += 0.1f;
|
s1520454056@5108
|
167 |
}
|
s1520454056@5108
|
168 |
if (Settings.zoom < 0.01f) {
|
s1520454056@5108
|
169 |
Settings.zoom = 0.01f;
|
s1520454056@5108
|
170 |
}
|
s1520454056@5108
|
171 |
repaint();
|
s1520454056@5057
|
172 |
}
|
s1520454056@5108
|
173 |
|
s1520454056@5057
|
174 |
}
|
s1520454056@5093
|
175 |
|
s1520454056@5093
|
176 |
def actionPerformed(e: ActionEvent): Unit = {
|
s1520454056@5093
|
177 |
|
s1520454056@5101
|
178 |
ast = TransformAstUtil.Update(
|
s1520454056@5101
|
179 |
ast,
|
s1520454056@5101
|
180 |
e.getSource().asInstanceOf[AstTextField].getAst,
|
s1520454056@5101
|
181 |
e.getSource().asInstanceOf[AstTextField].ToAstFunc)
|
s1520454056@5129
|
182 |
|
s1520454056@5129
|
183 |
|
s1520454056@5112
|
184 |
editorPanel.field.setVisible(false)
|
s1520454056@5093
|
185 |
repaint()
|
s1520454056@5093
|
186 |
|
s1520454056@5093
|
187 |
|
s1520454056@5093
|
188 |
}
|
s1520454056@5112
|
189 |
|
s1520454056@5112
|
190 |
def keyPressed(event: KeyEvent): Unit = {
|
s1520454056@5112
|
191 |
|
s1520454056@5112
|
192 |
}
|
s1520454056@5112
|
193 |
|
s1520454056@5112
|
194 |
def keyReleased(event: KeyEvent): Unit = {
|
s1520454056@5129
|
195 |
if (event.getKeyCode() == KeyEvent.VK_ENTER && event.isControlDown()) {
|
s1520454056@5131
|
196 |
ast = TransformAstUtil.Update(
|
s1520454056@5131
|
197 |
ast,
|
s1520454056@5131
|
198 |
editorPanel.field.getAst,
|
s1520454056@5131
|
199 |
editorPanel.field.ToAstFunc)
|
s1520454056@5131
|
200 |
|
s1520454056@5131
|
201 |
editorPanel.field.setVisible(false)
|
s1520454056@5131
|
202 |
repaint()
|
s1520454056@5129
|
203 |
|
s1520454056@5129
|
204 |
editorPanel.fireNotifyIsaCheck();
|
s1520454056@5129
|
205 |
}
|
s1520454056@5144
|
206 |
|
s1520454056@5112
|
207 |
}
|
s1520454056@5112
|
208 |
|
s1520454056@5112
|
209 |
def keyTyped(event: KeyEvent): Unit = {
|
s1520454056@5129
|
210 |
|
s1520454056@5112
|
211 |
}
|
s1520454056@5029
|
212 |
|
s1520454056@5144
|
213 |
def findHighesBoxOf(rootbox: Box, markedBoxes : List[Box]) : Box = {
|
s1520454056@5144
|
214 |
println("size: " + markedBoxes.length)
|
s1520454056@5144
|
215 |
|
s1520454056@5144
|
216 |
|
s1520454056@5144
|
217 |
|
s1520454056@5144
|
218 |
if (markedBoxes.forall(x => rootbox.Contains(x)) &&
|
s1520454056@5144
|
219 |
! rootbox.children.exists(x => markedBoxes.forall(y => x.Contains(y)))
|
s1520454056@5144
|
220 |
) {
|
s1520454056@5144
|
221 |
return rootbox
|
s1520454056@5144
|
222 |
|
s1520454056@5144
|
223 |
} else if (markedBoxes.forall(x => rootbox.Contains(x)) &&
|
s1520454056@5144
|
224 |
rootbox.children.exists(x => markedBoxes.forall(y => x.Contains(y)))) {
|
s1520454056@5144
|
225 |
|
s1520454056@5144
|
226 |
for( box <- rootbox.children) {
|
s1520454056@5144
|
227 |
var resb = findHighesBoxOf(box, markedBoxes)
|
s1520454056@5144
|
228 |
if (resb != null) {
|
s1520454056@5144
|
229 |
return resb
|
s1520454056@5144
|
230 |
}
|
s1520454056@5144
|
231 |
|
s1520454056@5144
|
232 |
}
|
s1520454056@5144
|
233 |
|
s1520454056@5144
|
234 |
|
s1520454056@5144
|
235 |
}
|
s1520454056@5144
|
236 |
return null
|
s1520454056@5144
|
237 |
|
s1520454056@5144
|
238 |
}
|
s1520454056@5144
|
239 |
|
s1520454056@5029
|
240 |
}
|
s1520454056@5029
|
241 |
|
s1520454056@5029
|
242 |
|
s1520454056@5029
|
243 |
|
s1520454056@5029
|
244 |
|
s1520454056@5029
|
245 |
|
s1520454056@5029
|
246 |
|
s1520454056@5029
|
247 |
|
s1520454056@5029
|
248 |
|
s1520454056@5029
|
249 |
|
s1520454056@5029
|
250 |
|
s1520454056@5029
|
251 |
|
s1520454056@5029
|
252 |
|
s1520454056@5029
|
253 |
|
s1520454056@5029
|
254 |
|
s1520454056@5029
|
255 |
|