diff --git a/lib/js/src/Config.bs.js b/lib/js/src/Config.bs.js index 2c05fa06..1d46748b 100644 --- a/lib/js/src/Config.bs.js +++ b/lib/js/src/Config.bs.js @@ -219,6 +219,24 @@ var InputMethod = { getActivationKey: getActivationKey }; +function getFontSize(param) { + var config = Vscode.workspace.getConfiguration("agdaMode", undefined); + var m = config.get("buffer.fontSize"); + var size; + if (m !== undefined) { + size = Caml_option.valFromOption(m); + } else { + var n = Vscode.workspace.getConfiguration("editor", undefined).get("fontSize"); + size = n !== undefined ? Caml_option.valFromOption(n) : 14; + } + config.update("buffer.fontSize", size, 1, undefined); + return String(size); +} + +var $$Buffer = { + getFontSize: getFontSize +}; + var VSRange; exports.VSRange = VSRange; @@ -229,4 +247,5 @@ exports.getLibraryPath = getLibraryPath; exports.Highlighting = Highlighting; exports.getBackend = getBackend; exports.InputMethod = InputMethod; +exports.$$Buffer = $$Buffer; /* vscode Not a pure module */ diff --git a/lib/js/src/Main.bs.js b/lib/js/src/Main.bs.js index b7d53bc4..f60a35d2 100644 --- a/lib/js/src/Main.bs.js +++ b/lib/js/src/Main.bs.js @@ -63,13 +63,15 @@ var Inputs = { function initialize(channels, extensionPath, globalStoragePath, editor, fileName) { var panel = Singleton$AgdaModeVscode.Panel.make(extensionPath); - WebviewPanel$AgdaModeVscode.onceDestroyed(panel).finally(function () { - Registry$AgdaModeVscode.removeAndDestroyAll(); - }); - var state = State$AgdaModeVscode.make(channels, globalStoragePath, extensionPath, editor); - Chan$AgdaModeVscode.once(state.onRemoveFromRegistry).finally(function () { - Registry$AgdaModeVscode.remove(fileName); - }); + $$Promise.get(WebviewPanel$AgdaModeVscode.onceDestroyed(panel), (function (param) { + Registry$AgdaModeVscode.removeAndDestroyAll(undefined); + + })); + var state = State$AgdaModeVscode.make(debugChan, globalStoragePath, extensionPath, editor); + State__View$AgdaModeVscode.Panel.setFontSize(state, Config$AgdaModeVscode.$$Buffer.getFontSize(undefined)); + $$Promise.get(Chan$AgdaModeVscode.once(state.onRemoveFromRegistry), (function (param) { + return Registry$AgdaModeVscode.remove(fileName); + })); var subscribe = function (disposable) { state.subscriptions.push(disposable); }; @@ -178,89 +180,134 @@ function activateWithoutContext(subscriptions, extensionPath, globalStoragePath) commandHandled: channels_commandHandled, log: channels_log }; - subscribe(onOpenEditor(function (editor) { - var fileName = Parser$AgdaModeVscode.filepath(editor.document.fileName); - if (isAgda(fileName)) { - return Core__Option.forEach(Registry$AgdaModeVscode.get(fileName), (function (state) { - state.editor = editor; - state.document = editor.document; - State__Command$AgdaModeVscode.dispatchCommand(state, "Refresh"); - })); - } - - })); - subscribe(Vscode.workspace.onDidChangeTextDocument(function ($$event) { - var $$document = $$event.document; - var fileName = Parser$AgdaModeVscode.filepath($$document.fileName); - if (isAgda(fileName)) { - return Core__Option.forEach(Registry$AgdaModeVscode.get(fileName), (function (state) { - Highlighting$AgdaModeVscode.updateSemanticHighlighting(state.highlighting, $$event); - })); - } - - })); - subscribe(Vscode.workspace.onDidCloseTextDocument(function ($$document) { - var fileName = Parser$AgdaModeVscode.filepath($$document.fileName); - if (isAgda(fileName)) { - Registry$AgdaModeVscode.removeAndDestroy(fileName); - finalize(false); - return ; - } - - })); - subscribeMany(onTriggerCommand(async function (command, editor) { - var fileName = Parser$AgdaModeVscode.filepath(editor.document.fileName); - if (typeof command !== "object") { - switch (command) { - case "Quit" : - await Registry$AgdaModeVscode.removeAndDestroy(fileName); - finalize(false); - break; - case "Restart" : - await Registry$AgdaModeVscode.removeAndDestroy(fileName); - finalize(true); - break; - default: - - } - } - var exit = 0; - if (typeof command !== "object") { - switch (command) { - case "Load" : - case "Restart" : - exit = 1; - break; - default: - - } - } else if (command.TAG === "InputMethod") { - var tmp = command._0; - if (typeof tmp !== "object" && tmp === "Activate") { - exit = 1; - } - - } - if (exit === 1) { - var match = Registry$AgdaModeVscode.get(fileName); - if (match === undefined) { - var state = initialize(channels, extensionPath, globalStoragePath, editor, fileName); - Registry$AgdaModeVscode.add(fileName, state); - } - - } - var state$1 = Registry$AgdaModeVscode.get(fileName); - if (state$1 !== undefined) { - await State__Command$AgdaModeVscode.dispatchCommand(state$1, command); - return { - TAG: "Ok", - _0: state$1, - [Symbol.for("name")]: "Ok" - }; - } + + var x = onOpenEditor(function (editor) { + var fileName = Parser$AgdaModeVscode.filepath(editor.document.fileName); + if (isAgda(fileName)) { + return Belt_Option.forEach(Registry$AgdaModeVscode.get(fileName), (function (state) { + state.editor = editor; + state.document = editor.document; + State__Command$AgdaModeVscode.dispatchCommand(state, /* Refresh */3); + + })); + } + + }); + subscriptions.push(x); + var x$1 = Vscode.workspace.onDidChangeTextDocument(function ($$event) { + var $$document = $$event.document; + var fileName = Parser$AgdaModeVscode.filepath($$document.fileName); + if (isAgda(fileName)) { + return Belt_Option.forEach(Registry$AgdaModeVscode.get(fileName), (function (state) { + return Highlighting$AgdaModeVscode.updateSemanticHighlighting(state.highlighting, $$event); + })); + } + + }); + subscriptions.push(x$1); + var x$2 = Vscode.workspace.onDidChangeConfiguration(function ($$event) { + var state = Belt_Array.reduce(Vscode.window.visibleTextEditors, undefined, (function (state, editor) { + if (state !== undefined) { + return state; + } else { + return Registry$AgdaModeVscode.get(Parser$AgdaModeVscode.filepath(editor.document.fileName)); + } + })); + var fontSizeChanged = $$event.affectsConfiguration("agdaMode.buffer.fontSize", undefined); + if (!fontSizeChanged) { + return ; + } + var size = Config$AgdaModeVscode.$$Buffer.getFontSize(undefined); + if (state !== undefined) { + State__View$AgdaModeVscode.Panel.setFontSize(state, size); + return ; + } + + }); + subscriptions.push(x$2); + var x$3 = Vscode.workspace.onDidCloseTextDocument(function ($$document) { + var fileName = Parser$AgdaModeVscode.filepath($$document.fileName); + if (isAgda(fileName)) { + Registry$AgdaModeVscode.removeAndDestroy(fileName); + finalize(false); + return ; + } + + }); + subscriptions.push(x$3); + var xs = onTriggerCommand(function (command, editor) { + var fileName = Parser$AgdaModeVscode.filepath(editor.document.fileName); + var tmp; + if (typeof command === "number" && command < 3) { + switch (command) { + case /* Load */0 : + tmp = $$Promise.resolved(undefined); + break; + case /* Quit */1 : + tmp = $$Promise.flatMap(Registry$AgdaModeVscode.removeAndDestroy(fileName), (function (param) { + return finalize(false); + })); + break; + case /* Restart */2 : + tmp = $$Promise.flatMap(Registry$AgdaModeVscode.removeAndDestroy(fileName), (function (param) { + return finalize(true); + })); + break; - })); - subscribe(registerDocumentSemanticTokensProvider()); + } + } else { + tmp = $$Promise.resolved(undefined); + } + return $$Promise.flatMap($$Promise.tap(tmp, (function (param) { + if (typeof command === "number") { + switch (command) { + case /* Load */0 : + case /* Restart */2 : + break; + default: + return ; + } + } else { + if (command.TAG !== /* InputMethod */14) { + return ; + } + if (command._0 !== 0) { + return ; + } + + } + var match = Registry$AgdaModeVscode.get(fileName); + if (match !== undefined) { + return ; + } + var state = initialize(channels, extensionPath, globalStoragePath, editor, fileName); + return Registry$AgdaModeVscode.add(fileName, state); + })), (function (param) { + var state = Registry$AgdaModeVscode.get(fileName); + if (state !== undefined) { + return $$Promise.map(State__Command$AgdaModeVscode.dispatchCommand(state, command), (function (result) { + if (result.TAG === /* Ok */0) { + return { + TAG: 0, + _0: state, + [Symbol.for("name")]: "Ok" + }; + } else { + return { + TAG: 1, + _0: result._0, + [Symbol.for("name")]: "Error" + }; + } + })); + } else { + return $$Promise.resolved(undefined); + } + })); + }); + Caml_splice_call.spliceObjApply(subscriptions, "push", [xs]); + var x$4 = registerDocumentSemanticTokensProvider(undefined); + subscriptions.push(x$4); return channels; } diff --git a/lib/js/src/State/State__View.bs.js b/lib/js/src/State/State__View.bs.js index 28981938..52022b86 100644 --- a/lib/js/src/State/State__View.bs.js +++ b/lib/js/src/State/State__View.bs.js @@ -100,6 +100,14 @@ function updatePromptIM(state, content) { }); } +function setFontSize(state, fontSize) { + return sendEvent(state, { + TAG: 5, + _0: fontSize, + [Symbol.for("name")]: "ConfigurationChange" + }); +} + function prompt(state, header, prompt$1, callbackOnPromptSuccess) { State__Type$AgdaModeVscode.Context.setPrompt(true); var request = { @@ -144,7 +152,8 @@ var Panel = { updateIM: updateIM, updatePromptIM: updatePromptIM, prompt: prompt, - interruptPrompt: interruptPrompt + interruptPrompt: interruptPrompt, + setFontSize: setFontSize }; function make(state) { diff --git a/lib/js/src/View/Panel/Panel.bs.js b/lib/js/src/View/Panel/Panel.bs.js index 21dbe1d6..44f9c7e0 100644 --- a/lib/js/src/View/Panel/Panel.bs.js +++ b/lib/js/src/View/Panel/Panel.bs.js @@ -59,6 +59,7 @@ function Panel(props) { var match$4 = React.useReducer(Keyboard$AgdaModeVscode.reducer, undefined); var runInputMethodAction = match$4[1]; var inputMethodState = match$4[0]; + var setFontSize = (function (n) { document.documentElement.style.setProperty("--agdaMode-buffer-font-size", n + "px"); }); React.useEffect((function () { Chan$AgdaModeVscode.emit(onEventFromView, "Initialized"); }), []); @@ -166,18 +167,22 @@ function Panel(props) { }); case "PromptIMUpdate" : var text$1 = $$event._0; - return setPrompt(function (x) { - if (x !== undefined) { - return [ - x[0], - x[1], - text$1 - ]; - } - - }); - case "InputMethod" : - return runInputMethodAction($$event._0); + + return Curry._1(setPrompt, (function (x) { + if (x !== undefined) { + return [ + x[0], + x[1], + text$1 + ]; + } + + })); + case /* InputMethod */4 : + return Curry._1(runInputMethodAction, $$event._0); + case /* ConfigurationChange */5 : + onSubmit(undefined); + return setFontSize($$event._0); } })); diff --git a/lib/js/src/View/View.bs.js b/lib/js/src/View/View.bs.js index ae518a3e..d69462d0 100644 --- a/lib/js/src/View/View.bs.js +++ b/lib/js/src/View/View.bs.js @@ -282,6 +282,8 @@ function toString$1(x) { return "PromptIMUpdate " + x._0; case "InputMethod" : return "InputMethod"; + case /* ConfigurationChange */5 : + return "ConfigurationChange"; } } @@ -301,6 +303,20 @@ var decode$3 = Util$AgdaModeVscode.Decode.sum(function (x) { })), [Symbol.for("name")]: "Payload" }; + case "ConfigurationChange" : + return { + TAG: 0, + _0: (function (param) { + return Json_decode.map((function (size) { + return { + TAG: 5, + _0: size, + [Symbol.for("name")]: "ConfigurationChange" + }; + }), Json_decode.string, param); + }), + [Symbol.for("name")]: "Contents" + }; case "Display" : return { TAG: "Payload", @@ -365,59 +381,115 @@ var decode$3 = Util$AgdaModeVscode.Decode.sum(function (x) { } }); -var encode$3 = Util$AgdaModeVscode.Encode.sum(function (x) { - if (typeof x !== "object") { - return { - TAG: "TagOnly", - _0: "PromptInterrupt", - [Symbol.for("name")]: "TagOnly" - }; - } - switch (x.TAG) { - case "Display" : - return { - TAG: "Payload", - _0: "Display", - _1: Json_Encode$JsonCombinators.tuple2(encode, Json_Encode$JsonCombinators.array(Item$AgdaModeVscode.encode))([ - x._0, - x._1 - ]), - [Symbol.for("name")]: "Payload" - }; - case "Append" : - return { - TAG: "Payload", - _0: "Append", - _1: Json_Encode$JsonCombinators.tuple2(encode, Json_Encode$JsonCombinators.array(Item$AgdaModeVscode.encode))([ - x._0, - x._1 - ]), - [Symbol.for("name")]: "Payload" - }; - case "SetStatus" : - return { - TAG: "Payload", - _0: "SetStatus", - _1: x._0, - [Symbol.for("name")]: "Payload" - }; - case "PromptIMUpdate" : - return { - TAG: "Payload", - _0: "PromptIMUpdate", - _1: x._0, - [Symbol.for("name")]: "Payload" - }; - case "InputMethod" : - return { - TAG: "Payload", - _0: "InputMethod", - _1: encode$2(x._0), - [Symbol.for("name")]: "Payload" - }; - - } - }); + +function encode$3(x) { + if (typeof x === "number") { + return Json_encode.object_({ + hd: [ + "tag", + "PromptInterrupt" + ], + tl: /* [] */0 + }); + } + switch (x.TAG | 0) { + case /* Display */0 : + return Json_encode.object_({ + hd: [ + "tag", + "Display" + ], + tl: { + hd: [ + "contents", + Json_encode.pair(encode, (function (param) { + return Json_encode.array(Item$AgdaModeVscode.encode, param); + }), [ + x._0, + x._1 + ]) + ], + tl: /* [] */0 + } + }); + case /* Append */1 : + return Json_encode.object_({ + hd: [ + "tag", + "Append" + ], + tl: { + hd: [ + "contents", + Json_encode.pair(encode, (function (param) { + return Json_encode.array(Item$AgdaModeVscode.encode, param); + }), [ + x._0, + x._1 + ]) + ], + tl: /* [] */0 + } + }); + case /* SetStatus */2 : + return Json_encode.object_({ + hd: [ + "tag", + "SetStatus" + ], + tl: { + hd: [ + "contents", + x._0 + ], + tl: /* [] */0 + } + }); + case /* PromptIMUpdate */3 : + return Json_encode.object_({ + hd: [ + "tag", + "PromptIMUpdate" + ], + tl: { + hd: [ + "contents", + x._0 + ], + tl: /* [] */0 + } + }); + case /* InputMethod */4 : + return Json_encode.object_({ + hd: [ + "tag", + "InputMethod" + ], + tl: { + hd: [ + "contents", + encode$2(x._0) + ], + tl: /* [] */0 + } + }); + case /* ConfigurationChange */5 : + return Json_encode.object_({ + hd: [ + "tag", + "ConfigurationChange" + ], + tl: { + hd: [ + "contents", + x._0 + ], + tl: /* [] */0 + } + }); + + } +} var EventToView = { InputMethod: InputMethod, diff --git a/package.json b/package.json index cf567ed9..0574aca1 100644 --- a/package.json +++ b/package.json @@ -916,6 +916,11 @@ "type": "string", "default": "\\", "description": "Key for activating Unicode input method" + }, + "agdaMode.buffer.fontSize": { + "type": "number", + "default": 14, + "description": "The font size of Agda buffer" } } } diff --git a/src/Config.res b/src/Config.res index 19adeea2..c99d767d 100644 --- a/src/Config.res +++ b/src/Config.res @@ -204,3 +204,23 @@ module InputMethod = { } } } + +module Buffer = { + let getFontSize = () => { + let config = Workspace.getConfiguration(Some("agdaMode"), None) + let size = + switch config->WorkspaceConfiguration.get("buffer.fontSize") { + | Some(m) => m + | None => + switch Workspace.getConfiguration(Some("editor"), None)->WorkspaceConfiguration.get("fontSize") { + | Some(n) => n + | _ => 14 + } + } + + config->WorkspaceConfiguration.updateGlobalSettings("buffer.fontSize", size, None)->ignore + + size->Int.toString + } +} + diff --git a/src/Main.res b/src/Main.res index 5c871626..00f87630 100644 --- a/src/Main.res +++ b/src/Main.res @@ -46,8 +46,9 @@ let initialize = (channels, extensionPath, globalStoragePath, editor, fileName) ->Promise.done // not in the Registry, instantiate a State - let state = State.make(channels, globalStoragePath, extensionPath, editor) - + let state = State.make(debugChan, globalStoragePath, extensionPath, editor) + // Set panel's font size by configuration + state->State__View.Panel.setFontSize(Config.Buffer.getFontSize())->ignore // remove it from the Registry on request state.onRemoveFromRegistry ->Chan.once @@ -251,6 +252,26 @@ let activateWithoutContext = (subscriptions, extensionPath, globalStoragePath) = } })->subscribe + VSCode.Workspace.onDidChangeConfiguration(.(event: VSCode.ConfigurationChangeEvent.t) => { + let getFileName = editor => editor->VSCode.TextEditor.document->VSCode.TextDocument.fileName->Parser.filepath + // Maybe we should check active editor + // or define some methods to send events without state since changing style is irrelevant to states of eidtors + // (Currently, sending an event to the webview has to get the view from a state and send the event with the view) + let state = Array.reduce(VSCode.Window.visibleTextEditors, None, (state, editor) => { switch state { + | None => editor->getFileName->Registry.get + | _ => state + }}) + let fontSizeChanged = event->VSCode.ConfigurationChangeEvent.affectsConfiguration("agdaMode.buffer.fontSize", #Others(None)) + + if fontSizeChanged { + let size = Config.Buffer.getFontSize() + switch state { + | Some(state) => state->State__View.Panel.setFontSize(size)->ignore + | None => () + } + } + })->subscribe + // on close editor Inputs.onCloseDocument(document => { let fileName = VSCode.TextDocument.fileName(document)->Parser.filepath diff --git a/src/State/State__View.res b/src/State/State__View.res index 312735a5..2de54b8b 100644 --- a/src/State/State__View.res +++ b/src/State/State__View.res @@ -23,6 +23,8 @@ module type Panel = { string => Promise.t, ) => Promise.t let interruptPrompt: state => Promise.t + // Style + let setFontSize: (state, string) => Promise.t } module Panel: Panel = { @@ -66,6 +68,8 @@ module Panel: Panel = { let updateIM = (state, event) => sendEvent(state, InputMethod(event)) let updatePromptIM = (state, content) => sendEvent(state, PromptIMUpdate(content)) + let setFontSize = (state, fontSize) => sendEvent(state, ConfigurationChange(fontSize)) + // Header + Prompt let prompt = ( state, diff --git a/src/View/Panel/Panel.res b/src/View/Panel/Panel.res index efbb8652..15957285 100644 --- a/src/View/Panel/Panel.res +++ b/src/View/Panel/Panel.res @@ -25,6 +25,8 @@ let make = ( let (inputMethodState, runInputMethodAction) = React.useReducer(Keyboard.reducer, None) + let setFontSize = %raw(` function (n) { document.documentElement.style.setProperty("--agdaMode-buffer-font-size", n + "px"); } `) + // emit event Initialized on mount React.useEffect1(() => { onEventFromView->Chan.emit(Initialized) @@ -98,6 +100,9 @@ let make = ( setHeader(_ => header) setBody(old => Array.concat(old, body)) // append instead of flush | SetStatus(text) => setStatus(_ => text) + | ConfigurationChange(n) => + onSubmit(None) + setFontSize(n) } ) diff --git a/src/View/View.res b/src/View/View.res index c9184961..940f5cb0 100644 --- a/src/View/View.res +++ b/src/View/View.res @@ -130,6 +130,7 @@ module EventToView = { | PromptInterrupt | PromptIMUpdate(string) | InputMethod(InputMethod.t) + | ConfigurationChange(string) let toString = x => switch x { @@ -139,43 +140,53 @@ module EventToView = { | PromptInterrupt => "PromptInterrupt" | PromptIMUpdate(s) => "PromptIMUpdate " ++ s | InputMethod(_) => "InputMethod" + | ConfigurationChange(_) => "ConfigurationChange" } - let decode = { - open JsonCombinators.Json.Decode - Util.Decode.sum(x => { - switch x { - | "Display" => - Payload( - tuple2(Header.decode, array(Item.decode))->map(((header, body)) => Display(header, body)), - ) - | "Append" => - Payload( - tuple2(Header.decode, array(Item.decode))->map(((header, body)) => Append(header, body)), - ) - | "SetStatus" => Payload(string->map(text => SetStatus(text))) - | "PromptInterrupt" => TagOnly(PromptInterrupt) - | "PromptIMUpdate" => Payload(string->map(text => PromptIMUpdate(text))) - | "InputMethod" => Payload(InputMethod.decode->map(payload => InputMethod(payload))) - | tag => raise(DecodeError("[EventToView] Unknown constructor: " ++ tag)) - } - }) - } - let encode = { - open JsonCombinators.Json.Encode - Util.Encode.sum(x => - switch x { - | Display(header, body) => - Payload("Display", tuple2(Header.encode, array(Item.encode))((header, body))) - | Append(header, body) => - Payload("Append", tuple2(Header.encode, array(Item.encode))((header, body))) - | SetStatus(text) => Payload("SetStatus", string(text)) - | PromptInterrupt => TagOnly("PromptInterrupt") - | PromptIMUpdate(text) => Payload("PromptIMUpdate", string(text)) - | InputMethod(payload) => Payload("InputMethod", InputMethod.encode(payload)) - } - , ...) + // JSON encode/decode + let decode: Json.Decode.decoder = Util.Decode.sum(x => { + open Json.Decode + switch x { + | "Display" => + Contents( + pair(Header.decode, array(Item.decode)) |> map(((header, body)) => Display(header, body)), + ) + | "Append" => + Contents( + pair(Header.decode, array(Item.decode)) |> map(((header, body)) => Append(header, body)), + ) + | "SetStatus" => Contents(string |> map(text => SetStatus(text))) + | "PromptInterrupt" => TagOnly(PromptInterrupt) + | "PromptIMUpdate" => Contents(string |> map(text => PromptIMUpdate(text))) + | "InputMethod" => Contents(InputMethod.decode |> map(x => InputMethod(x))) + | "ConfigurationChange" => Contents(string |> map(size => ConfigurationChange(size))) + | tag => raise(DecodeError("[EventToView] Unknown constructor: " ++ tag)) + } + }) + + let encode: Json.Encode.encoder = x => { + open Json.Encode + switch x { + | Display(header, body) => + object_(list{ + ("tag", string("Display")), + ("contents", (header, body) |> pair(Header.encode, array(Item.encode))), + }) + + | Append(header, body) => + object_(list{ + ("tag", string("Append")), + ("contents", (header, body) |> pair(Header.encode, array(Item.encode))), + }) + | SetStatus(text) => object_(list{("tag", string("SetStatus")), ("contents", text |> string)}) + | PromptInterrupt => object_(list{("tag", string("PromptInterrupt"))}) + | PromptIMUpdate(text) => + object_(list{("tag", string("PromptIMUpdate")), ("contents", text |> string)}) + | InputMethod(payload) => + object_(list{("tag", string("InputMethod")), ("contents", payload |> InputMethod.encode)}) + | ConfigurationChange(size) => object_(list{("tag", string("ConfigurationChange")), ("contents", size |> string)}) + } } } diff --git a/style/style.less b/style/style.less index ce75362c..df356285 100644 --- a/style/style.less +++ b/style/style.less @@ -150,14 +150,14 @@ .agda-mode-body { - @line-height: 1rem; + @line-height: calc(var(--agdaMode-buffer-font-size)/1rem) rem; padding-top: calc(@header-height + @padding); white-space: pre; font-family: var(--vscode-editor-font-family); - font-size : var(--vscode-editor-font-size); + font-size : var(--agdaMode-buffer-font-size); line-height: @line-height; .codicon { diff --git a/style/variables.less b/style/variables.less index cb2f3262..40eed0cf 100644 --- a/style/variables.less +++ b/style/variables.less @@ -1,3 +1,7 @@ +:root { + --agdaMode-buffer-font-size: var(--vscode-editor-font-size); +} + // colors of editor markers @error : var(--vscode-editorError-foreground);