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

PVS Bug 1017


Synopsis:        changing the default proof changes the cursor position
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Nov 27 14:50:00 2007
Originator:      Hendrik Tews
Organization:    cs.ru.nl
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  changing the default proof (in a Display Proofs buffer) changes
  the position of the emacs cursor. Typically to 21 lines below, if
  there is enough space in the theory. This can be reproduces with
  any lemma that has two proofs. I can provide concrete data if
  necessary. 
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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