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