/** * DokuWiki Plugin Mizar Verifiable Docs (View Screen Script) * */ // 必要なモジュールをインポート import { EditorState, Compartment, StateEffect, StateField, RangeSetBuilder } from "@codemirror/state"; import { EditorView, lineNumbers, showPanel, Decoration, ViewPlugin, keymap } from "@codemirror/view"; import { defaultKeymap, insertNewlineAndIndent } from "@codemirror/commands"; import { LRLanguage, LanguageSupport, syntaxHighlighting, HighlightStyle, syntaxTree, foldNodeProp, foldInside, foldGutter, foldKeymap, codeFolding, indentNodeProp, } from "@codemirror/language"; // ★ codeFoldingなど import { parser } from "./mizar-parser.js"; import { tags as t } from "@lezer/highlight"; import { highlighting } from "./highlight.js"; // highlight.js からインポート // ショートカット定義 const myKeymap = [ ...defaultKeymap, // 基本的なキー操作(例: Ctrl+Z など)を利用 ...foldKeymap, { key: "Enter", run: insertNewlineAndIndent }, // Enterで改行+インデント ]; // ----------------------------- // スタイルの定義 // ----------------------------- const highlightStyle = HighlightStyle.define([ { tag: t.controlKeyword, class: "control-keyword" }, { tag: t.function(t.keyword), class: "function-keyword" }, { tag: t.keyword, class: "general-keyword" }, { tag: t.typeName, class: "type-name" }, { tag: t.meta, class: "meta-info" }, { tag: t.lineComment, class: "line-comment" }, { tag: t.paren, class: "paren" }, { tag: t.brace, class: "brace" }, { tag: t.squareBracket, class: "square-bracket" }, ]); // ----------------------------- // パーサー設定: 折りたたみ可能なノードを指定 // ----------------------------- let parserWithMetadata = parser.configure({ props: [ highlighting, foldNodeProp.add({ DefinitionBlock: foldInside, Proof: foldInside, NowBlock: foldInside, HerebyBlock: foldInside, }), ], }); // ----------------------------- // 言語サポートの定義 // ----------------------------- const mizarLanguage = LRLanguage.define({ parser: parserWithMetadata, }); // ----------------------------- // インデントの定義 // ----------------------------- const myIndent = indentNodeProp.add({ // "Proof" ノードが来たら親のインデント +1 段 Proof(context) { return context.lineIndent(context.node.from) + context.unit; }, DefinitionBlock(context) { return context.lineIndent(context.node.from) + context.unit; }, NowBlock(context) { return context.lineIndent(context.node.from) + context.unit; }, HerebyBlock(context) { return context.lineIndent(context.node.from) + context.unit; } }); // インデント込みの拡張 (mizarWithIndent) const mizarWithIndent = mizarLanguage.configure({ props: [myIndent], }); // ★必要であれば、mizarWithIndent を直接使うか、 // 下記のように mizar() 関数内で呼び出して使ってもOK // mizar() は インデント拡張なしのバージョン export function mizar() { return new LanguageSupport(mizarLanguage); } // ----------------------------- // ブラケット強調のプラグイン (色分けなど) // ----------------------------- function bracketHighlighter() { return ViewPlugin.fromClass( class { constructor(view) { this.decorations = this.buildDecorations(view); } update(update) { if (update.docChanged || update.viewportChanged) { this.decorations = this.buildDecorations(update.view); } } buildDecorations(view) { const builder = new RangeSetBuilder(); const stack = []; const colors = [ "bracket-color-0", "bracket-color-1", "bracket-color-2", "bracket-color-3", "bracket-color-4", ]; syntaxTree(view.state).iterate({ enter: ({ type, from, to }) => { if ( type.is("OpenParen") || type.is("OpenBrace") || type.is("OpenBracket") ) { stack.push({ type, from, to }); const level = stack.length % colors.length; builder.add(from, to, Decoration.mark({ class: colors[level] })); } else if ( type.is("CloseParen") || type.is("CloseBrace") || type.is("CloseBracket") ) { const open = stack.pop(); if (open) { const level = (stack.length + 1) % colors.length; builder.add(from, to, Decoration.mark({ class: colors[level] })); } } }, }); return builder.finish(); } }, { decorations: (v) => v.decorations, } ); } // ----------------------------- // Compartment, editors,などのグローバル管理 // ----------------------------- const editableCompartment = new Compartment(); // 共有 const editors = (window.editors = window.editors || {}); const lineNumberConfigs = (window.lineNumberConfigs = window.lineNumberConfigs || {}); const editorOrder = (window.editorOrder = window.editorOrder || []); // エラーデコレーション用 const errorDecorationEffect = StateEffect.define(); const errorDecorationsField = StateField.define({ create: () => Decoration.none, update(decorations, tr) { decorations = decorations.map(tr.changes); for (let effect of tr.effects) { if (effect.is(errorDecorationEffect)) { decorations = decorations.update({ add: effect.value }); } } return decorations; }, provide: (f) => EditorView.decorations.from(f), }); // ----------------------------- // Hide/Show 関連 // ----------------------------- function toggleMizarEditor(wrapper, hide) { const elementsToToggle = wrapper.querySelectorAll( ".editor-container, .copy-button, .edit-button, .reset-button, .compile-button" ); elementsToToggle.forEach((el) => { el.style.display = hide ? "none" : ""; }); const hideButton = wrapper.querySelector(".hide-button"); const showButton = wrapper.querySelector(".show-button"); if (hideButton && showButton) { hideButton.style.display = hide ? "none" : "inline"; showButton.style.display = hide ? "inline" : "none"; } } // ----------------------------- // DOMContentLoaded時の初期化 // ----------------------------- document.addEventListener( "DOMContentLoaded", function () { window.mizarInitialized = true; const wrappers = document.querySelectorAll(".mizarWrapper"); if (wrappers.length === 0) { console.warn("No Mizar blocks found."); return; } wrappers.forEach((block) => { const mizarId = block.id.replace("mizarBlock", ""); if (!block.querySelector(".editor-container").firstChild) { setupMizarBlock(block, mizarId); } }); // Hide/Show ボタン const hideButtons = document.querySelectorAll(".hide-button"); hideButtons.forEach((button) => { button.addEventListener("click", () => { const parentWrapper = button.closest(".mizarWrapper"); if (!parentWrapper) return; toggleMizarEditor(parentWrapper, true); }); }); const showButtons = document.querySelectorAll(".show-button"); showButtons.forEach((button) => { button.addEventListener("click", () => { const parentWrapper = button.closest(".mizarWrapper"); if (!parentWrapper) return; toggleMizarEditor(parentWrapper, false); }); }); // Hide All, Show All const hideAllButton = document.getElementById("hideAllButton"); const showAllButton = document.getElementById("showAllButton"); const resetAllButton = document.getElementById("resetAllButton"); if (hideAllButton && showAllButton) { hideAllButton.addEventListener("click", (e) => { toggleAllWrappers(true); hideAllButton.style.display = "none"; showAllButton.style.display = ""; e.target.blur(); }); showAllButton.addEventListener("click", (e) => { toggleAllWrappers(false); showAllButton.style.display = "none"; hideAllButton.style.display = ""; e.target.blur(); }); } function toggleAllWrappers(hide) { const allWrappers = document.querySelectorAll(".mizarWrapper"); allWrappers.forEach((wrapper) => { toggleMizarEditor(wrapper, hide); }); } // Reset All ボタン if (resetAllButton) { resetAllButton.addEventListener("click", (e) => { const allWrappers = document.querySelectorAll(".mizarWrapper"); allWrappers.forEach((wrapper) => { const resetBtn = wrapper.querySelector("button[id^='resetButton']"); if (resetBtn) { resetBtn.click(); } }); e.target.blur(); }); } }, { once: true } ); // ----------------------------- // エラー表示パネル // ----------------------------- const toggleErrorPanel = StateEffect.define(); const errorPanelState = StateField.define({ create: () => null, update(value, tr) { for (let e of tr.effects) { if (e.is(toggleErrorPanel)) value = e.value; } return value; }, provide: (f) => showPanel.from(f, (val) => (val ? createPanel(val) : null)), }); function createPanel(content) { return (_view) => { let dom = document.createElement("div"); dom.innerHTML = content; dom.className = "cm-error-panel"; return { dom }; }; } function calculateStartLineNumber(targetMizarId) { let totalLines = 1; for (let mizarId of editorOrder) { if (mizarId === targetMizarId) { break; } totalLines += editors[mizarId].state.doc.lines; } return totalLines; } function adjustLineNumbersForAllEditors() { let totalLines = 1; for (let mizarId of editorOrder) { const editor = editors[mizarId]; const startLine = totalLines; const lineNumberExtension = lineNumbers({ formatNumber: (number) => `${number + startLine - 1}`, }); editor.dispatch({ effects: lineNumberConfigs[mizarId].reconfigure(lineNumberExtension), }); totalLines += editor.state.doc.lines; } } function getEditorForGlobalLine(globalLine) { let currentLine = 1; for (let mizarId of editorOrder) { const editor = editors[mizarId]; const editorLines = editor.state.doc.lines; if (globalLine >= currentLine && globalLine < currentLine + editorLines) { return { editor, localLine: globalLine - currentLine + 1 }; } currentLine += editorLines; } return null; } // ----------------------------- // エディタの初期設定 // ----------------------------- function setupMizarBlock(mizarBlock, mizarId) { const editorContainer = mizarBlock.querySelector(".editor-container"); editorContainer.id = `editorContainer${mizarId}`; const editorContent = editorContainer.getAttribute("data-content"); const tempDiv = document.createElement("div"); tempDiv.innerHTML = editorContent; const decodedContent = tempDiv.textContent || tempDiv.innerText || ""; const lineNumberConfig = new Compartment(); lineNumberConfigs[mizarId] = lineNumberConfig; // codeFolding()を追加して折りたたみを有効化 // ※ここで mizarWithIndent を使いたい場合は差し替えます const editor = new EditorView({ state: EditorState.create({ doc: decodedContent, extensions: [ lineNumberConfig.of( lineNumbers({ formatNumber: (number) => `${number + calculateStartLineNumber(mizarId) - 1}`, }) ), editableCompartment.of(EditorView.editable.of(false)), syntaxHighlighting(highlightStyle), codeFolding(), // ★ 折りたたみ foldGutter(), keymap.of(myKeymap), // ← キーマップを登録 bracketHighlighter(), EditorView.updateListener.of((update) => { if (update.docChanged) { adjustLineNumbersForAllEditors(); } }), errorPanelState, errorDecorationsField, mizarWithIndent, ], }), parent: editorContainer, }); window.editors[mizarId] = editor; editorOrder.push(mizarId); // ボタン系 const editButton = mizarBlock.querySelector("button[id^='editButton']"); const compileButton = mizarBlock.querySelector("button[id^='compileButton']"); const resetButton = mizarBlock.querySelector("button[id^='resetButton']"); editButton.addEventListener("click", () => { editor.dispatch({ effects: editableCompartment.reconfigure(EditorView.editable.of(true)), }); editButton.style.display = "none"; compileButton.style.display = "inline"; resetButton.style.display = "inline"; }); compileButton.addEventListener("click", () => { if (mizarBlock.isRequestInProgress) { return; } mizarBlock.isRequestInProgress = true; startMizarCompilation(mizarBlock, toggleErrorPanel, mizarId); }); resetButton.addEventListener("click", async () => { const initialContent = editorContainer.getAttribute("data-content"); const tempDiv = document.createElement("div"); tempDiv.innerHTML = initialContent; const decodedContent = tempDiv.textContent || tempDiv.innerText || ""; editor.dispatch({ changes: { from: 0, to: editor.state.doc.length, insert: decodedContent }, }); editor.dispatch({ effects: editableCompartment.reconfigure(EditorView.editable.of(false)), }); editButton.style.display = "inline"; compileButton.style.display = "none"; resetButton.style.display = "none"; editor.dispatch({ effects: toggleErrorPanel.of(null), }); editor.dispatch({ effects: errorDecorationEffect.of([]), }); try { const response = await fetch( DOKU_BASE + "lib/exe/ajax.php?call=clear_temp_files", { method: "POST", headers: { "Content-Type": "application/x-www-form-urlencoded", }, } ); const text = await response.text(); let data; try { data = JSON.parse(text); } catch (error) { throw new Error("Server returned a non-JSON response: " + text); } if (data.success) { console.log(data.message); } else { console.error("Failed to clear temporary files:", data.message); } } catch (error) { console.error("Error clearing temporary files:", error); } }); } // ----------------------------- // 行スクロール関連 // ----------------------------- function scrollToLine(editor, line) { const lineInfo = editor.state.doc.line(line); editor.dispatch({ scrollIntoView: { from: lineInfo.from, to: lineInfo.to }, }); } // ----------------------------- // コンパイル開始 // ----------------------------- async function startMizarCompilation(mizarBlock, toggleErrorPanel, mizarId) { if (mizarBlock.eventSource) { mizarBlock.eventSource.close(); } const combinedContent = getCombinedContentUntil(mizarBlock); const data = "content=" + encodeURIComponent(combinedContent); try { const response = await fetch(DOKU_BASE + "lib/exe/ajax.php?call=view_compile", { method: "POST", headers: { "Content-Type": "application/x-www-form-urlencoded", }, body: data, }); if (!response.ok) { throw new Error("Network response was not ok"); } mizarBlock.eventSource = new EventSource( DOKU_BASE + "lib/exe/ajax.php?call=view_sse&" + data ); mizarBlock.eventSource.onmessage = function (event) { const editor = editors[mizarId]; let content = editor.state.field(errorPanelState) || ""; content += event.data + "
"; editor.dispatch({ effects: toggleErrorPanel.of(content), }); if (content.includes("❌")) { editor.dom.querySelector(".cm-error-panel").style.backgroundColor = "#fcc"; } else { editor.dom.querySelector(".cm-error-panel").style.backgroundColor = "#ccffcc"; } }; mizarBlock.eventSource.addEventListener("compileErrors", function (event) { try { const errors = JSON.parse(event.data); let errorContent = editors[mizarId].state.field(errorPanelState) || ""; const decorationsPerEditor = {}; errors.forEach(function (error) { const { line, column, message } = error; const link = `[Ln ${line}, Col ${column}]`; errorContent += `❌ ${message} ${link}
`; const editorInfo = getEditorForGlobalLine(line); if (editorInfo) { const { editor, localLine } = editorInfo; const lineInfo = editor.state.doc.line(localLine); const from = lineInfo.from + (column - 1); const to = from + 1; if (from >= lineInfo.from && to <= lineInfo.to) { const deco = Decoration.mark({ class: "error-underline", attributes: { title: `${message} (Ln ${line}, Col ${column})`, }, }).range(from, to); const editorId = Object.keys(editors).find( (key) => editors[key] === editor ); if (!decorationsPerEditor[editorId]) { decorationsPerEditor[editorId] = []; } decorationsPerEditor[editorId].push(deco); } } }); for (let editorId in decorationsPerEditor) { const editor = editors[editorId]; const decorations = decorationsPerEditor[editorId]; if (decorations.length > 0) { editor.dispatch({ effects: errorDecorationEffect.of(decorations.sort((a, b) => a.from - b.from)), }); } } editors[mizarId].dispatch({ effects: [toggleErrorPanel.of(errorContent)], }); if (errorContent.includes("❌")) { editors[mizarId].dom.querySelector(".cm-error-panel").style.backgroundColor = "#fcc"; } else { editors[mizarId].dom.querySelector(".cm-error-panel").style.backgroundColor = "#ccffcc"; } const errorPanel = editors[mizarId].dom.querySelector(".cm-error-panel"); errorPanel.querySelectorAll(".error-link").forEach((link) => { link.addEventListener("click", function (e) { e.preventDefault(); const line = parseInt(link.getAttribute("data-line"), 10); const editorInfo = getEditorForGlobalLine(line); if (editorInfo) { const { editor, localLine } = editorInfo; scrollToLine(editor, localLine); } }); }); } catch (e) { console.error("Failed to parse error data:", e); console.error("Event data:", event.data); } }); mizarBlock.eventSource.onerror = () => { mizarBlock.eventSource.close(); mizarBlock.isRequestInProgress = false; finalizeCompilation(mizarBlock); }; } catch (error) { console.error("Fetch error: ", error); mizarBlock.isRequestInProgress = false; } } function getCombinedContentUntil(mizarBlock) { let combinedContent = ""; const mizarBlocks = document.querySelectorAll(".mizarWrapper"); const blockIndex = Array.from(mizarBlocks).indexOf(mizarBlock); for (let i = 0; i <= blockIndex; i++) { const mizarId = editorOrder[i]; const editor = editors[mizarId]; if (editor && editor.state) { const blockContent = editor.state.doc.toString(); combinedContent += blockContent + "\n"; } } return combinedContent.trim(); } function finalizeCompilation(mizarBlock) { const compileButton = mizarBlock.querySelector("[id^='compileButton']"); const resetButton = mizarBlock.querySelector("[id^='resetButton']"); compileButton.style.display = "none"; resetButton.style.display = "inline-block"; mizarBlock.isRequestInProgress = false; } // ----------------------------- // ファイル作成関連 // ----------------------------- window.createMizarFile = async function (filename) { const combinedContent = collectMizarContents(); if (!combinedContent) { console.error("Error: Combined content is empty."); return; } if (!filename.endsWith(".miz")) { filename += ".miz"; } try { const response = await fetch(DOKU_BASE + "lib/exe/ajax.php?call=create_combined_file", { method: "POST", headers: { "Content-Type": "application/x-www-form-urlencoded", }, body: "content=" + encodeURIComponent(combinedContent) + "&filename=" + encodeURIComponent(filename), }); if (!response.ok) { console.error("Failed to create file: Network response was not ok"); return; } const data = await response.json(); if (data.success) { console.log("File created successfully:", filename); const blob = new Blob([data.data.content], { type: "application/octet-stream" }); const url = URL.createObjectURL(blob); const contentWindow = window.open("", "_blank"); contentWindow.document.write( "
" +
          data.data.content
            .replace(/&/g, "&")
            .replace(//g, ">") +
          "
" ); contentWindow.document.title = filename; const downloadLink = contentWindow.document.createElement("a"); downloadLink.href = url; downloadLink.download = filename; downloadLink.textContent = "⬇️ Click here to download the file"; downloadLink.style.display = "block"; downloadLink.style.marginTop = "10px"; contentWindow.document.body.appendChild(downloadLink); contentWindow.addEventListener("unload", () => { URL.revokeObjectURL(url); }); } else { console.error("Failed to create file:", data.message); } } catch (error) { console.error("Error creating file:", error); } }; function collectMizarContents() { let combinedContent = ""; for (let mizarId of editorOrder) { const editor = editors[mizarId]; if (editor && editor.state) { combinedContent += editor.state.doc.toString() + "\n"; } } return combinedContent; } // ----------------------------- // Copyボタンの実装 // ----------------------------- document.addEventListener("DOMContentLoaded", () => { const copyButtons = document.querySelectorAll(".copy-button"); copyButtons.forEach((button) => { button.addEventListener("click", (event) => { const buttonElement = event.currentTarget; const mizarIdRaw = buttonElement.dataset.mizarid; const mizarId = mizarIdRaw.replace("mizarBlock", ""); if (!editors[mizarId]) { console.error("エディタが見つかりません: ", mizarIdRaw); return; } const editor = editors[mizarId]; const content = editor.state.doc.toString(); navigator.clipboard .writeText(content) .then(() => { buttonElement.textContent = "Copied!"; buttonElement.disabled = true; setTimeout(() => { buttonElement.textContent = "Copy"; buttonElement.disabled = false; }, 2000); }) .catch((err) => { console.error("コピーに失敗しました: ", err); }); }); }); });