isac-java/src/java/isac/bridge/BridgeMain.java
author Walther Neuper <wneuper@ist.tugraz.at>
Wed, 19 Dec 2018 12:51:51 +0100
changeset 5236 bdd3733fa7db
parent 5235 3ca9690d3e8b
child 5237 ee17f1b81a7f
permissions -rw-r--r--
------ connection to new math-engine on Isabelle2018: question 4 to Lars
wneuper@2707
     1
/**
rgradisc@859
     2
 * Created on Aug 13, 2003
tzilling@4472
     3
 *
wneuper@2707
     4
 * @author Richard Gradischnegg RG
rgradisc@859
     5
 */
rgradisc@859
     6
package isac.bridge;
rgradisc@859
     7
rgradisc@859
     8
/**
tzilling@4472
     9
 * BridgeMain: main class for bridge, does initialization and provides logging delegate and utility functionality.
tzilling@4472
    10
 *
wneuper@2707
    11
 * @author Richard Gradischnegg RG
rgradisc@1072
    12
 * @version 1.1
rgradisc@859
    13
 */
nsimic@3730
    14
import isac.util.BridgeMainPaths;
rkoenig@3838
    15
import isac.util.FixedPortRMISocketFactory;
wneuper@5229
    16
import info.hupel.isabelle.api.*;
wneuper@5229
    17
import info.hupel.isabelle.japi.*;
wneuper@5229
    18
import info.hupel.isabelle.setup.*;
wneuper@4721
    19
rgradisc@859
    20
import java.awt.BorderLayout;
rgradisc@859
    21
import java.awt.Color;
rgradisc@1066
    22
import java.awt.Font;
rgradisc@859
    23
import java.awt.event.WindowAdapter;
rgradisc@859
    24
import java.awt.event.WindowEvent;
rgradisc@859
    25
import java.awt.event.WindowListener;
rgradisc@859
    26
import java.io.BufferedReader;
rgradisc@859
    27
import java.io.IOException;
nsimic@3780
    28
import java.io.Serializable;
wneuper@5229
    29
import java.nio.file.Path;
wneuper@4848
    30
import java.nio.file.Paths;
rgradisc@1065
    31
import java.rmi.RemoteException;
nsimic@3783
    32
import java.rmi.server.RMISocketFactory;
wneuper@5229
    33
import java.util.Arrays;
rgradisc@859
    34
rgradisc@859
    35
import javax.swing.JFrame;
rgradisc@859
    36
import javax.swing.JPanel;
rgradisc@859
    37
import javax.swing.JScrollPane;
rgradisc@859
    38
import javax.swing.JTextArea;
rgradisc@859
    39
wneuper@1860
    40
import org.apache.log4j.Logger;
wneuper@1860
    41
rgradisc@1065
    42
/**
tzilling@4472
    43
 * Bridge main class: initializes connection to SML, starts auxillary threads, handles logging mechanism
tzilling@4472
    44
 *
rgradisc@1065
    45
 * @author rgradisc
rgradisc@1065
    46
 */
nsimic@3780
    47
class BridgeMain implements Serializable {
rgradisc@859
    48
tzilling@4472
    49
    private static final long serialVersionUID = 507L;
tzilling@4472
    50
    private static final Logger logger = Logger.getLogger(BridgeMain.class.getName());
tzilling@4472
    51
    private JFrame log_frame_;
tzilling@4472
    52
    private String path_;
tzilling@4472
    53
    JPanel panel_;
tzilling@4472
    54
    JTextArea text_area_;
tzilling@4472
    55
    JScrollPane scroll_pane_;
tzilling@4472
    56
    private Thread thread_sml_;
tzilling@4472
    57
    private BridgeLogger bridge_logger_;
wneuper@4700
    58
    private BufferedReader sml_reader_;
a@4971
    59
tzilling@4472
    60
    public int ignore_output_ = 0;
tzilling@4472
    61
    private boolean restoring_; // true = bridge is in restoring_ phase
wneuper@4721
    62
    private JSystem connection_to_kernel_;
tzilling@3950
    63
tzilling@4472
    64
    /**
tzilling@4472
    65
     * Constructor used to set up the bridge main program
tzilling@4472
    66
     *
wneuper@4858
    67
     * @param log_path_: path_ to initialization file
tzilling@4472
    68
     */
wneuper@4858
    69
    BridgeMain(String log_path, String isabelle_home) {
tzilling@4472
    70
        // hack for suppressing warning messages
tzilling@4472
    71
        // (no longer nescessary with j2sdk1.4.2)
tzilling@4472
    72
        // System.setProperty("java.util.prefs.syncInterval", "20000000000");
rgradisc@859
    73
tzilling@4472
    74
        if (logger.isDebugEnabled()) {
wneuper@4858
    75
            logger.debug("BridgeMain log_path =" + log_path);
tzilling@4472
    76
        }
a@4974
    77
        Integer.valueOf(BridgeMainPaths.BRIDGE_MAIN_PORT);
wneuper@4863
    78
wneuper@4858
    79
        bridge_logger_ = new BridgeLogger(log_path);
a@4974
    80
        new ClientList();
tzilling@4472
    81
        setUpBridgeLog();
wneuper@4828
    82
        //*TTY*/startThreadsFirstTime();
wneuper@5234
    83
/* cp from last working version:
wneuper@5233
    84
 *  https://hg.risc.uni-linz.ac.at/wneuper/isac/file/84f1ca6a6dd9/isac-java/src/java/isac/bridge/BridgeMain.java#l85
wneuper@5233
    85
    85         log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
wneuper@5233
    86
    86         Setup setup = new Setup(Paths.get(isabelle_home), JPlatform.guess(),
wneuper@5233
    87
    87           new Version("2015"), Setup.defaultPackageName());
wneuper@5234
    88
    88         Environment env = JSetup.makeEnvironment(setup); // without Duration
wneuper@5233
    89
    89         Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
wneuper@5233
    90
    90         JSystem sys = JSystem.create(env, config);
wneuper@5233
    91
    92         
wneuper@5233
    92
    93         connection_to_kernel_ = sys;
wneuper@5233
    93
    94         log(1, "<--ISA: connection established");
wneuper@5233
    94
 */
wneuper@5234
    95
/* cp from downloaded libisabelle, current version:
wneuper@5233
    96
package info.hupel.isabelle.examples.java;
wneuper@5233
    97
wneuper@5233
    98
import java.nio.file.Path;
wneuper@5233
    99
import java.nio.file.Paths;
wneuper@5233
   100
import java.util.Arrays;
wneuper@5233
   101
import info.hupel.isabelle.api.*;
wneuper@5233
   102
import info.hupel.isabelle.japi.*;
wneuper@5233
   103
import info.hupel.isabelle.setup.*;
wneuper@5233
   104
wneuper@5233
   105
public class Hello_PIDE {
wneuper@5233
   106
wneuper@5233
   107
  public static void main(String args[]) {
wneuper@5233
   108
    JResources res = JResources.dumpIsabelleResources();
wneuper@5233
   109
    Configuration config = Configuration.simple("Protocol");
wneuper@5233
   110
    Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2017")), res);
wneuper@5233
   111
    JSystem sys = JSystem.create(env, config);
wneuper@5233
   112
    String response = sys.invoke(Operations.HELLO, "world");
wneuper@5233
   113
    System.out.println(response);
wneuper@5233
   114
    sys.dispose();
wneuper@5233
   115
  }
wneuper@5233
   116
}
wneuper@5233
   117
 */
wneuper@5234
   118
        /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
wneuper@5234
   119
wneuper@5236
   120
        //these two values shall come from BridgeMail.properties
wneuper@5236
   121
        Path path = java.nio.file.Paths.get   //
wneuper@5236
   122
          ("/home/wneuper/.isabelle/isabisac/heaps/polyml-5.7.1_x86-linux/libisabelle_Isac");
wneuper@5236
   123
        String vers = "2018";
wneuper@5236
   124
        
wneuper@5236
   125
        JResources res = JResources.dumpIsabelleResources();
wneuper@5236
   126
        Setup setup = new Setup(path, JPlatform.guess(), new Version.Stable("2018"));
wneuper@5236
   127
        Environment env = JSetup.makeEnvironment(setup, res);
wneuper@5236
   128
        //Configuration config = Configuration.fromBuiltin("libisabelle_Isac"); //fromBuiltin is undefined
wneuper@5236
   129
        JSystem sys = JSystem.create(env, config);
wneuper@5233
   130
wneuper@4848
   131
        /*PIDE*/connection_to_kernel_ = sys;
wneuper@4828
   132
        /*PIDE*/log(1, "<--ISA: connection established");
wneuper@4721
   133
tzilling@4472
   134
    }
rgradisc@859
   135
wneuper@4750
   136
    protected JSystem getConnectionToKernel(){
wneuper@4750
   137
      return connection_to_kernel_;
wneuper@4750
   138
    }
tzilling@4472
   139
    private void setUpBridgeLog() {
tzilling@4472
   140
        if (BridgeMainPaths.SHOW_GUI_LOGGER) {
tzilling@4472
   141
            log_frame_ = new JFrame("Java<->SML");
tzilling@4472
   142
            log_frame_.setLocation(700, 250);
tzilling@4472
   143
            panel_ = new JPanel();
tzilling@4472
   144
            panel_.setSize(200, 300);
tzilling@4472
   145
            panel_.setLayout(new BorderLayout());
tzilling@4472
   146
            panel_.setBackground(Color.white);
rgradisc@1065
   147
tzilling@4472
   148
            text_area_ = new JTextArea();
tzilling@4472
   149
            text_area_.setFont(new Font("Monospaced", 0, 11));
tzilling@4472
   150
            scroll_pane_ = new JScrollPane(text_area_,
tzilling@4472
   151
                    JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
tzilling@4472
   152
                    JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
tzilling@4472
   153
            panel_.add("Center", scroll_pane_);
tzilling@4472
   154
            log_frame_.getContentPane().add(panel_);
rgradisc@859
   155
tzilling@4472
   156
            log_frame_.setTitle("BridgeLog Java <=> SML");
tzilling@4472
   157
            WindowListener l = new WindowAdapter() {
tzilling@4472
   158
                public void windowClosing(WindowEvent e) {
tzilling@4472
   159
                    System.exit(0);
tzilling@4472
   160
                }
tzilling@4472
   161
            };
tzilling@4472
   162
            log_frame_.addWindowListener(l);
tzilling@4472
   163
            log_frame_.pack();
tzilling@4472
   164
            log_frame_.setSize(300, 500);
tzilling@4472
   165
            log_frame_.setVisible(true);
tzilling@4472
   166
        }
tzilling@4472
   167
    }
rgradisc@859
   168
tzilling@4472
   169
    // Here goes the future load balancing functionality
tzilling@4472
   170
    // public void startNewKernel() {
tzilling@4472
   171
    // implement load balancing
tzilling@4472
   172
    // }
tzilling@4472
   173
    protected void finalize() throws Throwable {
tzilling@4472
   174
        super.finalize(); // gosling p.47
tzilling@4472
   175
        // Objects created in run method are finalized when
tzilling@4472
   176
        // program terminates and thread exits
tzilling@4472
   177
        while (thread_sml_.isAlive()) {
tzilling@4472
   178
            thread_sml_.interrupt();
tzilling@4472
   179
            log(1, "waiting for SML thread to quit..");
tzilling@4472
   180
        }
tzilling@4472
   181
        bridge_logger_.log(1, "finished");
tzilling@4472
   182
        bridge_logger_.close();
tzilling@4472
   183
    }
mlang@2448
   184
tzilling@4472
   185
    /**
tzilling@4472
   186
     * Log a message with a specified severity level
tzilling@4472
   187
     *
tzilling@4472
   188
     * @param level severity level
tzilling@4472
   189
     * @param msg the message to be logged
tzilling@4472
   190
     */
tzilling@4472
   191
    public void log(int level, String msg) {
tzilling@4472
   192
        if (BridgeMainPaths.LOG_TO_FILE) {
tzilling@4472
   193
            this.bridge_logger_.log(level, msg);
tzilling@4472
   194
        }
tzilling@4472
   195
        if (BridgeMainPaths.SHOW_GUI_LOGGER) {
tzilling@4472
   196
            this.text_area_.append(msg + "\n");
tzilling@4472
   197
        }
tzilling@4472
   198
    }
mlang@2448
   199
wneuper@4700
   200
    public BufferedReader getSmlReader() {
wneuper@3881
   201
        //if (logger.isDebugEnabled())
wneuper@3881
   202
        //    logger.debug("getSmlReader x");
tzilling@4472
   203
        return sml_reader_;
tzilling@4472
   204
    }
rgradisc@1035
   205
tzilling@4472
   206
    public String getPath() {
tzilling@4472
   207
        return path_;
tzilling@4472
   208
    }
wneuper@1860
   209
tzilling@4472
   210
    public void setRMI(BridgeRMI bridgeRMI) {
tzilling@4472
   211
        if (logger.isDebugEnabled()) {
wneuper@3881
   212
            logger.debug("setRMI: bridge_rmi_=" + bridgeRMI);
tzilling@4472
   213
        }
tzilling@4472
   214
        bridgeRMI.setRmiID(1); // only one BridgeRMI used so far
tzilling@4472
   215
    }
mlang@2448
   216
tzilling@4472
   217
    boolean isRestoring() {
tzilling@4472
   218
        return restoring_;
tzilling@4472
   219
    }
mlang@2448
   220
tzilling@4472
   221
    /**
tzilling@4472
   222
     * @param args commandline arguments (exactly 4 expected: _iniPath _host _port _dtdPath)
tzilling@4472
   223
     * @see BridgeMain()
tzilling@4472
   224
     */
tzilling@4472
   225
    public static void main(String[] args) {
rkoenig@3779
   226
tzilling@4472
   227
        System.out.println("Starting Bridge...");
rkoenig@3779
   228
tzilling@4472
   229
        String ini_load_result = BridgeMainPaths.loadFromFile(args[0]);
rkoenig@3779
   230
tzilling@4472
   231
        if (ini_load_result != null) {
tzilling@4472
   232
            ini_load_result += BridgeMainPaths.loadFromResource(args[0]);
tzilling@4472
   233
        }
mlang@2448
   234
tzilling@4472
   235
        if (ini_load_result != null) {
tzilling@4472
   236
            System.err.println(ini_load_result);
tzilling@4472
   237
            System.exit(1);
tzilling@4472
   238
        }
rkoenig@3779
   239
tzilling@4472
   240
        // initialize bridge main part
wneuper@4858
   241
        BridgeMain bridge = new BridgeMain(BridgeMainPaths.LOG_PATH, BridgeMainPaths.ISABELLE_HOME);
tzilling@4472
   242
        try {
rkoenig@3827
   243
            // Use ObjectManagerRMISocketFactory
tzilling@4472
   244
            // 6666 = dummy
tzilling@4472
   245
            RMISocketFactory.setSocketFactory(new FixedPortRMISocketFactory(BridgeMainPaths.BRIDGE_RMI_PORT));
nsimic@3783
   246
tzilling@4472
   247
            // setup rmi connection to to the clients
tzilling@4472
   248
            BridgeRMI rmi = new BridgeRMI(bridge, BridgeMainPaths.HOST,
tzilling@4472
   249
                    BridgeMainPaths.BRIDGE_MAIN_PORT, BridgeMainPaths.DTD_PATH);
tzilling@4472
   250
kober@4157
   251
//			System.out.println( rmi );
tzilling@4472
   252
tzilling@4472
   253
            bridge.setRMI(rmi);
tzilling@4472
   254
        } catch (RemoteException e) {
tzilling@4472
   255
            System.out.println("Could not instantiate RMI: exiting");
tzilling@4472
   256
            e.printStackTrace();
tzilling@4472
   257
        } catch (IOException e) {
tzilling@4472
   258
            System.out.println("Exception: " + e.getMessage());
tzilling@4472
   259
            e.printStackTrace();
nsimic@3783
   260
        }
tzilling@4472
   261
    }
mlang@2448
   262
}