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