diff --git a/server/index.mjs b/server/index.mjs index 3b2c1eef..c7a4856d 100644 --- a/server/index.mjs +++ b/server/index.mjs @@ -21,6 +21,9 @@ function logStats() { const __filename = url.fileURLToPath(import.meta.url); const __dirname = url.fileURLToPath(new URL('.', import.meta.url)); +// The path to the projects folder relative to the server +let projectsBasePath = path.join(__dirname, '..', 'Projects') + const environment = process.env.NODE_ENV const isGithubAction = process.env.GITHUB_ACTIONS const isDevelopment = environment === 'development' @@ -34,19 +37,19 @@ const app = express() app.use('/api/examples/*', (req, res, next) => { const filename = req.params[0] req.url = filename - express.static(path.join(__dirname, '..', 'Projects'))(req, res, next) + express.static(projectsBasePath)(req, res, next) }) // `*` is the project like `mathlib-demo` app.use('/api/manifest/*', (req, res, next) => { const project = req.params[0] req.url = 'lake-manifest.json' - express.static(path.join(__dirname, '..', 'Projects', project))(req, res, next) + express.static(path.join(projectsBasePath, project))(req, res, next) }) // `*` is the project like `mathlib-demo` app.use('/api/toolchain/*', (req, res, next) => { const project = req.params[0] req.url = 'lean-toolchain' - express.static(path.join(__dirname, '..', 'Projects', project))(req, res, next) + express.static(path.join(projectsBasePath, project))(req, res, next) }) // Using the client files app.use(express.static(path.join(__dirname, '..', 'client', 'dist'))) @@ -74,9 +77,6 @@ if (crtFile && keyFile) { const wss = new WebSocketServer({ server }) -// The path to the projects folder relative to the server -let projectsBasePath = path.join(__dirname, '..', 'Projects') - function startServerProcess(project) { let projectPath = path.join(projectsBasePath, project) @@ -110,7 +110,7 @@ function startServerProcess(project) { return serverProcess } -/** Transform client URI to valid file on the server */ +/** Transform client URI to valid file on the server by mutating obj */ function urisToFilenames(prefix, obj) { for (let key in obj) { if (obj.hasOwnProperty(key)) { @@ -126,10 +126,9 @@ function urisToFilenames(prefix, obj) { } } } - return obj; } -/** Transform server file back into client URI */ +/** Transform server file back into client URI by mutating obj */ function FilenamesToUri(prefix, obj) { for (let key in obj) { if (obj.hasOwnProperty(key)) { @@ -141,7 +140,6 @@ function FilenamesToUri(prefix, obj) { } } } - return obj; } wss.addListener("connection", function(ws, req) { @@ -153,31 +151,23 @@ wss.addListener("connection", function(ws, req) { const ip = anonymize(req.headers['x-forwarded-for'] || req.socket.remoteAddress) const ps = startServerProcess(project) - const socket = { + const reader = new rpc.WebSocketMessageReader({ onMessage: (cb) => { ws.on("message", cb) }, onError: (cb) => { ws.on("error", cb) }, onClose: (cb) => { ws.on("close", cb) }, + }) + const writer = new rpc.WebSocketMessageWriter({ send: (data, cb) => { ws.send(data,cb) } - } - const reader = new rpc.WebSocketMessageReader(socket) - const writer = new rpc.WebSocketMessageWriter(socket) + }) const socketConnection = jsonrpcserver.createConnection(reader, writer, () => ws.close()) const serverConnection = jsonrpcserver.createProcessStreamConnection(ps) socketConnection.forward(serverConnection, message => { - const prefix = isDevelopment ? projectsBasePath : "" - - if (!message.method === 'textDocument/definition') { - urisToFilenames(prefix, message) - } - if (isDevelopment && !isGithubAction) { console.log(`CLIENT: ${JSON.stringify(message)}`) } return message; }) serverConnection.forward(socketConnection, message => { - const prefix = isDevelopment ? projectsBasePath : "" - FilenamesToUri(prefix, message) if (isDevelopment && !isGithubAction) { console.log(`SERVER: ${JSON.stringify(message)}`) }