new setup for incremental build of jtree_of
authorWalther Neuper <wneuper@ist.tugraz.at>
Tue, 17 May 2016 15:52:28 +0200
changeset 49001bf92afe7757
parent 4899 7f5916a38769
child 4902 1d73085b1133
new setup for incremental build of jtree_of

Note: could not access a def in "class TestTerm ..",
need an "object ..."
isac-java/src/java-tests/isac/bridge/TestTerm.scala
isac-java/src/java-tests/isac/gui/mawen/TestTermTreeView.java
isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala
     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