mirror of
https://github.com/open-goal/opengoal-vscode.git
synced 2024-10-19 20:47:37 -04:00
parent
6f045ccc3f
commit
b3ce6e7ef4
|
@ -191,6 +191,11 @@
|
|||
"id": "opengoal-repl",
|
||||
"title": "REPL",
|
||||
"properties": {
|
||||
"opengoal.replPort": {
|
||||
"type": "number",
|
||||
"default": 8181,
|
||||
"description": "Port for the nREPL server"
|
||||
},
|
||||
"opengoal.replAutoJackIn": {
|
||||
"type": "boolean",
|
||||
"default": false,
|
||||
|
|
|
@ -5,6 +5,7 @@ export function getConfig() {
|
|||
|
||||
return {
|
||||
opengoalParinferMode: configOptions.get<string>("parinferMode"),
|
||||
replPort: configOptions.get<number>("replPort"),
|
||||
autoReplJackIn: configOptions.get<boolean>("replAutoJackIn"),
|
||||
reloadFileOnSave: configOptions.get<boolean>("reloadFileOnSave"),
|
||||
launchLspOnStartup: configOptions.get<boolean>("launchLspOnStartup"),
|
||||
|
|
|
@ -37,8 +37,11 @@ export async function jackIn() {
|
|||
socket = new PromiseSocket();
|
||||
socket.setEncoding("utf8");
|
||||
socket.socket.setTimeout(100);
|
||||
await socket.connect(8181, "127.0.0.1");
|
||||
jackedIn = true;
|
||||
const port = getConfig().replPort;
|
||||
if (port !== undefined) {
|
||||
await socket.connect(port, "127.0.0.1");
|
||||
jackedIn = true;
|
||||
}
|
||||
} catch (e) {
|
||||
console.error(e);
|
||||
socket = undefined;
|
||||
|
|
Loading…
Reference in a new issue