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

PVS Bug 565


Synopsis:        M-x siblings shifts *pvs* buffer
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed May 16 12:55:00 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  consider the following theory
  
      A : theory
      Begin
        a : Lemma 
  	    1 = 1 AND
  	    2 = 2 AND
  	    3 = 3 AND
  	    4 = 4 AND
  	    5 = 5 AND
  	    6 = 6 AND
  	    7 = 7 
  	 IMPLIES
  	    1 = 2 and 3 = 4 and 5 = 6 and 7 = 8 and 9 = 10
      end A
  
  invoke a proof with C-c p on a and do flatten followed by prop.
  Then do M-x siblings. This moves point in the *pvs* buffer such
  that the last proof state is not visible.
  
  I used PVS Version 2.3 (patch level 1.2.2.133) on Debian linux
  2.2.18.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed the output filter so that point remains the same when another
 buffer is popped up from lisp.

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