mizarverifiabledocs/src/script.js

/**
 * * DokuWiki Plugin Mizar Verifiable Docs (View Screen Script)
 *
 * ここでは、折りたたみ機能を追加するために foldGutter, foldKeymap, foldNodeProp, foldInside, codeFolding を追加しています。
 */
"use strict;"
// 必要なモジュールをインポート
import { EditorState, Compartment, StateEffect, StateField, RangeSetBuilder } from "@codemirror/state";
import { EditorView, lineNumbers, showPanel, Decoration, ViewPlugin, keymap } from "@codemirror/view";
import { LRLanguage, LanguageSupport, syntaxHighlighting, HighlightStyle, syntaxTree, foldNodeProp, foldInside, foldGutter, foldKeymap, codeFolding } 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 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({
            "Proof": foldInside
        })
    ]
});

// 言語サポートの定義
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;
    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()を追加して折りたたみを有効化
    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(foldKeymap), // ★ 折りたたみ用キーマップ
                bracketHighlighter(),
                EditorView.updateListener.of(update => {
                    if (update.docChanged) {
                        adjustLineNumbersForAllEditors();
                    }
                }),
                errorPanelState,
                errorDecorationsField,
                mizar()
            ]
        }),
        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);
        }
    });

    // 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 + '<br>';
            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 = `<a href="#" class="error-link" data-line="${line}" data-column="${column}">[Ln ${line}, Col ${column}]</a>`;
                    errorContent += `❌ ${message} ${link}<br>`;

                    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('<pre>' + data.data.content.replace(/&/g, '&amp;').replace(/</g, '&lt;').replace(/>/g, '&gt;') + '</pre>');
            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;
}

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);
            });
        });
    });
});