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