xref: /plugin/mizarverifiabledocs/action.php (revision 4f65af2c978c8b810c87fd11fcd551c84c6abad5) 
1<?php
2
3use dokuwiki\Extension\ActionPlugin;
4use dokuwiki\Extension\EventHandler;
5use dokuwiki\Extension\Event;
6
7/**
8 * DokuWiki Plugin Mizar Verifiable Docs (Action Component)
9 *
10 * @license GPL 2 http://www.gnu.org/licenses/gpl-2.0.html
11 * @author  Yamada, M.
12 */
13
14class action_plugin_mizarverifiabledocs extends ActionPlugin
15{
16    /**
17     * Registers a callback function for a given event
18     *
19     * @param EventHandler $controller DokuWiki's event controller object
20     * @return void
21     */
22    public function register(EventHandler $controller)
23    {
24        $controller->register_hook('AJAX_CALL_UNKNOWN', 'BEFORE', $this, 'handle_ajax_call');
25        $controller->register_hook('TPL_CONTENT_DISPLAY', 'BEFORE', $this, 'handle_tpl_content_display');
26    }
27
28    /**
29     * Handles the TPL_CONTENT_DISPLAY event to insert "Hide All" button
30     *
31     * @param Event $event
32     * @param mixed $_param Unused parameter
33     * @return void
34     */
35    public function handle_tpl_content_display(Event $event, $_param)
36    {
37        // データが文字列かどうか確認
38        if (!is_string($event->data)) {
39            error_log('handle_tpl_content_display: data is not a string! ' . print_r($event->data, true));
40            return;
41        }
42
43        $html = $event->data;
44
45        // "mizarWrapper" クラスが存在するか確認
46        if (strpos($html, 'mizarWrapper') !== false) {
47            // 既にボタンが挿入されているか確認（複数回挿入しないため）
48            if (strpos($html, 'id="hideAllButton"') === false) {
49                $buttonHtml = '<div class="hideAllContainer">'
50                            . '<button id="hideAllButton" class="hide-all-button">Hide All</button>'
51                            . '<button id="showAllButton" class="hide-all-button" style="display:none;">Show All</button>'
52                            . '</div>';
53
54                // 先頭にボタンを挿入
55                $html = $buttonHtml . $html;
56                $event->data = $html;
57
58                // デバッグ用ログ
59                error_log('handle_tpl_content_display: "Hide All" ボタンを挿入しました。');
60            } else {
61                // ボタンが既に存在する場合
62                error_log('handle_tpl_content_display: "Hide All" ボタンは既に存在します。');
63            }
64        }
65    }
66
67    /**
68     * Handles AJAX requests
69     *
70     * @param Event $event
71     * @param $param
72     */
73    public function handle_ajax_call(Event $event, $param)
74    {
75        unset($param); // 未使用のパラメータを無効化
76
77        switch ($event->data) {
78            case 'clear_temp_files':
79                $event->preventDefault();
80                $event->stopPropagation();
81                $this->clearTempFiles();
82                break;
83            case 'source_sse':
84                $event->preventDefault();
85                $event->stopPropagation();
86                $this->handleSourceSSERequest();
87                break;
88            case 'source_compile':
89                $event->preventDefault();
90                $event->stopPropagation();
91                $this->handleSourceCompileRequest();
92                break;
93            case 'view_compile':
94                $event->preventDefault();
95                $event->stopPropagation();
96                $this->handleViewCompileRequest();
97                break;
98            case 'view_sse':
99                $event->preventDefault();
100                $event->stopPropagation();
101                $this->handleViewSSERequest();
102                break;
103            case 'create_combined_file':
104                $event->preventDefault();
105                $event->stopPropagation();
106                $this->handle_create_combined_file();
107                break;
108        }
109    }
110
111    // source用のコンパイルリクエスト処理
112    private function handleSourceCompileRequest()
113    {
114        global $INPUT;
115        $pageContent = $INPUT->post->str('content');
116        $mizarData = $this->extractMizarContent($pageContent);
117
118        // エラーチェックを追加
119        if ($mizarData === null) {
120            $this->sendAjaxResponse(false, 'Mizar content not found');
121            return;
122        } elseif (isset($mizarData['error'])) {
123            $this->sendAjaxResponse(false, $mizarData['error']);
124            return;
125        }
126
127        $filePath = $this->saveMizarContent($mizarData);
128
129        session_start();
130        $_SESSION['source_filepath'] = $filePath;
131
132        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
133    }
134
135    // source用のSSEリクエスト処理
136    private function handleSourceSSERequest()
137    {
138        header('Content-Type: text/event-stream');
139        header('Cache-Control: no-cache');
140
141        session_start();
142        if (!isset($_SESSION['source_filepath'])) {
143            echo "data: Mizar file path not found in session\n\n";
144            ob_flush();
145            flush();
146            return;
147        }
148
149        $filePath = $_SESSION['source_filepath'];
150        $this->streamSourceOutput($filePath);
151
152        echo "event: end\n";
153        echo "data: Compilation complete\n\n";
154        ob_flush();
155        flush();
156    }
157
158    // view用のコンパイルリクエスト処理
159    private function handleViewCompileRequest()
160    {
161        global $INPUT;
162        $content = $INPUT->post->str('content');
163
164        $filePath = $this->createTempFile($content);
165
166        session_start();
167        $_SESSION['view_filepath'] = $filePath;
168
169        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
170    }
171
172    // view用のSSEリクエスト処理
173    private function handleViewSSERequest()
174    {
175        header('Content-Type: text/event-stream');
176        header('Cache-Control: no-cache');
177
178        session_start();
179        if (!isset($_SESSION['view_filepath'])) {
180            echo "data: Mizar file path not found in session\n\n";
181            ob_flush();
182            flush();
183            return;
184        }
185
186        $filePath = $_SESSION['view_filepath'];
187        $this->streamViewCompileOutput($filePath);
188
189        echo "event: end\n";
190        echo "data: Compilation complete\n\n";
191        ob_flush();
192        flush();
193    }
194
195    // Mizarコンテンツの抽出
196    private function extractMizarContent($pageContent)
197    {
198        $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s';
199        preg_match_all($pattern, $pageContent, $matches, PREG_SET_ORDER);
200
201        if (empty($matches)) {
202            return null;
203        }
204
205        // 最初のファイル名を取得し、拡張子を除去
206        $fileName = trim($matches[0][1]);
207        $fileNameWithoutExt = preg_replace('/\.miz$/i', '', $fileName);
208
209        // ファイル名のバリデーションを追加
210        if (!$this->isValidFileName($fileNameWithoutExt)) {
211            return ['error' => "Invalid characters in file name: '{$fileNameWithoutExt}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."];
212        }
213
214        $combinedContent = '';
215
216        foreach ($matches as $match) {
217            $currentFileName = trim($match[1]);
218            $currentFileNameWithoutExt = preg_replace('/\.miz$/i', '', $currentFileName);
219
220            if ($currentFileNameWithoutExt !== $fileNameWithoutExt) {
221                return ['error' => "File name mismatch in <mizar> tags: '{$fileNameWithoutExt}' and '{$currentFileNameWithoutExt}'"];
222            }
223
224            // バリデーションを各ファイル名にも適用
225            if (!$this->isValidFileName($currentFileNameWithoutExt)) {
226                return ['error' => "Invalid characters in file name: '{$currentFileNameWithoutExt}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."];
227            }
228
229            $combinedContent .= trim($match[2]) . "\n";
230        }
231
232        // ファイル名に拡張子を付加
233        $fullFileName = $fileNameWithoutExt . '.miz';
234
235        return ['fileName' => $fullFileName, 'content' => $combinedContent];
236    }
237
238    // ファイル名のバリデーション関数を追加
239    private function isValidFileName($fileName)
240    {
241        // ファイル名の長さをチェック（最大8文字）
242        if (strlen($fileName) > 8) {
243            return false;
244        }
245
246        // 許可される文字のみを含むかチェック
247        if (!preg_match('/^[A-Za-z0-9_\']+$/', $fileName)) {
248            return false;
249        }
250
251        return true;
252    }
253
254    // Mizarコンテンツの保存
255    private function saveMizarContent($mizarData)
256    {
257        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
258        $filePath = $workPath . "/TEXT/" . $mizarData['fileName'];
259        file_put_contents($filePath, $mizarData['content']);
260        return $filePath;
261    }
262
263    // source用の出力をストリーム
264    private function streamSourceOutput($filePath)
265    {
266        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
267        chdir($workPath);
268
269        $command = "miz2prel " . escapeshellarg($filePath);
270        $process = proc_open($command, array(1 => array("pipe", "w")), $pipes);
271
272        if (is_resource($process)) {
273            while ($line = fgets($pipes[1])) {
274                echo "data: " . $line . "\n\n";
275                ob_flush();
276                flush();
277            }
278            fclose($pipes[1]);
279
280            // エラー処理の追加
281            $errFilename = str_replace('.miz', '.err', $filePath);
282            if ($this->handleCompilationErrors($errFilename, rtrim($this->getConf('mizar_share_dir'), '/\\') . '/mizar.msg')) {
283                // エラーがあった場合は処理を終了
284                proc_close($process);
285                return;
286            }
287
288            proc_close($process);
289        }
290    }
291
292    // view用の一時ファイル作成
293    private function createTempFile($content)
294    {
295        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
296        $uniqueName = str_replace('.', '_', uniqid('tmp', true));
297        $tempFilename = $workPath . $uniqueName . ".miz";
298        file_put_contents($tempFilename, $content);
299        return $tempFilename;
300    }
301
302    // 一時ファイルの削除
303    private function clearTempFiles()
304    {
305        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
306        $files = glob($workPath . '*');  // TEXTフォルダ内のすべてのファイルを取得
307
308        $errors = [];
309        foreach ($files as $file) {
310            if (is_file($file)) {
311                // ファイルが使用中かどうか確認
312                if (!$this->is_file_locked($file)) {
313                    $retries = 3; // 最大3回リトライ
314                    while ($retries > 0) {
315                        if (unlink($file)) {
316                            break; // 削除成功
317                        }
318                        $errors[] = "Error deleting $file: " . error_get_last()['message'];
319                        $retries--;
320                        sleep(1); // 1秒待ってリトライ
321                    }
322                    if ($retries === 0) {
323                        $errors[] = "Failed to delete: $file";  // 削除失敗
324                    }
325                } else {
326                    $errors[] = "File is locked: $file";  // ファイルがロックされている
327                }
328            }
329        }
330
331        if (empty($errors)) {
332            $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
333        } else {
334            $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
335        }
336    }
337
338    // ファイルがロックされているかをチェックする関数
339    private function is_file_locked($file)
340    {
341        $fileHandle = @fopen($file, "r+");
342
343        if ($fileHandle === false) {
344            return true; // ファイルが開けない、つまりロックされているかアクセス権がない
345        }
346
347        $locked = !flock($fileHandle, LOCK_EX | LOCK_NB); // ロックの取得を試みる（非ブロッキングモード）
348
349        fclose($fileHandle);
350        return $locked; // ロックが取得できなければファイルはロックされている
351    }
352
353    // View用コンパイル出力のストリーム
354    private function streamViewCompileOutput($filePath)
355    {
356        $workPath = $this->getConf('mizar_work_dir');
357        $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/';
358
359        chdir($workPath);
360
361        $errFilename = str_replace('.miz', '.err', $filePath);
362        $command = "makeenv " . escapeshellarg($filePath);
363        $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes);
364
365        if (is_resource($process)) {
366            while ($line = fgets($pipes[1])) {
367                echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
368                ob_flush();
369                flush();
370            }
371            fclose($pipes[1]);
372
373            while ($line = fgets($pipes[2])) {
374                echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
375                ob_flush();
376                flush();
377            }
378            fclose($pipes[2]);
379            proc_close($process);
380
381            // makeenvのエラー処理
382            if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
383                return;
384            }
385
386            // verifierの実行
387            $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/';
388            $verifierPath = escapeshellarg($exePath . "verifier");
389            if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') {
390                $verifierPath .= ".exe";
391            }
392            $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath));
393
394            $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes);
395
396            if (is_resource($verifierProcess)) {
397                while ($line = fgets($verifierPipes[1])) {
398                    echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
399                    ob_flush();
400                    flush();
401                }
402                fclose($verifierPipes[1]);
403
404                while ($line = fgets($verifierPipes[2])) {
405                    echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
406                    ob_flush();
407                    flush();
408                }
409                fclose($verifierPipes[2]);
410                proc_close($verifierProcess);
411
412                // verifierのエラー処理
413                if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
414                    return;
415                }
416            } else {
417                echo "data: ERROR: Failed to execute verifier command.\n\n";
418                ob_flush();
419                flush();
420            }
421        } else {
422            echo "data: ERROR: Failed to execute makeenv command.\n\n";
423            ob_flush();
424            flush();
425        }
426    }
427
428    private function getMizarErrorMessages($mizarMsgFile)
429    {
430        $errorMessages = [];
431        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
432
433        $isReadingErrorMsg = false;
434        $key = 0;
435
436        foreach ($lines as $line) {
437            if (preg_match('/# (\d+)/', $line, $matches)) {
438                $isReadingErrorMsg = true;
439                $key = intval($matches[1]);
440            } elseif ($isReadingErrorMsg) {
441                $errorMessages[$key] = $line;
442                $isReadingErrorMsg = false;
443            }
444        }
445
446        return $errorMessages;
447    }
448
449    private function sendAjaxResponse($success, $message, $data = '')
450    {
451        header('Content-Type: application/json');
452        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
453        exit;
454    }
455
456    private function handleCompilationErrors($errFilename, $mizarMsgFilePath)
457    {
458        if (file_exists($errFilename)) {
459            $errors = [];
460            $errorLines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
461            foreach ($errorLines as $errorLine) {
462                if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
463                    $errorCode = intval($matches[3]);
464                    $errors[] = [
465                        'code' => $errorCode,
466                        'line' => intval($matches[1]),
467                        'column' => intval($matches[2]),
468                        'message' => $this->getMizarErrorMessages($mizarMsgFilePath)[$errorCode] ?? 'Unknown error'
469                    ];
470                }
471            }
472            if (!empty($errors)) {
473                echo "event: compileErrors\n";
474                echo "data: " . json_encode($errors) . "\n\n";
475                ob_flush();
476                flush();
477                return true;
478            }
479        }
480        return false;
481    }
482
483    private function handle_create_combined_file()
484    {
485        global $INPUT;
486
487        // 投稿されたコンテンツを取得
488        $combinedContent = $INPUT->post->str('content');
489        $filename = $INPUT->post->str('filename', 'combined_file.miz'); // デフォルトのファイル名を指定
490
491        // ファイルを保存せず、コンテンツを直接返す
492        if (!empty($combinedContent)) {
493            // ファイルの内容をレスポンスで返す（PHP側でファイルを作成しない）
494            $this->sendAjaxResponse(true, 'File created successfully', [
495                'filename' => $filename,
496                'content' => $combinedContent
497            ]);
498            error_log("File content sent: " . $filename);
499        } else {
500            $this->sendAjaxResponse(false, 'Content is empty, no file created');
501        }
502    }
503}
504