From 12de46477d2b817e4e4d7615c3da41aff46682ee Mon Sep 17 00:00:00 2001 From: ZYShih Date: Tue, 26 Sep 2023 14:30:03 +0800 Subject: [PATCH 1/3] Make the font size of Agda buffer the same as editors --- style/style.less | 2 +- style/variables.less | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/style/style.less b/style/style.less index c3286986..ef044a9d 100644 --- a/style/style.less +++ b/style/style.less @@ -155,7 +155,7 @@ white-space: pre; font-family: var(--vscode-editor-font-family); - font-size : 100%; + font-size : var(--vscode-editor-font-size); line-height: @line-height; .codicon { diff --git a/style/variables.less b/style/variables.less index 65d617be..cb2f3262 100644 --- a/style/variables.less +++ b/style/variables.less @@ -9,7 +9,7 @@ @foreground : var(--vscode-foreground); @foreground-subtle : var(--vscode-input-placeholderForeground); -@foreground-tenuous : var(--vscode-editorIndentGuide-activeBackground); +@foreground-tenuous : var(--vscode-editorIndentGuide-activeBackground); @foreground-highlight : var(--vscode-activityBar-foreground); @selection : var(--vscode-editor-selectionBackground); @header-background : var(--vscode-editor-background); From eb2ede64e7b3e5abccdeb175ea4211e70807f852 Mon Sep 17 00:00:00 2001 From: ZYShih Date: Wed, 25 Oct 2023 20:59:34 +0800 Subject: [PATCH 2/3] Add Agda buffer font size setting --- lib/js/src/Config.bs.js | 19 +++++++++++++++++++ lib/js/src/Main.bs.js | 30 ++++++++++++++++++++++++++---- lib/js/src/State/State__View.bs.js | 11 ++++++++++- lib/js/src/View/Panel/Panel.bs.js | 4 ++++ lib/js/src/View/View.bs.js | 30 ++++++++++++++++++++++++++++++ package.json | 5 +++++ src/Config.res | 20 ++++++++++++++++++++ src/Main.res | 20 ++++++++++++++++++++ src/State/State__View.res | 4 ++++ src/View/Panel/Panel.res | 5 +++++ src/View/View.res | 4 ++++ style/style.less | 2 +- style/variables.less | 4 ++++ 13 files changed, 152 insertions(+), 6 deletions(-) diff --git a/lib/js/src/Config.bs.js b/lib/js/src/Config.bs.js index fd39290f..d2ca8ea6 100644 --- a/lib/js/src/Config.bs.js +++ b/lib/js/src/Config.bs.js @@ -221,6 +221,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; @@ -231,4 +249,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 3da8f2b4..1d02fce1 100644 --- a/lib/js/src/Main.bs.js +++ b/lib/js/src/Main.bs.js @@ -73,6 +73,7 @@ function initialize(debugChan, extensionPath, globalStoragePath, editor, fileNam })); 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); })); @@ -202,7 +203,28 @@ function activateWithoutContext(subscriptions, extensionPath, globalStoragePath) }); subscriptions.push(x$1); - var x$2 = Vscode.workspace.onDidCloseTextDocument(function ($$document) { + 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 ; + } + console.log("configuration change"); + 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); @@ -211,7 +233,7 @@ function activateWithoutContext(subscriptions, extensionPath, globalStoragePath) } }); - subscriptions.push(x$2); + subscriptions.push(x$3); var xs = onTriggerCommand(function (command, editor) { var fileName = Parser$AgdaModeVscode.filepath(editor.document.fileName); var tmp; @@ -283,8 +305,8 @@ function activateWithoutContext(subscriptions, extensionPath, globalStoragePath) })); }); Caml_splice_call.spliceObjApply(subscriptions, "push", [xs]); - var x$3 = registerDocumentSemanticTokensProvider(undefined); - subscriptions.push(x$3); + 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 3f866b93..3bf9b9a6 100644 --- a/lib/js/src/State/State__View.bs.js +++ b/lib/js/src/State/State__View.bs.js @@ -118,6 +118,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 = { @@ -165,7 +173,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 8737b7c4..91d8ce52 100644 --- a/lib/js/src/View/Panel/Panel.bs.js +++ b/lib/js/src/View/Panel/Panel.bs.js @@ -53,6 +53,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 */0); @@ -182,6 +183,9 @@ function Panel(Props) { })); 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 b350a12c..0e839f47 100644 --- a/lib/js/src/View/View.bs.js +++ b/lib/js/src/View/View.bs.js @@ -381,6 +381,8 @@ function toString$1(x) { return "PromptIMUpdate " + x._0; case /* InputMethod */4 : return "InputMethod"; + case /* ConfigurationChange */5 : + return "ConfigurationChange"; } } @@ -406,6 +408,20 @@ var decode$3 = Util$AgdaModeVscode.Decode.sum(function (x) { }), [Symbol.for("name")]: "Contents" }; + 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: 0, @@ -573,6 +589,20 @@ function encode$3(x) { tl: /* [] */0 } }); + case /* ConfigurationChange */5 : + return Json_encode.object_({ + hd: [ + "tag", + "ConfigurationChange" + ], + tl: { + hd: [ + "contents", + x._0 + ], + tl: /* [] */0 + } + }); } } diff --git a/package.json b/package.json index 5abe7f4b..7327da9f 100644 --- a/package.json +++ b/package.json @@ -921,6 +921,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 41a6a176..ec0344e4 100644 --- a/src/Config.res +++ b/src/Config.res @@ -205,3 +205,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 ec445b74..4ff231a7 100644 --- a/src/Main.res +++ b/src/Main.res @@ -51,6 +51,8 @@ let initialize = (debugChan, extensionPath, globalStoragePath, editor, fileName) // not in the Registry, instantiate a State 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->Promise.get(() => Registry.remove(fileName)) @@ -242,6 +244,24 @@ 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 + 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 { + Js.log("configuration change") + 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 a0cd23da..35d1f53b 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 11c7105d..55a09d14 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) @@ -93,6 +95,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 b536b04a..eeb4dc60 100644 --- a/src/View/View.res +++ b/src/View/View.res @@ -143,6 +143,7 @@ module EventToView = { | PromptInterrupt | PromptIMUpdate(string) | InputMethod(InputMethod.t) + | ConfigurationChange(string) let toString = x => switch x { @@ -152,6 +153,7 @@ module EventToView = { | PromptInterrupt => "PromptInterrupt" | PromptIMUpdate(s) => "PromptIMUpdate " ++ s | InputMethod(_) => "InputMethod" + | ConfigurationChange(_) => "ConfigurationChange" } // JSON encode/decode @@ -170,6 +172,7 @@ module EventToView = { | "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)) } }) @@ -194,6 +197,7 @@ module EventToView = { 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 ef044a9d..d6a69fc2 100644 --- a/style/style.less +++ b/style/style.less @@ -155,7 +155,7 @@ 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); From fb05c03337b6cb406fcc9caccaf537de543cd65b Mon Sep 17 00:00:00 2001 From: ZYShih Date: Thu, 2 Nov 2023 17:51:40 +0800 Subject: [PATCH 3/3] Adjust Agda buffer's line height --- lib/js/src/Main.bs.js | 1 - src/Main.res | 4 +++- style/style.less | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/lib/js/src/Main.bs.js b/lib/js/src/Main.bs.js index 1d02fce1..285db436 100644 --- a/lib/js/src/Main.bs.js +++ b/lib/js/src/Main.bs.js @@ -215,7 +215,6 @@ function activateWithoutContext(subscriptions, extensionPath, globalStoragePath) if (!fontSizeChanged) { return ; } - console.log("configuration change"); var size = Config$AgdaModeVscode.$$Buffer.getFontSize(undefined); if (state !== undefined) { State__View$AgdaModeVscode.Panel.setFontSize(state, size); diff --git a/src/Main.res b/src/Main.res index 4ff231a7..61d8bda1 100644 --- a/src/Main.res +++ b/src/Main.res @@ -246,6 +246,9 @@ let activateWithoutContext = (subscriptions, extensionPath, globalStoragePath) = 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 @@ -253,7 +256,6 @@ let activateWithoutContext = (subscriptions, extensionPath, globalStoragePath) = let fontSizeChanged = event->VSCode.ConfigurationChangeEvent.affectsConfiguration("agdaMode.buffer.fontSize", #Others(None)) if fontSizeChanged { - Js.log("configuration change") let size = Config.Buffer.getFontSize() switch state { | Some(state) => state->State__View.Panel.setFontSize(size)->ignore diff --git a/style/style.less b/style/style.less index d6a69fc2..c86066bc 100644 --- a/style/style.less +++ b/style/style.less @@ -148,7 +148,7 @@ .agda-mode-body { - @line-height: 1rem; + @line-height: calc(var(--agdaMode-buffer-font-size)/1rem) rem; padding-top: calc(@header-height + @padding);