Skip to content

Commit

Permalink
refactor: rewrite logger to be compatible with browser (#494)
Browse files Browse the repository at this point in the history
The `Console` class does not seem to exist for the browser. This
implementation of the `logger` behaves exactly like before for all
`logger.log` and `logger.error` calls (which are the only ones used in
the project).
  • Loading branch information
abentkamp authored Dec 10, 2024
1 parent 45c3616 commit 2a1241f
Showing 1 changed file with 4 additions and 10 deletions.
14 changes: 4 additions & 10 deletions vscode-lean4/src/utils/logger.ts
Original file line number Diff line number Diff line change
@@ -1,10 +1,4 @@
import { Console } from 'console'

class Logger extends Console {
constructor(stdout: NodeJS.WritableStream, stderr?: NodeJS.WritableStream) {
super(stdout, stderr)
}

class Logger {
private static now(): string {
const now = new Date()
return (
Expand All @@ -19,13 +13,13 @@ class Logger extends Console {
}

log(msg: string) {
super.log(Logger.now(), '-', msg)
console.log(Logger.now(), '-', msg)
}

error(msg: string) {
super.error(Logger.now(), '-', msg)
console.error(Logger.now(), '-', msg)
}
}

const logger = new Logger(process.stdout, process.stderr)
const logger = new Logger()
export { logger }

0 comments on commit 2a1241f

Please sign in to comment.