/** * * DokuWiki Plugin Mizar Verifiable Docs (View Screen Script) * * @author Yamada, M. */ "use strict;" // 必要なモジュールをインポート import { EditorState, Compartment, StateEffect, StateField, RangeSetBuilder } from "@codemirror/state"; import { EditorView, lineNumbers, showPanel, Decoration, ViewPlugin } from "@codemirror/view"; import { LRLanguage, LanguageSupport, syntaxHighlighting, HighlightStyle, syntaxTree } from "@codemirror/language"; import { parser } from "./mizar-parser.js"; import { tags as t } from "@lezer/highlight"; import { highlighting } from "./highlight.js"; // highlight.js からインポート // スタイルの定義 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 // highlight.js からインポートした highlighting を使用 ] }); // 言語サポートの定義 const mizarLanguage = LRLanguage.define({ parser: parserWithMetadata }); 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 }); } const editableCompartment = new Compartment(); // 共有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) }); // 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); } }); }, { 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; // 最初の行を1に変更 for (let mizarId of editorOrder) { if (mizarId === targetMizarId) { break; } totalLines += editors[mizarId].state.doc.lines; } return totalLines; // ここで+1を追加しない } function adjustLineNumbersForAllEditors() { let totalLines = 1; // 最初の行を1に変更 for (let mizarId of editorOrder) { const editor = editors[mizarId]; const startLine = totalLines; const lineNumberExtension = lineNumbers({ formatNumber: number => `${number + startLine - 1}` }); // Compartmentのreconfigureメソッドを使用して設定を更新 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'); // テンポラリDOM要素を作成してinnerHTMLに設定することでデコードを実行 const tempDiv = document.createElement('div'); tempDiv.innerHTML = editorContent; const decodedContent = tempDiv.textContent || tempDiv.innerText || ""; const lineNumberConfig = new Compartment(); lineNumberConfigs[mizarId] = lineNumberConfig; // 各エディタの設定を保持 // EditorViewの初期化部分 const editor = new EditorView({ state: EditorState.create({ doc: decodedContent, // デコードされたコンテンツを使用 extensions: [ lineNumberConfig.of(lineNumbers({ formatNumber: number => `${number + calculateStartLineNumber(mizarId) - 1}` })), // EditorCustomThemeは削除 editableCompartment.of(EditorView.editable.of(false)), // 初期状態を読み取り専用に設定 syntaxHighlighting(highlightStyle), // 追加: ハイライトスタイルの適用 bracketHighlighter(), EditorView.updateListener.of(update => { if (update.docChanged) { adjustLineNumbersForAllEditors(); // すべてのエディタの行番号を更新 } }), errorPanelState, errorDecorationsField, syntaxHighlighting(highlightStyle), mizar() // Mizarの言語サポートを追加 ] }), parent: editorContainer }); window.editors[mizarId] = editor; // エディタをオブジェクトに追加 editorOrder.push(mizarId); // エディタのIDを順序付けて保持 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'; // resetボタンも表示 }); compileButton.addEventListener('click', () => { if (mizarBlock.isRequestInProgress) { return; // すでにこのブロックでリクエストが進行中 } mizarBlock.isRequestInProgress = true; // リクエスト開始をマーク startMizarCompilation(mizarBlock, toggleErrorPanel, mizarId); }); resetButton.addEventListener('click', async () => { // エディタを最初の状態に戻す(Wiki本体に保存されている文書を再読み込み) const initialContent = editorContainer.getAttribute('data-content'); // 初期コンテンツを再取得 const tempDiv = document.createElement('div'); // HTMLエンティティのデコード用 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" } }); // JSONで返ってくることを期待する const text = await response.text(); let data; try { data = JSON.parse(text); } catch (error) { // JSONのパースに失敗した場合はHTMLレスポンスだと判断 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); } }); // Enterキーで行を増やすリスナーを追加 editor.dom.addEventListener('keydown', (e) => { if (e.key === 'Enter' && editor.state.facet(EditorView.editable)) { e.preventDefault(); const transaction = editor.state.update({ changes: { from: editor.state.selection.main.head, insert: '\n' } }); editor.dispatch(transaction); } }); } 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('compileFinished', () => { finalizeCompilation(mizarBlock); }); // エラー情報がある場合に受信するイベントリスナー 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) { // mizarBlock から直接ボタン要素を取得 const compileButton = mizarBlock.querySelector('[id^="compileButton"]'); const resetButton = mizarBlock.querySelector('[id^="resetButton"]'); // compileButtonを非表示にし、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; } // ファイル名に拡張子 '.miz' がなければ追加 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); // Blobを作成(MIMEタイプを 'application/octet-stream' に設定) 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; // ファイル名を指定(.miz 拡張子付き) 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; } 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; // mizarBlock12 形式を取得 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); }); }); }); });