From bbafe47e7569fc6106bc5e5f03ec2eba7ff6534a Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Wed, 3 Apr 2013 11:13:25 +0200 Subject: [PATCH] [emacs] why.el renamed to why3.el [GTK sourceview] why.lang renamed to why3.lang --- CHANGES | 2 + Makefile.in | 38 ++-- share/emacs/why.el | 275 ----------------------------- share/emacs/why3.el | 176 ++++++++++++++++++ share/lang/{why.lang => why3.lang} | 29 ++- src/ide/gmain.ml | 4 +- 6 files changed, 211 insertions(+), 313 deletions(-) delete mode 100644 share/emacs/why.el create mode 100644 share/emacs/why3.el rename share/lang/{why.lang => why3.lang} (91%) diff --git a/CHANGES b/CHANGES index 3e143bec3..14a56bf10 100644 --- a/CHANGES +++ b/CHANGES @@ -1,5 +1,7 @@ * marks an incompatible change + * [emacs] why.el renamed to why3.el + * [GTK sourceview] why.lang renamed to why3.lang version 0.81, March 25, 2013 ========================== diff --git a/Makefile.in b/Makefile.in index 1f558fd7e..425a9cf9f 100644 --- a/Makefile.in +++ b/Makefile.in @@ -96,9 +96,9 @@ endif .PHONY: byte opt clean depend all install install_local install_no_local .PHONY: plugins plugins.byte plugins.opt -############# -# Why library -############# +############## +# Why3 library +############## LIBGENERATED = src/util/config.ml src/util/rc.ml src/parser/lexer.ml \ src/parser/parser.mli src/parser/parser.ml \ @@ -215,6 +215,7 @@ install_no_local:: mkdir -p $(DATADIR)/why3/images/boomy mkdir -p $(DATADIR)/why3/images/fatcow mkdir -p $(DATADIR)/why3/emacs + mkdir -p $(DATADIR)/why3/vim mkdir -p $(DATADIR)/why3/lang mkdir -p $(DATADIR)/why3/theories mkdir -p $(DATADIR)/why3/modules @@ -229,9 +230,10 @@ install_no_local:: cp -f share/images/fatcow/*.png $(DATADIR)/why3/images/fatcow cp -f share/why3session.dtd $(DATADIR)/why3 cp -rf share/javascript $(DATADIR)/why3/javascript - cp -f share/emacs/why.el $(DATADIR)/why3/emacs/why.el - cp -f share/lang/why.lang $(DATADIR)/why3/lang/why.lang -# if test -d /etc/bash_completion.d; then cp -f share/bash/why3 /etc/bash_completion.d; fi + cp -f share/emacs/why3.el $(DATADIR)/why3/emacs/why3.el + cp -f share/vim/why3.vim $(DATADIR)/why3/vim/why3.vim + cp -f share/lang/why3.lang $(DATADIR)/why3/lang/why3.lang + if test -d /etc/bash_completion.d; then cp -f share/bash/why3 /etc/bash_completion.d; fi install_no_local_lib:: rm -rf $(OCAMLLIB)/why3 @@ -241,8 +243,8 @@ install_no_local_lib:: ifeq (@enable_local@,yes) install install-lib: - @echo "Why is configured in local installation mode." - @echo "To install Why, run ./configure --disable-local ; make ; make install" + @echo "Why3 is configured in local installation mode." + @echo "To install Why3, run ./configure --disable-local ; make ; make install" else install: clean_old_install install_no_local install-lib: install_no_local_lib @@ -251,7 +253,7 @@ endif install-all: install install-lib ################## -# Why plugins +# Why3 plugins ################## PLUGGENERATED = plugins/tptp/tptp_lexer.ml \ @@ -499,7 +501,7 @@ clean:: local_config: bin/why3config.@OCAMLBEST@ WHY3LIB=$(PWD) WHY3DATA=$(PWD)/share bin/why3config.@OCAMLBEST@ \ - --detect --conf_file why.conf + --detect --conf_file why3.conf install_no_local:: cp -f bin/why3config.@OCAMLBEST@ $(BINDIR)/why3config$(EXE) @@ -1174,14 +1176,14 @@ testl-type: bin/why3.byte test-api.byte: examples/use_api/use_api.ml lib/why3/why3.cma $(if $(QUIET),@echo 'Ocaml $<' &&) \ ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \ - || (rm -f test-api.byte; printf "Test of Why API calls failed. Please fix it"; exit 2) + || (rm -f test-api.byte; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api.byte; test-api.opt: examples/use_api/use_api.ml lib/why3/why3.cmxa $(if $(QUIET),@echo 'Ocamlopt $<' &&) \ ($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-api.opt) \ - || (rm -f test-api.opt; printf "Test of Why API calls failed. Please fix it"; exit 2) + || (rm -f test-api.opt; printf "Test of Why3 API calls failed. Please fix it"; exit 2) @rm -f test-api.opt #test-shape: lib/why3/why3.cma @@ -1191,7 +1193,7 @@ test-session.byte: examples/use_api/create_session.ml lib/why3/why3.cma $(if $(QUIET),@echo 'Ocaml $<' &&) \ ocaml -I lib/why3 $(INCLUDES) $(EXTCMA) lib/why3/why3.cma $< \ || (rm -f why3session.xml; \ - printf "Test of Why API calls for Session module failed. Please fix it"; exit 2) + printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2) @rm -f why3session.xml test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa @@ -1199,7 +1201,7 @@ test-session.opt: examples/use_api/create_session.ml lib/why3/why3.cmxa ($(OCAMLOPT) -o $@ -I lib/why3 $(INCLUDES) $(EXTCMXA) lib/why3/why3.cmxa $< \ && ./test-session.opt) \ || (rm -f test-session.opt why3session.xml; \ - printf "Test of Why API calls for Session module failed. Please fix it"; exit 2) + printf "Test of Why3 API calls for Session module failed. Please fix it"; exit 2) @rm -f test-session.opt why3session.xml @@ -1479,7 +1481,7 @@ DISTRIB_FILES = Version Makefile.in configure.in configure \ share/javascript/themes/default/*.gif \ share/javascript/themes/default/*.png \ share/javascript/themes/default/*.css \ - share/emacs/why.el share/lang/*.lang \ + share/emacs/why3.el share/lang/*.lang \ share/images/icons.rc share/images/*.png share/images/*/*.png \ share/bash/why3 share/zsh/_why3 share/vim/why3.vim @@ -1631,9 +1633,9 @@ depend: rm -f $^ $(MAKE) $^ -################################################################# -# Building the Why platform with ocamlbuild (OCaml 3.10 needed) # -################################################################# +################################################################## +# Building the Why3 platform with ocamlbuild (OCaml 3.10 needed) # +################################################################## # There used to be targets here but they are no longer useful. diff --git a/share/emacs/why.el b/share/emacs/why.el deleted file mode 100644 index a1e1afda9..000000000 --- a/share/emacs/why.el +++ /dev/null @@ -1,275 +0,0 @@ - -;; why.el - GNU Emacs mode for Why -;; Copyright (C) 2002 Jean-Christophe FILLIATRE - -(defvar why-mode-hook nil) - -(defvar why-mode-map nil - "Keymap for Why major mode") - -(if why-mode-map nil - (setq why-mode-map (make-keymap)) - ;; (define-key why-mode-map "\C-c\C-c" 'why-generate-obligations) **) - ;; (define-key why-mode-map "\C-c\C-a" 'why-find-alternate-file) **) - ;; (define-key why-mode-map "\C-c\C-v" 'why-viewer) **) - (define-key why-mode-map [(control return)] 'font-lock-fontify-buffer)) - -(setq auto-mode-alist - (append - '(("\\.\\(why\\|mlw\\)" . why-mode)) - auto-mode-alist)) - -;; font-lock - -(defun why-regexp-opt (l) - (concat "\\<" (concat (regexp-opt l t) "\\>"))) - -(defconst why-font-lock-keywords-1 - (list - ;; Note: comment font-lock is guaranteed by suitable syntax entries - '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face) - '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face) - `(,(why-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private")) . font-lock-builtin-face) - `(,(why-regexp-opt '("any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "invariant" "variant" "for" "to" "downto" "do" "done" "label" "loop" "assert" "absurd" "assume" "check" "ghost" "try" "with" "theory" "uses" "module" "requires" "ensures" "returns" "raises" "reads" "writes")) . font-lock-keyword-face) - ; `(,(why-regexp-opt '("unit" "bool" "int" "float" "prop" "array")) . font-lock-type-face) - ) - "Minimal highlighting for Why mode") - -(defvar why-font-lock-keywords why-font-lock-keywords-1 - "Default highlighting for Why mode") - -(defvar why-indent 2 - "How many spaces to indent in why mode.") -(make-variable-buffer-local 'why-indent) - -;; syntax - -(defvar why-mode-syntax-table nil - "Syntax table for why-mode") - -(defun why-create-syntax-table () - (if why-mode-syntax-table - () - (setq why-mode-syntax-table (make-syntax-table)) - (set-syntax-table why-mode-syntax-table) - (modify-syntax-entry ?' "w" why-mode-syntax-table) - (modify-syntax-entry ?_ "w" why-mode-syntax-table) - ; comments - (modify-syntax-entry ?\( ". 1" why-mode-syntax-table) - (modify-syntax-entry ?\) ". 4" why-mode-syntax-table) - (modify-syntax-entry ?* ". 23" why-mode-syntax-table) - )) - -;; utility functions - -(defun why-go-and-get-next-proof () - (let ((bp (search-forward "Proof." nil t))) - (if (null bp) (progn (message "Cannot find a proof below") nil) - (let ((bs (re-search-forward "Save\\|Qed\\." nil t))) - (if (null bs) (progn (message "Cannot find a proof below") nil) - (if (> bs (+ bp 6)) - (let ((br (+ bp 1)) - (er (progn (goto-char bs) (beginning-of-line) (point)))) - (progn (kill-region br er) t)) - (why-go-and-get-next-proof))))))) - -(defun why-grab-next-proof () - "grab the next non-empty proof below and insert it at current point" - (interactive) - (if (save-excursion (why-go-and-get-next-proof)) (yank))) - -;; custom variables - -(require 'custom) - -(defcustom why-prover "coq" - "Why prover" - :group 'why :type '(choice (const :tag "Coq" "coq") - (const :tag "PVS" "pvs"))) - -(defcustom why-prog-name "why" - "Why executable name" - :group 'why :type 'string) - -(defcustom why-options "--valid" - "Why options" - :group 'why :type 'string) - -(defcustom why-viewer-prog-name "why_viewer" - "Why viewer executable name" - :group 'why :type 'string) - -(defun why-command-line (file) - (concat why-prog-name " -P " why-prover " " why-options " " file)) - -(defun why-find-alternate-file () - "switch to the proof obligations buffer" - (interactive) - (let* ((f (buffer-file-name)) - (fcoq (concat (file-name-sans-extension f) "_why.v"))) - (find-file fcoq))) - -(defun why-generate-obligations () - "generate the proof obligations" - (interactive) - (let ((f (buffer-name))) - (compile (why-command-line f)))) - -(defun why-viewer-command-line (file) - (concat why-viewer-prog-name " " file)) - -(defun why-viewer () - "launch the why viewer" - (interactive) - (let ((f (buffer-name))) - (compile (why-viewer-command-line f)))) - -(defun why-generate-ocaml () - "generate the ocaml code" - (interactive) - (let ((f (buffer-name))) - (compile (concat why-prog-name " --ocaml " f)))) - -;; menu - -(require 'easymenu) - -(defun why-menu () - (easy-menu-define - why-mode-menu (list why-mode-map) - "Why Mode Menu." - '("Why" - ["Customize Why mode" (customize-group 'why) t] - "---" - ["Type-check buffer" why-type-check t] - ; ["Show WP" why-show-wp t] - ["Why viewer" why-viewer t] - ["Generate obligations" why-generate-obligations t] - ["Switch to obligations buffer" why-find-alternate-file t] - ["Generate Ocaml code" why-generate-ocaml t] - ["Recolor buffer" font-lock-fontify-buffer t] - "---" - "Coq" - ["Grab next proof" why-grab-next-proof t] - "---" - "PVS" - "---" - )) - (easy-menu-add why-mode-menu)) - -;indentation - -;http://www.emacswiki.org/emacs/ModeTutorial -(defun why-indent-line () - "Indent current line as why logic" - (interactive) - (save-excursion - (beginning-of-line) - ;(debug) - (if (bobp) ; Check for rule 1 - (indent-line-to 0) - (let ((not-indented t) cur-indent) - (if (looking-at "^[ \t]*end") ; Check for rule 2 - (progn - (save-excursion - (forward-line -1) - (setq cur-indent (- (current-indentation) why-indent))) - (if (< cur-indent 0) - (setq cur-indent 0))) - (progn - (if (looking-at "^[ \t]*\\(logic\\|type\\|prop\\)") ; check for clone - (progn - (save-excursion - (forward-line -1) - (if (looking-at "^[ \t]*\\(logic\\|type\\|prop\\).*,[ \t]*$") - (progn - (setq cur-indent (current-indentation)) - (setq not-indented nil)) - (if (looking-at "^[ \t]*clone.*with ") - (progn - (setq cur-indent (+ (current-indentation) why-indent)) - (setq not-indented nil) - )))))) - ;For the definition its very badly done... - (if (looking-at "^[ \t]*$") - ;; (save-excursion - ;; (forward-line -1) - ;; (setq cur-indent (current-indentation)) - ;; (setq not-indented nil)) - (progn - (setq cur-indent 0) - (setq not-indented nil)) - (if (not - (looking-at "^[ \t]*(\*.*")) - (if (not - (looking-at "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\|use\\|theory\\|clone\\)")) - (save-excursion - (condition-case nil - (save-excursion - (backward-up-list) - (setq cur-indent (+ (current-column) 1)) - (setq not-indented nil)) - (error - (forward-line -1) - (if (looking-at - "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\)") - (setq cur-indent (+ (current-indentation) why-indent)) - (setq cur-indent (current-indentation))) - (setq not-indented nil))))))) - ;For inside theory or namespace - (save-excursion - (while not-indented - (forward-line -1) - (if (looking-at "^[ \t]*end") ; Check for rule 3 - (progn - (setq cur-indent (current-indentation)) - (setq not-indented nil)) - ; Check for rule 4 - (if (looking-at "^[ \t]*\\(theory\\|namespace\\)") - (progn - (setq cur-indent (+ (current-indentation) why-indent)) - (setq not-indented nil)) - (if (bobp) ; Check for rule 5 - (setq not-indented nil))))))) - (if cur-indent - (indent-line-to cur-indent) - (indent-line-to 0))))))) - -; compile will propose "why3ide file" is no Makefile is present - -(add-hook 'why-mode-hook - (lambda () - (unless (file-exists-p "Makefile") - (set (make-local-variable 'compile-command) - (let ((file (file-name-nondirectory buffer-file-name))) - (format "why3ide %s" file)))))) - - - -;; setting the mode -(defun why-mode () - "Major mode for editing Why programs. - -\\{why-mode-map}" - (interactive) - (kill-all-local-variables) - (why-create-syntax-table) - ; hilight - (make-local-variable 'font-lock-defaults) - (setq font-lock-defaults '(why-font-lock-keywords)) - ; indentation - ;(make-local-variable 'indent-line-function) - ;(setq indent-line-function 'why-indent-line) - ; OCaml style comments for comment-region, comment-dwim, etc. - (setq comment-start "(*" comment-end "*)") - ; menu - ; providing the mode - (setq major-mode 'why-mode) - (setq mode-name "WHY") - (use-local-map why-mode-map) - (font-lock-mode 1) - ; (why-menu) - (run-hooks 'why-mode-hook)) - -(provide 'why-mode) - diff --git a/share/emacs/why3.el b/share/emacs/why3.el new file mode 100644 index 000000000..a24394613 --- /dev/null +++ b/share/emacs/why3.el @@ -0,0 +1,176 @@ + +;; why3.el - GNU Emacs mode for Why3 + +(defvar why3-mode-hook nil) + +(defvar why3-mode-map nil + "Keymap for Why3 major mode") + +(if why3-mode-map nil + (setq why3-mode-map (make-keymap)) + ;; (define-key why3-mode-map "\C-c\C-c" 'why3-generate-obligations) **) + ;; (define-key why3-mode-map "\C-c\C-a" 'why3-find-alternate-file) **) + ;; (define-key why3-mode-map "\C-c\C-v" 'why3-viewer) **) + (define-key why3-mode-map [(control return)] 'font-lock-fontify-buffer)) + +(setq auto-mode-alist + (append + '(("\\.\\(why\\|mlw\\)" . why3-mode)) + auto-mode-alist)) + +;; font-lock + +(defun why3-regexp-opt (l) + (concat "\\<" (concat (regexp-opt l t) "\\>"))) + +(defconst why3-font-lock-keywords-1 + (list + ;; Note: comment font-lock is guaranteed by suitable syntax entries + '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face) +; '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face) + `(,(why3-regexp-opt '("invariant" "variant" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face) + `(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "try" "with" "theory" "uses" "module")) . font-lock-keyword-face) + ) + "Minimal highlighting for Why3 mode") + +(defvar why3-font-lock-keywords why3-font-lock-keywords-1 + "Default highlighting for Why3 mode") + +(defvar why3-indent 2 + "How many spaces to indent in why3 mode.") +(make-variable-buffer-local 'why3-indent) + +;; syntax + +(defvar why3-mode-syntax-table nil + "Syntax table for why3-mode") + +(defun why3-create-syntax-table () + (if why3-mode-syntax-table + () + (setq why3-mode-syntax-table (make-syntax-table)) + (set-syntax-table why3-mode-syntax-table) + (modify-syntax-entry ?' "w" why3-mode-syntax-table) + (modify-syntax-entry ?_ "w" why3-mode-syntax-table) + ; comments + (modify-syntax-entry ?\( ". 1" why3-mode-syntax-table) + (modify-syntax-entry ?\) ". 4" why3-mode-syntax-table) + (modify-syntax-entry ?* ". 23" why3-mode-syntax-table) + )) + +;indentation + +;http://www.emacswiki.org/emacs/ModeTutorial +(defun why3-indent-line () + "Indent current line as why3 logic" + (interactive) + (save-excursion + (beginning-of-line) + ;(debug) + (if (bobp) ; Check for rule 1 + (indent-line-to 0) + (let ((not-indented t) cur-indent) + (if (looking-at "^[ \t]*end") ; Check for rule 2 + (progn + (save-excursion + (forward-line -1) + (setq cur-indent (- (current-indentation) why3-indent))) + (if (< cur-indent 0) + (setq cur-indent 0))) + (progn + (if (looking-at "^[ \t]*\\(logic\\|type\\|prop\\)") ; check for clone + (progn + (save-excursion + (forward-line -1) + (if (looking-at "^[ \t]*\\(logic\\|type\\|prop\\).*,[ \t]*$") + (progn + (setq cur-indent (current-indentation)) + (setq not-indented nil)) + (if (looking-at "^[ \t]*clone.*with ") + (progn + (setq cur-indent (+ (current-indentation) why3-indent)) + (setq not-indented nil) + )))))) + ;For the definition its very badly done... + (if (looking-at "^[ \t]*$") + ;; (save-excursion + ;; (forward-line -1) + ;; (setq cur-indent (current-indentation)) + ;; (setq not-indented nil)) + (progn + (setq cur-indent 0) + (setq not-indented nil)) + (if (not + (looking-at "^[ \t]*(\*.*")) + (if (not + (looking-at "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\|use\\|theory\\|clone\\)")) + (save-excursion + (condition-case nil + (save-excursion + (backward-up-list) + (setq cur-indent (+ (current-column) 1)) + (setq not-indented nil)) + (error + (forward-line -1) + (if (looking-at + "^[ \t]*\\(logic\\|type\\|axiom\\|goal\\|lemma\\|inductive\\)") + (setq cur-indent (+ (current-indentation) why3-indent)) + (setq cur-indent (current-indentation))) + (setq not-indented nil))))))) + ;For inside theory or namespace + (save-excursion + (while not-indented + (forward-line -1) + (if (looking-at "^[ \t]*end") ; Check for rule 3 + (progn + (setq cur-indent (current-indentation)) + (setq not-indented nil)) + ; Check for rule 4 + (if (looking-at "^[ \t]*\\(theory\\|namespace\\)") + (progn + (setq cur-indent (+ (current-indentation) why3-indent)) + (setq not-indented nil)) + (if (bobp) ; Check for rule 5 + (setq not-indented nil))))))) + (if cur-indent + (indent-line-to cur-indent) + (indent-line-to 0))))))) + +; compile will propose "why3ide file" is no Makefile is present + +(add-hook 'why3-mode-hook + (lambda () + (unless (file-exists-p "Makefile") + (set (make-local-variable 'compile-command) + (let ((file (file-name-nondirectory buffer-file-name))) + (format "why3ide %s" file)))))) + + + +;; setting the mode +(defun why3-mode () + "Major mode for editing Why3 programs. + +\\{why3-mode-map}" + (interactive) + (kill-all-local-variables) + (why3-create-syntax-table) + ; hilight + (make-local-variable 'font-lock-defaults) + (setq font-lock-defaults '(why3-font-lock-keywords)) + ; indentation + ;(make-local-variable 'indent-line-function) + ;(setq indent-line-function 'why3-indent-line) + ; OCaml style comments for comment-region, comment-dwim, etc. + (setq comment-start "(*" comment-end "*)") + ; menu + ; providing the mode + (setq major-mode 'why3-mode) + (setq mode-name "Why3") + (use-local-map why3-mode-map) + (font-lock-mode 1) + ; (why3-menu) + (run-hooks 'why3-mode-hook)) + +(provide 'why3-mode) + diff --git a/share/lang/why.lang b/share/lang/why3.lang similarity index 91% rename from share/lang/why.lang rename to share/lang/why3.lang index 97dcc885c..6e0b25daf 100644 --- a/share/lang/why.lang +++ b/share/lang/why3.lang @@ -1,29 +1,22 @@ - + - text/x-why + text/x-why3 *.mlw;*.why (* *) @@ -61,7 +54,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. \%{char-esc} - + \(\*\) @@ -134,7 +127,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. \{ \} - + @@ -145,7 +138,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. \[\| \|\] - + @@ -155,7 +148,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. \[ (?<!\|)\] - + diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 3cebc3c1a..92751f85e 100644 --- a/src/ide/gmain.ml +++ b/src/ide/gmain.ml @@ -121,9 +121,9 @@ let (why_lang, any_lang) = languages_manager#set_search_path (load_path :: languages_manager#search_path); let why_lang = - match languages_manager#language "why" with + match languages_manager#language "why3" with | None -> - eprintf "language file for 'why' not found in directory %s@." + eprintf "language file for 'why3' not found in directory %s@." load_path; exit 1 | Some _ as l -> l in -- GitLab