------ connection to new math-engine on Isabelle2018: question 2 to Lars
authorWalther Neuper <wneuper@ist.tugraz.at>
Mon, 17 Dec 2018 12:58:12 +0100
changeset 5233f9e91d4ee161
parent 5232 34f18fdc3103
child 5234 22aabc469ebb
------ connection to new math-engine on Isabelle2018: question 2 to Lars
isac-java/src/java/isac/bridge/BridgeMain.java
     1.1 --- a/isac-java/src/java/isac/bridge/BridgeMain.java	Wed Nov 28 08:59:29 2018 +0100
     1.2 +++ b/isac-java/src/java/isac/bridge/BridgeMain.java	Mon Dec 17 12:58:12 2018 +0100
     1.3 @@ -82,12 +82,48 @@
     1.4          //*TTY*/startThreadsFirstTime();
     1.5          /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
     1.6          //see libisabelle/modules/examples/src/main/java/edu/tum/cs/isabelle/examples/Hello_PIDE.java
     1.7 +/* cp from
     1.8 + *  https://hg.risc.uni-linz.ac.at/wneuper/isac/file/84f1ca6a6dd9/isac-java/src/java/isac/bridge/BridgeMain.java#l85
     1.9 +    85         log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
    1.10 +    86         Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
    1.11 +    87           new Version("2015"), Setup.defaultPackageName());
    1.12 +    88         Environment env = JSetup.makeEnvironment(setup); // ohne Duration
    1.13 +    89         Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.14 +    90         JSystem sys = JSystem.create(env, config);
    1.15 +    92         
    1.16 +    93         connection_to_kernel_ = sys;
    1.17 +    94         log(1, "<--ISA: connection established");
    1.18 + */
    1.19 +/*         
    1.20 +package info.hupel.isabelle.examples.java;
    1.21 +
    1.22 +import java.nio.file.Path;
    1.23 +import java.nio.file.Paths;
    1.24 +import java.util.Arrays;
    1.25 +import info.hupel.isabelle.api.*;
    1.26 +import info.hupel.isabelle.japi.*;
    1.27 +import info.hupel.isabelle.setup.*;
    1.28 +
    1.29 +public class Hello_PIDE {
    1.30 +
    1.31 +  public static void main(String args[]) {
    1.32 +    JResources res = JResources.dumpIsabelleResources();
    1.33 +    Configuration config = Configuration.simple("Protocol");
    1.34 +    Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2017")), res);
    1.35 +    JSystem sys = JSystem.create(env, config);
    1.36 +    String response = sys.invoke(Operations.HELLO, "world");
    1.37 +    System.out.println(response);
    1.38 +    sys.dispose();
    1.39 +  }
    1.40 +}
    1.41 + */
    1.42          JResources res = JResources.dumpIsabelleResources();
    1.43 +        Path path = java.nio.file.Paths.get
    1.44 +          ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
    1.45          Configuration config = Configuration.simple("Protocol");
    1.46 -//        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    1.47          Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    1.48          JSystem sys = JSystem.create(env, config);
    1.49 -        
    1.50 +
    1.51          /*PIDE*/connection_to_kernel_ = sys;
    1.52          /*PIDE*/log(1, "<--ISA: connection established");
    1.53