1.1 Binary file isac-java/lib/setup-assembly-1.1.0-SNAPSHOT.jar has changed
2.1 --- a/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java Wed Apr 04 12:08:01 2018 +0200
2.2 +++ b/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java Wed Sep 12 16:24:42 2018 +0200
2.3 @@ -12,13 +12,14 @@
2.4 import java.nio.file.Paths;
2.5 import java.util.Properties;
2.6
2.7 -import edu.tum.cs.isabelle.api.Configuration;
2.8 -import edu.tum.cs.isabelle.api.Environment;
2.9 -import edu.tum.cs.isabelle.api.Version;
2.10 -import edu.tum.cs.isabelle.japi.JPlatform;
2.11 -import edu.tum.cs.isabelle.japi.JSetup;
2.12 -import edu.tum.cs.isabelle.japi.JSystem;
2.13 -import edu.tum.cs.isabelle.setup.Setup;
2.14 +import info.hupel.isabelle.api.Configuration;
2.15 +import info.hupel.isabelle.api.Environment;
2.16 +import info.hupel.isabelle.api.Version;
2.17 +import info.hupel.isabelle.japi.JPlatform;
2.18 +import info.hupel.isabelle.japi.JResources;
2.19 +import info.hupel.isabelle.japi.JSetup;
2.20 +import info.hupel.isabelle.japi.JSystem;
2.21 +import info.hupel.isabelle.setup.Setup;
2.22
2.23 /*
2.24 * Connect tests with Isac's mathematics engine.
2.25 @@ -45,11 +46,10 @@
2.26 try { inputStream.close();
2.27 } catch (IOException e) { e.printStackTrace(); }
2.28 }
2.29 - Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
2.30 - new Version("2015"), Setup.defaultPackageName());
2.31 - Environment env = JSetup.makeEnvironment(setup); // without Duration
2.32 + JResources res = JResources.dumpIsabelleResources();
2.33 Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
2.34 - return JSystem.create(env, config);
2.35 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
2.36 + return JSystem.create(env, config);
2.37 }
2.38
2.39 }
3.1 --- a/isac-java/src/java-tests/isac/bridge/TestPIDE.java Wed Apr 04 12:08:01 2018 +0200
3.2 +++ b/isac-java/src/java-tests/isac/bridge/TestPIDE.java Wed Sep 12 16:24:42 2018 +0200
3.3 @@ -18,12 +18,11 @@
3.4 import isac.util.formulae.Position;
3.5 import isac.util.formulae.Specification;
3.6 import isac.util.Formalization;
3.7 -
3.8 -import edu.tum.cs.isabelle.api.*;
3.9 -import edu.tum.cs.isabelle.japi.*;
3.10 -//import edu.tum.cs.isabelle.*; // OVERWRITES System.out.println
3.11 -import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
3.12 -import edu.tum.cs.isabelle.setup.Setup;
3.13 +import info.hupel.isabelle.api.*;
3.14 +import info.hupel.isabelle.japi.*;
3.15 +//import info.hupel.isabelle.*; // OVERWRITES System.out.println
3.16 +import info.hupel.isabelle.pure.*; // DEFINES type Term
3.17 +import info.hupel.isabelle.setup.Setup;
3.18
3.19 import java.io.FileNotFoundException;
3.20 import java.io.IOException;
3.21 @@ -67,14 +66,11 @@
3.22 System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");
3.23
3.24 System.out.println("---1 isac.bridge.TestPIDE#testConnection");
3.25 - Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
3.26 - new Version("2015"), Setup.defaultPackageName());
3.27 - Environment env = JSetup.makeEnvironment(setup); // ohne Duration
3.28 -
3.29 - System.out.println("---2 isac.bridge.TestPIDE#testConnection");
3.30 -/*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.31 - JSystem sys = JSystem.create(env, config);
3.32 -
3.33 + JResources res = JResources.dumpIsabelleResources();
3.34 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.35 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
3.36 + JSystem sys = JSystem.create(env, config);
3.37 +
3.38 System.out.println("---3 isac.bridge.TestPIDE#testConnection");
3.39 String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");
3.40
3.41 @@ -96,11 +92,10 @@
3.42 public void testMini_Test() {
3.43 System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
3.44
3.45 - Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
3.46 - new Version("2015"), Setup.defaultPackageName());
3.47 - Environment env = JSetup.makeEnvironment(setup); // ohne Duration
3.48 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.49 - JSystem sys = JSystem.create(env, config);
3.50 + JResources res = JResources.dumpIsabelleResources();
3.51 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.52 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
3.53 + JSystem sys = JSystem.create(env, config);
3.54
3.55 //----- step 1 ----------------------------------------------------------------
3.56 //build Formalization in Java and then convert to XML
3.57 @@ -228,16 +223,15 @@
3.58 * their format is still to be determined (String ?).
3.59 *
3.60 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
3.61 - * edu.tum.cs.isabelle.pure.Term and String.
3.62 + * info.hupel.isabelle.pure.Term and String.
3.63 */
3.64 public void testTermTransfer() {
3.65 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer");
3.66
3.67 - Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
3.68 - new Version("2015"), Setup.defaultPackageName());
3.69 - Environment env = JSetup.makeEnvironment(setup); // ohne Duration
3.70 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.71 - JSystem sys = JSystem.create(env, config);
3.72 + JResources res = JResources.dumpIsabelleResources();
3.73 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.74 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
3.75 + JSystem sys = JSystem.create(env, config);
3.76
3.77 //----- create test_term ------------------------------------------------------
3.78 Term test_term = TestsDATA.test_term();
3.79 @@ -261,16 +255,15 @@
3.80 * their format is String most likely during the next phase of devel.
3.81 *
3.82 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
3.83 - * edu.tum.cs.isabelle.pure.Term and String.
3.84 + * info.hupel.isabelle.pure.Term and String.
3.85 */
3.86 public void testTermOneWay() {
3.87 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay");
3.88
3.89 - Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
3.90 - new Version("2015"), Setup.defaultPackageName());
3.91 - Environment env = JSetup.makeEnvironment(setup); // ohne Duration
3.92 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.93 - JSystem sys = JSystem.create(env, config);
3.94 + JResources res = JResources.dumpIsabelleResources();
3.95 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.96 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
3.97 + JSystem sys = JSystem.create(env, config);
3.98
3.99 //----- create test_term ------------------------------------------------------
3.100 String term_str = "aaa + bbb::real";
4.1 --- a/isac-java/src/java-tests/isac/bridge/TestTerm.scala Wed Apr 04 12:08:01 2018 +0200
4.2 +++ b/isac-java/src/java-tests/isac/bridge/TestTerm.scala Wed Sep 12 16:24:42 2018 +0200
4.3 @@ -14,12 +14,12 @@
4.4 //import org.scalatest.junit.JUnit3Suite
4.5 //import org.scalatest.junit.AssertionsForJUnit
4.6
4.7 -import edu.tum.cs.isabelle._
4.8 -import edu.tum.cs.isabelle.api._
4.9 -import edu.tum.cs.isabelle.japi._
4.10 -import edu.tum.cs.isabelle.pure._
4.11 -import edu.tum.cs.isabelle.hol._
4.12 -import edu.tum.cs.isabelle.setup.Setup
4.13 +import info.hupel.isabelle._
4.14 +import info.hupel.isabelle.api._
4.15 +import info.hupel.isabelle.japi._
4.16 +import info.hupel.isabelle.pure._
4.17 +import info.hupel.isabelle.hol._
4.18 +import info.hupel.isabelle.setup.Setup
4.19
4.20 class TestTerm extends TestCase {
4.21
4.22 @@ -62,13 +62,15 @@
4.23
4.24
4.25 def testTerm() {
4.26 - //val setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(),
4.27 -// val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(),
4.28 - val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
4.29 - new Version("2015"), Setup.defaultPackageName)
4.30 - val env = JSetup.makeEnvironment(setup)
4.31 + val res = JResources.dumpIsabelleResources()
4.32 val config = Configuration.fromBuiltin("libisabelle_Isac")
4.33 - val sys = Await.result(System.create(env, config), 10.seconds)
4.34 + val env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res)
4.35 + val sys = JSystem.create(env, config)
4.36 +// val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
4.37 +// new Version("2015"), Setup.defaultPackageName)
4.38 +// val env = JSetup.makeEnvironment(setup)
4.39 +// val config = Configuration.fromBuiltin("libisabelle_Isac")
4.40 +// val sys = Await.result(System.create(env, config), 10.seconds)
4.41 val thy = Theory(sys, "Main")
4.42
4.43 val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)
5.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Wed Apr 04 12:08:01 2018 +0200
5.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Wed Sep 12 16:24:42 2018 +0200
5.3 @@ -26,8 +26,8 @@
5.4 import isac.util.tactics.StringListTactic;
5.5 import isac.util.tactics.Tactic;
5.6 import isac.util.tactics.Theorem;
5.7 -import edu.tum.cs.isabelle.api.XML;
5.8 -import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
5.9 +import info.hupel.isabelle.api.XML;
5.10 +import info.hupel.isabelle.pure.*; // DEFINES type Term
5.11
5.12 import java.util.Vector;
5.13
6.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala Wed Apr 04 12:08:01 2018 +0200
6.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala Wed Sep 12 16:24:42 2018 +0200
6.3 @@ -9,9 +9,9 @@
6.4 import isac.util.formulae.ModelItem
6.5 import isac.gui.mawen.scalaterm.Util
6.6
6.7 -import edu.tum.cs.isabelle._ // for Codec
6.8 -import edu.tum.cs.isabelle.api.XML
6.9 -import edu.tum.cs.isabelle.pure._ // DEFINES type Term
6.10 +import info.hupel.isabelle._ // for Codec
6.11 +import info.hupel.isabelle.api.XML
6.12 +import info.hupel.isabelle.pure._ // DEFINES type Term
6.13
6.14 import java.util.Vector
6.15 import scala.collection.JavaConverters._
7.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java Wed Apr 04 12:08:01 2018 +0200
7.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java Wed Sep 12 16:24:42 2018 +0200
7.3 @@ -7,7 +7,7 @@
7.4 package isac.bridge.xml;
7.5
7.6 import isac.bridge.xml.TestsDATA; // DataTypes.scala
7.7 -import edu.tum.cs.isabelle.api.XML;
7.8 +import info.hupel.isabelle.api.XML;
7.9 import junit.framework.TestCase;
7.10
7.11 /**
8.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala Wed Apr 04 12:08:01 2018 +0200
8.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala Wed Sep 12 16:24:42 2018 +0200
8.3 @@ -6,8 +6,8 @@
8.4 */
8.5 package isac.bridge.xml
8.6
8.7 -import edu.tum.cs.isabelle.api.XML
8.8 -import edu.tum.cs.isabelle.pure._ // DEFINES type Term
8.9 +import info.hupel.isabelle.api.XML
8.10 +import info.hupel.isabelle.pure._ // DEFINES type Term
8.11
8.12 /*
8.13 * Compile test data for TestDataTypes.java.
9.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala Wed Apr 04 12:08:01 2018 +0200
9.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala Wed Sep 12 16:24:42 2018 +0200
9.3 @@ -7,7 +7,7 @@
9.4 package isac.gui.mawen
9.5
9.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
9.7 -import edu.tum.cs.isabelle.api.XML
9.8 +import info.hupel.isabelle.api.XML
9.9
9.10 /*
9.11 * terms for tests
10.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala Wed Apr 04 12:08:01 2018 +0200
10.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala Wed Sep 12 16:24:42 2018 +0200
10.3 @@ -10,7 +10,7 @@
10.4 import isac.bridge.xml.DataTypes
10.5 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
10.6
10.7 -import edu.tum.cs.isabelle.japi._
10.8 +import info.hupel.isabelle.japi._
10.9
10.10 import junit.framework.TestCase
10.11 import org.junit.Assert._
11.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala Wed Apr 04 12:08:01 2018 +0200
11.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala Wed Sep 12 16:24:42 2018 +0200
11.3 @@ -2,9 +2,9 @@
11.4
11.5 import isac.bridge.Isabelle_Isac
11.6 import isac.bridge.xml.DataTypes
11.7 -import edu.tum.cs.isabelle.pure._ // for Term
11.8 -import edu.tum.cs.isabelle._ // for Codec
11.9 -import edu.tum.cs.isabelle.japi._ // for JSystem
11.10 +import info.hupel.isabelle.pure._ // for Term
11.11 +import info.hupel.isabelle._ // for Codec
11.12 +import info.hupel.isabelle.japi._ // for JSystem
11.13
11.14 import junit.framework.TestCase
11.15 import org.junit.Assert._
12.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala Wed Apr 04 12:08:01 2018 +0200
12.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala Wed Sep 12 16:24:42 2018 +0200
12.3 @@ -1,7 +1,7 @@
12.4 package isac.gui.mawen.scalaterm
12.5
12.6 import isac.gui.mawen.syntax.Ast
12.7 -import edu.tum.cs.isabelle.pure._
12.8 +import info.hupel.isabelle.pure._
12.9 import junit.framework.TestCase
12.10 import java.lang.String
12.11 import org.junit.Assert._
13.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala Wed Apr 04 12:08:01 2018 +0200
13.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala Wed Sep 12 16:24:42 2018 +0200
13.3 @@ -1,6 +1,6 @@
13.4 package isac.gui.mawen.scalaterm
13.5
13.6 -import edu.tum.cs.isabelle.pure._
13.7 +import info.hupel.isabelle.pure._
13.8 import isac.gui.mawen.syntax.Ast
13.9
13.10 object TestsDATA {
14.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Wed Apr 04 12:08:01 2018 +0200
14.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Wed Sep 12 16:24:42 2018 +0200
14.3 @@ -9,7 +9,7 @@
14.4 import isac.bridge.Isabelle_Isac
14.5 import isac.bridge.xml.DataTypes
14.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
14.7 -import edu.tum.cs.isabelle.japi._ // for JSystem
14.8 +import info.hupel.isabelle.japi._ // for JSystem
14.9
14.10 import junit.framework.TestCase
14.11 import org.junit.Assert._
15.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Wed Apr 04 12:08:01 2018 +0200
15.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Wed Sep 12 16:24:42 2018 +0200
15.3 @@ -3,7 +3,7 @@
15.4 import isac.gui.mawen.scalaterm.TestsDATA
15.5 import isac.gui.mawen.TestDATA
15.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
15.7 -import edu.tum.cs.isabelle.pure._ // for Term
15.8 +import info.hupel.isabelle.pure._ // for Term
15.9 import isac.gui.mawen.syntax.isabelle.XLibrary
15.10 import isac.gui.mawen.editor.TestDATAeditor
15.11
16.1 --- a/isac-java/src/java/isac/bridge/BridgeMain.java Wed Apr 04 12:08:01 2018 +0200
16.2 +++ b/isac-java/src/java/isac/bridge/BridgeMain.java Wed Sep 12 16:24:42 2018 +0200
16.3 @@ -13,13 +13,9 @@
16.4 */
16.5 import isac.util.BridgeMainPaths;
16.6 import isac.util.FixedPortRMISocketFactory;
16.7 -import edu.tum.cs.isabelle.api.Configuration;
16.8 -import edu.tum.cs.isabelle.api.Environment;
16.9 -import edu.tum.cs.isabelle.api.Version;
16.10 -import edu.tum.cs.isabelle.japi.JPlatform;
16.11 -import edu.tum.cs.isabelle.japi.JSetup;
16.12 -import edu.tum.cs.isabelle.japi.JSystem;
16.13 -import edu.tum.cs.isabelle.setup.Setup;
16.14 +import info.hupel.isabelle.api.*;
16.15 +import info.hupel.isabelle.japi.*;
16.16 +import info.hupel.isabelle.setup.*;
16.17
16.18 import java.awt.BorderLayout;
16.19 import java.awt.Color;
16.20 @@ -30,9 +26,11 @@
16.21 import java.io.BufferedReader;
16.22 import java.io.IOException;
16.23 import java.io.Serializable;
16.24 +import java.nio.file.Path;
16.25 import java.nio.file.Paths;
16.26 import java.rmi.RemoteException;
16.27 import java.rmi.server.RMISocketFactory;
16.28 +import java.util.Arrays;
16.29
16.30 import javax.swing.JFrame;
16.31 import javax.swing.JPanel;
16.32 @@ -83,12 +81,10 @@
16.33 setUpBridgeLog();
16.34 //*TTY*/startThreadsFirstTime();
16.35 /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
16.36 - Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
16.37 - new Version("2015"), Setup.defaultPackageName());
16.38 - Environment env = JSetup.makeEnvironment(setup); // ohne Duration
16.39 + JResources res = JResources.dumpIsabelleResources();
16.40 Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
16.41 + Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
16.42 JSystem sys = JSystem.create(env, config);
16.43 -
16.44
16.45 /*PIDE*/connection_to_kernel_ = sys;
16.46 /*PIDE*/log(1, "<--ISA: connection established");
17.1 --- a/isac-java/src/java/isac/bridge/BridgeRMI.java Wed Apr 04 12:08:01 2018 +0200
17.2 +++ b/isac-java/src/java/isac/bridge/BridgeRMI.java Wed Sep 12 16:24:42 2018 +0200
17.3 @@ -39,8 +39,8 @@
17.4 import isac.util.tactics.SimpleTactic;
17.5 import isac.util.tactics.Tactic;
17.6 import isac.wsdialog.IContextProvider.ContextType;
17.7 -import edu.tum.cs.isabelle.api.XML;
17.8 -import edu.tum.cs.isabelle.japi.JSystem;
17.9 +import info.hupel.isabelle.api.XML;
17.10 +import info.hupel.isabelle.japi.JSystem;
17.11
17.12 import java.io.BufferedReader;
17.13 import java.io.IOException;
18.1 --- a/isac-java/src/java/isac/bridge/IsacOperations.java Wed Apr 04 12:08:01 2018 +0200
18.2 +++ b/isac-java/src/java/isac/bridge/IsacOperations.java Wed Sep 12 16:24:42 2018 +0200
18.3 @@ -1,7 +1,7 @@
18.4 package isac.bridge;
18.5
18.6 -import edu.tum.cs.isabelle.*;
18.7 -import edu.tum.cs.isabelle.api.XML;
18.8 +import info.hupel.isabelle.*;
18.9 +import info.hupel.isabelle.api.XML;
18.10
18.11 public class IsacOperations {
18.12 // for Test_PIDE.java
19.1 --- a/isac-java/src/java/isac/bridge/IsacOperationsScala.scala Wed Apr 04 12:08:01 2018 +0200
19.2 +++ b/isac-java/src/java/isac/bridge/IsacOperationsScala.scala Wed Sep 12 16:24:42 2018 +0200
19.3 @@ -1,7 +1,7 @@
19.4 package isac.bridge
19.5
19.6 -import edu.tum.cs.isabelle._
19.7 -import edu.tum.cs.isabelle.api.XML
19.8 +import info.hupel.isabelle._
19.9 +import info.hupel.isabelle.api.XML
19.10
19.11 object IsacOperationsScala {
19.12
20.1 --- a/isac-java/src/java/isac/bridge/xml/DataTypes.scala Wed Apr 04 12:08:01 2018 +0200
20.2 +++ b/isac-java/src/java/isac/bridge/xml/DataTypes.scala Wed Sep 12 16:24:42 2018 +0200
20.3 @@ -45,9 +45,9 @@
20.4 import isac.util.tactics.Theorem
20.5 import isac.util.Variant
20.6
20.7 -import edu.tum.cs.isabelle.api.XML
20.8 -import edu.tum.cs.isabelle.pure._ // for Term
20.9 -import edu.tum.cs.isabelle._ // for Codec
20.10 +import info.hupel.isabelle.api.XML
20.11 +import info.hupel.isabelle.pure._ // for Term
20.12 +import info.hupel.isabelle._ // for Codec
20.13
20.14 import java.util.ArrayList
20.15 import java.util.Vector
21.1 --- a/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java Wed Apr 04 12:08:01 2018 +0200
21.2 +++ b/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java Wed Sep 12 16:24:42 2018 +0200
21.3 @@ -17,7 +17,7 @@
21.4 import isac.util.tactics.StringListTactic;
21.5 import isac.util.tactics.SubProblemTactic;
21.6 import isac.util.tactics.Tactic;
21.7 -import edu.tum.cs.isabelle.api.XML;
21.8 +import info.hupel.isabelle.api.XML;
21.9
21.10 /**
21.11 * Trials to cope with type conversions between Java and Scala.
22.1 --- a/isac-java/src/java/isac/bridge/xml/IsaToJava.scala Wed Apr 04 12:08:01 2018 +0200
22.2 +++ b/isac-java/src/java/isac/bridge/xml/IsaToJava.scala Wed Sep 12 16:24:42 2018 +0200
22.3 @@ -26,7 +26,7 @@
22.4 import isac.util.formulae.Specification
22.5 import isac.util.Message
22.6
22.7 -import edu.tum.cs.isabelle.api.XML
22.8 +import info.hupel.isabelle.api.XML
22.9
22.10 import java.util.ArrayList
22.11 import java.util.Vector
23.1 --- a/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala Wed Apr 04 12:08:01 2018 +0200
23.2 +++ b/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala Wed Sep 12 16:24:42 2018 +0200
23.3 @@ -18,7 +18,7 @@
23.4 import isac.util.Formalization
23.5 import isac.wsdialog.IContextProvider.ContextType;
23.6
23.7 -import edu.tum.cs.isabelle.api.XML
23.8 +import info.hupel.isabelle.api.XML
23.9
23.10 import java.util.ArrayList
23.11 import java.util.Vector
24.1 --- a/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Wed Apr 04 12:08:01 2018 +0200
24.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Wed Sep 12 16:24:42 2018 +0200
24.3 @@ -3,7 +3,7 @@
24.4 import isac.gui.mawen.editor.Box.DrawBox
24.5 import isac.gui.mawen.syntax.Ast._
24.6 import isac.interfaces.IEditor
24.7 -import edu.tum.cs.isabelle.api.Implementation
24.8 +import info.hupel.isabelle.api.Implementation
24.9
24.10 import javax.swing._
24.11 import java.awt._
25.1 --- a/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Wed Apr 04 12:08:01 2018 +0200
25.2 +++ b/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Wed Sep 12 16:24:42 2018 +0200
25.3 @@ -5,9 +5,9 @@
25.4 import isac.gui.mawen.termtree.TreeNodeContent
25.5 import javax.swing.tree.DefaultMutableTreeNode
25.6
25.7 -import edu.tum.cs.isabelle.api.XML
25.8 -import edu.tum.cs.isabelle.pure._
25.9 -import edu.tum.cs.isabelle._ // for Codec
25.10 +import info.hupel.isabelle.api.XML
25.11 +import info.hupel.isabelle.pure._
25.12 +import info.hupel.isabelle._ // for Codec
25.13
25.14 object Util {
25.15
26.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala Wed Apr 04 12:08:01 2018 +0200
26.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala Wed Sep 12 16:24:42 2018 +0200
26.3 @@ -10,11 +10,11 @@
26.4
26.5 package isac.gui.mawen.syntax.isabelle
26.6
26.7 -import edu.tum.cs.isabelle.pure._
26.8 +import info.hupel.isabelle.pure._
26.9
26.10 object XTerm
26.11 {
26.12 - /* //---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------\\
26.13 + /* //---------- this would overwrite info.hupel.isabelle.pure._ ----------\\
26.14
26.15 type Indexname = (String, Int)
26.16
26.17 @@ -35,7 +35,7 @@
26.18 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
26.19 case class App(fun: Term, arg: Term) extends Term
26.20
26.21 - \\---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------// */
26.22 + \\---------- this would overwrite info.hupel.isabelle.pure._ ----------// */
26.23
26.24 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\
26.25 // see ~~/src/Pure/General/symbol.scala: is digit
27.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala Wed Apr 04 12:08:01 2018 +0200
27.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala Wed Sep 12 16:24:42 2018 +0200
27.3 @@ -13,7 +13,7 @@
27.4 import scala.collection.mutable
27.5 import scala.util.Sorting
27.6
27.7 -import edu.tum.cs.isabelle.api.XML // + for Isabelle/Isac
27.8 +import info.hupel.isabelle.api.XML // + for Isabelle/Isac
27.9
27.10
27.11 object Text
28.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Wed Apr 04 12:08:01 2018 +0200
28.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Wed Sep 12 16:24:42 2018 +0200
28.3 @@ -11,7 +11,7 @@
28.4 import isac.gui.mawen.syntax.isabelle.XTerm
28.5 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
28.6
28.7 -import edu.tum.cs.isabelle.pure._
28.8 +import info.hupel.isabelle.pure._
28.9
28.10 import scala.collection.immutable.TreeMap
28.11
29.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Wed Apr 04 12:08:01 2018 +0200
29.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Wed Sep 12 16:24:42 2018 +0200
29.3 @@ -11,7 +11,7 @@
29.4
29.5 import isac.gui.mawen.syntax.isabelle.XLibrary
29.6 import isac.gui.mawen.syntax.isabelle.XTerm
29.7 -import edu.tum.cs.isabelle.pure._
29.8 +import info.hupel.isabelle.pure._
29.9
29.10 object Syntax_Phases {
29.11
30.1 --- a/isac-java/src/java/isac/util/Formalization.java Wed Apr 04 12:08:01 2018 +0200
30.2 +++ b/isac-java/src/java/isac/util/Formalization.java Wed Sep 12 16:24:42 2018 +0200
30.3 @@ -10,7 +10,7 @@
30.4 package isac.util;
30.5
30.6 import isac.bridge.xml.DataTypes; // from libisabelle-full.jar
30.7 -import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
30.8 +import info.hupel.isabelle.api.XML; // from libisabelle-full.jar
30.9
30.10 import java.io.Serializable;
30.11 import java.util.ArrayList;
31.1 --- a/isac-java/src/java/isac/util/Variant.java Wed Apr 04 12:08:01 2018 +0200
31.2 +++ b/isac-java/src/java/isac/util/Variant.java Wed Sep 12 16:24:42 2018 +0200
31.3 @@ -12,7 +12,7 @@
31.4 import isac.util.formulae.Specification;
31.5 import isac.bridge.xml.DataTypes; //.scala
31.6
31.7 -import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
31.8 +import info.hupel.isabelle.api.XML; // from libisabelle's setup-assembly-*.jar
31.9
31.10 import java.io.Serializable;
31.11 import java.util.ArrayList;
31.12 @@ -83,7 +83,7 @@
31.13 * Format the object in a way that libisabelle/PIDE can handle it
31.14 * @return XML representation of this Variant
31.15 */
31.16 - // conversion is done in Scala, because it is much simpler there
31.17 + // conversion is done in Scala, because it is much simpler here
31.18 public XML.Tree toXML() {
31.19 return DataTypes.xml_of_Variant(this);
31.20 }
32.1 --- a/isac-java/src/java/isac/util/formulae/Specification.java Wed Apr 04 12:08:01 2018 +0200
32.2 +++ b/isac-java/src/java/isac/util/formulae/Specification.java Wed Sep 12 16:24:42 2018 +0200
32.3 @@ -5,7 +5,7 @@
32.4 package isac.util.formulae;
32.5 import isac.bridge.xml.DataTypes; //.scala
32.6
32.7 -import edu.tum.cs.isabelle.api.XML; //.scala
32.8 +import info.hupel.isabelle.api.XML; //.scala
32.9
32.10 import java.io.Serializable;
32.11