| 1 | (1) (file-mode-spec/warning) Error in File mode specification: Cannot open load file: "executable" |
|---|
| 2 | |
|---|
| 3 | Backtrace follows: |
|---|
| 4 | |
|---|
| 5 | signal(file-error ("Cannot open load file" "executable")) |
|---|
| 6 | # bind (path handler filename nosuffix nomessage noerror file) |
|---|
| 7 | load("executable" nil nil nil) |
|---|
| 8 | # (unwind-protect ...) |
|---|
| 9 | (executable-find progname) |
|---|
| 10 | # bind (exec-path) |
|---|
| 11 | (let ((exec-path (append exec-path extrapath))) (executable-find progname)) |
|---|
| 12 | (cond ((fboundp (quote executable-find)) (let ((exec-path (append exec-path extrapath))) (executable-find progname))) ((fboundp (quote locate-file)) (locate-file progname (append (split-path (getenv "PATH")) extrapath) (if proof-running-on-win32 (quote (".exe"))) 1))) |
|---|
| 13 | (or (cond ((fboundp (quote executable-find)) (let ((exec-path (append exec-path extrapath))) (executable-find progname))) ((fboundp (quote locate-file)) (locate-file progname (append (split-path (getenv "PATH")) extrapath) (if proof-running-on-win32 (quote (".exe"))) 1))) (if returnnopath progname)) |
|---|
| 14 | # bind (extrapath returnnopath progname) |
|---|
| 15 | proof-locate-executable("isabelle" t ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")) |
|---|
| 16 | (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))) |
|---|
| 17 | eval((if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/"))))) |
|---|
| 18 | # bind (value symbol) |
|---|
| 19 | custom-initialize-reset(isabelle-program-name (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/"))))) |
|---|
| 20 | # bind (initialize requests args doc default symbol) |
|---|
| 21 | custom-declare-variable(isabelle-program-name (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))) "*Default name of program to run Isabelle.\n\nThe default value except when running under Windows is \"isabelle\",\nwhich will get expanded using PATH if possible, or in a number\nof standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). \n\nThe default value when running under Windows is:\n\n C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\\n\nThis expects SML/NJ in C:\\sml and Isabelle images in C:Isabelle. \nThe logic image name is tagged onto the end. \n\nNB: The Isabelle settings mechanism or the environment variable\nISABELLE will always override this setting." :type file :group isabelle) |
|---|
| 22 | (defcustom isabelle-program-name (if (fboundp (quote proof-running-on-win32)) "C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\" (proof-locate-executable "isabelle" t (quote ("/usr/local/Isabelle/bin/" "/opt/Isabelle/bin/" "/usr/Isabelle/bin/" "/usr/share/Isabelle/bin/")))) "*Default name of program to run Isabelle.\n\nThe default value except when running under Windows is \"isabelle\",\nwhich will get expanded using PATH if possible, or in a number\nof standard locations (/usr/local/Isabelle/, /opt/Isabelle, etc). \n\nThe default value when running under Windows is:\n\n C:\\sml\\bin\\.run\\run.x86-win32.exe @SMLload=C:\\Isabelle\\\n\nThis expects SML/NJ in C:\\sml and Isabelle images in C:Isabelle. \nThe logic image name is tagged onto the end. \n\nNB: The Isabelle settings mechanism or the environment variable\nISABELLE will always override this setting." :type (quote file) :group (quote isabelle)) |
|---|
| 23 | # (unwind-protect ...) |
|---|
| 24 | # (unwind-protect ...) |
|---|
| 25 | # (unwind-protect ...) |
|---|
| 26 | # (unwind-protect ...) |
|---|
| 27 | # (unwind-protect ...) |
|---|
| 28 | # (unwind-protect ...) |
|---|
| 29 | # (unwind-protect ...) |
|---|
| 30 | # (unwind-protect ...) |
|---|
| 31 | load-internal("isabelle-system" nil require nil undecided) |
|---|
| 32 | # bind (path handler filename nosuffix nomessage noerror file) |
|---|
| 33 | load("isabelle-system" nil require nil) |
|---|
| 34 | # (unwind-protect ...) |
|---|
| 35 | require(isabelle-system) |
|---|
| 36 | # (unwind-protect ...) |
|---|
| 37 | # (unwind-protect ...) |
|---|
| 38 | # (unwind-protect ...) |
|---|
| 39 | # (unwind-protect ...) |
|---|
| 40 | # (unwind-protect ...) |
|---|
| 41 | # (unwind-protect ...) |
|---|
| 42 | # (unwind-protect ...) |
|---|
| 43 | # (unwind-protect ...) |
|---|
| 44 | load-internal("isar" nil nil nil undecided) |
|---|
| 45 | # bind (path handler filename nosuffix nomessage noerror file) |
|---|
| 46 | load("isar") |
|---|
| 47 | # bind (library) |
|---|
| 48 | load-library("isar") |
|---|
| 49 | (cond ((and (boundp (quote proof-assistant)) (not (string-equal proof-assistant ""))) (or (string-equal proof-assistant "Isabelle") (message (concat "Isabelle" " Proof General error: Proof General already in use for " proof-assistant)))) (t (proof-ready-for-assistant "Isabelle" (quote isar)) (load-library "isar") (isar-mode))) |
|---|
| 50 | isar-mode() |
|---|
| 51 | # bind (alist mode name keep-going) |
|---|
| 52 | # (unwind-protect ...) |
|---|
| 53 | # bind (just-from-file-name) |
|---|
| 54 | set-auto-mode() |
|---|
| 55 | #<compiled-function nil "...(5)" [set-auto-mode t] 1>() |
|---|
| 56 | # (unwind-protect ...) |
|---|
| 57 | call-with-condition-handler(#<compiled-function (__call_trapping_errors_arg__) "...(17)" [__call_trapping_errors_arg__ errstr error-message-string lwarn file-mode-spec warning "Error in %s: %s\n\nBacktrace follows:\n\n%s" "File mode specification" backtrace-in-condition-handler-eliminating-handler] 8> #<compiled-function nil "...(5)" [set-auto-mode t] 1>) |
|---|
| 58 | # (condition-case ... . ((error))) |
|---|
| 59 | # bind (find-file) |
|---|
| 60 | normal-mode(t) |
|---|
| 61 | # bind (nomodes after-find-file-from-revert-buffer noauto warn error) |
|---|
| 62 | after-find-file(t t) |
|---|
| 63 | # (unwind-protect ...) |
|---|
| 64 | # bind (inhibit-read-only error number truename rawfile nowarn filename buf) |
|---|
| 65 | find-file-noselect-1(#<buffer "Scratch.thy"> "/usr/local/Scratch.thy" nil nil "/usr/local/Scratch.thy" nil) |
|---|
| 66 | byte-code("..." [number truename rawfile nowarn filename buf set-buffer-major-mode find-file-noselect-1] 7) |
|---|
| 67 | # (condition-case ... . ((t (byte-code "Â!Ã @ A\"" [buf data kill-buffer signal] 3)))) |
|---|
| 68 | # bind (number truename buf wildcards rawfile nowarn filename) |
|---|
| 69 | find-file-noselect("/usr/local/Scratch.thy" nil nil nil) |
|---|
| 70 | # bind (wildcards codesys filename) |
|---|
| 71 | find-file("/usr/local/Scratch.thy") |
|---|
| 72 | # bind (dir file-count line end-of-options file-p arg tem) |
|---|
| 73 | command-line-1() |
|---|
| 74 | # bind (command-line-args-left) |
|---|
| 75 | command-line() |
|---|
| 76 | # (condition-case ... . ((t (byte-code " Â" [error-data data nil] 1)))) |
|---|
| 77 | # bind (error-data) |
|---|
| 78 | normal-top-level() |
|---|
| 79 | # (condition-case ... . error) |
|---|
| 80 | # (catch top-level ...) |
|---|
| 81 | |
|---|
| 82 | |
|---|
