Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 781


Synopsis:        minute highlighting omission: CODATATYPE
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Jun 18 23:20:00 2003
Originator:      Kai Engelhardt
Organization:    cse.unsw.edu.au
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  ----Next_Part(Thu_Jun_19_15:56:28_2003_254)--
  Content-Type: Text/Plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  The keyword CODATATYPE was missing from the definition of pvs-keywords
  in pvs-menu.el. To keep the attached patch small, the line length is
  slightly larger than usual. (I assume that pvs-menu.el in
  emacs/emacs20 and xemacs21 are linked to the one I patch in
  emacs/emacs-src, which they are not in the distribution, but perhaps
  in your sources.)
  
  BTW the Makefiles mentioned in emacs/README don't exist (anymore).
  
  Cheers,
  Kai
  
  ----Next_Part(Thu_Jun_19_15:56:28_2003_254)--
  Content-Type: Text/Plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline; filename=codatatype-hilitpatch
  
  *** pvs3.1-orig/emacs/emacs-src/pvs-menu.el	Tue Feb 11 21:11:16 2003
  --- pvs3.1-patched/emacs/emacs-src/pvs-menu.el	Thu Jun 19 15:28:34 200
 3
  ***************
  *** 240,244 ****
      '("AND" "ANDTHEN" "ARRAY" "AS" "ASSUMING" "ASSUMPTION" "AUTO_REWRITE"
        "AUTO_REWRITE+" "AUTO_REWRITE-" "AXIOM" "BEGIN" "BUT" "BY" "CASES"
  !     "CHALLENGE" "CLAIM" "CLOSURE" "COINDUCTIVE" "COND" "CONJECTURE"
        "CONTAINING" "CONVERSION" "CONVERSION+" "CONVERSION-" "COROLLARY"
        "DATATYPE" "ELSE" "ELSIF" "END" "ENDASSUMING" "ENDCASES" "ENDCOND" "END
 IF"
  --- 240,244 ----
      '("AND" "ANDTHEN" "ARRAY" "AS" "ASSUMING" "ASSUMPTION" "AUTO_REWRITE"
        "AUTO_REWRITE+" "AUTO_REWRITE-" "AXIOM" "BEGIN" "BUT" "BY" "CASES"
  !     "CHALLENGE" "CLAIM" "CLOSURE" "CODATATYPE" "COINDUCTIVE" "COND" "CONJEC
 TURE"
        "CONTAINING" "CONVERSION" "CONVERSION+" "CONVERSION-" "COROLLARY"
        "DATATYPE" "ELSE" "ELSIF" "END" "ENDASSUMING" "ENDCASES" "ENDCOND" "END
 IF"
  
  ----Next_Part(Thu_Jun_19_15:56:28_2003_254)----

How-To-Repeat: 

Fix: 
Added the CODATATYPE keyword as suggested.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools