isac-java/src/java/isac/bridge/BridgeMain.java
author Walther Neuper <walther.neuper@jku.at>
Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239 b4e3883d7b66
parent 5237 ee17f1b81a7f
permissions -rw-r--r--
reset mathematics-engine to Isabelle2015

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