xref: /plugin/mizarverifiabledocs/action.php (revision 47595f9cd8561fbcdf3e998c36a8f1c1be7116a8) 
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        }
57    }
58
59    // source用のコンパイルリクエスト処理
60    private function handleSourceCompileRequest()
61    {
62        global $INPUT;
63        $pageContent = $INPUT->post->str('content');
64        $mizarData = $this->extractMizarContent($pageContent);
65
66        if ($mizarData === null) {
67            $this->sendAjaxResponse(false, 'Mizar content not found');
68            return;
69        }
70
71        $filePath = $this->saveMizarContent($mizarData);
72
73        session_start();
74        $_SESSION['source_filepath'] = $filePath;
75
76        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
77    }
78
79    // source用のSSEリクエスト処理
80    private function handleSourceSSERequest()
81    {
82        header('Content-Type: text/event-stream');
83        header('Cache-Control: no-cache');
84
85        session_start();
86        if (!isset($_SESSION['source_filepath'])) {
87            echo "data: Mizar file path not found in session\n\n";
88            ob_flush();
89            flush();
90            return;
91        }
92
93        $filePath = $_SESSION['source_filepath'];
94        $this->streamSourceOutput($filePath);
95
96        echo "event: end\n";
97        echo "data: Compilation complete\n\n";
98        ob_flush();
99        flush();
100    }
101
102    // view用のコンパイルリクエスト処理
103    private function handleViewCompileRequest()
104    {
105        global $INPUT;
106        $content = $INPUT->post->str('content');
107
108        $filePath = $this->createTempFile($content);
109
110        session_start();
111        $_SESSION['view_filepath'] = $filePath;
112
113        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
114    }
115
116    // view用のSSEリクエスト処理
117    private function handleViewSSERequest()
118    {
119        header('Content-Type: text/event-stream');
120        header('Cache-Control: no-cache');
121
122        session_start();
123        if (!isset($_SESSION['view_filepath'])) {
124            echo "data: Mizar file path not found in session\n\n";
125            ob_flush();
126            flush();
127            return;
128        }
129
130        $filePath = $_SESSION['view_filepath'];
131        $this->streamCompileOutput($filePath);
132
133        echo "event: end\n";
134        echo "data: Compilation complete\n\n";
135        ob_flush();
136        flush();
137    }
138
139    // Mizarコンテンツの抽出
140    private function extractMizarContent($pageContent)
141    {
142        $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s';
143        preg_match_all($pattern, $pageContent, $matches, PREG_SET_ORDER);
144
145        if (empty($matches)) {
146            return null;
147        }
148
149        $fileName = trim($matches[0][1]);
150        $combinedContent = '';
151
152        foreach ($matches as $match) {
153            if (trim($match[1]) !== $fileName) {
154                return ['error' => 'File name mismatch in <mizar> tags'];
155            }
156            $combinedContent .= trim($match[2]) . "\n";
157        }
158
159        return ['fileName' => $fileName, 'content' => $combinedContent];
160    }
161
162    // Mizarコンテンツの保存
163    private function saveMizarContent($mizarData)
164    {
165        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
166        $filePath = $workPath . "/TEXT/" . $mizarData['fileName'];
167        file_put_contents($filePath, $mizarData['content']);
168        return $filePath;
169    }
170
171    // source用の出力をストリーム
172    private function streamSourceOutput($filePath)
173    {
174        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\');
175        chdir($workPath);
176
177        $command = "miz2prel " . escapeshellarg($filePath);
178        $process = proc_open($command, array(1 => array("pipe", "w")), $pipes);
179
180        if (is_resource($process)) {
181            while ($line = fgets($pipes[1])) {
182                echo "data: " . $line . "\n\n";
183                ob_flush();
184                flush();
185            }
186            fclose($pipes[1]);
187            proc_close($process);
188        }
189    }
190
191    // view用の一時ファイル作成
192    private function createTempFile($content)
193    {
194        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
195        $uniqueName = str_replace('.', '_', uniqid('tmp', true));
196        $tempFilename = $workPath . $uniqueName . ".miz";
197        file_put_contents($tempFilename, $content);
198        return $tempFilename;
199    }
200
201    //  Clear all temporary files in the TEXT folder
202        private function clearTempFiles()
203    {
204        $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/';
205        $files = glob($workPath . '*');  // TEXTフォルダ内のすべてのファイルを取得
206
207        $errors = [];
208        foreach ($files as $file) {
209            if (is_file($file)) {
210                // ファイルが使用中かどうか確認
211                if (!$this->is_file_locked($file)) {
212                    $retries = 3; // 最大3回リトライ
213                    while ($retries > 0) {
214                        if (unlink($file)) {
215                            break; // 削除成功
216                        }
217                        $retries--;
218                        sleep(1); // 1秒待ってリトライ
219                    }
220                    if ($retries === 0) {
221                        $errors[] = "Failed to delete: $file";  // 削除失敗
222                    }
223                } else {
224                    $errors[] = "File is locked: $file";  // ファイルがロックされている
225                }
226            }
227        }
228
229        if (empty($errors)) {
230            $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
231        } else {
232            $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
233        }
234    }
235
236    // ファイルがロックされているかをチェックする関数
237    private function is_file_locked($file)
238    {
239        $fileHandle = @fopen($file, "r+");
240
241        if ($fileHandle === false) {
242            return true; // ファイルが開けない、つまりロックされているかアクセス権がない
243        }
244
245        $locked = !flock($fileHandle, LOCK_EX | LOCK_NB); // ロックの取得を試みる（非ブロッキングモード）
246
247        fclose($fileHandle);
248        return $locked; // ロックが取得できなければファイルはロックされている
249    }
250
251    // コンパイル出力のストリーム
252    private function streamCompileOutput($filePath)
253    {
254        $workPath = $this->getConf('mizar_work_dir');
255        $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/';
256
257        chdir($workPath);
258
259        $tempErrFilename = str_replace('.miz', '.err', $filePath);
260        $command = "makeenv " . escapeshellarg($filePath);
261        $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes);
262
263        if (is_resource($process)) {
264            while ($line = fgets($pipes[1])) {
265                echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
266                ob_flush();
267                flush();
268            }
269            fclose($pipes[1]);
270
271            while ($line = fgets($pipes[2])) {
272                echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
273                ob_flush();
274                flush();
275            }
276            fclose($pipes[2]);
277            proc_close($process);
278
279            // エラー処理
280            if (file_exists($tempErrFilename)) {
281                $errors = [];
282                $errorLines = file($tempErrFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
283                foreach ($errorLines as $errorLine) {
284                    if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
285                        $errors[] = [
286                            'code' => intval($matches[3]),
287                            'line' => intval($matches[1]),
288                            'column' => intval($matches[2]),
289                            'message' => $this->getMizarErrorMessages($sharePath . '/mizar.msg')[intval($matches[3])] ?? 'Unknown error'
290                        ];
291                    }
292                }
293                if (!empty($errors)) {
294                    echo "event: compileErrors\n";
295                    echo "data: " . json_encode($errors) . "\n\n";
296                    ob_flush();
297                    flush();
298                    return;
299                }
300            }
301
302            // verifierの実行
303            $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/';
304            $verifierPath = escapeshellarg($exePath . "verifier");
305            if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') {
306                $verifierPath .= ".exe";
307            }
308            $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath));
309
310            $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes);
311
312            if (is_resource($verifierProcess)) {
313                while ($line = fgets($verifierPipes[1])) {
314                    echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
315                    ob_flush();
316                    flush();
317                }
318                fclose($verifierPipes[1]);
319
320                while ($line = fgets($verifierPipes[2])) {
321                    echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
322                    ob_flush();
323                    flush();
324                }
325                fclose($verifierPipes[2]);
326                proc_close($verifierProcess);
327            } else {
328                echo "data: ERROR: Failed to execute verifier command.\n\n";
329                ob_flush();
330                flush();
331            }
332        } else {
333            echo "data: ERROR: Failed to execute makeenv command.\n\n";
334            ob_flush();
335            flush();
336        }
337    }
338
339    private function getMizarErrorMessages($mizarMsgFile)
340    {
341        $errorMessages = [];
342        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
343
344        $isReadingErrorMsg = false;
345        $key = 0;
346
347        foreach ($lines as $line) {
348            if (preg_match('/# (\d+)/', $line, $matches)) {
349                $isReadingErrorMsg = true;
350                $key = intval($matches[1]);
351            } elseif ($isReadingErrorMsg) {
352                $errorMessages[$key] = $line;
353                $isReadingErrorMsg = false;
354            }
355        }
356
357        return $errorMessages;
358    }
359
360    private function sendAjaxResponse($success, $message, $data = '')
361    {
362        header('Content-Type: application/json');
363        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
364        exit;
365    }
366}
367