From 323a7907e331005a6a732f12a1cd53e85e15eeff Mon Sep 17 00:00:00 2001 From: Muffleee Date: Mon, 24 Feb 2025 11:48:18 +0100 Subject: [PATCH 1/3] add font size menu and shift+c shortcut for it --- packages/application/src/plugins/rise.ts | 139 ++++++++++++++++++++++- packages/application/style/base.css | 15 ++- packages/lab/schema/plugin.json | 5 + 3 files changed, 155 insertions(+), 4 deletions(-) diff --git a/packages/application/src/plugins/rise.ts b/packages/application/src/plugins/rise.ts index 1f90d74..75ebf20 100644 --- a/packages/application/src/plugins/rise.ts +++ b/packages/application/src/plugins/rise.ts @@ -45,10 +45,56 @@ namespace CommandIDs { export const riseChalkboardColorNext = 'RISE:chalkboard-colorNext'; export const riseChalkboardDownload = 'RISE:chalkboard-download'; export const riseNotesOpen = 'RISE:notes-open'; + export const riseFontSizeCommand = 'RISE:change-font-size'; export const riseShowConfig = 'RISE:show-configuration'; } +const style = document.createElement('style'); + +function SetStyleValue(type:string, newValue:string) { + const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.replace("\n", "")?.split(";"); + + if(text == undefined) return; + + let result = ":root {\n"; + + for (let i = 0; i < text?.length; i++) { + let styleRule = text[i]?.trim(); + + if(!styleRule.startsWith(type)) { + result += styleRule; + if (i < text.length - 1) { + result += ";"; + } + continue; + } + + result += type + ": " + newValue + "px !important;"; + } + result += "}"; + + style.textContent = result; +} + +function GetStyleValue(type:string) { + const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.split(";"); + + if(text == undefined) return "10"; + + for (let i = 0; i < text?.length; i++) { + let styleRule = text[i]?.trim(); + + if(!styleRule.startsWith(type)) continue; + + styleRule = styleRule.replace(type + ": ", ""); + styleRule = styleRule.replace("px !important", ""); + + return styleRule; + } + return "10"; +} + /** * Open the notebook with RISE. */ @@ -68,6 +114,21 @@ export const plugin: JupyterFrontEndPlugin = { // Uncomment in dev mode to send logs to the parent window //Private.setupLog(); + // Override css variables (change default values here if needed) + style.textContent = ` + :root { + --jp-code-font-size: 20px !important; + --jp-ui-font-size0-rise: 50px !important; + --jp-ui-font-size1-rise: 40px !important; + --jp-ui-font-size2-rise: 35px !important; + --jp-ui-font-size3-rise: 30px !important; + --jp-ui-font-size4-rise: 25px !important; + --jp-ui-table-font-size-rise: 20px !important; + --jp-ui-code-output: 20px !important; + } + `; + document.head.appendChild(style); + const trans = (translator ?? nullTranslator).load('rise'); // Get the active cell index from query argument @@ -115,7 +176,8 @@ export const plugin: JupyterFrontEndPlugin = { CommandIDs.riseChalkboardClear, CommandIDs.riseChalkboardReset, CommandIDs.riseChalkboardColorNext, - CommandIDs.riseChalkboardColorPrev + CommandIDs.riseChalkboardColorPrev, + CommandIDs.riseFontSizeCommand ].forEach(command => { palette.addItem({ command, @@ -349,6 +411,7 @@ namespace Rise { const reveal_actions: { [id: string]: () => void } = {}; // RISE/reveal.js API calls + reveal_actions[CommandIDs.riseFontSizeCommand] = () => openFontSizeMenu; reveal_actions[CommandIDs.riseFirstSlide] = () => Reveal.slide(0); // jump to first slide reveal_actions[CommandIDs.riseLastSlide] = () => Reveal.slide(Number.MAX_VALUE); // jump to last slide @@ -855,6 +918,79 @@ namespace Rise { ); } + function openFontSizeMenu() { + const content = document.createElement('div'); + content.style.display = 'flex'; + content.style.flexDirection = 'column'; + + function GetAppendData(label: string, varName: string) { + const container = document.createElement('div'); + container.style.display = 'flex'; + container.style.alignItems = 'center'; + const labelElem = document.createElement('label'); + labelElem.textContent = label; + const input = document.createElement('input'); + input.type = 'number'; + input.value = GetStyleValue(varName) || "0"; + input.min = '8'; + input.max = '72'; + input.style.width = '60px'; + input.style.fontSize = '14px'; + container.appendChild(labelElem); + container.appendChild(input); + + return {container: container, input: input, label: labelElem, originalVal: input.value}; + } + + const headerSizeData = GetAppendData("Header Font Size:", "--jp-ui-font-size0-rise"); + const codeFontSizeData = GetAppendData("Code Font Size:", "--jp-code-font-size"); + const outputFontSizeData = GetAppendData("Output Font Size:", "--jp-ui-code-output"); + const tableFontSizeData = GetAppendData("Table Font Size:", "--jp-ui-table-font-size-rise"); + + content.appendChild(headerSizeData.label); + content.appendChild(headerSizeData.input); + content.appendChild(document.createElement('br')); + content.appendChild(codeFontSizeData.label); + content.appendChild(codeFontSizeData.input); + content.appendChild(document.createElement('br')); + content.appendChild(outputFontSizeData.label); + content.appendChild(outputFontSizeData.input); + content.appendChild(document.createElement('br')); + content.appendChild(tableFontSizeData.label); + content.appendChild(tableFontSizeData.input); + + const contentWidget = new Widget(); + contentWidget.node.appendChild(content); + + const dialog = showDialog({ + title: 'Font Size Settings', + body: contentWidget, + buttons: [ + Dialog.cancelButton(), + Dialog.okButton({ label: 'Apply' }) + ] + }); + + dialog.then(result => { + if (result.button.accept) { + SetStyleValue("--jp-code-font-size", codeFontSizeData.input.value); + SetStyleValue("--jp-ui-table-font-size-rise", tableFontSizeData.input.value); + SetStyleValue("--jp-ui-code-output", outputFontSizeData.input.value); + + if(headerSizeData.input.value != headerSizeData.originalVal) { + const headerSize = headerSizeData.input.value + SetStyleValue("--jp-ui-font-size0-rise", headerSizeData.input.value); + SetStyleValue("--jp-ui-font-size1-rise", (Number(headerSize) * 0.8).toString()); + SetStyleValue("--jp-ui-font-size2-rise", (Number(headerSize) * 0.7).toString()); + SetStyleValue("--jp-ui-font-size3-rise", (Number(headerSize) * 0.6).toString()); + SetStyleValue("--jp-ui-font-size4-rise", (Number(headerSize) * 0.5).toString()); + } + } + + contentWidget.dispose(); + }); + } + function toggleAllRiseButtons() { for (const selector of ['#help-b', '#toggle-chalkboard', '#toggle-notes']) { const element = document.querySelector(selector) as HTMLElement | null; @@ -1244,6 +1380,7 @@ namespace Rise { } { if (Object.keys(reveal_helpstr).length === 0) { // RISE/reveal.js API calls + reveal_helpstr[CommandIDs.riseFontSizeCommand] = trans.__('set font sizes') reveal_helpstr[CommandIDs.riseFirstSlide] = trans.__( 'jump to first slide' ); diff --git a/packages/application/style/base.css b/packages/application/style/base.css index 699ece3..76901cc 100644 --- a/packages/application/style/base.css +++ b/packages/application/style/base.css @@ -217,7 +217,7 @@ } .rise-enabled .jp-OutputArea pre { - font-size: 14px; + font-size: var(--jp-ui-code-output); } .rise-enabled .jp-OutputPrompt { @@ -252,25 +252,30 @@ } .rise-enabled .jp-RenderedHTMLCommon h1 { + font-size: var(--jp-ui-font-size0-rise); font-weight: bold; } .rise-enabled .jp-RenderedHTMLCommon h2 { + font-size: var(--jp-ui-font-size1-rise); font-weight: bold; } .rise-enabled .jp-RenderedHTMLCommon h3 { + font-size: var(--jp-ui-font-size2-rise); font-weight: bold; } .rise-enabled .jp-RenderedHTMLCommon h4 { + font-size: var(--jp-ui-font-size3-rise); font-weight: bold; - font-style: italic; + /* font-style: italic; */ } .rise-enabled .jp-RenderedHTMLCommon h5 { + font-size: var(--jp-ui-font-size4-rise); font-weight: bold; - font-style: italic; + /* font-style: italic; */ } .rise-enabled .CodeMirror { @@ -406,6 +411,10 @@ left: 7em !important; } +.rise-enabled .jp-RenderedHTMLCommon table { + font-size: var(--jp-ui-table-font-size-rise); +} + /* fix for reveal dark themes */ body.rise-enabled.theme-black div.jp-RenderedHTMLCommon diff --git a/packages/lab/schema/plugin.json b/packages/lab/schema/plugin.json index 9af249b..58b0b9e 100644 --- a/packages/lab/schema/plugin.json +++ b/packages/lab/schema/plugin.json @@ -117,6 +117,11 @@ "command": "RISE:smart-exec", "keys": ["Shift Enter"], "selector": ".lm-Widget.reveal .jp-Notebook:focus" + }, + { + "command": "RISE:change-font-size", + "keys": ["Shift C"], + "selector": ".lm-Widget.reveal .jp-Notebook:focus" } ], "type": "object", From ced6fb63c81a84ddf17b22e1a6dde0d12f662f77 Mon Sep 17 00:00:00 2001 From: Muffleee Date: Wed, 26 Feb 2025 14:04:01 +0100 Subject: [PATCH 2/3] fix double equals signs --- packages/application/src/plugins/rise.ts | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/packages/application/src/plugins/rise.ts b/packages/application/src/plugins/rise.ts index 75ebf20..f909116 100644 --- a/packages/application/src/plugins/rise.ts +++ b/packages/application/src/plugins/rise.ts @@ -55,7 +55,7 @@ const style = document.createElement('style'); function SetStyleValue(type:string, newValue:string) { const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.replace("\n", "")?.split(";"); - if(text == undefined) return; + if(text === undefined) return; let result = ":root {\n"; @@ -80,7 +80,7 @@ function SetStyleValue(type:string, newValue:string) { function GetStyleValue(type:string) { const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.split(";"); - if(text == undefined) return "10"; + if(text === undefined) return "10"; for (let i = 0; i < text?.length; i++) { let styleRule = text[i]?.trim(); @@ -977,7 +977,7 @@ namespace Rise { SetStyleValue("--jp-ui-table-font-size-rise", tableFontSizeData.input.value); SetStyleValue("--jp-ui-code-output", outputFontSizeData.input.value); - if(headerSizeData.input.value != headerSizeData.originalVal) { + if(headerSizeData.input.value !== headerSizeData.originalVal) { const headerSize = headerSizeData.input.value SetStyleValue("--jp-ui-font-size0-rise", headerSizeData.input.value); SetStyleValue("--jp-ui-font-size1-rise", (Number(headerSize) * 0.8).toString()); From 0a43c1817a72919edbdf84c5d91d4d4aaf5fb0a8 Mon Sep 17 00:00:00 2001 From: Muffleee Date: Tue, 4 Mar 2025 10:11:14 +0100 Subject: [PATCH 3/3] Add comments --- packages/application/src/plugins/rise.ts | 37 +++++++++++++++++------- 1 file changed, 26 insertions(+), 11 deletions(-) diff --git a/packages/application/src/plugins/rise.ts b/packages/application/src/plugins/rise.ts index f909116..b2dcbcb 100644 --- a/packages/application/src/plugins/rise.ts +++ b/packages/application/src/plugins/rise.ts @@ -52,13 +52,16 @@ namespace CommandIDs { const style = document.createElement('style'); +// Sets the value of a style variable that is active (defined in base.css) function SetStyleValue(type:string, newValue:string) { + // Get an array of css entries const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.replace("\n", "")?.split(";"); if(text === undefined) return; - let result = ":root {\n"; + let result = ":root {\n"; // Start building new css entry + // Find entry to change and set new value for (let i = 0; i < text?.length; i++) { let styleRule = text[i]?.trim(); @@ -77,11 +80,14 @@ function SetStyleValue(type:string, newValue:string) { style.textContent = result; } +// Returns the current value of a style variable function GetStyleValue(type:string) { + // Get an array of css entries const text = style.textContent?.replace(":root {", "")?.replace("}", "")?.split(";"); - if(text === undefined) return "10"; + if(text === undefined) return "10"; // Return default value if no css is found + // Loop through css entries and search for the right entry for (let i = 0; i < text?.length; i++) { let styleRule = text[i]?.trim(); @@ -90,9 +96,9 @@ function GetStyleValue(type:string) { styleRule = styleRule.replace(type + ": ", ""); styleRule = styleRule.replace("px !important", ""); - return styleRule; + return styleRule; // Variable found, return its value } - return "10"; + return "10"; // Variable not found, return a default value so nothing breaks } /** @@ -918,12 +924,14 @@ namespace Rise { ); } + // Function to open the Font-Size-Menu function openFontSizeMenu() { const content = document.createElement('div'); content.style.display = 'flex'; content.style.flexDirection = 'column'; - function GetAppendData(label: string, varName: string) { + // Helper function to get the data needed, to append an entry + function getAppendData(label: string, varName: string) { const container = document.createElement('div'); container.style.display = 'flex'; container.style.alignItems = 'center'; @@ -939,14 +947,16 @@ namespace Rise { container.appendChild(labelElem); container.appendChild(input); - return {container: container, input: input, label: labelElem, originalVal: input.value}; + return {container: container, input: input, label: labelElem, originalVal: input.value}; // Return all the values needed } - const headerSizeData = GetAppendData("Header Font Size:", "--jp-ui-font-size0-rise"); - const codeFontSizeData = GetAppendData("Code Font Size:", "--jp-code-font-size"); - const outputFontSizeData = GetAppendData("Output Font Size:", "--jp-ui-code-output"); - const tableFontSizeData = GetAppendData("Table Font Size:", "--jp-ui-table-font-size-rise"); + // Build the window + const headerSizeData = getAppendData("Header Font Size:", "--jp-ui-font-size0-rise"); + const codeFontSizeData = getAppendData("Code Font Size:", "--jp-code-font-size"); + const outputFontSizeData = getAppendData("Output Font Size:", "--jp-ui-code-output"); + const tableFontSizeData = getAppendData("Table Font Size:", "--jp-ui-table-font-size-rise"); + // Append all values content.appendChild(headerSizeData.label); content.appendChild(headerSizeData.input); content.appendChild(document.createElement('br')); @@ -962,6 +972,7 @@ namespace Rise { const contentWidget = new Widget(); contentWidget.node.appendChild(content); + // Show the dialog window const dialog = showDialog({ title: 'Font Size Settings', body: contentWidget, @@ -971,12 +982,15 @@ namespace Rise { ] }); + // Handle result dialog.then(result => { if (result.button.accept) { + // Set new values SetStyleValue("--jp-code-font-size", codeFontSizeData.input.value); SetStyleValue("--jp-ui-table-font-size-rise", tableFontSizeData.input.value); SetStyleValue("--jp-ui-code-output", outputFontSizeData.input.value); + // If header value changed, change the others accordingly if(headerSizeData.input.value !== headerSizeData.originalVal) { const headerSize = headerSizeData.input.value SetStyleValue("--jp-ui-font-size0-rise", headerSizeData.input.value); @@ -987,6 +1001,7 @@ namespace Rise { } } + // Remove the window contentWidget.dispose(); }); } @@ -1469,4 +1484,4 @@ namespace Private { _error(...args); }; } -} +} \ No newline at end of file