1.1 --- a/isac-java/src/java-tests/isac/bridge/TestTerm.scala Tue May 17 15:09:08 2016 +0200
1.2 +++ b/isac-java/src/java-tests/isac/bridge/TestTerm.scala Tue May 17 15:52:28 2016 +0200
1.3 @@ -101,31 +101,4 @@
1.4 }
1.5 }
1.6
1.7 - //TODO incremental build ...
1.8 - def jtree_o(t: Term/*, jt: JTree*/): String = t match {
1.9 - case App(App(Const("Product_Type.Pair", _), t1), t2)
1.10 - => "11111"
1.11 - case App(App(Const(str, _), t1), t2)
1.12 - => "2222222"
1.13 - case App(Const(str, _), t1) => "33333"
1.14 - case Free(str, _) => str
1.15 - case Const(str, _) => str
1.16 - case _ => throw new IllegalArgumentException("makeJTreeOfTerm WRONG arg: " + t)
1.17 - }
1.18 - def jtree_of(t: Term): String = {
1.19 - null
1.20 - }
1.21 -
1.22 - def test_jtree_of() {
1.23 - println("/--BEGIN isac.bridge.TestTerm#test_jtree_of");
1.24 -
1.25 - val ct = new isac.gui.mawen.MockCalcTreeSIMPLIFY
1.26 -
1.27 - val t5 = ct.getTree.elementAt(5).getFormula.getTerm
1.28 - println(jtree_of(t5))
1.29 -
1.30 - println("\\--END isac.bridge.TestTerm#test_jtree_of");
1.31 - }
1.32 -
1.33 -
1.34 }
1.35 \ No newline at end of file
2.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestTermTreeView.java Tue May 17 15:09:08 2016 +0200
2.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestTermTreeView.java Tue May 17 15:52:28 2016 +0200
2.3 @@ -11,6 +11,8 @@
2.4 import isac.util.formulae.Formula;
2.5 import isac.util.formulae.Position;
2.6
2.7 +import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
2.8 +
2.9 import java.awt.BorderLayout;
2.10 import java.awt.GridBagLayout;
2.11 import java.awt.event.ActionEvent;
2.12 @@ -138,7 +140,10 @@
2.13 Position pos = new Position(vec, "Res");
2.14 MockCalcTreeSIMPLIFY ct = new MockCalcTreeSIMPLIFY();
2.15
2.16 - System.out.println("--- "+ Util.string_of(ct.get(pos).getTerm()));
2.17 + Term t = ct.get(pos).getTerm();
2.18 + System.out.println("--- "+ Util.string_of(t));
2.19 +// JTree jt = TestTerm.jtree_of(t);
2.20 +// drawTestTree(jt);
2.21
2.22 System.out.println("\\--END isac.gui.mawen.TestTermTreeView#test_jtree_of");
2.23 }
3.1 --- a/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Tue May 17 15:09:08 2016 +0200
3.2 +++ b/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Tue May 17 15:52:28 2016 +0200
3.3 @@ -1,5 +1,7 @@
3.4 package isac.gui.mawen.scalaterm
3.5
3.6 +import javax.swing.JTree;
3.7 +
3.8 import edu.tum.cs.isabelle.api.XML
3.9 import edu.tum.cs.isabelle.pure._
3.10 import edu.tum.cs.isabelle._ // for Codec
3.11 @@ -93,7 +95,18 @@
3.12 XML.Elem(("ISA", Nil), List(XML.Text("aaa + bbb::real"))),
3.13 XML.Elem(("TERM", Nil), List(Codec[Term].encode(t)))))
3.14
3.15 - //TODO
3.16 - def jtree_of (t: Term): javax.swing.JTree =
3.17 - null
3.18 + // incremental build via TestTermTreeView:
3.19 + def jtree_o(t: Term, jt: JTree): JTree = t match {
3.20 + case App(App(Const("Product_Type.Pair", _), t1), t2)
3.21 + => null
3.22 + case App(App(Const(str, _), t1), t2)
3.23 + => null
3.24 + case App(Const(str, _), t1) => null
3.25 + case Free(str, _) => null //ST_isa(str)
3.26 + case Const(str, _) => null //ST_isa(str)
3.27 + case _ => throw new IllegalArgumentException("jtree_of WRONG arg: " + t)
3.28 + }
3.29 + def jtree_of(t: Term): JTree = jtree_o(t, new JTree)
3.30 +
3.31 +
3.32 }
3.33 \ No newline at end of file