xref: /plugin/mizarverifiabledocs/action.php (revision fcd231cde6b357b64711d8d52974edea8539d616) 
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        chdir($workPath);
267
268        $command = "miz2prel " . escapeshellarg($filePath);
269        $process = proc_open($command, array(1 => array("pipe", "w")), $pipes);
270
271        if (is_resource($process)) {
272            while ($line = fgets($pipes[1])) {
273                echo "data: " . $line . "\n\n";
274                ob_flush();
275                flush();
276            }
277            fclose($pipes[1]);
278
279            // エラー処理の追加
280            $errFilename = str_replace('.miz', '.err', $filePath);
281            if ($this->handleCompilationErrors($errFilename, rtrim($this->getConf('mizar_share_dir'), '/\\') . '/mizar.msg')) {
282                // エラーがあった場合は処理を終了
283                proc_close($process);
284                return;
285            }
286
287            proc_close($process);
288        }
289    }
290
291    // view用の一時ファイル作成
292    private function createTempFile($content)
293    {
294        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
295        $uniqueName = str_replace('.', '_', uniqid('tmp', true));
296        $tempFilename = $workPath . $uniqueName . ".miz";
297        file_put_contents($tempFilename, $content);
298        return $tempFilename;
299    }
300
301    // 一時ファイルの削除
302    private function clearTempFiles()
303    {
304        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
305        $files = glob($workPath . '*');  // TEXTフォルダ内のすべてのファイルを取得
306
307        $errors = [];
308        foreach ($files as $file) {
309            if (is_file($file)) {
310                // ファイルが使用中かどうか確認
311                if (!$this->is_file_locked($file)) {
312                    $retries = 3; // 最大3回リトライ
313                    while ($retries > 0) {
314                        if (unlink($file)) {
315                            break; // 削除成功
316                        }
317                        $errors[] = "Error deleting $file: " . error_get_last()['message'];
318                        $retries--;
319                        sleep(1); // 1秒待ってリトライ
320                    }
321                    if ($retries === 0) {
322                        $errors[] = "Failed to delete: $file";  // 削除失敗
323                    }
324                } else {
325                    $errors[] = "File is locked: $file";  // ファイルがロックされている
326                }
327            }
328        }
329
330        if (empty($errors)) {
331            $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
332        } else {
333            $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
334        }
335    }
336
337    // ファイルがロックされているかをチェックする関数
338    private function is_file_locked($file)
339    {
340        $fileHandle = @fopen($file, "r+");
341
342        if ($fileHandle === false) {
343            return true; // ファイルが開けない、つまりロックされているかアクセス権がない
344        }
345
346        $locked = !flock($fileHandle, LOCK_EX | LOCK_NB); // ロックの取得を試みる（非ブロッキングモード）
347
348        fclose($fileHandle);
349        return $locked; // ロックが取得できなければファイルはロックされている
350    }
351
352    // View用コンパイル出力のストリーム
353    private function streamViewCompileOutput($filePath)
354    {
355        $workPath = $this->getConf('mizar_work_dir');
356        $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/';
357
358        chdir($workPath);
359
360        $errFilename = str_replace('.miz', '.err', $filePath);
361        $command = "makeenv " . escapeshellarg($filePath);
362        $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes);
363
364        if (is_resource($process)) {
365            while ($line = fgets($pipes[1])) {
366                echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
367                ob_flush();
368                flush();
369            }
370            fclose($pipes[1]);
371
372            while ($line = fgets($pipes[2])) {
373                echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
374                ob_flush();
375                flush();
376            }
377            fclose($pipes[2]);
378            proc_close($process);
379
380            // makeenvのエラー処理
381            if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
382                return;
383            }
384
385            // verifierの実行
386            $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/';
387            $verifierPath = escapeshellarg($exePath . "verifier");
388            if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') {
389                $verifierPath .= ".exe";
390            }
391            $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath));
392
393            $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes);
394
395            if (is_resource($verifierProcess)) {
396                while ($line = fgets($verifierPipes[1])) {
397                    echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
398                    ob_flush();
399                    flush();
400                }
401                fclose($verifierPipes[1]);
402
403                while ($line = fgets($verifierPipes[2])) {
404                    echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
405                    ob_flush();
406                    flush();
407                }
408                fclose($verifierPipes[2]);
409                proc_close($verifierProcess);
410
411                // verifierのエラー処理
412                if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
413                    return;
414                }
415            } else {
416                echo "data: ERROR: Failed to execute verifier command.\n\n";
417                ob_flush();
418                flush();
419            }
420        } else {
421            echo "data: ERROR: Failed to execute makeenv command.\n\n";
422            ob_flush();
423            flush();
424        }
425    }
426
427    private function getMizarErrorMessages($mizarMsgFile)
428    {
429        $errorMessages = [];
430        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
431
432        $isReadingErrorMsg = false;
433        $key = 0;
434
435        foreach ($lines as $line) {
436            if (preg_match('/# (\d+)/', $line, $matches)) {
437                $isReadingErrorMsg = true;
438                $key = intval($matches[1]);
439            } elseif ($isReadingErrorMsg) {
440                $errorMessages[$key] = $line;
441                $isReadingErrorMsg = false;
442            }
443        }
444
445        return $errorMessages;
446    }
447
448    private function sendAjaxResponse($success, $message, $data = '')
449    {
450        header('Content-Type: application/json');
451        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
452        exit;
453    }
454
455    private function handleCompilationErrors($errFilename, $mizarMsgFilePath)
456    {
457        if (file_exists($errFilename)) {
458            $errors = [];
459            $errorLines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
460            foreach ($errorLines as $errorLine) {
461                if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
462                    $errorCode = intval($matches[3]);
463                    $errors[] = [
464                        'code' => $errorCode,
465                        'line' => intval($matches[1]),
466                        'column' => intval($matches[2]),
467                        'message' => $this->getMizarErrorMessages($mizarMsgFilePath)[$errorCode] ?? 'Unknown error'
468                    ];
469                }
470            }
471            if (!empty($errors)) {
472                echo "event: compileErrors\n";
473                echo "data: " . json_encode($errors) . "\n\n";
474                ob_flush();
475                flush();
476                return true;
477            }
478        }
479        return false;
480    }
481
482    private function handle_create_combined_file()
483    {
484        global $INPUT;
485
486        // 投稿されたコンテンツを取得
487        $combinedContent = $INPUT->post->str('content');
488        $filename = $INPUT->post->str('filename', 'combined_file.miz'); // デフォルトのファイル名を指定
489
490        // ファイルを保存せず、コンテンツを直接返す
491        if (!empty($combinedContent)) {
492            // ファイルの内容をレスポンスで返す（PHP側でファイルを作成しない）
493            $this->sendAjaxResponse(true, 'File created successfully', [
494                'filename' => $filename,
495                'content' => $combinedContent
496            ]);
497            error_log("File content sent: " . $filename);
498        } else {
499            $this->sendAjaxResponse(false, 'Content is empty, no file created');
500        }
501    }
502}
503