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