xref: /plugin/mizarverifiabledocs/action.php (revision 6b7e227ce526b3ffe234cde59c47249d4e050425) 
1<?php
2class action_plugin_mizarproofchecker extends \dokuwiki\Extension\ActionPlugin {
3    /** @inheritDoc */
4    function register(Doku_Event_Handler $controller) {
5        $controller->register_hook('AJAX_CALL_UNKNOWN', 'BEFORE', $this, 'handle_ajax_call');
6    }
7
8    function handle_ajax_call(Doku_Event $event, $param) {
9        unset($param); // 未使用のパラメータを無効化
10        if ($event->data === 'source_sse') {
11            $event->preventDefault();
12            $event->stopPropagation();
13            $this->handleSourceSSERequest();
14            return;
15        } elseif ($event->data === 'source_compile') {
16            $event->preventDefault();
17            $event->stopPropagation();
18            $this->handleSourceCompileRequest();
19            return;
20        } elseif ($event->data === 'view_compile') {
21            $event->preventDefault();
22            $event->stopPropagation();
23            $this->handleViewCompileRequest();
24            return;
25        } elseif ($event->data === 'view_sse') {
26            $event->preventDefault();
27            $event->stopPropagation();
28            $this->handleViewSSERequest();
29            return;
30        }
31    }
32
33    // source用のコンパイルリクエスト処理
34    private function handleSourceCompileRequest() {
35        global $INPUT;
36        $pageContent = $INPUT->post->str('content');
37
38        $mizarData = $this->extractMizarContent($pageContent);
39
40        if ($mizarData === null) {
41            $this->sendAjaxResponse(false, 'Mizar content not found');
42            return;
43        }
44
45        $filePath = $this->saveMizarContent($mizarData);
46
47        // セッションにファイルパスを保存
48        session_start();
49        $_SESSION['source_filepath'] = $filePath;
50
51        // コンパイルが成功したことをクライアントに通知
52        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
53    }
54
55    // source用のSSEリクエスト処理
56    private function handleSourceSSERequest() {
57        header('Content-Type: text/event-stream');
58        header('Cache-Control: no-cache');
59
60        session_start();
61        if (!isset($_SESSION['source_filepath'])) {
62            echo "data: Mizar file path not found in session\n\n";
63            ob_flush();
64            flush();
65            return;
66        }
67
68        $filePath = $_SESSION['source_filepath'];
69
70        // miz2prelコマンドを実行し、結果をストリーミング
71        $this->streamSourceOutput($filePath);
72
73        echo "event: end\n";
74        echo "data: Compilation complete\n\n";
75        ob_flush();
76        flush();
77    }
78
79    private function extractMizarContent($pageContent) {
80        $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s';
81        preg_match_all($pattern, $pageContent, $matches, PREG_SET_ORDER);
82
83        if (empty($matches)) {
84            return null; // <mizar>タグが見つからない場合
85        }
86
87        $fileName = trim($matches[0][1]); // 最初の<mizar>タグからファイル名を取得
88        $combinedContent = '';
89
90        foreach ($matches as $match) {
91            // 各<mizar>タグのファイル名が一致することを確認
92            if (trim($match[1]) !== $fileName) {
93                return ['error' => 'File name mismatch in <mizar> tags'];
94            }
95
96            // 各<mizar>タグの内容を連結
97            $combinedContent .= trim($match[2]) . "\n";
98        }
99
100        return ['fileName' => $fileName, 'content' => $combinedContent];
101    }
102
103    private function saveMizarContent($mizarData) {
104        // ワークパスを取得し、末尾にスラッシュやバックスラッシュがあれば削除
105        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
106        $filePath = $workPath . "/TEXT/" . $mizarData['fileName'];
107        file_put_contents($filePath, $mizarData['content']);
108        return $filePath;
109    }
110
111    private function streamSourceOutput($filePath) {
112        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
113        chdir($workPath);
114
115        $command = "miz2prel " . escapeshellarg($filePath);
116        $process = proc_open($command, array(1 => array("pipe", "w")), $pipes);
117
118        if (is_resource($process)) {
119            while ($line = fgets($pipes[1])) {
120                echo "data: " . $line . "\n\n";
121                ob_flush();
122                flush();
123            }
124            fclose($pipes[1]);
125            proc_close($process);
126        }
127    }
128
129    // view用のコンパイルリクエスト処理
130    private function handleViewCompileRequest() {
131        global $INPUT;
132        $content = $INPUT->post->str('content');
133
134        // 一時ファイルの作成
135        $filePath = $this->createTempFile($content);
136
137        // セッションにファイルパスを保存
138        session_start();
139        $_SESSION['view_filepath'] = $filePath;
140
141        // コンパイル準備完了をレスポンス
142        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
143    }
144
145    // view用のSSEリクエスト処理
146    private function handleViewSSERequest() {
147        header('Content-Type: text/event-stream');
148        header('Cache-Control: no-cache');
149
150        session_start();
151        if (!isset($_SESSION['view_filepath'])) {
152            echo "data: Mizar file path not found in session\n\n";
153            ob_flush();
154            flush();
155            return;
156        }
157
158        $filePath = $_SESSION['view_filepath'];
159
160        // コンパイル結果をストリーミング
161        $this->streamCompileOutput($filePath);
162
163        echo "event: end\n";
164        echo "data: Compilation complete\n\n";
165        ob_flush();
166        flush();
167    }
168
169    // 一時ファイル作成はviewでのみ使用
170    private function createTempFile($content) {
171        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
172        $uniqueName = str_replace('.', '_', uniqid('mizar', true));
173        $tempFilename = $workPath . $uniqueName . ".miz";
174        file_put_contents($tempFilename, $content);
175        return $tempFilename;
176    }
177
178    private function streamCompileOutput($filePath) {
179        $workPath = $this->getConf('mizar_work_dir');
180        $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/';
181
182        chdir($workPath);
183
184        $tempErrFilename = str_replace('.miz', '.err', $filePath);
185        $command = "makeenv " . escapeshellarg($filePath);
186        $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes);
187
188        if (is_resource($process)) {
189            while ($line = fgets($pipes[1])) {
190                echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
191                ob_flush();
192                flush();
193            }
194            fclose($pipes[1]);
195
196            while ($line = fgets($pipes[2])) {
197                echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
198                ob_flush();
199                flush();
200            }
201            fclose($pipes[2]);
202            proc_close($process);
203
204            if (file_exists($tempErrFilename)) {
205                $errors = [];
206                $errorLines = file($tempErrFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
207                foreach ($errorLines as $errorLine) {
208                    if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
209                        $errors[] = [
210                            'code' => intval($matches[3]),
211                            'line' => intval($matches[1]),
212                            'column' => intval($matches[2]),
213                            'message' => $this->getMizarErrorMessages($sharePath . '/mizar.msg')[intval($matches[3])] ?? 'Unknown error'
214                        ];
215                    }
216                }
217                if (!empty($errors)) {
218                    echo "event: compileErrors\n";
219                    echo "data: " . json_encode($errors) . "\n\n";
220                    ob_flush();
221                    flush();
222                    return;
223                }
224            }
225
226            // verifierの実行
227            $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/';
228            $verifierPath = escapeshellarg($exePath . "verifier");
229            if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') {
230                $verifierPath .= ".exe";
231            }
232            $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath));
233
234            $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes);
235
236            if (is_resource($verifierProcess)) {
237                while ($line = fgets($verifierPipes[1])) {
238                    echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
239                    ob_flush();
240                    flush();
241                }
242                fclose($verifierPipes[1]);
243
244                while ($line = fgets($verifierPipes[2])) {
245                    echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
246                    ob_flush();
247                    flush();
248                }
249                fclose($verifierPipes[2]);
250                proc_close($verifierProcess);
251
252                if (file_exists($tempErrFilename)) {
253                    $errors = [];
254                    $errorLines = file($tempErrFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
255                    foreach ($errorLines as $errorLine) {
256                        if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
257                            $errors[] = [
258                                'code' => intval($matches[3]),
259                                'line' => intval($matches[1]),
260                                'column' => intval($matches[2]),
261                                'message' => $this->getMizarErrorMessages($workPath . '/MIZAR/mizar.msg')[intval($matches[3])] ?? 'Unknown error'
262                            ];
263                        }
264                    }
265                    echo "event: compileErrors\n";
266                    echo "data: " . json_encode($errors) . "\n\n";
267                    ob_flush();
268                    flush();
269                }
270            } else {
271                echo "data: ERROR: Failed to execute verifier command.\n\n";
272                ob_flush();
273                flush();
274            }
275        } else {
276            echo "data: ERROR: Failed to execute makeenv command.\n\n";
277            ob_flush();
278            flush();
279        }
280    }
281
282    // Mizarエラーメッセージを取得するメソッド
283    private function getMizarErrorMessages($mizarMsgFile) {
284        $errorMessages = [];
285        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
286
287        $isReadingErrorMsg = false;
288        $key = 0;
289
290        foreach ($lines as $line) {
291            if (preg_match('/# (\d+)/', $line, $matches)) {
292                $isReadingErrorMsg = true;
293                $key = intval($matches[1]);
294            } elseif ($isReadingErrorMsg) {
295                $errorMessages[$key] = $line;
296                $isReadingErrorMsg = false;
297            }
298        }
299
300        return $errorMessages;
301    }
302
303    private function sendAjaxResponse($success, $message, $data = '') {
304        header('Content-Type: application/json');
305        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
306        exit;
307    }
308}
309