1.1 --- a/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Thu Jul 06 16:10:42 2017 +0200
1.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Wed Aug 02 09:09:40 2017 +0200
1.3 @@ -126,9 +126,14 @@
1.4 def mouseReleased(e: MouseEvent ) {
1.5 pressedMousePoint = null
1.6 marker.setSize(0, 0)
1.7 - var highest : DrawBox = findHighesBoxOf(box, markedBoxes)
1.8 - if (highest != null)
1.9 - ast = TransformAstUtil.Update(ast, highest.ast, TransformAstUtil.Box)
1.10 + findHighestBoxOf(box, markedBoxes) match {
1.11 + case Some(highest) => {
1.12 + this.ast = TransformAstUtil.Update(ast, highest.ast, TransformAstUtil.Box)
1.13 + }
1.14 + case None => {}
1.15 + }
1.16 +
1.17 +
1.18
1.19 markedBoxes = List.empty[DrawBox]
1.20 repaint()
1.21 @@ -190,27 +195,26 @@
1.22
1.23
1.24
1.25 - //TODOWN rename to findHighestBoxOf
1.26 - def findHighesBoxOf(rootbox: DrawBox, markedBoxes : List[DrawBox]) : DrawBox = {
1.27 +
1.28 + def findHighestBoxOf(rootbox: DrawBox, markedBoxes : List[DrawBox]) : Option[DrawBox] = {
1.29 if (markedBoxes != null && rootbox != null && rootbox.children != null) {
1.30 if (markedBoxes.forall(x => Box.Contains(rootbox,x)) &&
1.31 ! rootbox.children.exists(x => markedBoxes.forall(y => Box.Contains(x, y)))
1.32 ) {
1.33 - return rootbox
1.34 + return Some(rootbox)
1.35
1.36 } else if (markedBoxes.forall(x => Box.Contains(rootbox, x)) &&
1.37 rootbox.children.exists(x => markedBoxes.forall(y => Box.Contains(x, y)))) {
1.38
1.39 for( box <- rootbox.children) {
1.40 - var resb = findHighesBoxOf(box, markedBoxes)
1.41 - if (resb != null) {
1.42 - return resb
1.43 - }
1.44 -
1.45 + findHighestBoxOf(box, markedBoxes) match {
1.46 + case Some(box) => return Some(box)
1.47 + case None => {}
1.48 + }
1.49 }
1.50 }
1.51 }
1.52 - return null //TODOWN Option[DrawBox]
1.53 + return None
1.54 }
1.55 }
1.56
2.1 --- a/isac-java/src/java/isac/gui/mawen/editor/Box.scala Thu Jul 06 16:10:42 2017 +0200
2.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/Box.scala Wed Aug 02 09:09:40 2017 +0200
2.3 @@ -51,7 +51,7 @@
2.4 def drawBox(b: DrawBox, g: Graphics) {
2.5 if (b.isBoxed) {
2.6 g.setColor(Settings.CollorMapping(b.colorCode))
2.7 - g.fillRect(b.x, b.y - b.height, b.width, b.height)
2.8 + g.drawRect(b.x, b.y - b.height, b.width, b.height)
2.9 g.setColor(java.awt.Color.BLACK)
2.10 }
2.11 }
3.1 --- a/isac-java/src/java/isac/gui/mawen/editor/BoxUtil.scala Thu Jul 06 16:10:42 2017 +0200
3.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/BoxUtil.scala Wed Aug 02 09:09:40 2017 +0200
3.3 @@ -10,6 +10,7 @@
3.4 import java.awt.Font
3.5 import isac.gui.mawen.editor.Box._
3.6 import java.awt.Graphics2D
3.7 +import isac.gui.mawen.syntax.XSyntax
3.8
3.9 /**
3.10 * <code>paint</code>s a <code>Box</code> according to
3.11 @@ -43,7 +44,7 @@
3.12
3.13 }
3.14 def drawCursor(g: Graphics, box : DrawBox) = System.currentTimeMillis() match {
3.15 - case n if (n / 250) % 2 == 0 => box.ast match {
3.16 + case n if (n / 250) % 1 == 0 => box.ast match {
3.17 case Appl(List(Constant("CURSOR"), a)) => {
3.18 g.setColor(Color.RED)
3.19 g.asInstanceOf[Graphics2D].drawLine(box.x, box.y, box.x + box.width , box.y)
3.20 @@ -84,6 +85,8 @@
3.21
3.22
3.23 def drawPlus(g: Graphics, box : DrawBox) {
3.24 + val font_var = new Font("CMCSC8", Font.PLAIN, CalcUtil.fontsizeOf(box.level))
3.25 + g.setFont(font_var)
3.26
3.27 g.drawString("+", box.x0, box.y0)
3.28 drawBox(box, g)
3.29 @@ -95,11 +98,28 @@
3.30 drawBox(box, g)
3.31 }
3.32 def drawString(g: Graphics, box : DrawBox) {
3.33 - val font_var = new Font("CMCSC8", Font.PLAIN, CalcUtil.fontsizeOf(box.level))
3.34 - g.setFont(font_var)
3.35 + // operator
3.36 + XSyntax.ast_const.get(box.name) match {
3.37 + case Some((_,_,_,_, fontname, charIndex)) => {
3.38 + // Operator
3.39 + val font_var = new Font(fontname, Font.PLAIN, CalcUtil.fontsizeOf(box.level))
3.40 + g.setFont(font_var)
3.41 + g.drawString(charIndex.toChar.toString(), box.x0, box.y0)
3.42 + drawBox(box, g)
3.43 +
3.44 + }
3.45 + case None => {
3.46 + // Ident
3.47 + val font_var = new Font("CMMI12", Font.PLAIN, CalcUtil.fontsizeOf(box.level))
3.48 + g.setFont(font_var)
3.49 +
3.50 + g.drawString(box.name, box.x0, box.y0)
3.51 + drawBox(box, g)
3.52 + }
3.53 + }
3.54 +
3.55
3.56 - g.drawString(box.name, box.x0, box.y0)
3.57 - drawBox(box, g)
3.58 +
3.59 }
3.60
3.61
4.1 --- a/isac-java/src/java/isac/gui/mawen/editor/CalcUtil.scala Thu Jul 06 16:10:42 2017 +0200
4.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/CalcUtil.scala Wed Aug 02 09:09:40 2017 +0200
4.3 @@ -99,7 +99,6 @@
4.4 val midline = y0 - (fontsizeOf(level) * (2f / 3f)*(1f / 3f)).round
4.5 val newY = ((box.y - y0) * -1) - box.height /2 + midline
4.6
4.7 -
4.8
4.9 val b = DrawBox(op, level, box.x, y0, box.width, fontWidthOf(fontsizeOf(level)),x0, newY, ast)
4.10
5.1 --- a/isac-java/src/java/isac/gui/mawen/editor/EventUtil.scala Thu Jul 06 16:10:42 2017 +0200
5.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/EventUtil.scala Wed Aug 02 09:09:40 2017 +0200
5.3 @@ -52,7 +52,6 @@
5.4
5.5 f(g, box)
5.6 }
5.7 -
5.8 }
5.9 }
5.10
6.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Thu Jul 06 16:10:42 2017 +0200
6.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Wed Aug 02 09:09:40 2017 +0200
6.3 @@ -45,17 +45,17 @@
6.4 * _0: string used in Isabelle Term
6.5 */
6.6 val ast_const = Map (
6.7 - "=" -> ("HOL.eq", " = ", "infixl", 50), //see ~~/src/HOL/HOL.thy
6.8 - "+" -> ("Groups.plus_class.plus", " + ", "infixl", 65), //see ~~/src/HOL/Groups.thy
6.9 - "-" -> ("Groups.minus_class.minus", " - ", "infixl", 65), //see ~~/src/HOL/Groups.thy
6.10 - "-" -> ("Groups.plus_class.uminus", " -", "prefix", 80), //see ~~/src/HOL/Groups.thy
6.11 - "*" -> ("Groups.times_class.times", " * ", "infixl", 70), //see ~~/src/HOL/Groups.thy
6.12 - "/" -> ("Fields.inverse_class.divide", " / ", "infixl", 70), //see ~~/src/HOL/Fields.thy
6.13 - "^" -> ("Atools.pow", " ^ ", "infixr", 80), //see ~~/src/Tools/isac/Knowledge/Atools.thy
6.14 - "^" -> ("Power.power_class.power", " ", "infixr", 80), //see ~~/src/HOL/Power.thy
6.15 - "sin" -> ("Transcendental.sin", "sin ", "prefix", 70), //see ~~/src/HOL/Transcendental.thy
6.16 - "cos" -> ("Transcendental.cos", "cos ", "prefix", 70), //see ~~/src/HOL/Transcendental.thy
6.17 - "Integral" -> ("Integrate.Integral", "Integral ", "prefix", 91) //see ~~/src/Tools/isac/Knowledge/Integrate.thy
6.18 + "=" -> ("HOL.eq", " = ", "infixl", 50, "CMCSC8", '='.toInt), //see ~~/src/HOL/HOL.thy
6.19 + "+" -> ("Groups.plus_class.plus", " + ", "infixl", 65, "CMCSC8", '+'.toInt), //see ~~/src/HOL/Groups.thy
6.20 + "-" -> ("Groups.minus_class.minus", " - ", "infixl", 65, "CMCSC8", '-'.toInt), //see ~~/src/HOL/Groups.thy
6.21 + "-" -> ("Groups.plus_class.uminus", " -", "prefix", 80, "CMCSC8", '-'.toInt), //see ~~/src/HOL/Groups.thy
6.22 + "*" -> ("Groups.times_class.times", " * ", "infixl", 70, "CMCSC8", '*'.toInt), //see ~~/src/HOL/Groups.thy
6.23 + "/" -> ("Fields.inverse_class.divide", " / ", "infixl", 70, "", 0), //see ~~/src/HOL/Fields.thy
6.24 + "^" -> ("Atools.pow", " ^ ", "infixr", 80, "", 0), //see ~~/src/Tools/isac/Knowledge/Atools.thy
6.25 + "^" -> ("Power.power_class.power", " ", "infixr", 80, "", 0), //see ~~/src/HOL/Power.thy
6.26 + "sin" -> ("Transcendental.sin", "sin ", "prefix", 70, "", 0), //see ~~/src/HOL/Transcendental.thy
6.27 + "cos" -> ("Transcendental.cos", "cos ", "prefix", 70, "", 0), //see ~~/src/HOL/Transcendental.thy
6.28 + "Integral" -> ("Integrate.Integral", "Integral ", "prefix", 91, "", 0) //see ~~/src/Tools/isac/Knowledge/Integrate.thy
6.29 //...ERROR: implicit conversion found: ...
6.30 )
6.31 /* so not every constant needs to be in Util.isa_const */
6.32 @@ -65,7 +65,7 @@
6.33 case None => str.substring(str.lastIndexOf(".") + 1)}}
6.34 def ast_isa(str: String): String = { //key is the String in Ast.Constant
6.35 ast_const.get(str) match {
6.36 - case Some((ast, _, _, _)) => ast
6.37 + case Some((ast, _, _, _, _, _)) => ast
6.38 case None => str.substring(str.lastIndexOf(".") + 1)}}
6.39
6.40 def isa_math(str: String): String = { //key is the String in Term.Const
6.41 @@ -74,7 +74,7 @@
6.42 case None => str.substring(str.lastIndexOf(".") + 1) + " "}}
6.43 def ast_math(str: String): String = { //key is the String in Ast.Constant
6.44 ast_const.get(str) match {
6.45 - case Some((_, isa, _, _)) => isa
6.46 + case Some((_, isa, _, _, _, _)) => isa
6.47 case None => str.substring(str.lastIndexOf(".") + 1) + " "}}
6.48
6.49 def isa_fix(str: String): String = { //key is the String in Term.Const
6.50 @@ -83,7 +83,7 @@
6.51 case None => "prefix"}}
6.52 def ast_fix(str: String): String = { //key is the String in Ast.Constant
6.53 ast_const.get(str) match {
6.54 - case Some((_, _, fix, _)) => fix
6.55 + case Some((_, _, fix, _, _, _)) => fix
6.56 case None => "prefix"}}
6.57
6.58 def isa_prior(str: String): Int = { //key is the String in Term.Const
6.59 @@ -92,7 +92,7 @@
6.60 case None => 99}}
6.61 def ast_prior(str: String): Int = { //key is the String in Ast.Constant
6.62 ast_const.get(str) match {
6.63 - case Some((_, _, _, prior)) => prior
6.64 + case Some((_, _, _, prior, _, _)) => prior
6.65 case None => 99}}
6.66
6.67 /* ~~/src/Pure/Syntax/syntax.ML: