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