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