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