Searched refs:errFilename (Results 1 – 3 of 3) sorted by relevance
| /plugin/mizarproofchecker/ |
| D | action.php | 202 $errFilename = str_replace('.miz', '.err', $filePath);
203 …if ($this->handleCompilationErrors($errFilename, rtrim($this->getConf('mizar_share_dir'), '/\\') .…
282 $errFilename = str_replace('.miz', '.err', $filePath);
303 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
334 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
377 private function handleCompilationErrors($errFilename, $mizarMsgFilePath) argument
379 if (file_exists($errFilename)) {
381 $errorLines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
|
| /plugin/mizarveifiabledocs/ |
| D | action.php | 202 $errFilename = str_replace('.miz', '.err', $filePath);
203 …if ($this->handleCompilationErrors($errFilename, rtrim($this->getConf('mizar_share_dir'), '/\\') .…
282 $errFilename = str_replace('.miz', '.err', $filePath);
303 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
334 if ($this->handleCompilationErrors($errFilename, $sharePath . '/mizar.msg')) {
377 private function handleCompilationErrors($errFilename, $mizarMsgFilePath) argument
379 if (file_exists($errFilename)) {
381 $errorLines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
|
| /plugin/mizarverifiabledocs/ |
| D | action.php | 362 $errFilename = str_replace('.miz', '.err', $filePath);
363 … $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
384 $errFilename = str_replace('.miz', '.err', $filePath);
385 …if ($this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg')) …
399 … $this->handleCompilationErrors($errFilename, $sharePath . DIRECTORY_SEPARATOR . 'mizar.msg');
417 private function handleCompilationErrors($errFilename, $mizarMsgFilePath) argument
419 if (!file_exists($errFilename)) return false;
420 $errs = []; $lines = file($errFilename, FILE_IGNORE_NEW_LINES | FILE_SKIP_EMPTY_LINES);
|