isac-java/src/java/isac/bridge/BridgeMain.java
author Walther Neuper <wneuper@ist.tugraz.at>
Thu, 13 Sep 2018 11:14:30 +0200
changeset 5231 ed1bee7c6784
parent 5229 6bf0e95981e3
child 5233 f9e91d4ee161
permissions -rw-r--r--
------ connection to new math-engine on Isabelle2018: question 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@4858
    83
        /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
wneuper@5231
    84
        //see libisabelle/modules/examples/src/main/java/edu/tum/cs/isabelle/examples/Hello_PIDE.java
wneuper@5229
    85
        JResources res = JResources.dumpIsabelleResources();
wneuper@5231
    86
        Configuration config = Configuration.simple("Protocol");
wneuper@5231
    87
//        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
wneuper@5229
    88
        Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
wneuper@4862
    89
        JSystem sys = JSystem.create(env, config);
wneuper@4848
    90
        
wneuper@4848
    91
        /*PIDE*/connection_to_kernel_ = sys;
wneuper@4828
    92
        /*PIDE*/log(1, "<--ISA: connection established");
wneuper@4721
    93
tzilling@4472
    94
    }
rgradisc@859
    95
wneuper@4750
    96
    protected JSystem getConnectionToKernel(){
wneuper@4750
    97
      return connection_to_kernel_;
wneuper@4750
    98
    }
tzilling@4472
    99
    private void setUpBridgeLog() {
tzilling@4472
   100
        if (BridgeMainPaths.SHOW_GUI_LOGGER) {
tzilling@4472
   101
            log_frame_ = new JFrame("Java<->SML");
tzilling@4472
   102
            log_frame_.setLocation(700, 250);
tzilling@4472
   103
            panel_ = new JPanel();
tzilling@4472
   104
            panel_.setSize(200, 300);
tzilling@4472
   105
            panel_.setLayout(new BorderLayout());
tzilling@4472
   106
            panel_.setBackground(Color.white);
rgradisc@1065
   107
tzilling@4472
   108
            text_area_ = new JTextArea();
tzilling@4472
   109
            text_area_.setFont(new Font("Monospaced", 0, 11));
tzilling@4472
   110
            scroll_pane_ = new JScrollPane(text_area_,
tzilling@4472
   111
                    JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
tzilling@4472
   112
                    JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
tzilling@4472
   113
            panel_.add("Center", scroll_pane_);
tzilling@4472
   114
            log_frame_.getContentPane().add(panel_);
rgradisc@859
   115
tzilling@4472
   116
            log_frame_.setTitle("BridgeLog Java <=> SML");
tzilling@4472
   117
            WindowListener l = new WindowAdapter() {
tzilling@4472
   118
                public void windowClosing(WindowEvent e) {
tzilling@4472
   119
                    System.exit(0);
tzilling@4472
   120
                }
tzilling@4472
   121
            };
tzilling@4472
   122
            log_frame_.addWindowListener(l);
tzilling@4472
   123
            log_frame_.pack();
tzilling@4472
   124
            log_frame_.setSize(300, 500);
tzilling@4472
   125
            log_frame_.setVisible(true);
tzilling@4472
   126
        }
tzilling@4472
   127
    }
rgradisc@859
   128
tzilling@4472
   129
    // Here goes the future load balancing functionality
tzilling@4472
   130
    // public void startNewKernel() {
tzilling@4472
   131
    // implement load balancing
tzilling@4472
   132
    // }
tzilling@4472
   133
    protected void finalize() throws Throwable {
tzilling@4472
   134
        super.finalize(); // gosling p.47
tzilling@4472
   135
        // Objects created in run method are finalized when
tzilling@4472
   136
        // program terminates and thread exits
tzilling@4472
   137
        while (thread_sml_.isAlive()) {
tzilling@4472
   138
            thread_sml_.interrupt();
tzilling@4472
   139
            log(1, "waiting for SML thread to quit..");
tzilling@4472
   140
        }
tzilling@4472
   141
        bridge_logger_.log(1, "finished");
tzilling@4472
   142
        bridge_logger_.close();
tzilling@4472
   143
    }
mlang@2448
   144
tzilling@4472
   145
    /**
tzilling@4472
   146
     * Log a message with a specified severity level
tzilling@4472
   147
     *
tzilling@4472
   148
     * @param level severity level
tzilling@4472
   149
     * @param msg the message to be logged
tzilling@4472
   150
     */
tzilling@4472
   151
    public void log(int level, String msg) {
tzilling@4472
   152
        if (BridgeMainPaths.LOG_TO_FILE) {
tzilling@4472
   153
            this.bridge_logger_.log(level, msg);
tzilling@4472
   154
        }
tzilling@4472
   155
        if (BridgeMainPaths.SHOW_GUI_LOGGER) {
tzilling@4472
   156
            this.text_area_.append(msg + "\n");
tzilling@4472
   157
        }
tzilling@4472
   158
    }
mlang@2448
   159
wneuper@4700
   160
    public BufferedReader getSmlReader() {
wneuper@3881
   161
        //if (logger.isDebugEnabled())
wneuper@3881
   162
        //    logger.debug("getSmlReader x");
tzilling@4472
   163
        return sml_reader_;
tzilling@4472
   164
    }
rgradisc@1035
   165
tzilling@4472
   166
    public String getPath() {
tzilling@4472
   167
        return path_;
tzilling@4472
   168
    }
wneuper@1860
   169
tzilling@4472
   170
    public void setRMI(BridgeRMI bridgeRMI) {
tzilling@4472
   171
        if (logger.isDebugEnabled()) {
wneuper@3881
   172
            logger.debug("setRMI: bridge_rmi_=" + bridgeRMI);
tzilling@4472
   173
        }
tzilling@4472
   174
        bridgeRMI.setRmiID(1); // only one BridgeRMI used so far
tzilling@4472
   175
    }
mlang@2448
   176
tzilling@4472
   177
    boolean isRestoring() {
tzilling@4472
   178
        return restoring_;
tzilling@4472
   179
    }
mlang@2448
   180
tzilling@4472
   181
    /**
tzilling@4472
   182
     * @param args commandline arguments (exactly 4 expected: _iniPath _host _port _dtdPath)
tzilling@4472
   183
     * @see BridgeMain()
tzilling@4472
   184
     */
tzilling@4472
   185
    public static void main(String[] args) {
rkoenig@3779
   186
tzilling@4472
   187
        System.out.println("Starting Bridge...");
rkoenig@3779
   188
tzilling@4472
   189
        String ini_load_result = BridgeMainPaths.loadFromFile(args[0]);
rkoenig@3779
   190
tzilling@4472
   191
        if (ini_load_result != null) {
tzilling@4472
   192
            ini_load_result += BridgeMainPaths.loadFromResource(args[0]);
tzilling@4472
   193
        }
mlang@2448
   194
tzilling@4472
   195
        if (ini_load_result != null) {
tzilling@4472
   196
            System.err.println(ini_load_result);
tzilling@4472
   197
            System.exit(1);
tzilling@4472
   198
        }
rkoenig@3779
   199
tzilling@4472
   200
        // initialize bridge main part
wneuper@4858
   201
        BridgeMain bridge = new BridgeMain(BridgeMainPaths.LOG_PATH, BridgeMainPaths.ISABELLE_HOME);
tzilling@4472
   202
        try {
rkoenig@3827
   203
            // Use ObjectManagerRMISocketFactory
tzilling@4472
   204
            // 6666 = dummy
tzilling@4472
   205
            RMISocketFactory.setSocketFactory(new FixedPortRMISocketFactory(BridgeMainPaths.BRIDGE_RMI_PORT));
nsimic@3783
   206
tzilling@4472
   207
            // setup rmi connection to to the clients
tzilling@4472
   208
            BridgeRMI rmi = new BridgeRMI(bridge, BridgeMainPaths.HOST,
tzilling@4472
   209
                    BridgeMainPaths.BRIDGE_MAIN_PORT, BridgeMainPaths.DTD_PATH);
tzilling@4472
   210
kober@4157
   211
//			System.out.println( rmi );
tzilling@4472
   212
tzilling@4472
   213
            bridge.setRMI(rmi);
tzilling@4472
   214
        } catch (RemoteException e) {
tzilling@4472
   215
            System.out.println("Could not instantiate RMI: exiting");
tzilling@4472
   216
            e.printStackTrace();
tzilling@4472
   217
        } catch (IOException e) {
tzilling@4472
   218
            System.out.println("Exception: " + e.getMessage());
tzilling@4472
   219
            e.printStackTrace();
nsimic@3783
   220
        }
tzilling@4472
   221
    }
mlang@2448
   222
}