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 |
} |