xref: /plugin/mizarverifiabledocs/action.php (revision e813ba0eff7bb751c51a2fb3ab0a0028c280df1e) 
1<?php
2
3use dokuwiki\Extension\ActionPlugin;
4use dokuwiki\Extension\EventHandler;
5use dokuwiki\Extension\Event;
6
7/**
8 * DokuWiki Plugin Mizar Verifiable Docs (Action Component)
9 * @license GPL 2 http://www.gnu.org/licenses/gpl-2.0.html
10 * @author  Yamada
11 */
12class action_plugin_mizarverifiabledocs extends ActionPlugin
13{
14    /* ===================== Register ===================== */
15
16    public function register(EventHandler $controller)
17    {
18        $controller->register_hook('AJAX_CALL_UNKNOWN', 'BEFORE', $this, 'handle_ajax_call');
19        $controller->register_hook('TPL_CONTENT_DISPLAY', 'BEFORE', $this, 'handle_tpl_content_display');
20    }
21
22    public function handle_tpl_content_display(Event $event, $_param)
23    {
24        if (!is_string($event->data)) return;
25
26        $html = $event->data;
27        if (strpos($html, 'mizarWrapper') !== false && strpos($html, 'id="hideAllButton"') === false) {
28            $buttonHtml = '<div class="hideAllContainer">'
29                        . '<button id="hideAllButton" class="hide-all-button">Hide All</button>'
30                        . '<button id="showAllButton" class="hide-all-button" style="display:none;">Show All</button>'
31                        . '<button id="resetAllButton" class="reset-all-button">Reset All</button>'
32                        . '</div>';
33            $event->data = $buttonHtml . $html;
34        }
35    }
36
37    public function handle_ajax_call(Event $event, $param)
38    {
39        unset($param);
40        switch ($event->data) {
41            case 'clear_temp_files':
42                $event->preventDefault(); $event->stopPropagation();
43                $this->clearTempFiles(); break;
44
45            case 'source_compile':
46                $event->preventDefault(); $event->stopPropagation();
47                $this->handleSourceCompileRequest(); break;
48
49            case 'source_sse':
50                $event->preventDefault(); $event->stopPropagation();
51                $this->handleSourceSSERequest(); break;
52
53            case 'view_compile':
54                $event->preventDefault(); $event->stopPropagation();
55                $this->handleViewCompileRequest(); break;
56
57            case 'view_sse':
58                $event->preventDefault(); $event->stopPropagation();
59                $this->handleViewSSERequest(); break;
60
61            case 'create_combined_file':
62                $event->preventDefault(); $event->stopPropagation();
63                $this->handle_create_combined_file(); break;
64
65            case 'view_graph':
66                $event->preventDefault(); $event->stopPropagation();
67                $this->handleViewGraphRequest(); break;
68        }
69    }
70
71    /* ===================== Helpers ===================== */
72
73    private function isWindows(): bool {
74        return strncasecmp(PHP_OS, 'WIN', 3) === 0;
75    }
76
77    /** 設定→未設定なら htdocs(= DOKU_INC の1つ上) 相対にフォールバックして正規化 */
78    private function resolvePaths(): array
79    {
80        // DokuWiki ルート（末尾スラッシュなしに正規化）
81        $dokuroot = rtrim(realpath(DOKU_INC), '/\\');
82
83        // htdocs を「dokuwiki の 1つ上」から求める
84        $htdocs = realpath($dokuroot . DIRECTORY_SEPARATOR . '..');
85        if ($htdocs === false) $htdocs = dirname($dokuroot);
86
87        $defM = $htdocs . DIRECTORY_SEPARATOR . 'MIZAR';
88        $defW = $htdocs . DIRECTORY_SEPARATOR . 'work';
89
90        // 設定値取得（空ならフォールバック）。相対指定が来たら htdocs 基準に解決
91        $exe   = trim((string)$this->getConf('mizar_exe_dir'));
92        $share = trim((string)$this->getConf('mizar_share_dir'));
93        $work  = trim((string)$this->getConf('mizar_work_dir'));
94
95        $isAbs = function(string $p): bool {
96            // Windowsドライブ/UNC/Unix ざっくり対応
97            return $p !== '' && (preg_match('~^[A-Za-z]:[\\/]|^\\\\\\\\|^/~', $p) === 1);
98        };
99
100        if ($exe   !== '' && !$isAbs($exe))   $exe   = $htdocs . DIRECTORY_SEPARATOR . $exe;
101        if ($share !== '' && !$isAbs($share)) $share = $htdocs . DIRECTORY_SEPARATOR . $share;
102        if ($work  !== '' && !$isAbs($work))  $work  = $htdocs . DIRECTORY_SEPARATOR . $work;
103
104        $exe   = rtrim($exe   ?: $defM, '/\\');
105        $share = rtrim($share ?: $defM, '/\\');
106        $work  = rtrim($work  ?: $defW, '/\\');
107
108        return ['exe' => $exe, 'share' => $share, 'work' => $work];
109    }
110
111    /** exeDir 直下 or exeDir\bin から実行ファイルを探す（.exe/.bat/.cmd 対応） */
112    private function findExe(string $exeDir, string $name): ?string
113    {
114        if ($this->isWindows()) {
115            $candidates = [
116                "$exeDir\\$name.exe",          "$exeDir\\bin\\$name.exe",
117                "$exeDir\\$name.bat",          "$exeDir\\bin\\$name.bat",
118                "$exeDir\\$name.cmd",          "$exeDir\\bin\\$name.cmd",
119                "$exeDir\\windows\\bin\\$name.exe",
120                "$exeDir\\win\\bin\\$name.exe",
121            ];
122        } else {
123            $candidates = [
124                "$exeDir/$name",               "$exeDir/bin/$name",
125            ];
126        }
127        foreach ($candidates as $p) {
128            if (is_file($p)) return $p;
129        }
130        return null;
131    }
132
133    /** 出力をUTF-8へ（WinはSJIS-WIN想定） */
134    private function outUTF8(string $s): string
135    {
136        return $this->isWindows() ? mb_convert_encoding($s, 'UTF-8', 'SJIS-WIN') : $s;
137    }
138
139    /**
140     * .exe は配列＋bypass_shell、.bat/.cmd は「cmd /C ""...""」の文字列＋shell経由で起動
141     * @return array [$proc, $pipes] 失敗時は [null, []]
142     */
143    private function openProcess(string $exeOrBat, array $args, string $cwd): array
144    {
145        $des = [1 => ['pipe','w'], 2 => ['pipe','w']];
146
147        if ($this->isWindows() && preg_match('/\.(bat|cmd)$/i', $exeOrBat)) {
148            // cmd /C ""C:\path\tool.bat" "arg1" "arg2""
149            $cmd = 'cmd.exe /C "'
150                 . '"' . $exeOrBat . '"';
151            foreach ($args as $a) {
152                $cmd .= ' ' . escapeshellarg($a);
153            }
154            $cmd .= '"';
155            $proc = proc_open($cmd, $des, $pipes, $cwd); // shell経由（bypass_shell=false）
156        } else {
157            $cmd = array_merge([$exeOrBat], $args);
158            $proc = proc_open($cmd, $des, $pipes, $cwd, null, ['bypass_shell' => true]);
159        }
160
161        if (!is_resource($proc)) return [null, []];
162        return [$proc, $pipes];
163    }
164
165    /* ===================== Source ===================== */
166
167    private function handleSourceCompileRequest()
168    {
169        global $INPUT;
170        $pageContent = $INPUT->post->str('content');
171        $mizarData = $this->extractMizarContent($pageContent);
172
173        if ($mizarData === null) { $this->sendAjaxResponse(false, 'Mizar content not found'); return; }
174        if (isset($mizarData['error'])) { $this->sendAjaxResponse(false, $mizarData['error']); return; }
175
176        $filePath = $this->saveMizarContent($mizarData);
177        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
178        $_SESSION['source_filepath'] = $filePath;
179
180        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
181    }
182
183    private function handleSourceSSERequest()
184    {
185        header('Content-Type: text/event-stream');
186        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
187        header('Pragma: no-cache');
188        header('Expires: 0');
189
190        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
191        if (empty($_SESSION['source_filepath'])) {
192            echo "data: Mizar file path not found in session\n\n"; @ob_flush(); @flush(); return;
193        }
194
195        $this->streamSourceOutput($_SESSION['source_filepath']);
196
197        echo "event: end\n";
198        echo "data: Compilation complete\n\n";
199        @ob_flush(); @flush();
200    }
201
202    /* ===================== View ===================== */
203
204    private function handleViewCompileRequest()
205    {
206        global $INPUT;
207        $content = $INPUT->post->str('content');
208        $filePath = $this->createTempFile($content);
209
210        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
211        $_SESSION['view_filepath'] = $filePath;
212
213        $this->sendAjaxResponse(true, 'Mizar content processed successfully');
214    }
215
216    private function handleViewSSERequest()
217    {
218        header('Content-Type: text/event-stream');
219        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
220        header('Pragma: no-cache');
221        header('Expires: 0');
222
223        if (session_status() !== PHP_SESSION_ACTIVE) session_start();
224        if (empty($_SESSION['view_filepath'])) {
225            echo "data: Mizar file path not found in session\n\n"; @ob_flush(); @flush(); return;
226        }
227
228        $this->streamViewCompileOutput($_SESSION['view_filepath']);
229
230        echo "event: end\n";
231        echo "data: Compilation complete\n\n";
232        @ob_flush(); @flush();
233    }
234
235    /***** view_graph: SVG を返す *****/
236    private function handleViewGraphRequest()
237    {
238        global $INPUT;
239        $content = $INPUT->post->str('content', '');
240        if ($content === '') { $this->sendAjaxResponse(false, 'Empty content'); return; }
241
242        $tmp = tempnam(sys_get_temp_dir(), 'miz');
243        $miz = $tmp . '.miz';
244        rename($tmp, $miz);
245        file_put_contents($miz, $content);
246
247        $parser = __DIR__ . '/script/miz2svg.py';
248        $py     = $this->getConf('py_cmd') ?: 'python';
249        $svg    = shell_exec(escapeshellcmd($py) . ' ' . escapeshellarg($parser) . ' ' . escapeshellarg($miz));
250        @unlink($miz);
251
252        if ($svg) $this->sendAjaxResponse(true, 'success', ['svg' => $svg]);
253        else      $this->sendAjaxResponse(false, 'conversion failed');
254    }
255
256    /* ===================== Content utils ===================== */
257
258    private function extractMizarContent($pageContent)
259    {
260        $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s';
261        preg_match_all($pattern, $pageContent, $m, PREG_SET_ORDER);
262        if (empty($m)) return null;
263
264        $fn   = trim($m[0][1]);
265        $stem = preg_replace('/\.miz$/i', '', $fn);
266        if (!$this->isValidFileName($stem)) {
267            return ['error' => "Invalid characters in file name: '{$stem}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."];
268        }
269
270        $combined = '';
271        foreach ($m as $mm) {
272            $cur = preg_replace('/\.miz$/i', '', trim($mm[1]));
273            if ($cur !== $stem) return ['error' => "File name mismatch in <mizar> tags: '{$stem}' and '{$cur}'"];
274            if (!$this->isValidFileName($cur)) return ['error' => "Invalid characters in file name: '{$cur}'."];
275            $combined .= trim($mm[2]) . "\n";
276        }
277        return ['fileName' => $stem . '.miz', 'content' => $combined];
278    }
279
280    private function isValidFileName($fileName)
281    {
282        if (strlen($fileName) > 8) return false;
283        return (bool)preg_match('/^[A-Za-z0-9_\']+$/', $fileName);
284    }
285
286    private function saveMizarContent($mizarData)
287    {
288        $paths = $this->resolvePaths();
289        $textDir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT';
290        if (!is_dir($textDir)) @mkdir($textDir, 0777, true);
291
292        $filePath = $textDir . DIRECTORY_SEPARATOR . $mizarData['fileName'];
293        file_put_contents($filePath, $mizarData['content']);
294        return $filePath;
295    }
296
297    private function createTempFile($content)
298    {
299        $paths = $this->resolvePaths();
300        $textDir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT';
301        if (!is_dir($textDir)) @mkdir($textDir, 0777, true);
302
303        $tempFilename = $textDir . DIRECTORY_SEPARATOR . str_replace('.', '_', uniqid('tmp', true)) . ".miz";
304        file_put_contents($tempFilename, $content);
305        return $tempFilename;
306    }
307
308    private function clearTempFiles()
309    {
310        $paths = $this->resolvePaths();
311        $dir = $paths['work'] . DIRECTORY_SEPARATOR . 'TEXT' . DIRECTORY_SEPARATOR;
312        $files = glob($dir . '*');
313
314        $errors = [];
315        foreach ($files as $f) {
316            if (is_file($f)) {
317                if (!$this->is_file_locked($f)) {
318                    $ok = false; $retries = 5;
319                    while ($retries-- > 0) { if (@unlink($f)) { $ok = true; break; } sleep(2); }
320                    if (!$ok) $errors[] = "Failed to delete: $f";
321                } else {
322                    $errors[] = "File is locked: $f";
323                }
324            }
325        }
326        if ($errors) $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors);
327        else         $this->sendAjaxResponse(true, 'Temporary files cleared successfully');
328    }
329
330    private function is_file_locked($file)
331    {
332        $fp = @fopen($file, "r+");
333        if ($fp === false) return true;
334        $locked = !flock($fp, LOCK_EX | LOCK_NB);
335        fclose($fp);
336        return $locked;
337    }
338
339    /* ===================== Run (miz2prel/makeenv/verifier) ===================== */
340
341    private function streamSourceOutput($filePath)
342    {
343        $paths = $this->resolvePaths();
344        $workPath  = $paths['work'];
345        $sharePath = $paths['share'];
346        putenv("MIZFILES={$sharePath}");
347
348        $exe = $this->findExe($paths['exe'], 'miz2prel');
349        if ($exe === null) {
350            echo "data: ERROR: miz2prel not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return;
351        }
352
353        [$proc, $pipes] = $this->openProcess($exe, [$filePath], $workPath);
354        if (!$proc) { echo "data: ERROR: Failed to execute miz2prel.\n\n"; @ob_flush(); @flush(); return; }
355
356        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
357        fclose($pipes[1]);
358        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
359        fclose($pipes[2]);
360        proc_close($proc);
361
362        $errFilename = str_replace('.miz', '.err', $filePath);
363        $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
364    }
365
366    private function streamViewCompileOutput($filePath)
367    {
368        $paths = $this->resolvePaths();
369        $workPath  = $paths['work'];
370        $sharePath = $paths['share'];
371        putenv("MIZFILES={$sharePath}");
372
373        // makeenv
374        $makeenv = $this->findExe($paths['exe'], 'makeenv');
375        if ($makeenv === null) { echo "data: ERROR: makeenv not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return; }
376        [$proc, $pipes] = $this->openProcess($makeenv, [$filePath], $workPath);
377        if (!$proc) { echo "data: ERROR: Failed to execute makeenv.\n\n"; @ob_flush(); @flush(); return; }
378        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
379        fclose($pipes[1]);
380        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
381        fclose($pipes[2]);
382        proc_close($proc);
383
384        $errFilename = str_replace('.miz', '.err', $filePath);
385        if ($this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg')) return;
386
387        // verifier
388        $verifier = $this->findExe($paths['exe'], 'verifier');
389        if ($verifier === null) { echo "data: ERROR: verifier not found under {$paths['exe']} (or bin)\n\n"; @ob_flush(); @flush(); return; }
390        $rel = 'TEXT' . DIRECTORY_SEPARATOR . basename($filePath);
391        [$proc, $pipes] = $this->openProcess($verifier, ['-q','-l',$rel], $workPath);
392        if (!$proc) { echo "data: ERROR: Failed to execute verifier.\n\n"; @ob_flush(); @flush(); return; }
393        while (($line = fgets($pipes[1])) !== false) { echo "data: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
394        fclose($pipes[1]);
395        while (($line = fgets($pipes[2])) !== false) { echo "data: ERROR: " . $this->outUTF8($line) . "\n\n"; @ob_flush(); @flush(); }
396        fclose($pipes[2]);
397        proc_close($proc);
398
399        $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
400    }
401
402    /* ===================== Errors ===================== */
403
404    private function getMizarErrorMessages($mizarMsgFile)
405    {
406        if (!is_file($mizarMsgFile)) return [];
407        $errorMessages = [];
408        $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
409        $isReading = false; $key = 0;
410        foreach ($lines as $line) {
411            if (preg_match('/# (\d+)/', $line, $m)) { $isReading = true; $key = (int)$m[1]; }
412            elseif ($isReading) { $errorMessages[$key] = $line; $isReading = false; }
413        }
414        return $errorMessages;
415    }
416
417    private function handleCompilationErrors($errFilename, $mizarMsgFilePath)
418    {
419        if (!file_exists($errFilename)) return false;
420        $errs = []; $lines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
421        foreach ($lines as $ln) {
422            if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $ln, $m)) {
423                $code = (int)$m[3];
424                $errs[] = [
425                    'code'    => $code,
426                    'line'    => (int)$m[1],
427                    'column'  => (int)$m[2],
428                    'message' => $this->getMizarErrorMessages($mizarMsgFilePath)[$code] ?? 'Unknown error'
429                ];
430            }
431        }
432        if ($errs) {
433            echo "event: compileErrors\n";
434            echo "data: " . json_encode($errs) . "\n\n";
435            @ob_flush(); @flush();
436            return true;
437        }
438        return false;
439    }
440
441    private function sendAjaxResponse($success, $message, $data = '')
442    {
443        header('Content-Type: application/json');
444        header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0');
445        header('Pragma: no-cache');
446        header('Expires: 0');
447        echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]);
448        exit;
449    }
450
451    private function handle_create_combined_file()
452    {
453        global $INPUT;
454        $combinedContent = $INPUT->post->str('content');
455        $filename = $INPUT->post->str('filename', 'combined_file.miz');
456
457        if (!empty($combinedContent)) {
458            $this->sendAjaxResponse(true, 'File created successfully', [
459                'filename' => $filename,
460                'content'  => $combinedContent
461            ]);
462        } else {
463            $this->sendAjaxResponse(false, 'Content is empty, no file created');
464        }
465    }
466}
467