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 * 10 * @license GPL 2 http://www.gnu.org/licenses/gpl-2.0.html 11 * @author Yamada, M. 12 */ 13 14class action_plugin_mizarverifiabledocs extends ActionPlugin 15{ 16 /** 17 * Registers a callback function for a given event 18 * 19 * @param EventHandler $controller DokuWiki's event controller object 20 * @return void 21 */ 22 public function register(EventHandler $controller) 23 { 24 $controller->register_hook('AJAX_CALL_UNKNOWN', 'BEFORE', $this, 'handle_ajax_call'); 25 $controller->register_hook('TPL_CONTENT_DISPLAY', 'BEFORE', $this, 'handle_tpl_content_display'); 26 } 27 28 /** 29 * Handles the TPL_CONTENT_DISPLAY event to insert "Hide All" button 30 * 31 * @param Event $event 32 * @param mixed $_param Unused parameter 33 * @return void 34 */ 35 public function handle_tpl_content_display(Event $event, $_param) 36 { 37 // データが文字列かどうか確認 38 if (!is_string($event->data)) { 39 error_log('handle_tpl_content_display: data is not a string! ' . print_r($event->data, true)); 40 return; 41 } 42 43 $html = $event->data; 44 45 // "mizarWrapper" クラスが存在するか確認 46 if (strpos($html, 'mizarWrapper') !== false) { 47 // 既にボタンが挿入されているか確認（複数回挿入しないため） 48 if (strpos($html, 'id="hideAllButton"') === false) { 49 $buttonHtml = '<div class="hideAllContainer">' 50 . '<button id="hideAllButton" class="hide-all-button">Hide All</button>' 51 . '<button id="showAllButton" class="hide-all-button" style="display:none;">Show All</button>' 52 . '<button id="resetAllButton" class="reset-all-button">Reset All</button>' // ★ 追加 53 . '</div>'; 54 55 // 先頭にボタンを挿入 56 $html = $buttonHtml . $html; 57 $event->data = $html; 58 } 59 } 60 } 61 62 /** 63 * Handles AJAX requests 64 * 65 * @param Event $event 66 * @param $param 67 */ 68 public function handle_ajax_call(Event $event, $param) 69 { 70 unset($param); // 未使用のパラメータを無効化 71 72 switch ($event->data) { 73 case 'clear_temp_files': 74 $event->preventDefault(); 75 $event->stopPropagation(); 76 $this->clearTempFiles(); 77 break; 78 case 'source_sse': 79 $event->preventDefault(); 80 $event->stopPropagation(); 81 $this->handleSourceSSERequest(); 82 break; 83 case 'source_compile': 84 $event->preventDefault(); 85 $event->stopPropagation(); 86 $this->handleSourceCompileRequest(); 87 break; 88 case 'view_compile': 89 $event->preventDefault(); 90 $event->stopPropagation(); 91 $this->handleViewCompileRequest(); 92 break; 93 case 'view_sse': 94 $event->preventDefault(); 95 $event->stopPropagation(); 96 $this->handleViewSSERequest(); 97 break; 98 case 'create_combined_file': 99 $event->preventDefault(); 100 $event->stopPropagation(); 101 $this->handle_create_combined_file(); 102 break; 103 case 'view_graph': 104 $event->preventDefault(); 105 $event->stopPropagation(); 106 $this->handleViewGraphRequest(); 107 break; 108 } 109 } 110 111 // source用のコンパイルリクエスト処理 112 private function handleSourceCompileRequest() 113 { 114 global $INPUT; 115 $pageContent = $INPUT->post->str('content'); 116 $mizarData = $this->extractMizarContent($pageContent); 117 118 // エラーチェックを追加 119 if ($mizarData === null) { 120 $this->sendAjaxResponse(false, 'Mizar content not found'); 121 return; 122 } elseif (isset($mizarData['error'])) { 123 $this->sendAjaxResponse(false, $mizarData['error']); 124 return; 125 } 126 127 $filePath = $this->saveMizarContent($mizarData); 128 129 session_start(); 130 $_SESSION['source_filepath'] = $filePath; 131 132 $this->sendAjaxResponse(true, 'Mizar content processed successfully'); 133 } 134 135 // source用のSSEリクエスト処理 136 private function handleSourceSSERequest() 137 { 138 header('Content-Type: text/event-stream'); 139 header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0'); 140 header('Pragma: no-cache'); 141 header('Expires: 0'); 142 143 session_start(); 144 if (!isset($_SESSION['source_filepath'])) { 145 echo "data: Mizar file path not found in session\n\n"; 146 ob_flush(); 147 flush(); 148 return; 149 } 150 151 $filePath = $_SESSION['source_filepath']; 152 $this->streamSourceOutput($filePath); 153 154 echo "event: end\n"; 155 echo "data: Compilation complete\n\n"; 156 ob_flush(); 157 flush(); 158 } 159 160 // view用のコンパイルリクエスト処理 161 private function handleViewCompileRequest() 162 { 163 global $INPUT; 164 $content = $INPUT->post->str('content'); 165 166 $filePath = $this->createTempFile($content); 167 168 session_start(); 169 $_SESSION['view_filepath'] = $filePath; 170 171 $this->sendAjaxResponse(true, 'Mizar content processed successfully'); 172 } 173 174 // view用のSSEリクエスト処理 175 private function handleViewSSERequest() 176 { 177 header('Content-Type: text/event-stream'); 178 header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0'); 179 header('Pragma: no-cache'); 180 header('Expires: 0'); 181 182 session_start(); 183 if (!isset($_SESSION['view_filepath'])) { 184 echo "data: Mizar file path not found in session\n\n"; 185 ob_flush(); 186 flush(); 187 return; 188 } 189 190 $filePath = $_SESSION['view_filepath']; 191 $this->streamViewCompileOutput($filePath); 192 193 echo "event: end\n"; 194 echo "data: Compilation complete\n\n"; 195 ob_flush(); 196 flush(); 197 } 198 199 /***** view_graph: 上から該当ブロックまでを結合し SVG を返す *****/ 200 private function handleViewGraphRequest() 201 { 202 global $INPUT; 203 $content = $INPUT->post->str('content', ''); 204 205 // 空チェック 206 if ($content === '') { 207 $this->sendAjaxResponse(false, 'Empty content'); 208 return; 209 } 210 211 // 一時 .miz ファイルを作成 212 $tmp = tempnam(sys_get_temp_dir(), 'miz'); 213 $miz = $tmp . '.miz'; 214 rename($tmp, $miz); // tempnam が拡張子無しなのでリネーム 215 file_put_contents($miz, $content); 216 217 // Python 可視化スクリプト呼び出し 218 $parser = escapeshellarg(__DIR__ . '/script/miz2svg.py'); 219 $py = escapeshellcmd($this->getConf('py_cmd') ?: 'python'); 220 $svg = shell_exec("$py $parser ".escapeshellarg($miz)); 221 unlink($miz); // 後片付け 222 223 // 結果返却 224 if ($svg) { 225 $this->sendAjaxResponse(true, 'success', ['svg' => $svg]); 226 } else { 227 $this->sendAjaxResponse(false, 'conversion failed'); 228 } 229 } 230 231 // Mizarコンテンツの抽出 232 private function extractMizarContent($pageContent) 233 { 234 $pattern = '/<mizar\s+([^>]+)>(.*?)<\/mizar>/s'; 235 preg_match_all($pattern, $pageContent, $matches, PREG_SET_ORDER); 236 237 if (empty($matches)) { 238 return null; 239 } 240 241 // 最初のファイル名を取得し、拡張子を除去 242 $fileName = trim($matches[0][1]); 243 $fileNameWithoutExt = preg_replace('/\.miz$/i', '', $fileName); 244 245 // ファイル名のバリデーションを追加 246 if (!$this->isValidFileName($fileNameWithoutExt)) { 247 return ['error' => "Invalid characters in file name: '{$fileNameWithoutExt}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."]; 248 } 249 250 $combinedContent = ''; 251 252 foreach ($matches as $match) { 253 $currentFileName = trim($match[1]); 254 $currentFileNameWithoutExt = preg_replace('/\.miz$/i', '', $currentFileName); 255 256 if ($currentFileNameWithoutExt !== $fileNameWithoutExt) { 257 return ['error' => "File name mismatch in <mizar> tags: '{$fileNameWithoutExt}' and '{$currentFileNameWithoutExt}'"]; 258 } 259 260 // バリデーションを各ファイル名にも適用 261 if (!$this->isValidFileName($currentFileNameWithoutExt)) { 262 return ['error' => "Invalid characters in file name: '{$currentFileNameWithoutExt}'. Only letters, numbers, underscores (_), and apostrophes (') are allowed, up to 8 characters."]; 263 } 264 265 $combinedContent .= trim($match[2]) . "\n"; 266 } 267 268 // ファイル名に拡張子を付加 269 $fullFileName = $fileNameWithoutExt . '.miz'; 270 271 return ['fileName' => $fullFileName, 'content' => $combinedContent]; 272 } 273 274 // ファイル名のバリデーション関数を追加 275 private function isValidFileName($fileName) 276 { 277 // ファイル名の長さをチェック（最大8文字） 278 if (strlen($fileName) > 8) { 279 return false; 280 } 281 282 // 許可される文字のみを含むかチェック 283 if (!preg_match('/^[A-Za-z0-9_\']+$/', $fileName)) { 284 return false; 285 } 286 287 return true; 288 } 289 290 // Mizarコンテンツの保存 291 private function saveMizarContent($mizarData) 292 { 293 $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\'); 294 $filePath = $workPath . "/TEXT/" . $mizarData['fileName']; 295 file_put_contents($filePath, $mizarData['content']); 296 return $filePath; 297 } 298 299 // source用の出力をストリーム 300 private function streamSourceOutput($filePath) 301 { 302 $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\'); 303 $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\'); 304 305 // ★追加：環境変数 MIZFILESをPHP内で設定 306 putenv("MIZFILES=$sharePath"); 307 308 chdir($workPath); 309 310 $command = "miz2prel " . escapeshellarg($filePath); 311 $process = proc_open($command, array(1 => array("pipe", "w")), $pipes); 312 313 if (is_resource($process)) { 314 while ($line = fgets($pipes[1])) { 315 echo "data: " . $line . "\n\n"; 316 ob_flush(); 317 flush(); 318 } 319 fclose($pipes[1]); 320 321 // エラー処理の追加 322 $errFilename = str_replace('.miz', '.err', $filePath); 323 if ($this->handleCompilationErrors($errFilename, rtrim($this->getConf('mizar_share_dir'), '/\\') . '/mizar.msg')) { 324 // エラーがあった場合は処理を終了 325 proc_close($process); 326 return; 327 } 328 329 proc_close($process); 330 } 331 } 332 333 // view用の一時ファイル作成 334 private function createTempFile($content) 335 { 336 $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/'; 337 $uniqueName = str_replace('.', '_', uniqid('tmp', true)); 338 $tempFilename = $workPath . $uniqueName . ".miz"; 339 file_put_contents($tempFilename, $content); 340 return $tempFilename; 341 } 342 343 // 一時ファイルの削除 (clearTempFiles関数の修正版) 344 private function clearTempFiles() 345 { 346 $workPath = rtrim($this->getConf('mizar_work_dir'), '/\\') . '/TEXT/'; 347 $files = glob($workPath . '*'); // TEXTフォルダ内のすべてのファイルを取得 348 349 $errors = []; 350 foreach ($files as $file) { 351 if (is_file($file)) { 352 // ファイルが使用中かどうか確認 353 if (!$this->is_file_locked($file)) { 354 $retries = 5; // リトライを増やす 355 while ($retries > 0) { 356 if (@unlink($file)) { // ← エラー抑制を追加 357 break; // 削除成功 358 } 359 $errors[] = "Error deleting $file: " . error_get_last()['message']; 360 $retries--; 361 sleep(2); // 2秒待ってリトライ 362 } 363 if ($retries === 0) { 364 $errors[] = "Failed to delete: $file"; // 削除失敗 365 } 366 } else { 367 $errors[] = "File is locked: $file"; // ファイルがロックされている 368 } 369 } 370 } 371 372 if (empty($errors)) { 373 $this->sendAjaxResponse(true, 'Temporary files cleared successfully'); 374 } else { 375 $this->sendAjaxResponse(false, 'Some files could not be deleted', $errors); 376 } 377 } 378 379 380 // ファイルがロックされているかをチェックする関数 381 private function is_file_locked($file) 382 { 383 $fileHandle = @fopen($file, "r+"); 384 385 if ($fileHandle === false) { 386 return true; // ファイルが開けない、つまりロックされているかアクセス権がない 387 } 388 389 $locked = !flock($fileHandle, LOCK_EX | LOCK_NB); // ロックの取得を試みる（非ブロッキングモード） 390 391 fclose($fileHandle); 392 return $locked; // ロックが取得できなければファイルはロックされている 393 } 394 395 // View用コンパイル出力のストリーム 396 private function streamViewCompileOutput($filePath) 397 { 398 $workPath = $this->getConf('mizar_work_dir'); 399 $sharePath = rtrim($this->getConf('mizar_share_dir'), '/\\') . '/'; 400 401 // ★追加：環境変数 MIZFILESをPHP内で設定 402 putenv("MIZFILES=$sharePath"); 403 404 chdir($workPath); 405 406 $errFilename = str_replace('.miz', '.err', $filePath); 407 $command = "makeenv " . escapeshellarg($filePath); 408 $process = proc_open($command, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $pipes); 409 410 if (is_resource($process)) { 411 while ($line = fgets($pipes[1])) { 412 echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n"; 413 ob_flush(); 414 flush(); 415 } 416 fclose($pipes[1]); 417 418 while ($line = fgets($pipes[2])) { 419 echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n"; 420 ob_flush(); 421 flush(); 422 } 423 fclose($pipes[2]); 424 proc_close($process); 425 426 // makeenvのエラー処理 427 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) { 428 return; 429 } 430 431 // verifierの実行 432 $exePath = rtrim($this->getConf('mizar_exe_dir'), '/\\') . '/'; 433 $verifierPath = escapeshellarg($exePath . "verifier"); 434 if (strtoupper(substr(PHP_OS, 0, 3)) === 'WIN') { 435 $verifierPath .= ".exe"; 436 } 437 $verifierCommand = $verifierPath . " -q -l " . escapeshellarg("TEXT/" . basename($filePath)); 438 439 $verifierProcess = proc_open($verifierCommand, array(1 => array("pipe", "w"), 2 => array("pipe", "w")), $verifierPipes); 440 441 if (is_resource($verifierProcess)) { 442 while ($line = fgets($verifierPipes[1])) { 443 echo "data: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n"; 444 ob_flush(); 445 flush(); 446 } 447 fclose($verifierPipes[1]); 448 449 while ($line = fgets($verifierPipes[2])) { 450 echo "data: ERROR: " . mb_convert_encoding($line, 'UTF-8', 'SJIS') . "\n\n"; 451 ob_flush(); 452 flush(); 453 } 454 fclose($verifierPipes[2]); 455 proc_close($verifierProcess); 456 457 // verifierのエラー処理 458 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) { 459 return; 460 } 461 } else { 462 echo "data: ERROR: Failed to execute verifier command.\n\n"; 463 ob_flush(); 464 flush(); 465 } 466 } else { 467 echo "data: ERROR: Failed to execute makeenv command.\n\n"; 468 ob_flush(); 469 flush(); 470 } 471 } 472 473 private function getMizarErrorMessages($mizarMsgFile) 474 { 475 $errorMessages = []; 476 $lines = file($mizarMsgFile, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES); 477 478 $isReadingErrorMsg = false; 479 $key = 0; 480 481 foreach ($lines as $line) { 482 if (preg_match('/# (\d+)/', $line, $matches)) { 483 $isReadingErrorMsg = true; 484 $key = intval($matches[1]); 485 } elseif ($isReadingErrorMsg) { 486 $errorMessages[$key] = $line; 487 $isReadingErrorMsg = false; 488 } 489 } 490 491 return $errorMessages; 492 } 493 494 private function sendAjaxResponse($success, $message, $data = '') 495 { 496 header('Content-Type: application/json'); 497 header('Cache-Control: no-store, no-cache, must-revalidate, max-age=0'); 498 header('Pragma: no-cache'); 499 header('Expires: 0'); 500 echo json_encode(['success' => $success, 'message' => $message, 'data' => $data]); 501 exit; 502 } 503 504 private function handleCompilationErrors($errFilename, $mizarMsgFilePath) 505 { 506 if (file_exists($errFilename)) { 507 $errors = []; 508 $errorLines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES); 509 foreach ($errorLines as $errorLine) { 510 if (preg_match('/(\d+)\s+(\d+)\s+(\d+)/', $errorLine, $matches)) { 511 $errorCode = intval($matches[3]); 512 $errors[] = [ 513 'code' => $errorCode, 514 'line' => intval($matches[1]), 515 'column' => intval($matches[2]), 516 'message' => $this->getMizarErrorMessages($mizarMsgFilePath)[$errorCode] ?? 'Unknown error' 517 ]; 518 } 519 } 520 if (!empty($errors)) { 521 echo "event: compileErrors\n"; 522 echo "data: " . json_encode($errors) . "\n\n"; 523 ob_flush(); 524 flush(); 525 return true; 526 } 527 } 528 return false; 529 } 530 531 private function handle_create_combined_file() 532 { 533 global $INPUT; 534 535 // 投稿されたコンテンツを取得 536 $combinedContent = $INPUT->post->str('content'); 537 $filename = $INPUT->post->str('filename', 'combined_file.miz'); // デフォルトのファイル名を指定 538 539 // ファイルを保存せず、コンテンツを直接返す 540 if (!empty($combinedContent)) { 541 // ファイルの内容をレスポンスで返す（PHP側でファイルを作成しない） 542 $this->sendAjaxResponse(true, 'File created successfully', [ 543 'filename' => $filename, 544 'content' => $combinedContent 545 ]); 546 error_log("File content sent: " . $filename); 547 } else { 548 $this->sendAjaxResponse(false, 'Content is empty, no file created'); 549 } 550 } 551} 552