1.1 --- a/isac-java/src/java-tests/isac/bridge/TestPIDE.java	Tue Sep 22 14:33:32 2020 +0200
     1.2 +++ b/isac-java/src/java-tests/isac/bridge/TestPIDE.java	Fri Mar 26 10:45:05 2021 +0100
     1.3 @@ -18,11 +18,12 @@
     1.4  import isac.util.formulae.Position;
     1.5  import isac.util.formulae.Specification;
     1.6  import isac.util.Formalization;
     1.7 -import info.hupel.isabelle.api.*;
     1.8 -import info.hupel.isabelle.japi.*;
     1.9 -//import info.hupel.isabelle.*;    // OVERWRITES System.out.println
    1.10 -import info.hupel.isabelle.pure.*; // DEFINES type Term
    1.11 -import info.hupel.isabelle.setup.Setup;
    1.12 +
    1.13 +import edu.tum.cs.isabelle.api.*;
    1.14 +import edu.tum.cs.isabelle.japi.*;
    1.15 +//import edu.tum.cs.isabelle.*;    // OVERWRITES System.out.println
    1.16 +import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
    1.17 +import edu.tum.cs.isabelle.setup.Setup;
    1.18  
    1.19  import java.io.FileNotFoundException;
    1.20  import java.io.IOException;
    1.21 @@ -66,11 +67,14 @@
    1.22          System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");
    1.23  
    1.24  		System.out.println("---1 isac.bridge.TestPIDE#testConnection");        
    1.25 -        JResources res = JResources.dumpIsabelleResources();
    1.26 -        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.27 -        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.28 -        JSystem sys = JSystem.create(env, config);      
    1.29 -        
    1.30 +		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
    1.31 +          new Version("2015"), Setup.defaultPackageName());
    1.32 +        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
    1.33 +
    1.34 +        System.out.println("---2 isac.bridge.TestPIDE#testConnection");        
    1.35 +/*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.36 +	    JSystem sys = JSystem.create(env, config);
    1.37 +
    1.38  		System.out.println("---3 isac.bridge.TestPIDE#testConnection");        
    1.39  		String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");
    1.40  
    1.41 @@ -92,10 +96,11 @@
    1.42  	public void testMini_Test() {
    1.43  		System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
    1.44  
    1.45 -        JResources res = JResources.dumpIsabelleResources();
    1.46 -        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.47 -        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.48 -        JSystem sys = JSystem.create(env, config);
    1.49 +		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
    1.50 +          new Version("2015"), Setup.defaultPackageName());
    1.51 +        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
    1.52 +	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.53 +	    JSystem sys = JSystem.create(env, config);
    1.54  
    1.55  	    //----- step 1 ----------------------------------------------------------------
    1.56  	    //build Formalization in Java and then convert to XML
    1.57 @@ -223,15 +228,16 @@
    1.58       * their format is still to be determined (String ?).
    1.59       * 
    1.60       * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
    1.61 -     * info.hupel.isabelle.pure.Term and String.
    1.62 +     * edu.tum.cs.isabelle.pure.Term and String.
    1.63       */
    1.64  	public void testTermTransfer() {
    1.65  		System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer");
    1.66  
    1.67 -        JResources res = JResources.dumpIsabelleResources();
    1.68 -        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.69 -        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.70 -        JSystem sys = JSystem.create(env, config);
    1.71 +		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
    1.72 +           new Version("2015"), Setup.defaultPackageName());
    1.73 +        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
    1.74 +	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.75 +	    JSystem sys = JSystem.create(env, config);
    1.76  
    1.77  	    //----- create test_term ------------------------------------------------------
    1.78  	    Term test_term = TestsDATA.test_term();
    1.79 @@ -255,15 +261,16 @@
    1.80       * their format is String most likely during the next phase of devel.
    1.81       * 
    1.82       * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
    1.83 -     * info.hupel.isabelle.pure.Term and String.
    1.84 +     * edu.tum.cs.isabelle.pure.Term and String.
    1.85       */
    1.86  	public void testTermOneWay() {
    1.87  		System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay");
    1.88  
    1.89 -        JResources res = JResources.dumpIsabelleResources();
    1.90 -        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.91 -        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.92 -        JSystem sys = JSystem.create(env, config);
    1.93 +		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
    1.94 +           new Version("2015"), Setup.defaultPackageName());
    1.95 +        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
    1.96 +	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.97 +	    JSystem sys = JSystem.create(env, config);
    1.98  
    1.99  	    //----- create test_term ------------------------------------------------------
   1.100  	    String term_str = "aaa + bbb::real";