Add Lean support

README.md

@@ -7,7 +7,7 @@ The result is shown only after the execution is finished. It is not possible to
 ![Video that shows how the plugin works.](https://github.com/twibiral/obsidian-execute-code/blob/master/images/execute_code_example.gif?raw=true)
 
 
-The following [languages are supported](#supported-programming-languages): C, CPP, Golang, Groovy, Kotlin, Java, JavaScript, TypeScript, Lua, CSharp, Prolog, Rust, Python, R, Wolfram Mathematica, Haskell, Scala, Shell & Powershell. 
+The following [languages are supported](#supported-programming-languages): C, CPP, Golang, Groovy, Kotlin, Java, JavaScript, TypeScript, Lean, Lua, CSharp, Prolog, Rust, Python, R, Wolfram Mathematica, Haskell, Scala, Shell & Powershell. 
 
 
 Python and Rust support embedded plots. All languages support ["magic" commands](#magic-commands) that help you to access paths in obsidian or show images in your notes.
@@ -134,6 +134,19 @@ print('Hello, World!')
 ```
 </details>
 
+<details>
+<summary>Lean</summary>
+
+- Requirements: install lean and config lean path.
+
+```lean
+def main : IO Unit :=
+  IO.println s!"Hello, World!"
+
+#eval main
+```
+</details>
+
 <details>
 <summary>C++</summary>
 

src/main.ts

@@ -17,7 +17,7 @@ import ExecutorManagerView, {
 import runAllCodeBlocks from './runAllCodeBlocks';
 
 export const languageAliases = ["javascript", "typescript", "bash", "csharp", "wolfram", "nb", "wl", "hs", "py"] as const;
-export const canonicalLanguages = ["js", "ts", "cs", "lua", "python", "cpp",
+export const canonicalLanguages = ["js", "ts", "cs", "lean", "lua", "python", "cpp",
 	"prolog", "shell", "groovy", "r", "go", "rust", "java", "powershell", "kotlin", "mathematica", "haskell", "scala", "c"] as const;
 export const supportedLanguages = [...languageAliases, ...canonicalLanguages] as const;
 
@@ -297,6 +297,13 @@ export default class ExecuteCodePlugin extends Plugin {
 				this.runCodeInShell(transformedCode, out, button, this.settings.tsPath, this.settings.tsArgs, "ts", language, file);
 			});
 
+		} else if (language === "lean") {
+			button.addEventListener("click", async () => {
+				button.className = runButtonDisabledClass;
+				const transformedCode = await new CodeInjector(this.app, this.settings, language).injectCode(srcCode);
+				this.runCodeInShell(transformedCode, out, button, this.settings.leanPath, this.settings.leanArgs, "lean", language, file);
+			});
+
 		} else if (language === "lua") {
 			button.addEventListener("click", async () => {
 				button.className = runButtonDisabledClass;

src/settings/Settings.ts

@@ -15,6 +15,9 @@ export interface ExecutorSettings {
 	tsPath: string;
 	tsArgs: string;
 	tsInject: string;
+	leanPath: string;
+	leanArgs: string;
+	leanInject: string;
 	luaPath: string;
 	luaArgs: string;
 	luaInject: string;
@@ -86,6 +89,7 @@ export interface ExecutorSettings {
 	jsInteractive: boolean;
 	tsInteractive: boolean;
 	csInteractive: boolean;
+	leanInteractive: boolean;
 	luaInteractive: boolean;
 	pythonInteractive: boolean;
 	cppInteractive: boolean;
@@ -121,6 +125,9 @@ export const DEFAULT_SETTINGS: ExecutorSettings = {
 	tsPath: "ts-node",
 	tsArgs: "",
 	tsInject: "",
+	leanPath: "lean",
+	leanArgs: "",
+	leanInject: "",
 	luaPath: "lua",
 	luaArgs: "",
 	luaInject: "",
@@ -192,6 +199,7 @@ export const DEFAULT_SETTINGS: ExecutorSettings = {
 	jsInteractive: true,
 	tsInteractive: false,
 	csInteractive: false,
+	leanInteractive: false,
 	luaInteractive: false,
 	pythonInteractive: true,
 	cppInteractive: false,

src/settings/SettingsTab.ts

@@ -10,6 +10,7 @@ import makeHaskellSettings from "./per-lang/makeHaskellSettings";
 import makeJavaSettings from "./per-lang/makeJavaSettings";
 import makeJsSettings from "./per-lang/makeJsSettings";
 import makeKotlinSettings from "./per-lang/makeKotlinSettings";
+import makeLeanSettings from "./per-lang/makeLeanSettings";
 import makeLuaSettings from "./per-lang/makeLuaSettings";
 import makeMathematicaSettings from "./per-lang/makeMathematicaSettings";
 import makePowershellSettings from "./per-lang/makePowershellSettings";
@@ -117,6 +118,9 @@ export class SettingsTab extends PluginSettingTab {
 		// ========== TypeScript ==========
 		makeTsSettings(this, this.makeContainerFor("ts"));
 
+		// ========== Lean ==========
+		makeLeanSettings(this, this.makeContainerFor("lean"));
+
 		// ========== Lua ==========
 		makeLuaSettings(this, this.makeContainerFor("lua"));
 

src/settings/languageDisplayName.ts

@@ -9,6 +9,7 @@ export const DISPLAY_NAMES: Record<LanguageId, string> = {
     java: "Java",
     js: "Javascript",
     kotlin: "Kotlin",
+    lean: "Lean",
     lua: "Lua",
     mathematica: "Mathematica",
     powershell: "Powershell",
@@ -20,4 +21,4 @@ export const DISPLAY_NAMES: Record<LanguageId, string> = {
     ts: "Typescript",
     scala: "Scala",
     c: "C"
-} as const;
+} as const;

src/settings/per-lang/makeLeanSettings.ts

@@ -0,0 +1,26 @@
+import { Setting } from "obsidian";
+import { SettingsTab } from "../SettingsTab";
+
+export default (tab: SettingsTab, containerEl: HTMLElement) => {
+    containerEl.createEl('h3', { text: 'Lean Settings' });
+    new Setting(containerEl)
+        .setName('lean path')
+        .addText(text => text
+            .setValue(tab.plugin.settings.leanPath)
+            .onChange(async (value) => {
+                const sanitized = tab.sanitizePath(value);
+                tab.plugin.settings.leanPath = sanitized;
+                console.log('lean path set to: ' + sanitized);
+                await tab.plugin.saveSettings();
+            }));
+    new Setting(containerEl)
+        .setName('Lean arguments')
+        .addText(text => text
+            .setValue(tab.plugin.settings.leanArgs)
+            .onChange(async (value) => {
+                tab.plugin.settings.leanArgs = value;
+                console.log('Lean args set to: ' + value);
+                await tab.plugin.saveSettings();
+            }));
+    tab.makeInjectSetting(containerEl, "lean");
+}