[emacs] why.el renamed to why3.el

[GTK sourceview] why.lang renamed to why3.lang

CHANGES

 * 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
 ==========================

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.
 

share/emacs/why.el → share/emacs/why3.el

 
-;; why.el - GNU Emacs mode for Why
-;; Copyright (C) 2002 Jean-Christophe FILLIATRE
+;; why3.el - GNU Emacs mode for Why3
 
-(defvar why-mode-hook nil)
+(defvar why3-mode-hook nil)
 
-(defvar why-mode-map nil
-  "Keymap for Why major mode")
+(defvar why3-mode-map nil
+  "Keymap for Why3 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))
+(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\\)" . why-mode))
+       '(("\\.\\(why\\|mlw\\)" . why3-mode))
        auto-mode-alist))
 
 ;; font-lock
 
-(defun why-regexp-opt (l)
+(defun why3-regexp-opt (l)
   (concat "\\<" (concat (regexp-opt l t) "\\>")))
 
-(defconst why-font-lock-keywords-1
+(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)
-   `(,(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)
+;   '("{}\\|{[^|]\\([^}]*\\)}" . 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 Why mode")
+  "Minimal highlighting for Why3 mode")
 
-(defvar why-font-lock-keywords why-font-lock-keywords-1
-  "Default highlighting for Why mode")
+(defvar why3-font-lock-keywords why3-font-lock-keywords-1
+  "Default highlighting for Why3 mode")
 
-(defvar why-indent 2
-  "How many spaces to indent in why mode.")
-(make-variable-buffer-local 'why-indent)
+(defvar why3-indent 2
+  "How many spaces to indent in why3 mode.")
+(make-variable-buffer-local 'why3-indent)
 
 ;; syntax
 
-(defvar why-mode-syntax-table nil
-  "Syntax table for why-mode")
+(defvar why3-mode-syntax-table nil
+  "Syntax table for why3-mode")
 
-(defun why-create-syntax-table ()
-  (if why-mode-syntax-table
+(defun why3-create-syntax-table ()
+  (if why3-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)
+    (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" why-mode-syntax-table)
-    (modify-syntax-entry ?\) ". 4" why-mode-syntax-table)
-    (modify-syntax-entry ?* ". 23" why-mode-syntax-table)
+    (modify-syntax-entry ?\( ". 1" why3-mode-syntax-table)
+    (modify-syntax-entry ?\) ". 4" why3-mode-syntax-table)
+    (modify-syntax-entry ?* ". 23" why3-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"
+(defun why3-indent-line ()
+  "Indent current line as why3 logic"
   (interactive)
   (save-excursion
     (beginning-of-line)
@@ -173,7 +74,7 @@
             (progn
               (save-excursion
                 (forward-line -1)
-                (setq cur-indent (- (current-indentation) why-indent)))
+                (setq cur-indent (- (current-indentation) why3-indent)))
               (if (< cur-indent 0)
                   (setq cur-indent 0)))
           (progn
@@ -187,7 +88,7 @@
                           (setq not-indented nil))
                       (if (looking-at "^[ \t]*clone.*with ")
                           (progn
-                            (setq cur-indent (+ (current-indentation) why-indent))
+                            (setq cur-indent (+ (current-indentation) why3-indent))
                             (setq not-indented nil)
                             ))))))
         ;For the definition its very badly done...
@@ -213,7 +114,7 @@
                      (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) why3-indent))
                        (setq cur-indent (current-indentation)))
                      (setq not-indented nil)))))))
           ;For inside theory or namespace
@@ -227,7 +128,7 @@
                                         ; Check for rule 4
                 (if (looking-at "^[ \t]*\\(theory\\|namespace\\)")
                     (progn
-                      (setq cur-indent (+ (current-indentation) why-indent))
+                      (setq cur-indent (+ (current-indentation) why3-indent))
                       (setq not-indented nil))
                   (if (bobp) ; Check for rule 5
                       (setq not-indented nil)))))))
@@ -237,7 +138,7 @@
 
 ; compile will propose "why3ide file" is no Makefile is present
 
-(add-hook 'why-mode-hook
+(add-hook 'why3-mode-hook
           (lambda ()
             (unless (file-exists-p "Makefile")
               (set (make-local-variable 'compile-command)
@@ -247,29 +148,29 @@
 
 
 ;; setting the mode
-(defun why-mode ()
-  "Major mode for editing Why programs.
+(defun why3-mode ()
+  "Major mode for editing Why3 programs.
 
-\\{why-mode-map}"
+\\{why3-mode-map}"
   (interactive)
   (kill-all-local-variables)
-  (why-create-syntax-table)
+  (why3-create-syntax-table)
   ; hilight
   (make-local-variable 'font-lock-defaults)
-  (setq font-lock-defaults '(why-font-lock-keywords))
+  (setq font-lock-defaults '(why3-font-lock-keywords))
   ; indentation
   ;(make-local-variable 'indent-line-function)
-  ;(setq indent-line-function 'why-indent-line)
+  ;(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 'why-mode)
-  (setq mode-name "WHY")
-  (use-local-map why-mode-map)
+  (setq major-mode 'why3-mode)
+  (setq mode-name "Why3")
+  (use-local-map why3-mode-map)
   (font-lock-mode 1)
-  ; (why-menu)
-  (run-hooks 'why-mode-hook))
+  ; (why3-menu)
+  (run-hooks 'why3-mode-hook))
 
-(provide 'why-mode)
+(provide 'why3-mode)
 

share/lang/why.lang → share/lang/why3.lang

 <?xml version="1.0" encoding="UTF-8"?>
 <!--
 
-Copyright (C) 2010-
-  Francois Bobot
-  Jean-Christophe Filliatre
-  Johannes Kanig
-  Andrei Paskevich
+The Why3 Verification Platform   /   The Why3 Development Team
+Copyright 2010-2013   -    INRIA - CNRS - Paris-Sud University
 
-This software is free software; you can redistribute it and/or
-modify it under the terms of the GNU Library General Public
-License version 2.1, with the special exception on linking
-described in file LICENSE.
+This software is distributed under the terms of the GNU Lesser
+General Public License version 2.1, with the special exception
+on linking described in file LICENSE.
 
-This software is distributed in the hope that it will be useful,
-but WITHOUT ANY WARRANTY; without even the implied warranty of
-MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 -->
 <!--
  This file was based on ocaml.lang by
  Copyright (C) 2007 Eric Cooper <ecc@cmu.edu>
  Copyright (C) 2007 Eric Norige <thelema314@gmail.com>
 -->
-<language id="why" _name="Why3" version="2.0" _section="Sources">
+<language id="why3" _name="Why3" version="2.0" _section="Sources">
   <metadata>
-    <property name="mimetypes">text/x-why</property>
+    <property name="mimetypes">text/x-why3</property>
     <property name="globs">*.mlw;*.why</property>
     <property name="block-comment-start">(*</property>
     <property name="block-comment-end">*)</property>
@@ -61,7 +54,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
       <match>\%{char-esc}</match>
     </context>
     <!-- here's the main context -->
-    <context id="why">
+    <context id="why3">
       <include>
 	<context id="symbol-star">
 	  <match>\(\*\)</match>
@@ -134,7 +127,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 	  <start>\{</start>
 	  <end>\}</end>
 	  <include>
-	    <context ref="why"/>
+	    <context ref="why3"/>
 	  </include>
 	</context>
 	<context id="badrecord" style-ref="error" extend-parent="false">
@@ -145,7 +138,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 	  <start>\[\|</start>
 	  <end>\|\]</end>
 	  <include>
-	    <context ref="why"/>
+	    <context ref="why3"/>
 	  </include>
 	</context>
 	<context id="badarray" style-ref="error" extend-parent="false">
@@ -155,7 +148,7 @@ MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
 	  <start>\[</start>
 	  <end>(?&lt;!\|)\]</end>
 	  <include>
-	    <context ref="why"/>
+	    <context ref="why3"/>
 	  </include>
 	</context>
 	<context id="badlist" style-ref="error" extend-parent="false">

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