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
     1 /**
     2  * Created on Aug 13, 2003
     3  *
     4  * @author Richard Gradischnegg RG
     5  */
     6 package isac.bridge;
     7 
     8 /**
     9  * BridgeMain: main class for bridge, does initialization and provides logging delegate and utility functionality.
    10  *
    11  * @author Richard Gradischnegg RG
    12  * @version 1.1
    13  */
    14 import isac.util.BridgeMainPaths;
    15 import isac.util.FixedPortRMISocketFactory;
    16 import info.hupel.isabelle.api.*;
    17 import info.hupel.isabelle.japi.*;
    18 import info.hupel.isabelle.setup.*;
    19 
    20 import java.awt.BorderLayout;
    21 import java.awt.Color;
    22 import java.awt.Font;
    23 import java.awt.event.WindowAdapter;
    24 import java.awt.event.WindowEvent;
    25 import java.awt.event.WindowListener;
    26 import java.io.BufferedReader;
    27 import java.io.IOException;
    28 import java.io.Serializable;
    29 import java.nio.file.Path;
    30 import java.nio.file.Paths;
    31 import java.rmi.RemoteException;
    32 import java.rmi.server.RMISocketFactory;
    33 import java.util.Arrays;
    34 
    35 import javax.swing.JFrame;
    36 import javax.swing.JPanel;
    37 import javax.swing.JScrollPane;
    38 import javax.swing.JTextArea;
    39 
    40 import org.apache.log4j.Logger;
    41 
    42 /**
    43  * Bridge main class: initializes connection to SML, starts auxillary threads, handles logging mechanism
    44  *
    45  * @author rgradisc
    46  */
    47 class BridgeMain implements Serializable {
    48 
    49     private static final long serialVersionUID = 507L;
    50     private static final Logger logger = Logger.getLogger(BridgeMain.class.getName());
    51     private JFrame log_frame_;
    52     private String path_;
    53     JPanel panel_;
    54     JTextArea text_area_;
    55     JScrollPane scroll_pane_;
    56     private Thread thread_sml_;
    57     private BridgeLogger bridge_logger_;
    58     private BufferedReader sml_reader_;
    59 
    60     public int ignore_output_ = 0;
    61     private boolean restoring_; // true = bridge is in restoring_ phase
    62     private JSystem connection_to_kernel_;
    63 
    64     /**
    65      * Constructor used to set up the bridge main program
    66      *
    67      * @param log_path_: path_ to initialization file
    68      */
    69     BridgeMain(String log_path, String isabelle_home) {
    70         // hack for suppressing warning messages
    71         // (no longer nescessary with j2sdk1.4.2)
    72         // System.setProperty("java.util.prefs.syncInterval", "20000000000");
    73 
    74         if (logger.isDebugEnabled()) {
    75             logger.debug("BridgeMain log_path =" + log_path);
    76         }
    77         Integer.valueOf(BridgeMainPaths.BRIDGE_MAIN_PORT);
    78 
    79         bridge_logger_ = new BridgeLogger(log_path);
    80         new ClientList();
    81         setUpBridgeLog();
    82         //*TTY*/startThreadsFirstTime();
    83         /*PIDE*/log(1, "-->ISA: try connection with ISABELLE_HOME=\"" + isabelle_home + "\"...");
    84         //see libisabelle/modules/examples/src/main/java/edu/tum/cs/isabelle/examples/Hello_PIDE.java
    85         JResources res = JResources.dumpIsabelleResources();
    86         Configuration config = Configuration.simple("Protocol");
    87 //        Configuration config = Configuration.fromBuiltin("libisabelle_Isac");
    88         Environment env = JSetup.makeEnvironment(JSetup.defaultSetup(new Version.Stable("2018")), res);
    89         JSystem sys = JSystem.create(env, config);
    90         
    91         /*PIDE*/connection_to_kernel_ = sys;
    92         /*PIDE*/log(1, "<--ISA: connection established");
    93 
    94     }
    95 
    96     protected JSystem getConnectionToKernel(){
    97       return connection_to_kernel_;
    98     }
    99     private void setUpBridgeLog() {
   100         if (BridgeMainPaths.SHOW_GUI_LOGGER) {
   101             log_frame_ = new JFrame("Java<->SML");
   102             log_frame_.setLocation(700, 250);
   103             panel_ = new JPanel();
   104             panel_.setSize(200, 300);
   105             panel_.setLayout(new BorderLayout());
   106             panel_.setBackground(Color.white);
   107 
   108             text_area_ = new JTextArea();
   109             text_area_.setFont(new Font("Monospaced", 0, 11));
   110             scroll_pane_ = new JScrollPane(text_area_,
   111                     JScrollPane.VERTICAL_SCROLLBAR_ALWAYS,
   112                     JScrollPane.HORIZONTAL_SCROLLBAR_ALWAYS);
   113             panel_.add("Center", scroll_pane_);
   114             log_frame_.getContentPane().add(panel_);
   115 
   116             log_frame_.setTitle("BridgeLog Java <=> SML");
   117             WindowListener l = new WindowAdapter() {
   118                 public void windowClosing(WindowEvent e) {
   119                     System.exit(0);
   120                 }
   121             };
   122             log_frame_.addWindowListener(l);
   123             log_frame_.pack();
   124             log_frame_.setSize(300, 500);
   125             log_frame_.setVisible(true);
   126         }
   127     }
   128 
   129     // Here goes the future load balancing functionality
   130     // public void startNewKernel() {
   131     // implement load balancing
   132     // }
   133     protected void finalize() throws Throwable {
   134         super.finalize(); // gosling p.47
   135         // Objects created in run method are finalized when
   136         // program terminates and thread exits
   137         while (thread_sml_.isAlive()) {
   138             thread_sml_.interrupt();
   139             log(1, "waiting for SML thread to quit..");
   140         }
   141         bridge_logger_.log(1, "finished");
   142         bridge_logger_.close();
   143     }
   144 
   145     /**
   146      * Log a message with a specified severity level
   147      *
   148      * @param level severity level
   149      * @param msg the message to be logged
   150      */
   151     public void log(int level, String msg) {
   152         if (BridgeMainPaths.LOG_TO_FILE) {
   153             this.bridge_logger_.log(level, msg);
   154         }
   155         if (BridgeMainPaths.SHOW_GUI_LOGGER) {
   156             this.text_area_.append(msg + "\n");
   157         }
   158     }
   159 
   160     public BufferedReader getSmlReader() {
   161         //if (logger.isDebugEnabled())
   162         //    logger.debug("getSmlReader x");
   163         return sml_reader_;
   164     }
   165 
   166     public String getPath() {
   167         return path_;
   168     }
   169 
   170     public void setRMI(BridgeRMI bridgeRMI) {
   171         if (logger.isDebugEnabled()) {
   172             logger.debug("setRMI: bridge_rmi_=" + bridgeRMI);
   173         }
   174         bridgeRMI.setRmiID(1); // only one BridgeRMI used so far
   175     }
   176 
   177     boolean isRestoring() {
   178         return restoring_;
   179     }
   180 
   181     /**
   182      * @param args commandline arguments (exactly 4 expected: _iniPath _host _port _dtdPath)
   183      * @see BridgeMain()
   184      */
   185     public static void main(String[] args) {
   186 
   187         System.out.println("Starting Bridge...");
   188 
   189         String ini_load_result = BridgeMainPaths.loadFromFile(args[0]);
   190 
   191         if (ini_load_result != null) {
   192             ini_load_result += BridgeMainPaths.loadFromResource(args[0]);
   193         }
   194 
   195         if (ini_load_result != null) {
   196             System.err.println(ini_load_result);
   197             System.exit(1);
   198         }
   199 
   200         // initialize bridge main part
   201         BridgeMain bridge = new BridgeMain(BridgeMainPaths.LOG_PATH, BridgeMainPaths.ISABELLE_HOME);
   202         try {
   203             // Use ObjectManagerRMISocketFactory
   204             // 6666 = dummy
   205             RMISocketFactory.setSocketFactory(new FixedPortRMISocketFactory(BridgeMainPaths.BRIDGE_RMI_PORT));
   206 
   207             // setup rmi connection to to the clients
   208             BridgeRMI rmi = new BridgeRMI(bridge, BridgeMainPaths.HOST,
   209                     BridgeMainPaths.BRIDGE_MAIN_PORT, BridgeMainPaths.DTD_PATH);
   210 
   211 //			System.out.println( rmi );
   212 
   213             bridge.setRMI(rmi);
   214         } catch (RemoteException e) {
   215             System.out.println("Could not instantiate RMI: exiting");
   216             e.printStackTrace();
   217         } catch (IOException e) {
   218             System.out.println("Exception: " + e.getMessage());
   219             e.printStackTrace();
   220         }
   221     }
   222 }