------ connection to new math-engine on Isabelle2018: question 4 to Lars
authorWalther Neuper <wneuper@ist.tugraz.at>
Wed, 19 Dec 2018 12:51:51 +0100
changeset 5236bdd3733fa7db
parent 5235 3ca9690d3e8b
child 5237 ee17f1b81a7f
------ connection to new math-engine on Isabelle2018: question 4 to Lars
isac-java/src/java/isac/bridge/BridgeMain.java
isac-java/src/java/isac/bridge/ToKernel.scala
     1.1 --- a/isac-java/src/java/isac/bridge/BridgeMain.java	Tue Dec 18 08:05:43 2018 +0100
     1.2 +++ b/isac-java/src/java/isac/bridge/BridgeMain.java	Wed Dec 19 12:51:51 2018 +0100
     1.3 @@ -117,7 +117,16 @@
     1.4   */
     1.5          /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
     1.6  
     1.7 -        JSystem sys = ToKernel.connect(); //does NOT yet work
     1.8 +        //these two values shall come from BridgeMail.properties
     1.9 +        Path path = java.nio.file.Paths.get   //
    1.10 +          ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
    1.11 +        String vers = "2018";
    1.12 +        
    1.13 +        JResources res = JResources.dumpIsabelleResources();
    1.14 +        Setup setup = new Setup(path, JPlatform.guess(), new Version.Stable("2018"));
    1.15 +        Environment env = JSetup.makeEnvironment(setup, res);
    1.16 +        //Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); //fromBuiltin is undefined
    1.17 +        JSystem sys = JSystem.create(env, config);
    1.18  
    1.19          /*PIDE*/connection_to_kernel_ = sys;
    1.20          /*PIDE*/log(1, "<--ISA: connection established");
     2.1 --- a/isac-java/src/java/isac/bridge/ToKernel.scala	Tue Dec 18 08:05:43 2018 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,25 +0,0 @@
     2.4 -//cp from Hello_PIDE.scala, two unresolved problems
     2.5 -
     2.6 -import info.hupel.isabelle.Platform
     2.7 -import info.hupel.isabelle.api._
     2.8 -import info.hupel.isabelle.japi._
     2.9 -import info.hupel.isabelle.setup._
    2.10 -import java.nio.file.Path;
    2.11 -
    2.12 -class ToKernel {
    2.13 -
    2.14 -  //these two will go into a property file:
    2.15 -  val path_str = "/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac"
    2.16 -  val version_str = "2018"
    2.17 -  
    2.18 -  val path = java.nio.file.Paths.get(path_str)	
    2.19 -  val platform = Platform.guess.getOrElse(sys.error(Setup.UnknownPlatform.explain))
    2.20 -  val version = Version.Stable(version_str)
    2.21 -    
    2.22 -  val setup = Setup(path, platform, version)
    2.23 -  val res = Resources.dumpIsabelleResources().right.get
    2.24 -  val config = Configuration.simple("Protocol")
    2.25 -  val env = setup.makeEnvironment(res, Nil)           //problem with scheduler
    2.26 -  
    2.27 -  def connect : JSystem = System.create(env, config)  //problem with types
    2.28 -}
    2.29 \ No newline at end of file