1.1 Binary file isac-java/lib/cli-assembly-0.3.3.jar has changed
2.1 Binary file isac-java/lib/setup-assembly-1.1.0-SNAPSHOT.jar has changed
3.1 --- a/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java Tue Sep 22 14:33:32 2020 +0200
3.2 +++ b/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java Fri Mar 26 10:45:05 2021 +0100
3.3 @@ -12,14 +12,13 @@
3.4 import java.nio.file.Paths;
3.5 import java.util.Properties;
3.6
3.7 -import info.hupel.isabelle.api.Configuration;
3.8 -import info.hupel.isabelle.api.Environment;
3.9 -import info.hupel.isabelle.api.Version;
3.10 -import info.hupel.isabelle.japi.JPlatform;
3.11 -import info.hupel.isabelle.japi.JResources;
3.12 -import info.hupel.isabelle.japi.JSetup;
3.13 -import info.hupel.isabelle.japi.JSystem;
3.14 -import info.hupel.isabelle.setup.Setup;
3.15 +import edu.tum.cs.isabelle.api.Configuration;
3.16 +import edu.tum.cs.isabelle.api.Environment;
3.17 +import edu.tum.cs.isabelle.api.Version;
3.18 +import edu.tum.cs.isabelle.japi.JPlatform;
3.19 +import edu.tum.cs.isabelle.japi.JSetup;
3.20 +import edu.tum.cs.isabelle.japi.JSystem;
3.21 +import edu.tum.cs.isabelle.setup.Setup;
3.22
3.23 /*
3.24 * Connect tests with Isac's mathematics engine.
3.25 @@ -46,10 +45,11 @@
3.26 try { inputStream.close();
3.27 } catch (IOException e) { e.printStackTrace(); }
3.28 }
3.29 - JResources res = JResources.dumpIsabelleResources();
3.30 + Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
3.31 + new Version("2015"), Setup.defaultPackageName());
3.32 + Environment env = JSetup.makeEnvironment(setup); // without Duration
3.33 Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
3.34 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
3.35 - return JSystem.create(env, config);
3.36 + return JSystem.create(env, config);
3.37 }
3.38
3.39 }
4.1 --- a/isac-java/src/java-tests/isac/bridge/TestPIDE.java Tue Sep 22 14:33:32 2020 +0200
4.2 +++ b/isac-java/src/java-tests/isac/bridge/TestPIDE.java Fri Mar 26 10:45:05 2021 +0100
4.3 @@ -18,11 +18,12 @@
4.4 import isac.util.formulae.Position;
4.5 import isac.util.formulae.Specification;
4.6 import isac.util.Formalization;
4.7 -import info.hupel.isabelle.api.*;
4.8 -import info.hupel.isabelle.japi.*;
4.9 -//import info.hupel.isabelle.*; // OVERWRITES System.out.println
4.10 -import info.hupel.isabelle.pure.*; // DEFINES type Term
4.11 -import info.hupel.isabelle.setup.Setup;
4.12 +
4.13 +import edu.tum.cs.isabelle.api.*;
4.14 +import edu.tum.cs.isabelle.japi.*;
4.15 +//import edu.tum.cs.isabelle.*; // OVERWRITES System.out.println
4.16 +import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
4.17 +import edu.tum.cs.isabelle.setup.Setup;
4.18
4.19 import java.io.FileNotFoundException;
4.20 import java.io.IOException;
4.21 @@ -66,11 +67,14 @@
4.22 System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");
4.23
4.24 System.out.println("---1 isac.bridge.TestPIDE#testConnection");
4.25 - JResources res = JResources.dumpIsabelleResources();
4.26 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.27 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
4.28 - JSystem sys = JSystem.create(env, config);
4.29 -
4.30 + Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
4.31 + new Version("2015"), Setup.defaultPackageName());
4.32 + Environment env = JSetup.makeEnvironment(setup); // ohne Duration
4.33 +
4.34 + System.out.println("---2 isac.bridge.TestPIDE#testConnection");
4.35 +/*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.36 + JSystem sys = JSystem.create(env, config);
4.37 +
4.38 System.out.println("---3 isac.bridge.TestPIDE#testConnection");
4.39 String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");
4.40
4.41 @@ -92,10 +96,11 @@
4.42 public void testMini_Test() {
4.43 System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
4.44
4.45 - JResources res = JResources.dumpIsabelleResources();
4.46 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.47 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
4.48 - JSystem sys = JSystem.create(env, config);
4.49 + Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
4.50 + new Version("2015"), Setup.defaultPackageName());
4.51 + Environment env = JSetup.makeEnvironment(setup); // ohne Duration
4.52 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.53 + JSystem sys = JSystem.create(env, config);
4.54
4.55 //----- step 1 ----------------------------------------------------------------
4.56 //build Formalization in Java and then convert to XML
4.57 @@ -223,15 +228,16 @@
4.58 * their format is still to be determined (String ?).
4.59 *
4.60 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
4.61 - * info.hupel.isabelle.pure.Term and String.
4.62 + * edu.tum.cs.isabelle.pure.Term and String.
4.63 */
4.64 public void testTermTransfer() {
4.65 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer");
4.66
4.67 - JResources res = JResources.dumpIsabelleResources();
4.68 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.69 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
4.70 - JSystem sys = JSystem.create(env, config);
4.71 + Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
4.72 + new Version("2015"), Setup.defaultPackageName());
4.73 + Environment env = JSetup.makeEnvironment(setup); // ohne Duration
4.74 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.75 + JSystem sys = JSystem.create(env, config);
4.76
4.77 //----- create test_term ------------------------------------------------------
4.78 Term test_term = TestsDATA.test_term();
4.79 @@ -255,15 +261,16 @@
4.80 * their format is String most likely during the next phase of devel.
4.81 *
4.82 * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
4.83 - * info.hupel.isabelle.pure.Term and String.
4.84 + * edu.tum.cs.isabelle.pure.Term and String.
4.85 */
4.86 public void testTermOneWay() {
4.87 System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay");
4.88
4.89 - JResources res = JResources.dumpIsabelleResources();
4.90 - Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.91 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
4.92 - JSystem sys = JSystem.create(env, config);
4.93 + Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
4.94 + new Version("2015"), Setup.defaultPackageName());
4.95 + Environment env = JSetup.makeEnvironment(setup); // ohne Duration
4.96 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
4.97 + JSystem sys = JSystem.create(env, config);
4.98
4.99 //----- create test_term ------------------------------------------------------
4.100 String term_str = "aaa + bbb::real";
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/isac-java/src/java-tests/isac/bridge/TestTerm.scala Fri Mar 26 10:45:05 2021 +0100
5.3 @@ -0,0 +1,108 @@
5.4 +package isac.bridge
5.5 +
5.6 +import junit.framework.TestCase
5.7 +
5.8 +import isac.util.BridgeMainPaths
5.9 +
5.10 +import java.nio.file.Paths
5.11 +import java.io.InputStream
5.12 +import junit.framework.Assert._
5.13 +
5.14 +import scala.concurrent._
5.15 +import scala.concurrent.ExecutionContext.Implicits.global
5.16 +import scala.concurrent.duration._
5.17 +//import org.scalatest.junit.JUnit3Suite
5.18 +//import org.scalatest.junit.AssertionsForJUnit
5.19 +
5.20 +import edu.tum.cs.isabelle._
5.21 +import edu.tum.cs.isabelle.api._
5.22 +import edu.tum.cs.isabelle.japi._
5.23 +import edu.tum.cs.isabelle.pure._
5.24 +import edu.tum.cs.isabelle.hol._
5.25 +import edu.tum.cs.isabelle.setup.Setup
5.26 +
5.27 +class TestTerm extends TestCase {
5.28 +
5.29 + val ReadTerm = Operation.implicitly[(String, Typ, String), Option[Term]]("read_term")
5.30 +
5.31 + val MakeInt = Operation.implicitly[Unit, Term]("make_int")
5.32 +
5.33 + var IsabelleHome: String = _
5.34 +
5.35 + // get ISABELLE_HOME from BridgeMain.properties, compare isac.bridge.TestPIDE in java
5.36 +// override def setUp() {
5.37 +// var inputStream: InputStream = null
5.38 +// try {
5.39 +// val prop = new Properties()
5.40 +// GOON
5.41 +// }
5.42 +// catch { case e: Exception =>
5.43 +// e.printStackTrace()
5.44 +// sys.exit(1)
5.45 +// }
5.46 +//
5.47 +// IsabelleHome = new StringBuilder("TODO")
5.48 +// }
5.49 +
5.50 + // another temmplate: http://stackoverflow.com/questions/15658310/scala-load-java-properties
5.51 +// override def setUp() {
5.52 +// val IsabelleHome =
5.53 +// try {
5.54 +// //val prop = new Properties(List[String])
5.55 +// val prop = new Properties()
5.56 +// prop.load(new FileInputStream("TODO"))
5.57 +// (
5.58 +// new String(prop.getProperty("ISABELLE_HOME"))
5.59 +// )
5.60 +// } catch { case e: Exception =>
5.61 +// e.printStackTrace()
5.62 +// sys.exit(1)
5.63 +// }
5.64 +// }
5.65 +
5.66 +
5.67 + def testTerm() {
5.68 + //val setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(),
5.69 +// val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(),
5.70 + val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
5.71 + new Version("2015"), Setup.defaultPackageName)
5.72 + val env = JSetup.makeEnvironment(setup)
5.73 + val config = Configuration.fromBuiltin("libisabelle_Isac")
5.74 + val sys = Await.result(System.create(env, config), 10.seconds)
5.75 + val thy = Theory(sys, "Main")
5.76 +
5.77 + val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)
5.78 + println(expr)
5.79 +
5.80 + val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds)
5.81 + println(expr2)
5.82 +
5.83 + val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds)
5.84 + println(expr3)
5.85 + //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3
5.86 + // HOLogic.mk_number @{typ int} 3
5.87 + //--- ouput in SML:
5.88 + // Const ("Num.numeral_class.numeral", "num ⇒ int") $ (
5.89 + // Const ("Num.num.Bit1", "num ⇒ num") $
5.90 + // Const ("Num.num.One", "num"))
5.91 + //----- from ../TestTerm.scala:
5.92 + // result(sys.invoke(MakeInt)(())
5.93 + //--- ouput in scala:
5.94 + // Success(
5.95 + // App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))),
5.96 + // App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),
5.97 + // Const(Num.num.One,Type(Num.num,List())))))
5.98 +
5.99 + val t: Term = Const("HOL.True", Typ.dummyT)
5.100 +
5.101 + t match {
5.102 + case Const(_, _) =>
5.103 + case Free(_, _) =>
5.104 + case Abs(_, _, _) =>
5.105 + case App(_, _) =>
5.106 + case Var(_, _) =>
5.107 + case Bound(_) =>
5.108 + }
5.109 + }
5.110 +
5.111 +}
5.112 \ No newline at end of file
6.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Tue Sep 22 14:33:32 2020 +0200
6.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java Fri Mar 26 10:45:05 2021 +0100
6.3 @@ -26,8 +26,8 @@
6.4 import isac.util.tactics.StringListTactic;
6.5 import isac.util.tactics.Tactic;
6.6 import isac.util.tactics.Theorem;
6.7 -import info.hupel.isabelle.api.XML;
6.8 -import info.hupel.isabelle.pure.*; // DEFINES type Term
6.9 +import edu.tum.cs.isabelle.api.XML;
6.10 +import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
6.11
6.12 import java.util.Vector;
6.13
6.14 @@ -385,4 +385,4 @@
6.15 System.out.println("\\--END isac.bridge.DataTypes#testTactics");
6.16
6.17 }
6.18 -}
6.19 \ No newline at end of file
6.20 +}
7.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala Tue Sep 22 14:33:32 2020 +0200
7.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala Fri Mar 26 10:45:05 2021 +0100
7.3 @@ -9,9 +9,9 @@
7.4 import isac.util.formulae.ModelItem
7.5 import isac.gui.mawen.scalaterm.Util
7.6
7.7 -import info.hupel.isabelle._ // for Codec
7.8 -import info.hupel.isabelle.api.XML
7.9 -import info.hupel.isabelle.pure._ // DEFINES type Term
7.10 +import edu.tum.cs.isabelle._ // for Codec
7.11 +import edu.tum.cs.isabelle.api.XML
7.12 +import edu.tum.cs.isabelle.pure._ // DEFINES type Term
7.13
7.14 import java.util.Vector
7.15 import scala.collection.JavaConverters._
8.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java Tue Sep 22 14:33:32 2020 +0200
8.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java Fri Mar 26 10:45:05 2021 +0100
8.3 @@ -7,7 +7,7 @@
8.4 package isac.bridge.xml;
8.5
8.6 import isac.bridge.xml.TestsDATA; // DataTypes.scala
8.7 -import info.hupel.isabelle.api.XML;
8.8 +import edu.tum.cs.isabelle.api.XML;
8.9 import junit.framework.TestCase;
8.10
8.11 /**
8.12 @@ -63,4 +63,4 @@
8.13 System.out.println("\\--END isac.bridge.xml.TestXMLout#test_is_message");
8.14
8.15 }
8.16 -}
8.17 \ No newline at end of file
8.18 +}
9.1 --- a/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala Tue Sep 22 14:33:32 2020 +0200
9.2 +++ b/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala Fri Mar 26 10:45:05 2021 +0100
9.3 @@ -6,8 +6,8 @@
9.4 */
9.5 package isac.bridge.xml
9.6
9.7 -import info.hupel.isabelle.api.XML
9.8 -import info.hupel.isabelle.pure._ // DEFINES type Term
9.9 +import edu.tum.cs.isabelle.api.XML
9.10 +import edu.tum.cs.isabelle.pure._ // DEFINES type Term
9.11
9.12 /*
9.13 * Compile test data for TestDataTypes.java.
9.14 @@ -114,4 +114,4 @@
9.15 def term_mini_subpbl_1 (): Term = {
9.16 App(Const("Equation.solve",Type("fun",List(Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List()))), Type("List.list",List(Type("HOL.bool",List())))))),App(App(Const("Product_Type.Pair",Type("fun",List(Type("HOL.bool",List()), Type("fun",List(Type("Real.real",List()), Type("Product_Type.prod",List(Type("HOL.bool",List()), Type("Real.real",List())))))))),App(App(Const("HOL.eq",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("HOL.bool",List())))))),App(App(Const("Groups.plus_class.plus",Type("fun",List(Type("Real.real",List()), Type("fun",List(Type("Real.real",List()), Type("Real.real",List())))))),Free("x",Type("Real.real",List()))),Free("1",Type("Real.real",List())))),Free("2",Type("Real.real",List())))),Free("x",Type("Real.real",List()))))
9.17 }
9.18 -}
9.19 \ No newline at end of file
9.20 +}
10.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala Tue Sep 22 14:33:32 2020 +0200
10.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala Fri Mar 26 10:45:05 2021 +0100
10.3 @@ -7,7 +7,7 @@
10.4 package isac.gui.mawen
10.5
10.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
10.7 -import info.hupel.isabelle.api.XML
10.8 +import edu.tum.cs.isabelle.api.XML
10.9
10.10 /*
10.11 * terms for tests
10.12 @@ -202,4 +202,4 @@
10.13 Constant("BOX.4"), //added to above
10.14 Variable("GAP")))))))))
10.15
10.16 -}
10.17 \ No newline at end of file
10.18 +}
11.1 --- a/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala Tue Sep 22 14:33:32 2020 +0200
11.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala Fri Mar 26 10:45:05 2021 +0100
11.3 @@ -10,7 +10,7 @@
11.4 import isac.bridge.xml.DataTypes
11.5 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
11.6
11.7 -import info.hupel.isabelle.japi._
11.8 +import edu.tum.cs.isabelle.japi._
11.9
11.10 import junit.framework.TestCase
11.11 import org.junit.Assert._
11.12 @@ -322,4 +322,4 @@
11.13 sys_.dispose()
11.14 super.tearDown()
11.15 }
11.16 -}
11.17 \ No newline at end of file
11.18 +}
12.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala Tue Sep 22 14:33:32 2020 +0200
12.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala Fri Mar 26 10:45:05 2021 +0100
12.3 @@ -2,9 +2,9 @@
12.4
12.5 import isac.bridge.Isabelle_Isac
12.6 import isac.bridge.xml.DataTypes
12.7 -import info.hupel.isabelle.pure._ // for Term
12.8 -import info.hupel.isabelle._ // for Codec
12.9 -import info.hupel.isabelle.japi._ // for JSystem
12.10 +import edu.tum.cs.isabelle.pure._ // for Term
12.11 +import edu.tum.cs.isabelle._ // for Codec
12.12 +import edu.tum.cs.isabelle.japi._ // for JSystem
12.13
12.14 import junit.framework.TestCase
12.15 import org.junit.Assert._
12.16 @@ -93,4 +93,4 @@
12.17 sys_.dispose()
12.18 super.tearDown()
12.19 }
12.20 -}
12.21 \ No newline at end of file
12.22 +}
13.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala Tue Sep 22 14:33:32 2020 +0200
13.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala Fri Mar 26 10:45:05 2021 +0100
13.3 @@ -1,7 +1,7 @@
13.4 package isac.gui.mawen.scalaterm
13.5
13.6 import isac.gui.mawen.syntax.Ast
13.7 -import info.hupel.isabelle.pure._
13.8 +import edu.tum.cs.isabelle.pure._
13.9 import junit.framework.TestCase
13.10 import java.lang.String
13.11 import org.junit.Assert._
13.12 @@ -39,4 +39,4 @@
13.13 println("\\--END isac.gui.mawen.scalaterm.TestUtil#mathml_of");
13.14 }
13.15
13.16 -}
13.17 \ No newline at end of file
13.18 +}
14.1 --- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala Tue Sep 22 14:33:32 2020 +0200
14.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala Fri Mar 26 10:45:05 2021 +0100
14.3 @@ -1,6 +1,6 @@
14.4 package isac.gui.mawen.scalaterm
14.5
14.6 -import info.hupel.isabelle.pure._
14.7 +import edu.tum.cs.isabelle.pure._
14.8 import isac.gui.mawen.syntax.Ast
14.9
14.10 object TestsDATA {
14.11 @@ -156,4 +156,4 @@
14.12 def a_2 = Ast.Variable("yyy")
14.13
14.14 def a_3 = Ast.Variable("zzz")
14.15 -}
14.16 \ No newline at end of file
14.17 +}
15.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Tue Sep 22 14:33:32 2020 +0200
15.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Fri Mar 26 10:45:05 2021 +0100
15.3 @@ -9,7 +9,7 @@
15.4 import isac.bridge.Isabelle_Isac
15.5 import isac.bridge.xml.DataTypes
15.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
15.7 -import info.hupel.isabelle.japi._ // for JSystem
15.8 +import edu.tum.cs.isabelle.japi._ // for JSystem
15.9
15.10 import junit.framework.TestCase
15.11 import org.junit.Assert._
15.12 @@ -51,4 +51,4 @@
15.13 sys_.dispose()
15.14 super.tearDown()
15.15 }
15.16 -}
15.17 \ No newline at end of file
15.18 +}
16.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Tue Sep 22 14:33:32 2020 +0200
16.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Fri Mar 26 10:45:05 2021 +0100
16.3 @@ -3,7 +3,7 @@
16.4 import isac.gui.mawen.scalaterm.TestsDATA
16.5 import isac.gui.mawen.TestDATA
16.6 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
16.7 -import info.hupel.isabelle.pure._ // for Term
16.8 +import edu.tum.cs.isabelle.pure._ // for Term
16.9 import isac.gui.mawen.syntax.isabelle.XLibrary
16.10 import isac.gui.mawen.editor.TestDATAeditor
16.11
17.1 --- a/isac-java/src/java/isac/bridge/BridgeMain.java Tue Sep 22 14:33:32 2020 +0200
17.2 +++ b/isac-java/src/java/isac/bridge/BridgeMain.java Fri Mar 26 10:45:05 2021 +0100
17.3 @@ -13,9 +13,13 @@
17.4 */
17.5 import isac.util.BridgeMainPaths;
17.6 import isac.util.FixedPortRMISocketFactory;
17.7 -import info.hupel.isabelle.api.*;
17.8 -import info.hupel.isabelle.japi.*;
17.9 -import info.hupel.isabelle.setup.*;
17.10 +import edu.tum.cs.isabelle.api.Configuration;
17.11 +import edu.tum.cs.isabelle.api.Environment;
17.12 +import edu.tum.cs.isabelle.api.Version;
17.13 +import edu.tum.cs.isabelle.japi.JPlatform;
17.14 +import edu.tum.cs.isabelle.japi.JSetup;
17.15 +import edu.tum.cs.isabelle.japi.JSystem;
17.16 +import edu.tum.cs.isabelle.setup.Setup;
17.17
17.18 import java.awt.BorderLayout;
17.19 import java.awt.Color;
17.20 @@ -26,11 +30,9 @@
17.21 import java.io.BufferedReader;
17.22 import java.io.IOException;
17.23 import java.io.Serializable;
17.24 -import java.nio.file.Path;
17.25 import java.nio.file.Paths;
17.26 import java.rmi.RemoteException;
17.27 import java.rmi.server.RMISocketFactory;
17.28 -import java.util.Arrays;
17.29
17.30 import javax.swing.JFrame;
17.31 import javax.swing.JPanel;
17.32 @@ -80,52 +82,11 @@
17.33 new ClientList();
17.34 setUpBridgeLog();
17.35 //*TTY*/startThreadsFirstTime();
17.36 -/* cp from last working version:
17.37 - * https://hg.risc.uni-linz.ac.at/wneuper/isac/file/84f1ca6a6dd9/isac-java/src/java/isac/bridge/BridgeMain.java#l85
17.38 - 85 log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
17.39 - 86 Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
17.40 - 87 new Version("2015"), Setup.defaultPackageName());
17.41 - 88 Environment env = JSetup.makeEnvironment(setup); // without Duration
17.42 - 89 Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
17.43 - 90 JSystem sys = JSystem.create(env, config);
17.44 - 92
17.45 - 93 connection_to_kernel_ = sys;
17.46 - 94 log(1, "<--ISA: connection established");
17.47 - */
17.48 -/* cp from downloaded libisabelle, current version:
17.49 -package info.hupel.isabelle.examples.java;
17.50 -
17.51 -import java.nio.file.Path;
17.52 -import java.nio.file.Paths;
17.53 -import java.util.Arrays;
17.54 -import info.hupel.isabelle.api.*;
17.55 -import info.hupel.isabelle.japi.*;
17.56 -import info.hupel.isabelle.setup.*;
17.57 -
17.58 -public class Hello_PIDE {
17.59 -
17.60 - public static void main(String args[]) {
17.61 - JResources res = JResources.dumpIsabelleResources();
17.62 - Configuration config = Configuration.simple("Protocol");
17.63 - Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2017")), res);
17.64 - JSystem sys = JSystem.create(env, config);
17.65 - String response = sys.invoke(Operations.HELLO, "world");
17.66 - System.out.println(response);
17.67 - sys.dispose();
17.68 - }
17.69 -}
17.70 - */
17.71 /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
17.72 -
17.73 - //these two values shall come from BridgeMail.properties
17.74 - Path path = java.nio.file.Paths.get //
17.75 - ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
17.76 - String vers = "2018";
17.77 -
17.78 - JResources res = JResources.dumpIsabelleResources();
17.79 - Setup setup = new Setup(path, JPlatform.guess(), new Version.Stable(vers));
17.80 - Environment env = JSetup.makeEnvironment(setup, res);
17.81 - //Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); //fromBuiltin is undefined
17.82 + Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
17.83 + new Version("2015"), Setup.defaultPackageName());
17.84 + Environment env = JSetup.makeEnvironment(setup); // ohne Duration
17.85 + Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
17.86 JSystem sys = JSystem.create(env, config);
17.87
17.88 /*PIDE*/connection_to_kernel_ = sys;
17.89 @@ -259,4 +220,4 @@
17.90 e.printStackTrace();
17.91 }
17.92 }
17.93 -}
17.94 \ No newline at end of file
17.95 +}
18.1 --- a/isac-java/src/java/isac/bridge/BridgeRMI.java Tue Sep 22 14:33:32 2020 +0200
18.2 +++ b/isac-java/src/java/isac/bridge/BridgeRMI.java Fri Mar 26 10:45:05 2021 +0100
18.3 @@ -39,8 +39,8 @@
18.4 import isac.util.tactics.SimpleTactic;
18.5 import isac.util.tactics.Tactic;
18.6 import isac.wsdialog.IContextProvider.ContextType;
18.7 -import info.hupel.isabelle.api.XML;
18.8 -import info.hupel.isabelle.japi.JSystem;
18.9 +import edu.tum.cs.isabelle.api.XML;
18.10 +import edu.tum.cs.isabelle.japi.JSystem;
18.11
18.12 import java.io.BufferedReader;
18.13 import java.io.IOException;
18.14 @@ -1958,4 +1958,4 @@
18.15 }
18.16
18.17
18.18 -}
18.19 \ No newline at end of file
18.20 +}
19.1 --- a/isac-java/src/java/isac/bridge/IsacOperations.java Tue Sep 22 14:33:32 2020 +0200
19.2 +++ b/isac-java/src/java/isac/bridge/IsacOperations.java Fri Mar 26 10:45:05 2021 +0100
19.3 @@ -1,7 +1,7 @@
19.4 package isac.bridge;
19.5
19.6 -import info.hupel.isabelle.*;
19.7 -import info.hupel.isabelle.api.XML;
19.8 +import edu.tum.cs.isabelle.*;
19.9 +import edu.tum.cs.isabelle.api.XML;
19.10
19.11 public class IsacOperations {
19.12 // for Test_PIDE.java
20.1 --- a/isac-java/src/java/isac/bridge/IsacOperationsScala.scala Tue Sep 22 14:33:32 2020 +0200
20.2 +++ b/isac-java/src/java/isac/bridge/IsacOperationsScala.scala Fri Mar 26 10:45:05 2021 +0100
20.3 @@ -1,7 +1,7 @@
20.4 package isac.bridge
20.5
20.6 -import info.hupel.isabelle._
20.7 -import info.hupel.isabelle.api.XML
20.8 +import edu.tum.cs.isabelle._
20.9 +import edu.tum.cs.isabelle.api.XML
20.10
20.11 object IsacOperationsScala {
20.12
20.13 @@ -72,4 +72,4 @@
20.14 //-------------------------------------------------------------------
20.15 val UseThys = implicitly[List[String], Unit]("use_thys")
20.16
20.17 -}
20.18 \ No newline at end of file
20.19 +}
21.1 --- a/isac-java/src/java/isac/bridge/xml/DataTypes.scala Tue Sep 22 14:33:32 2020 +0200
21.2 +++ b/isac-java/src/java/isac/bridge/xml/DataTypes.scala Fri Mar 26 10:45:05 2021 +0100
21.3 @@ -45,9 +45,9 @@
21.4 import isac.util.tactics.Theorem
21.5 import isac.util.Variant
21.6
21.7 -import info.hupel.isabelle.api.XML
21.8 -import info.hupel.isabelle.pure._ // for Term
21.9 -import info.hupel.isabelle._ // for Codec
21.10 +import edu.tum.cs.isabelle.api.XML
21.11 +import edu.tum.cs.isabelle.pure._ // for Term
21.12 +import edu.tum.cs.isabelle._ // for Codec
21.13
21.14 import java.util.ArrayList
21.15 import java.util.Vector
21.16 @@ -844,4 +844,4 @@
21.17 case _ => throw new IllegalArgumentException("xml_to_CChanged wrong arg: " + t)
21.18 }
21.19
21.20 -}
21.21 \ No newline at end of file
21.22 +}
22.1 --- a/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java Tue Sep 22 14:33:32 2020 +0200
22.2 +++ b/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java Fri Mar 26 10:45:05 2021 +0100
22.3 @@ -17,7 +17,7 @@
22.4 import isac.util.tactics.StringListTactic;
22.5 import isac.util.tactics.SubProblemTactic;
22.6 import isac.util.tactics.Tactic;
22.7 -import info.hupel.isabelle.api.XML;
22.8 +import edu.tum.cs.isabelle.api.XML;
22.9
22.10 /**
22.11 * Trials to cope with type conversions between Java and Scala.
23.1 --- a/isac-java/src/java/isac/bridge/xml/IsaToJava.scala Tue Sep 22 14:33:32 2020 +0200
23.2 +++ b/isac-java/src/java/isac/bridge/xml/IsaToJava.scala Fri Mar 26 10:45:05 2021 +0100
23.3 @@ -26,7 +26,7 @@
23.4 import isac.util.formulae.Specification
23.5 import isac.util.Message
23.6
23.7 -import info.hupel.isabelle.api.XML
23.8 +import edu.tum.cs.isabelle.api.XML
23.9
23.10 import java.util.ArrayList
23.11 import java.util.Vector
23.12 @@ -534,4 +534,4 @@
23.13 //fun setTheory : calcID -> thyID -> XML.tree
23.14 def set_thy_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)
23.15
23.16 -}
23.17 \ No newline at end of file
23.18 +}
24.1 --- a/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala Tue Sep 22 14:33:32 2020 +0200
24.2 +++ b/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala Fri Mar 26 10:45:05 2021 +0100
24.3 @@ -18,7 +18,7 @@
24.4 import isac.util.Formalization
24.5 import isac.wsdialog.IContextProvider.ContextType;
24.6
24.7 -import info.hupel.isabelle.api.XML
24.8 +import edu.tum.cs.isabelle.api.XML
24.9
24.10 import java.util.ArrayList
24.11 import java.util.Vector
24.12 @@ -356,4 +356,4 @@
24.13 }
24.14
24.15
24.16 -}
24.17 \ No newline at end of file
24.18 +}
25.1 --- a/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Tue Sep 22 14:33:32 2020 +0200
25.2 +++ b/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala Fri Mar 26 10:45:05 2021 +0100
25.3 @@ -3,7 +3,7 @@
25.4 import isac.gui.mawen.editor.Box.DrawBox
25.5 import isac.gui.mawen.syntax.Ast._
25.6 import isac.interfaces.IEditor
25.7 -import info.hupel.isabelle.api.Implementation
25.8 +import edu.tum.cs.isabelle.api.Implementation
25.9
25.10 import javax.swing._
25.11 import java.awt._
26.1 --- a/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Tue Sep 22 14:33:32 2020 +0200
26.2 +++ b/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Fri Mar 26 10:45:05 2021 +0100
26.3 @@ -5,9 +5,9 @@
26.4 import isac.gui.mawen.termtree.TreeNodeContent
26.5 import javax.swing.tree.DefaultMutableTreeNode
26.6
26.7 -import info.hupel.isabelle.api.XML
26.8 -import info.hupel.isabelle.pure._
26.9 -import info.hupel.isabelle._ // for Codec
26.10 +import edu.tum.cs.isabelle.api.XML
26.11 +import edu.tum.cs.isabelle.pure._
26.12 +import edu.tum.cs.isabelle._ // for Codec
26.13
26.14 object Util {
26.15
26.16 @@ -150,4 +150,4 @@
26.17 }
26.18 def mathml_of(t: Term): String = "<math xmlns="+"\"&mathml;\""+"><mrow>" + matml_of(t, 0, "none") + "</mrow></math>"
26.19
26.20 -}
26.21 \ No newline at end of file
26.22 +}
27.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/symbol.scala Tue Sep 22 14:33:32 2020 +0200
27.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/symbol.scala Fri Mar 26 10:45:05 2021 +0100
27.3 @@ -57,10 +57,7 @@
27.4
27.5 def ascii(c: Char): Symbol =
27.6 {
27.7 - if (c > 127) {
27.8 - Console.printf("Non-ASCII character: " + XLibrary.quote(c.toString));
27.9 - "Non-ASCII character: " + XLibrary.quote(c.toString)
27.10 - }
27.11 + if (c > 127) error("Non-ASCII character: " + XLibrary.quote(c.toString))
27.12 else char_symbols(c.toInt)
27.13 }
27.14
28.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala Tue Sep 22 14:33:32 2020 +0200
28.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala Fri Mar 26 10:45:05 2021 +0100
28.3 @@ -10,11 +10,11 @@
28.4
28.5 package isac.gui.mawen.syntax.isabelle
28.6
28.7 -import info.hupel.isabelle.pure._
28.8 +import edu.tum.cs.isabelle.pure._
28.9
28.10 object XTerm
28.11 {
28.12 - /* //---------- this would overwrite info.hupel.isabelle.pure._ ----------\\
28.13 + /* //---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------\\
28.14
28.15 type Indexname = (String, Int)
28.16
28.17 @@ -35,7 +35,7 @@
28.18 case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
28.19 case class App(fun: Term, arg: Term) extends Term
28.20
28.21 - \\---------- this would overwrite info.hupel.isabelle.pure._ ----------// */
28.22 + \\---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------// */
28.23
28.24 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\
28.25 // see ~~/src/Pure/General/symbol.scala: is digit
29.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala Tue Sep 22 14:33:32 2020 +0200
29.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala Fri Mar 26 10:45:05 2021 +0100
29.3 @@ -13,7 +13,7 @@
29.4 import scala.collection.mutable
29.5 import scala.util.Sorting
29.6
29.7 -import info.hupel.isabelle.api.XML // + for Isabelle/Isac
29.8 +import edu.tum.cs.isabelle.api.XML // + for Isabelle/Isac
29.9
29.10
29.11 object Text
29.12 @@ -41,7 +41,7 @@
29.13 {
29.14 // denotation: {start} Un {i. start < i & i < stop}
29.15 if (start > stop)
29.16 - Console.printf("Bad range: [" + start.toString + ":" + stop.toString + "]")
29.17 + error("Bad range: [" + start.toString + ":" + stop.toString + "]")
29.18
29.19 override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
29.20
29.21 @@ -187,4 +187,4 @@
29.22
29.23 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\
29.24
29.25 -}
29.26 \ No newline at end of file
29.27 +}
30.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Tue Sep 22 14:33:32 2020 +0200
30.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala Fri Mar 26 10:45:05 2021 +0100
30.3 @@ -11,7 +11,7 @@
30.4 import isac.gui.mawen.syntax.isabelle.XTerm
30.5 import isac.gui.mawen.syntax.Ast._ //"._" simplifies "Ast.Ast" to "Ast"
30.6
30.7 -import info.hupel.isabelle.pure._
30.8 +import edu.tum.cs.isabelle.pure._
30.9
30.10 import scala.collection.immutable.TreeMap
30.11
30.12 @@ -142,4 +142,4 @@
30.13 def print_rules (key: String): List[Tuple2[Ast, Ast]] =
30.14 if (symtab.contains(key)) symtab(key) else List()
30.15
30.16 -}
30.17 \ No newline at end of file
30.18 +}
31.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Tue Sep 22 14:33:32 2020 +0200
31.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Fri Mar 26 10:45:05 2021 +0100
31.3 @@ -11,7 +11,7 @@
31.4
31.5 import isac.gui.mawen.syntax.isabelle.XLibrary
31.6 import isac.gui.mawen.syntax.isabelle.XTerm
31.7 -import info.hupel.isabelle.pure._
31.8 +import edu.tum.cs.isabelle.pure._
31.9
31.10 object Syntax_Phases {
31.11
31.12 @@ -60,4 +60,4 @@
31.13
31.14 // we do NOT submit Term to Isabelle_Isac, only String (and let parse again)
31.15 def ast_to_term(ast: Ast.Ast) : Term = Const("DUMMY", Type("DUMMY"))
31.16 -}
31.17 \ No newline at end of file
31.18 +}
32.1 --- a/isac-java/src/java/isac/util/Formalization.java Tue Sep 22 14:33:32 2020 +0200
32.2 +++ b/isac-java/src/java/isac/util/Formalization.java Fri Mar 26 10:45:05 2021 +0100
32.3 @@ -10,7 +10,7 @@
32.4 package isac.util;
32.5
32.6 import isac.bridge.xml.DataTypes; // from libisabelle-full.jar
32.7 -import info.hupel.isabelle.api.XML; // from libisabelle-full.jar
32.8 +import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
32.9
32.10 import java.io.Serializable;
32.11 import java.util.ArrayList;
32.12 @@ -122,4 +122,4 @@
32.13 public Object next() {
32.14 return it_.next();
32.15 }
32.16 -}
32.17 \ No newline at end of file
32.18 +}
33.1 --- a/isac-java/src/java/isac/util/Variant.java Tue Sep 22 14:33:32 2020 +0200
33.2 +++ b/isac-java/src/java/isac/util/Variant.java Fri Mar 26 10:45:05 2021 +0100
33.3 @@ -12,7 +12,7 @@
33.4 import isac.util.formulae.Specification;
33.5 import isac.bridge.xml.DataTypes; //.scala
33.6
33.7 -import info.hupel.isabelle.api.XML; // from libisabelle's setup-assembly-*.jar
33.8 +import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
33.9
33.10 import java.io.Serializable;
33.11 import java.util.ArrayList;
33.12 @@ -83,7 +83,7 @@
33.13 * Format the object in a way that libisabelle/PIDE can handle it
33.14 * @return XML representation of this Variant
33.15 */
33.16 - // conversion is done in Scala, because it is much simpler here
33.17 + // conversion is done in Scala, because it is much simpler there
33.18 public XML.Tree toXML() {
33.19 return DataTypes.xml_of_Variant(this);
33.20 }
33.21 @@ -99,4 +99,4 @@
33.22 return isa_strings_;
33.23 }
33.24
33.25 -}
33.26 \ No newline at end of file
33.27 +}
34.1 --- a/isac-java/src/java/isac/util/formulae/Specification.java Tue Sep 22 14:33:32 2020 +0200
34.2 +++ b/isac-java/src/java/isac/util/formulae/Specification.java Fri Mar 26 10:45:05 2021 +0100
34.3 @@ -5,7 +5,7 @@
34.4 package isac.util.formulae;
34.5 import isac.bridge.xml.DataTypes; //.scala
34.6
34.7 -import info.hupel.isabelle.api.XML; //.scala
34.8 +import edu.tum.cs.isabelle.api.XML; //.scala
34.9
34.10 import java.io.Serializable;
34.11
34.12 @@ -78,4 +78,4 @@
34.13 public XML.Tree toXML() {
34.14 return DataTypes.xml_of_Specification(this);
34.15 }
34.16 -}
34.17 \ No newline at end of file
34.18 +}