xref: /plugin/mizarverifiabledocs/action.php (revision 5cbf3a5300a651c7fd7958742a36e6290b0f78b2) 
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                        $errors[] = "Error deleting $file: " . error_get_last()['message'];
218                        $retries--;
219                        sleep(1); // 1秒待ってリトライ
220                    }
221                    if ($retries === 0) {
222                        $errors[] = "Failed to delete: $file";  // 削除失敗
223                    }
224                } else {
225                    $errors[] = "File is locked: $file";  // ファイルがロックされている
226                }
227            }
228        }
229
230        if (empty($errors)) {
231            $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
232        } else {
233            $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
234        }
235    }
236
237    // ファイルがロックされているかをチェックする関数
238    private function is_file_locked($file)
239    {
240        $fileHandle = @fopen($file, "r+");
241
242        if ($fileHandle === false) {
243            return true; // ファイルが開けない、つまりロックされているかアクセス権がない
244        }
245
246        $locked = !flock($fileHandle, LOCK_EX | LOCK_NB); // ロックの取得を試みる（非ブロッキングモード）
247
248        fclose($fileHandle);
249        return $locked; // ロックが取得できなければファイルはロックされている
250    }
251
252    // コンパイル出力のストリーム
253    private function streamCompileOutput($filePath)
254    {
255        $workPath = $this->getConf('mizar_work_dir');
256        $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/';
257
258        chdir($workPath);
259
260        $tempErrFilename = str_replace('.miz', '.err', $filePath);
261        $command = "makeenv " . escapeshellarg($filePath);
262        $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes);
263
264        if (is_resource($process)) {
265            while ($line = fgets($pipes[1])) {
266                echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
267                ob_flush();
268                flush();
269            }
270            fclose($pipes[1]);
271
272            while ($line = fgets($pipes[2])) {
273                echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
274                ob_flush();
275                flush();
276            }
277            fclose($pipes[2]);
278            proc_close($process);
279
280            // エラー処理
281            if (file_exists($tempErrFilename)) {
282                $errors = [];
283                $errorLines = file($tempErrFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
284                foreach ($errorLines as $errorLine) {
285                    if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) {
286                        $errors[] = [
287                            'code' => intval($matches[3]),
288                            'line' => intval($matches[1]),
289                            'column' => intval($matches[2]),
290                            'message' => $this->getMizarErrorMessages($sharePath . '/mizar.msg')[intval($matches[3])] ?? 'Unknown error'
291                        ];
292                    }
293                }
294                if (!empty($errors)) {
295                    echo "event: compileErrors\n";
296                    echo "data: " . json_encode($errors) . "\n\n";
297                    ob_flush();
298                    flush();
299                    return;
300                }
301            }
302
303            // verifierの実行
304            $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/';
305            $verifierPath = escapeshellarg($exePath . "verifier");
306            if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') {
307                $verifierPath .= ".exe";
308            }
309            $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath));
310
311            $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes);
312
313            if (is_resource($verifierProcess)) {
314                while ($line = fgets($verifierPipes[1])) {
315                    echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
316                    ob_flush();
317                    flush();
318                }
319                fclose($verifierPipes[1]);
320
321                while ($line = fgets($verifierPipes[2])) {
322                    echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n";
323                    ob_flush();
324                    flush();
325                }
326                fclose($verifierPipes[2]);
327                proc_close($verifierProcess);
328            } else {
329                echo "data: ERROR: Failed to execute verifier command.\n\n";
330                ob_flush();
331                flush();
332            }
333        } else {
334            echo "data: ERROR: Failed to execute makeenv command.\n\n";
335            ob_flush();
336            flush();
337        }
338    }
339
340    private function getMizarErrorMessages($mizarMsgFile)
341    {
342        $errorMessages = [];
343        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
344
345        $isReadingErrorMsg = false;
346        $key = 0;
347
348        foreach ($lines as $line) {
349            if (preg_match('/# (\d+)/', $line, $matches)) {
350                $isReadingErrorMsg = true;
351                $key = intval($matches[1]);
352            } elseif ($isReadingErrorMsg) {
353                $errorMessages[$key] = $line;
354                $isReadingErrorMsg = false;
355            }
356        }
357
358        return $errorMessages;
359    }
360
361    private function sendAjaxResponse($success, $message, $data = '')
362    {
363        header('Content-Type: application/json');
364        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
365        exit;
366    }
367}