1 package isac.gui.mawen.editor |
1 package isac.gui.mawen.editor |
2 |
2 |
|
3 import isac.gui.mawen.editor.Box.DrawBox |
|
4 import isac.gui.mawen.syntax.Ast._ |
|
5 import isac.interfaces.IEditor |
|
6 import edu.tum.cs.isabelle.api.Implementation |
|
7 |
3 import javax.swing._ |
8 import javax.swing._ |
4 import isac.gui.mawen.syntax.Ast._ |
|
5 import java.awt._ |
9 import java.awt._ |
6 import java.awt.geom._ |
10 import java.awt.geom._ |
7 import java.awt.font._ |
11 import java.awt.font._ |
8 import edu.tum.cs.isabelle.api.Implementation |
|
9 import java.awt.event._ |
12 import java.awt.event._ |
10 import java.awt.font._ |
13 import java.awt.font._ |
11 import shapeless.Widen //WHY not java ? |
|
12 import org.drools.xml.ExtensibleXmlParser.Null |
14 import org.drools.xml.ExtensibleXmlParser.Null |
13 import scala.collection.immutable.List |
15 import scala.collection.immutable.List |
14 import isac.gui.mawen.editor.Box.DrawBox |
16 import shapeless.Widen //WHY not java ? |
15 import isac.interfaces.IEditor |
|
16 |
17 |
17 /** |
18 /** |
18 * The Java Swing component for a formula |
19 * The Java Swing component for a formula |
19 * represented by an <code>Ast</code> |
20 * represented by an <code>Ast</code> |
20 */ |
21 */ |
21 class AstComponent(var ast: Ast) extends JComponent with AstContainer with MouseListener with MouseMotionListener { |
22 class AstComponent(var ast: Ast) extends JComponent with AstContainer with MouseListener with MouseMotionListener { |
22 |
23 |
23 addMouseListener(this) |
24 addMouseListener(this) |
24 addMouseMotionListener(this) |
25 addMouseMotionListener(this) |
25 |
|
26 var pressedMousePoint : Point = null |
26 var pressedMousePoint : Point = null |
27 var marker : Rectangle = new Rectangle() |
27 var marker : Rectangle = new Rectangle() |
28 //list of boxes touched by mouse while drawing a rectangle; the outmost is relevant |
28 //list of boxes touched by mouse while drawing a rectangle; the outmost is relevant |
29 var markedBoxes : List[DrawBox] = List.empty[DrawBox] |
29 var markedBoxes : List[DrawBox] = List.empty[DrawBox] |
30 |
|
31 var mousePositionFunction : (Graphics, Int, Int, String, Box) => Unit = null |
30 var mousePositionFunction : (Graphics, Int, Int, String, Box) => Unit = null |
32 |
|
33 var box : DrawBox = null |
31 var box : DrawBox = null |
34 |
|
35 setFocusable(true) |
32 setFocusable(true) |
36 addKeyListener(EventUtil.CreateKeyEventHandler(this)) |
33 addKeyListener(EventUtil.CreateKeyEventHandler(this)) |
37 addMouseWheelListener(EventUtil.CreateMouseWheelHandler(this)) |
34 addMouseWheelListener(EventUtil.CreateMouseWheelHandler(this)) |
38 |
|
39 setSize(50,150) |
35 setSize(50,150) |
40 |
36 |
41 new Thread(new Runnable() { |
37 new Thread(new Runnable() { |
42 def run() { |
38 def run() { |
43 while (true) { |
39 while (true) { |
50 def setAst(ast: Ast) = { |
46 def setAst(ast: Ast) = { |
51 this.ast = ast |
47 this.ast = ast |
52 repaint() |
48 repaint() |
53 } |
49 } |
54 def getAst() : Ast = this.ast |
50 def getAst() : Ast = this.ast |
55 |
51 |
56 |
|
57 override def paint(g: Graphics) = { |
52 override def paint(g: Graphics) = { |
58 Settings.g = g |
53 Settings.g = g |
59 val g2 = g.asInstanceOf[Graphics2D] |
54 val g2 = g.asInstanceOf[Graphics2D] |
60 |
|
61 // enable antialiasing for Text |
55 // enable antialiasing for Text |
62 val rh = new RenderingHints( |
56 val rh = new RenderingHints( |
63 RenderingHints.KEY_TEXT_ANTIALIASING, |
57 RenderingHints.KEY_TEXT_ANTIALIASING, |
64 RenderingHints.VALUE_TEXT_ANTIALIAS_ON); |
58 RenderingHints.VALUE_TEXT_ANTIALIAS_ON); |
65 g2.setRenderingHints(rh); |
59 g2.setRenderingHints(rh); |
66 |
|
67 |
|
68 |
|
69 |
|
70 // white background |
60 // white background |
71 g.setColor(Color.WHITE) |
61 g.setColor(Color.WHITE) |
72 g.fillRect(0, 0, getWidth, getHeight) |
62 g.fillRect(0, 0, getWidth, getHeight) |
73 |
|
74 |
|
75 g.setColor(Color.BLACK) |
63 g.setColor(Color.BLACK) |
76 g.translate(Settings.translateX, Settings.translateY) |
64 g.translate(Settings.translateX, Settings.translateY) |
77 g2.scale(Settings.zoom, Settings.zoom) |
65 g2.scale(Settings.zoom, Settings.zoom) |
78 |
|
79 Settings.fillStringbounds(ast, g2) |
66 Settings.fillStringbounds(ast, g2) |
80 |
|
81 box = CalcUtil.assembleBoxes(ast, (box: DrawBox) => |
67 box = CalcUtil.assembleBoxes(ast, (box: DrawBox) => |
82 { |
68 { |
83 if (EventUtil.foreachBoxFunction != null) { |
69 if (EventUtil.foreachBoxFunction != null) { |
84 EventUtil.foreachBoxFunction(g2, box) |
70 EventUtil.foreachBoxFunction(g2, box) |
85 } |
71 } |
86 } |
72 } |
87 ) |
73 ) |
88 |
|
89 BoxUtil.Draw(box , g) |
74 BoxUtil.Draw(box , g) |
90 |
|
91 setSize((box.width * Settings.zoom).round + 50 + Settings.translateX, Math.max((box.height * Settings.zoom).round, 50) + Settings.translateY) |
75 setSize((box.width * Settings.zoom).round + 50 + Settings.translateX, Math.max((box.height * Settings.zoom).round, 50) + Settings.translateY) |
92 setPreferredSize(getSize) |
76 setPreferredSize(getSize) |
93 |
|
94 |
|
95 |
|
96 EventUtil.foreachBoxFunction = null |
77 EventUtil.foreachBoxFunction = null |
97 |
|
98 g.drawRect(marker.x, marker.y, marker.width, marker.height) |
78 g.drawRect(marker.x, marker.y, marker.width, marker.height) |
99 } |
79 } |
100 |
80 |
101 |
|
102 // /--- enforced by trait MouseListener --------------------------------------\ |
81 // /--- enforced by trait MouseListener --------------------------------------\ |
103 def mouseEntered(e: MouseEvent) { |
82 def mouseEntered(e: MouseEvent) {} |
104 |
83 def mouseExited(e: MouseEvent ) {} |
105 |
|
106 } |
|
107 def mouseExited(e: MouseEvent ) { |
|
108 |
|
109 |
|
110 } |
|
111 def mousePressed(e: MouseEvent ) { |
84 def mousePressed(e: MouseEvent ) { |
112 val boxAst : Ast = AstInfoUtil.FindBox(ast) |
85 val boxAst : Ast = AstInfoUtil.FindBox(ast) |
113 if (boxAst != null) { |
86 if (boxAst != null) { |
114 ast =TransformAstUtil.Update(ast, boxAst, TransformAstUtil.UnBox) |
87 ast =TransformAstUtil.Update(ast, boxAst, TransformAstUtil.UnBox) |
115 } |
88 } |
116 val cursorAst : Ast = AstInfoUtil.FindCursor(ast) |
89 val cursorAst : Ast = AstInfoUtil.FindCursor(ast) |
117 if (cursorAst != null) { |
90 if (cursorAst != null) { |
118 ast =TransformAstUtil.Update(ast, cursorAst , TransformAstUtil.CursorToAst) |
91 ast =TransformAstUtil.Update(ast, cursorAst , TransformAstUtil.CursorToAst) |
119 } |
92 } |
120 |
|
121 |
|
122 pressedMousePoint = new Point ( Settings.translateX - e.getX , Settings.translateY - e.getY) |
93 pressedMousePoint = new Point ( Settings.translateX - e.getX , Settings.translateY - e.getY) |
123 marker.setLocation((e.getX / Settings.zoom ).round - (Settings.translateX / Settings.zoom).round, |
94 marker.setLocation((e.getX / Settings.zoom ).round - (Settings.translateX / Settings.zoom).round, |
124 (e.getY / Settings.zoom ).round - (Settings.translateY / Settings.zoom).round) |
95 (e.getY / Settings.zoom ).round - (Settings.translateY / Settings.zoom).round) |
125 } |
96 } |
126 def mouseReleased(e: MouseEvent ) { |
97 def mouseReleased(e: MouseEvent ) { |