------ connection to new math-engine on Isabelle2018: question 3 to Lars
authorWalther Neuper <wneuper@ist.tugraz.at>
Tue, 18 Dec 2018 08:05:43 +0100
changeset 52353ca9690d3e8b
parent 5234 22aabc469ebb
child 5236 bdd3733fa7db
------ connection to new math-engine on Isabelle2018: question 3 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	Mon Dec 17 13:02:16 2018 +0100
     1.2 +++ b/isac-java/src/java/isac/bridge/BridgeMain.java	Tue Dec 18 08:05:43 2018 +0100
     1.3 @@ -117,12 +117,7 @@
     1.4   */
     1.5          /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
     1.6  
     1.7 -        JResources res = JResources.dumpIsabelleResources();
     1.8 -        Path path = java.nio.file.Paths.get
     1.9 -          ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
    1.10 -        Configuration config = Configuration.simple("Protocol");
    1.11 -        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.12 -        JSystem sys = JSystem.create(env, config);
    1.13 +        JSystem sys = ToKernel.connect(); //does NOT yet work
    1.14  
    1.15          /*PIDE*/connection_to_kernel_ = sys;
    1.16          /*PIDE*/log(1, "<--ISA: connection established");
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/isac-java/src/java/isac/bridge/ToKernel.scala	Tue Dec 18 08:05:43 2018 +0100
     2.3 @@ -0,0 +1,25 @@
     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