# HG changeset patch
# User Walther Neuper <walther.neuper@jku.at>
# Date 1616751905 -3600
# Node ID b4e3883d7b66f8e7a73dff41b4a89ee37c848275
# Parent  d9f9cfd09b0f9e7181b96a73ad7d3159ca36acaa
reset mathematics-engine to Isabelle2015

note: for this version libisabelle was available,
which connects front-end (Java) and back-end (Isabelle/ML)

diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/lib/cli-assembly-0.3.3.jar
Binary file isac-java/lib/cli-assembly-0.3.3.jar has changed
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/lib/setup-assembly-1.1.0-SNAPSHOT.jar
Binary file isac-java/lib/setup-assembly-1.1.0-SNAPSHOT.jar has changed
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java
--- a/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/Isabelle_Isac.java	Fri Mar 26 10:45:05 2021 +0100
@@ -12,14 +12,13 @@
 import java.nio.file.Paths;
 import java.util.Properties;
 
-import info.hupel.isabelle.api.Configuration;
-import info.hupel.isabelle.api.Environment;
-import info.hupel.isabelle.api.Version;
-import info.hupel.isabelle.japi.JPlatform;
-import info.hupel.isabelle.japi.JResources;
-import info.hupel.isabelle.japi.JSetup;
-import info.hupel.isabelle.japi.JSystem;
-import info.hupel.isabelle.setup.Setup;
+import edu.tum.cs.isabelle.api.Configuration;
+import edu.tum.cs.isabelle.api.Environment;
+import edu.tum.cs.isabelle.api.Version;
+import edu.tum.cs.isabelle.japi.JPlatform;
+import edu.tum.cs.isabelle.japi.JSetup;
+import edu.tum.cs.isabelle.japi.JSystem;
+import edu.tum.cs.isabelle.setup.Setup;
 
 /*
  * Connect tests with Isac's mathematics engine.
@@ -46,10 +45,11 @@
         try { inputStream.close();
       } catch (IOException e) { e.printStackTrace(); }
       }
-    JResources res = JResources.dumpIsabelleResources();
+    Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
+               new Version("2015"), Setup.defaultPackageName());
+    Environment env = JSetup.makeEnvironment(setup); // without Duration
     Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-    Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
-    return JSystem.create(env, config);
+    return JSystem.create(env, config);    
   }
 
 }
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/TestPIDE.java
--- a/isac-java/src/java-tests/isac/bridge/TestPIDE.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/TestPIDE.java	Fri Mar 26 10:45:05 2021 +0100
@@ -18,11 +18,12 @@
 import isac.util.formulae.Position;
 import isac.util.formulae.Specification;
 import isac.util.Formalization;
-import info.hupel.isabelle.api.*;
-import info.hupel.isabelle.japi.*;
-//import info.hupel.isabelle.*;    // OVERWRITES System.out.println
-import info.hupel.isabelle.pure.*; // DEFINES type Term
-import info.hupel.isabelle.setup.Setup;
+
+import edu.tum.cs.isabelle.api.*;
+import edu.tum.cs.isabelle.japi.*;
+//import edu.tum.cs.isabelle.*;    // OVERWRITES System.out.println
+import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
+import edu.tum.cs.isabelle.setup.Setup;
 
 import java.io.FileNotFoundException;
 import java.io.IOException;
@@ -66,11 +67,14 @@
         System.out.println("/--BEGIN isac.bridge.TestPIDE#testConnection");
 
 		System.out.println("---1 isac.bridge.TestPIDE#testConnection");        
-        JResources res = JResources.dumpIsabelleResources();
-        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
-        JSystem sys = JSystem.create(env, config);      
-        
+		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
+          new Version("2015"), Setup.defaultPackageName());
+        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
+
+        System.out.println("---2 isac.bridge.TestPIDE#testConnection");        
+/*Error*/Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
+	    JSystem sys = JSystem.create(env, config);
+
 		System.out.println("---3 isac.bridge.TestPIDE#testConnection");        
 		String hello_out = sys.invoke(Operations.HELLO, "should-be-returned");
 
@@ -92,10 +96,11 @@
 	public void testMini_Test() {
 		System.out.println("/--BEGIN isac.bridge.TestPIDE#testMini_Test");
 
-        JResources res = JResources.dumpIsabelleResources();
-        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
-        JSystem sys = JSystem.create(env, config);
+		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
+          new Version("2015"), Setup.defaultPackageName());
+        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
+	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
+	    JSystem sys = JSystem.create(env, config);
 
 	    //----- step 1 ----------------------------------------------------------------
 	    //build Formalization in Java and then convert to XML
@@ -223,15 +228,16 @@
      * their format is still to be determined (String ?).
      * 
      * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
-     * info.hupel.isabelle.pure.Term and String.
+     * edu.tum.cs.isabelle.pure.Term and String.
      */
 	public void testTermTransfer() {
 		System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermTransfer");
 
-        JResources res = JResources.dumpIsabelleResources();
-        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
-        JSystem sys = JSystem.create(env, config);
+		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
+           new Version("2015"), Setup.defaultPackageName());
+        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
+	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
+	    JSystem sys = JSystem.create(env, config);
 
 	    //----- create test_term ------------------------------------------------------
 	    Term test_term = TestsDATA.test_term();
@@ -255,15 +261,16 @@
      * their format is String most likely during the next phase of devel.
      * 
      * Terms isac-java <-- Isabelle/Isac the other way round pack two formats,
-     * info.hupel.isabelle.pure.Term and String.
+     * edu.tum.cs.isabelle.pure.Term and String.
      */
 	public void testTermOneWay() {
 		System.out.println("/--BEGIN isac.bridge.TestPIDE#testTermOneWay");
 
-        JResources res = JResources.dumpIsabelleResources();
-        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
-        JSystem sys = JSystem.create(env, config);
+		Setup setup = new Setup(Paths.get(isabelle_home_), JPlatform.guess(),
+           new Version("2015"), Setup.defaultPackageName());
+        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
+	    Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
+	    JSystem sys = JSystem.create(env, config);
 
 	    //----- create test_term ------------------------------------------------------
 	    String term_str = "aaa + bbb::real";
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/TestTerm.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/isac-java/src/java-tests/isac/bridge/TestTerm.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -0,0 +1,108 @@
+package isac.bridge
+
+import junit.framework.TestCase
+
+import isac.util.BridgeMainPaths
+
+import java.nio.file.Paths
+import java.io.InputStream
+import junit.framework.Assert._
+
+import scala.concurrent._
+import scala.concurrent.ExecutionContext.Implicits.global
+import scala.concurrent.duration._
+//import org.scalatest.junit.JUnit3Suite
+//import org.scalatest.junit.AssertionsForJUnit
+
+import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.api._
+import edu.tum.cs.isabelle.japi._
+import edu.tum.cs.isabelle.pure._
+import edu.tum.cs.isabelle.hol._
+import edu.tum.cs.isabelle.setup.Setup
+
+class TestTerm extends TestCase {
+
+  val ReadTerm = Operation.implicitly[(String, Typ, String), Option[Term]]("read_term")
+  
+  val MakeInt = Operation.implicitly[Unit, Term]("make_int")
+  
+  var IsabelleHome: String = _
+  
+  // get ISABELLE_HOME from BridgeMain.properties, compare isac.bridge.TestPIDE in java
+//  override def setUp() {
+//    var inputStream: InputStream = null
+//    try {
+//      val prop = new Properties()
+//      GOON
+//    }
+//    catch { case e: Exception =>
+//      e.printStackTrace()
+//      sys.exit(1)
+//    }
+//    
+//    IsabelleHome = new StringBuilder("TODO")
+//  }
+
+  // another temmplate: http://stackoverflow.com/questions/15658310/scala-load-java-properties
+//  override def setUp() {
+//    val IsabelleHome = 
+//      try {
+//        //val prop = new Properties(List[String])
+//        val prop = new Properties()
+//        prop.load(new FileInputStream("TODO"))
+//        (
+//          new String(prop.getProperty("ISABELLE_HOME"))
+//        ) 
+//        } catch { case e: Exception => 
+//          e.printStackTrace()
+//          sys.exit(1)
+//        }
+//    }
+ 
+  
+  def testTerm() {
+    //val setup = Setup(Paths.get(IsabelleHome), JPlatform.guess(),
+//  val setup = Setup(Paths.get(BridgeMainPaths.ISABELLE_HOME), JPlatform.guess(),
+    val setup = Setup(Paths.get("/usr/local/isabisac/"), JPlatform.guess(),
+          new Version("2015"), Setup.defaultPackageName)
+    val env = JSetup.makeEnvironment(setup)
+    val config = Configuration.fromBuiltin("libisabelle_Isac")
+    val sys = Await.result(System.create(env, config), 10.seconds)
+    val thy = Theory(sys, "Main")
+    
+    val expr = Await.result(Expr.ofString[scala.math.BigInt](thy, "3"), 10.seconds)
+    println(expr)
+    
+    val expr2 = Await.result(sys.invoke(ReadTerm)(("3", Type("Int.int", Nil), "Main")), 10.seconds)
+    println(expr2)
+    
+    val expr3 = Await.result(sys.invoke(MakeInt)(()), 10.seconds)
+    println(expr3)
+    //----- in Protocol.thy#operation_setup make_int: HOLogic.mk_number @{typ int} 3
+    // HOLogic.mk_number @{typ int} 3
+    //--- ouput in SML:
+    //       Const ("Num.numeral_class.numeral", "num ⇒ int") $ (
+    //         Const ("Num.num.Bit1", "num ⇒ num") $ 
+    //         Const ("Num.num.One", "num"))
+    //----- from ../TestTerm.scala:
+    // result(sys.invoke(MakeInt)(())
+    //--- ouput in scala:
+    // Success(
+    //   App(Const(Num.numeral_class.numeral,Type(fun,List(Type(Num.num,List()), Type(Int.int,List())))),
+    //     App(Const(Num.num.Bit1,Type(fun,List(Type(Num.num,List()), Type(Num.num,List())))),
+    //         Const(Num.num.One,Type(Num.num,List())))))
+    
+    val t: Term = Const("HOL.True", Typ.dummyT)
+    
+    t match {
+      case Const(_, _) =>
+      case Free(_, _) =>
+      case Abs(_, _, _) =>
+      case App(_, _) =>
+      case Var(_, _) =>
+      case Bound(_) =>
+    }
+  }
+
+}
\ No newline at end of file
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java
--- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypes.java	Fri Mar 26 10:45:05 2021 +0100
@@ -26,8 +26,8 @@
 import isac.util.tactics.StringListTactic;
 import isac.util.tactics.Tactic;
 import isac.util.tactics.Theorem;
-import info.hupel.isabelle.api.XML;
-import info.hupel.isabelle.pure.*; // DEFINES type Term
+import edu.tum.cs.isabelle.api.XML;
+import edu.tum.cs.isabelle.pure.*; // DEFINES type Term
 
 import java.util.Vector;
 
@@ -385,4 +385,4 @@
         System.out.println("\\--END isac.bridge.DataTypes#testTactics");
 
     }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala
--- a/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/xml/TestDataTypesDATA.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -9,9 +9,9 @@
 import isac.util.formulae.ModelItem
 import isac.gui.mawen.scalaterm.Util
 
-import info.hupel.isabelle._      // for Codec
-import info.hupel.isabelle.api.XML
-import info.hupel.isabelle.pure._ // DEFINES type Term
+import edu.tum.cs.isabelle._      // for Codec
+import edu.tum.cs.isabelle.api.XML
+import edu.tum.cs.isabelle.pure._ // DEFINES type Term
 
 import java.util.Vector
 import scala.collection.JavaConverters._
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java
--- a/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/xml/TestXMLout.java	Fri Mar 26 10:45:05 2021 +0100
@@ -7,7 +7,7 @@
 package isac.bridge.xml;
 
 import isac.bridge.xml.TestsDATA; // DataTypes.scala
-import info.hupel.isabelle.api.XML;
+import edu.tum.cs.isabelle.api.XML;
 import junit.framework.TestCase;
 
 /**
@@ -63,4 +63,4 @@
 	System.out.println("\\--END isac.bridge.xml.TestXMLout#test_is_message");
 
 	}
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala
--- a/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/bridge/xml/TestsDATA.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -6,8 +6,8 @@
  */
 package isac.bridge.xml
 
-import info.hupel.isabelle.api.XML
-import info.hupel.isabelle.pure._ // DEFINES type Term
+import edu.tum.cs.isabelle.api.XML
+import edu.tum.cs.isabelle.pure._ // DEFINES type Term
 
 /*
  * Compile test data for TestDataTypes.java.
@@ -114,4 +114,4 @@
   def term_mini_subpbl_1 (): Term = {
     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()))))
   }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/TestDATA.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -7,7 +7,7 @@
 package isac.gui.mawen
 
 import isac.gui.mawen.syntax.Ast._  //"._" simplifies "Ast.Ast" to "Ast"
-import info.hupel.isabelle.api.XML
+import edu.tum.cs.isabelle.api.XML
 
   /*
    * terms for tests
@@ -202,4 +202,4 @@
               Constant("BOX.4"),     //added to above
               Variable("GAP")))))))))
 
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/TestUseCases.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -10,7 +10,7 @@
 import isac.bridge.xml.DataTypes
 import isac.gui.mawen.syntax.Ast._   //"._" simplifies "Ast.Ast" to "Ast"
 
-import info.hupel.isabelle.japi._
+import edu.tum.cs.isabelle.japi._
 
 import junit.framework.TestCase
 import org.junit.Assert._
@@ -322,4 +322,4 @@
     sys_.dispose()
     super.tearDown()
   }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/ScalaTermFromString.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -2,9 +2,9 @@
 
 import isac.bridge.Isabelle_Isac
 import isac.bridge.xml.DataTypes
-import info.hupel.isabelle.pure._  // for Term
-import info.hupel.isabelle._       // for Codec
-import info.hupel.isabelle.japi._  // for JSystem
+import edu.tum.cs.isabelle.pure._  // for Term
+import edu.tum.cs.isabelle._       // for Codec
+import edu.tum.cs.isabelle.japi._  // for JSystem
 
 import junit.framework.TestCase
 import org.junit.Assert._
@@ -93,4 +93,4 @@
     sys_.dispose()
     super.tearDown()
   }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestUtil.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -1,7 +1,7 @@
 package isac.gui.mawen.scalaterm
 
 import isac.gui.mawen.syntax.Ast
-import info.hupel.isabelle.pure._
+import edu.tum.cs.isabelle.pure._
 import junit.framework.TestCase
 import java.lang.String
 import org.junit.Assert._
@@ -39,4 +39,4 @@
     println("\\--END isac.gui.mawen.scalaterm.TestUtil#mathml_of");
   }
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/scalaterm/TestsDATA.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -1,6 +1,6 @@
 package isac.gui.mawen.scalaterm
 
-import info.hupel.isabelle.pure._
+import edu.tum.cs.isabelle.pure._
 import isac.gui.mawen.syntax.Ast
 
 object TestsDATA {
@@ -156,4 +156,4 @@
   def a_2 = Ast.Variable("yyy")
   
   def a_3 = Ast.Variable("zzz")
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -9,7 +9,7 @@
 import isac.bridge.Isabelle_Isac
 import isac.bridge.xml.DataTypes
 import isac.gui.mawen.syntax.Ast._   //"._" simplifies "Ast.Ast" to "Ast"
-import info.hupel.isabelle.japi._    // for JSystem
+import edu.tum.cs.isabelle.japi._    // for JSystem
 
 import junit.framework.TestCase
 import org.junit.Assert._
@@ -51,4 +51,4 @@
     sys_.dispose()
     super.tearDown()
   }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala
--- a/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -3,7 +3,7 @@
 import isac.gui.mawen.scalaterm.TestsDATA
 import isac.gui.mawen.TestDATA
 import isac.gui.mawen.syntax.Ast._  //"._" simplifies "Ast.Ast" to "Ast"
-import info.hupel.isabelle.pure._   // for Term
+import edu.tum.cs.isabelle.pure._   // for Term
 import isac.gui.mawen.syntax.isabelle.XLibrary
 import isac.gui.mawen.editor.TestDATAeditor
 
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/BridgeMain.java
--- a/isac-java/src/java/isac/bridge/BridgeMain.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/BridgeMain.java	Fri Mar 26 10:45:05 2021 +0100
@@ -13,9 +13,13 @@
  */
 import isac.util.BridgeMainPaths;
 import isac.util.FixedPortRMISocketFactory;
-import info.hupel.isabelle.api.*;
-import info.hupel.isabelle.japi.*;
-import info.hupel.isabelle.setup.*;
+import edu.tum.cs.isabelle.api.Configuration;
+import edu.tum.cs.isabelle.api.Environment;
+import edu.tum.cs.isabelle.api.Version;
+import edu.tum.cs.isabelle.japi.JPlatform;
+import edu.tum.cs.isabelle.japi.JSetup;
+import edu.tum.cs.isabelle.japi.JSystem;
+import edu.tum.cs.isabelle.setup.Setup;
 
 import java.awt.BorderLayout;
 import java.awt.Color;
@@ -26,11 +30,9 @@
 import java.io.BufferedReader;
 import java.io.IOException;
 import java.io.Serializable;
-import java.nio.file.Path;
 import java.nio.file.Paths;
 import java.rmi.RemoteException;
 import java.rmi.server.RMISocketFactory;
-import java.util.Arrays;
 
 import javax.swing.JFrame;
 import javax.swing.JPanel;
@@ -80,52 +82,11 @@
         new ClientList();
         setUpBridgeLog();
         //*TTY*/startThreadsFirstTime();
-/* cp from last working version:
- *  https://hg.risc.uni-linz.ac.at/wneuper/isac/file/84f1ca6a6dd9/isac-java/src/java/isac/bridge/BridgeMain.java#l85
-    85         log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
-    86         Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
-    87           new Version("2015"), Setup.defaultPackageName());
-    88         Environment env = JSetup.makeEnvironment(setup); // without Duration
-    89         Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
-    90         JSystem sys = JSystem.create(env, config);
-    92         
-    93         connection_to_kernel_ = sys;
-    94         log(1, "<--ISA: connection established");
- */
-/* cp from downloaded libisabelle, current version:
-package info.hupel.isabelle.examples.java;
-
-import java.nio.file.Path;
-import java.nio.file.Paths;
-import java.util.Arrays;
-import info.hupel.isabelle.api.*;
-import info.hupel.isabelle.japi.*;
-import info.hupel.isabelle.setup.*;
-
-public class Hello_PIDE {
-
-  public static void main(String args[]) {
-    JResources res = JResources.dumpIsabelleResources();
-    Configuration config = Configuration.simple("Protocol");
-    Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2017")), res);
-    JSystem sys = JSystem.create(env, config);
-    String response = sys.invoke(Operations.HELLO, "world");
-    System.out.println(response);
-    sys.dispose();
-  }
-}
- */
         /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
-
-        //these two values shall come from BridgeMail.properties
-        Path path = java.nio.file.Paths.get   //
-          ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
-        String vers = "2018";
-        
-        JResources res = JResources.dumpIsabelleResources();
-        Setup setup = new Setup(path, JPlatform.guess(), new Version.Stable(vers));
-        Environment env = JSetup.makeEnvironment(setup, res);
-        //Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); //fromBuiltin is undefined
+        Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
+          new Version("2015"), Setup.defaultPackageName());
+        Environment env = JSetup.makeEnvironment(setup); // ohne Duration
+        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
         JSystem sys = JSystem.create(env, config);
 
         /*PIDE*/connection_to_kernel_ = sys;
@@ -259,4 +220,4 @@
             e.printStackTrace();
         }
     }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/BridgeRMI.java
--- a/isac-java/src/java/isac/bridge/BridgeRMI.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/BridgeRMI.java	Fri Mar 26 10:45:05 2021 +0100
@@ -39,8 +39,8 @@
 import isac.util.tactics.SimpleTactic;
 import isac.util.tactics.Tactic;
 import isac.wsdialog.IContextProvider.ContextType;
-import info.hupel.isabelle.api.XML;
-import info.hupel.isabelle.japi.JSystem;
+import edu.tum.cs.isabelle.api.XML;
+import edu.tum.cs.isabelle.japi.JSystem;
 
 import java.io.BufferedReader;
 import java.io.IOException;
@@ -1958,4 +1958,4 @@
     }
 
     
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/IsacOperations.java
--- a/isac-java/src/java/isac/bridge/IsacOperations.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/IsacOperations.java	Fri Mar 26 10:45:05 2021 +0100
@@ -1,7 +1,7 @@
 package isac.bridge;
 
-import info.hupel.isabelle.*;
-import info.hupel.isabelle.api.XML;
+import edu.tum.cs.isabelle.*;
+import edu.tum.cs.isabelle.api.XML;
 
 public class IsacOperations {
 	  // for Test_PIDE.java
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/IsacOperationsScala.scala
--- a/isac-java/src/java/isac/bridge/IsacOperationsScala.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/IsacOperationsScala.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -1,7 +1,7 @@
 package isac.bridge
 
-import info.hupel.isabelle._
-import info.hupel.isabelle.api.XML
+import edu.tum.cs.isabelle._
+import edu.tum.cs.isabelle.api.XML
 
 object IsacOperationsScala {
   
@@ -72,4 +72,4 @@
   //-------------------------------------------------------------------
   val UseThys = implicitly[List[String], Unit]("use_thys")
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/xml/DataTypes.scala
--- a/isac-java/src/java/isac/bridge/xml/DataTypes.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/xml/DataTypes.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -45,9 +45,9 @@
 import isac.util.tactics.Theorem
 import isac.util.Variant
 
-import info.hupel.isabelle.api.XML
-import info.hupel.isabelle.pure._  // for Term
-import info.hupel.isabelle._       // for Codec
+import edu.tum.cs.isabelle.api.XML
+import edu.tum.cs.isabelle.pure._  // for Term
+import edu.tum.cs.isabelle._       // for Codec
 
 import java.util.ArrayList
 import java.util.Vector
@@ -844,4 +844,4 @@
     case _ => throw new IllegalArgumentException("xml_to_CChanged wrong arg: " + t)
   }
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java
--- a/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/xml/DataTypesCompanion.java	Fri Mar 26 10:45:05 2021 +0100
@@ -17,7 +17,7 @@
 import isac.util.tactics.StringListTactic;
 import isac.util.tactics.SubProblemTactic;
 import isac.util.tactics.Tactic;
-import info.hupel.isabelle.api.XML;
+import edu.tum.cs.isabelle.api.XML;
 
 /**
  * Trials to cope with type conversions between Java and Scala.
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/xml/IsaToJava.scala
--- a/isac-java/src/java/isac/bridge/xml/IsaToJava.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/xml/IsaToJava.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -26,7 +26,7 @@
 import isac.util.formulae.Specification
 import isac.util.Message
 
-import info.hupel.isabelle.api.XML
+import edu.tum.cs.isabelle.api.XML
 
 import java.util.ArrayList
 import java.util.Vector
@@ -534,4 +534,4 @@
   //fun setTheory : calcID -> thyID -> XML.tree
   def set_thy_out(t: XML.Tree): IntCalcHead = modify_calchead_out(t)
 
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/bridge/xml/JavaToIsa.scala
--- a/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/bridge/xml/JavaToIsa.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -18,7 +18,7 @@
 import isac.util.Formalization
 import isac.wsdialog.IContextProvider.ContextType;
 
-import info.hupel.isabelle.api.XML
+import edu.tum.cs.isabelle.api.XML
 
 import java.util.ArrayList
 import java.util.Vector
@@ -356,4 +356,4 @@
   } 
 
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala
--- a/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/editor/AstComponent.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -3,7 +3,7 @@
 import isac.gui.mawen.editor.Box.DrawBox
 import isac.gui.mawen.syntax.Ast._
 import isac.interfaces.IEditor
-import info.hupel.isabelle.api.Implementation
+import edu.tum.cs.isabelle.api.Implementation
 
 import javax.swing._
 import java.awt._
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala
--- a/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -5,9 +5,9 @@
 import isac.gui.mawen.termtree.TreeNodeContent
 import javax.swing.tree.DefaultMutableTreeNode
 
-import info.hupel.isabelle.api.XML
-import info.hupel.isabelle.pure._
-import info.hupel.isabelle._      // for Codec
+import edu.tum.cs.isabelle.api.XML
+import edu.tum.cs.isabelle.pure._
+import edu.tum.cs.isabelle._      // for Codec
 
 object Util {
 
@@ -150,4 +150,4 @@
   }
   def mathml_of(t: Term): String = "<math xmlns="+"\"&mathml;\""+"><mrow>" + matml_of(t, 0, "none") + "</mrow></math>"
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/syntax/isabelle/symbol.scala
--- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/symbol.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/symbol.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -57,10 +57,7 @@
 
   def ascii(c: Char): Symbol =
   {
-    if (c > 127) {
-      Console.printf("Non-ASCII character: " + XLibrary.quote(c.toString));
-      "Non-ASCII character: " + XLibrary.quote(c.toString)
-    }
+    if (c > 127) error("Non-ASCII character: " + XLibrary.quote(c.toString))
     else char_symbols(c.toInt)
   }
 
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala
--- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -10,11 +10,11 @@
 
 package isac.gui.mawen.syntax.isabelle
 
-import info.hupel.isabelle.pure._
+import edu.tum.cs.isabelle.pure._
 
 object XTerm
 {
-  /* //---------- this would overwrite info.hupel.isabelle.pure._ ----------\\
+  /* //---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------\\
   
   type Indexname = (String, Int)
 
@@ -35,7 +35,7 @@
   case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
   case class App(fun: Term, arg: Term) extends Term
   
-  \\---------- this would overwrite info.hupel.isabelle.pure._ ----------// */
+  \\---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------// */
 
 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\
   // see ~~/src/Pure/General/symbol.scala: is digit
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala
--- a/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/syntax/isabelle/text.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -13,7 +13,7 @@
 import scala.collection.mutable
 import scala.util.Sorting
 
-import info.hupel.isabelle.api.XML // + for Isabelle/Isac
+import edu.tum.cs.isabelle.api.XML // + for Isabelle/Isac
 
 
 object Text
@@ -41,7 +41,7 @@
   {
     // denotation: {start} Un {i. start < i & i < stop}
     if (start > stop)
-      Console.printf("Bad range: [" + start.toString + ":" + stop.toString + "]")
+      error("Bad range: [" + start.toString + ":" + stop.toString + "]")
 
     override def toString: String = "[" + start.toString + ":" + stop.toString + "]"
 
@@ -187,4 +187,4 @@
   
 //----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\
   
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/syntax/syntax.scala
--- a/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -11,7 +11,7 @@
 import isac.gui.mawen.syntax.isabelle.XTerm
 import isac.gui.mawen.syntax.Ast._  //"._" simplifies "Ast.Ast" to "Ast"
 
-import info.hupel.isabelle.pure._
+import edu.tum.cs.isabelle.pure._
 
 import scala.collection.immutable.TreeMap
 
@@ -142,4 +142,4 @@
   def print_rules (key: String): List[Tuple2[Ast, Ast]] =
     if (symtab.contains(key)) symtab(key) else List()
 
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala
--- a/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala	Fri Mar 26 10:45:05 2021 +0100
@@ -11,7 +11,7 @@
 
 import isac.gui.mawen.syntax.isabelle.XLibrary
 import isac.gui.mawen.syntax.isabelle.XTerm
-import info.hupel.isabelle.pure._
+import edu.tum.cs.isabelle.pure._
 
 object Syntax_Phases {
   
@@ -60,4 +60,4 @@
   
   // we do NOT submit Term to Isabelle_Isac, only String (and let parse again)
   def ast_to_term(ast: Ast.Ast) : Term = Const("DUMMY", Type("DUMMY"))
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/util/Formalization.java
--- a/isac-java/src/java/isac/util/Formalization.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/util/Formalization.java	Fri Mar 26 10:45:05 2021 +0100
@@ -10,7 +10,7 @@
 package isac.util;
 
 import isac.bridge.xml.DataTypes; // from libisabelle-full.jar
-import info.hupel.isabelle.api.XML; // from libisabelle-full.jar
+import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
 
 import java.io.Serializable;
 import java.util.ArrayList;
@@ -122,4 +122,4 @@
     public Object next() {
         return it_.next();
     }
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/util/Variant.java
--- a/isac-java/src/java/isac/util/Variant.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/util/Variant.java	Fri Mar 26 10:45:05 2021 +0100
@@ -12,7 +12,7 @@
 import isac.util.formulae.Specification;
 import isac.bridge.xml.DataTypes; //.scala
 
-import info.hupel.isabelle.api.XML; // from libisabelle's setup-assembly-*.jar
+import edu.tum.cs.isabelle.api.XML; // from libisabelle-full.jar
 
 import java.io.Serializable;
 import java.util.ArrayList;
@@ -83,7 +83,7 @@
      * Format the object in a way that libisabelle/PIDE can handle it
      * @return XML representation of this Variant
      */
-    // conversion is done in Scala, because it is much simpler here
+    // conversion is done in Scala, because it is much simpler there
     public XML.Tree toXML() {
     	return DataTypes.xml_of_Variant(this);
     }
@@ -99,4 +99,4 @@
         return isa_strings_;
     }
 
-}
\ No newline at end of file
+}
diff -r d9f9cfd09b0f -r b4e3883d7b66 isac-java/src/java/isac/util/formulae/Specification.java
--- a/isac-java/src/java/isac/util/formulae/Specification.java	Tue Sep 22 14:33:32 2020 +0200
+++ b/isac-java/src/java/isac/util/formulae/Specification.java	Fri Mar 26 10:45:05 2021 +0100
@@ -5,7 +5,7 @@
 package isac.util.formulae;
 import isac.bridge.xml.DataTypes; //.scala
 
-import info.hupel.isabelle.api.XML; //.scala
+import edu.tum.cs.isabelle.api.XML; //.scala
 
 import java.io.Serializable;
 
@@ -78,4 +78,4 @@
     public XML.Tree toXML() {
     	return DataTypes.xml_of_Specification(this);
     }
-}
\ No newline at end of file
+}