Handling of Multiple Files
==========================

[C depends on A and B]

Notation: A  means that buffer A.l is unlocked
          A+ means that buffer A.l is partly locked
          A* means that buffer A.l is locked
	  ? means that behaviour might be different for proof systems
  	    with non-linear contexts


Test Protocol
-------------

 1) visit A.l                 EFFECTS A
 2) visit C.l                 EFFECTS A     C
 3) assert C                  EFFECTS A*    C*
 4) visit B.l                 EFFECTS A* B* C*
 5) visit D.l                 EFFECTS A* B* C* D
 6) retract to middle of B    EFFECTS A* B  C  D
 7) assert first command of B EFFECTS A* B+ C  D
 8) assert C                  EFFECTS A* B+ C  D [error message]
 9) assert B                  EFFECTS A* B* C  D
10) assert D                  EFFECTS A* B* C  D*
11) retract B                 EFFECTS A* B  C  D?
12) assert C                  EFFECTS A* B* C* D?
13) retract B                 EFFECTS A* B  C  D?
14) assert B                  EFFECTS A* B* C  D?
15) assert C                  EFFECTS A* B* C* D?
16) retract to middle of B    EFFECTS A* B+ C  D?
14) M-x proof-shell-restart   EFFECTS A  B  C  D