Test files for multiple file handling with Isabelle.


Test schedule
=============

[C depends on A and B, D is independent]

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

Borrowed from Thomas's lego tests:  (v 1.2)

 1) visit A.ML                EFFECTS A
 2) visit C.ML                EFFECTS A     C
 3) assert C                  EFFECTS A*    C*
 4) visit B.ML,B.thy,C.thy    EFFECTS A* B* C*    C.thy* B.thy*
 5) visit D.ML,D.thy          EFFECTS A* B* C* D  D.thy
 6) retract to middle of B    EFFECTS A* B  C  D  B.thy* (*thy remains locked*)
 7) assert first command of B EFFECTS A* B+ C  D
 8) assert C                  EFFECTS A* B+ C  D [error message, correctly]
 9) assert B                  EFFECTS A* B* C  D 
10) assert D                  EFFECTS A* B* C  D*  D.thy*
11) retract B                 EFFECTS A* B  C  D? [D* D.thy* for Isabelle]
12) assert C                  EFFECTS A* B* C* D? 
13) retract B                 EFFECTS A* B  C  D? [B.thy* D*,D.thy* again]
14) assert B                  EFFECTS A* B* C  D? 
15) assert C                  EFFECTS A* B* C* D? [everything locked]
16) retract to middle of B    EFFECTS A* B+ C  D?
	BROKEN!  Now retracts whole thing.
14) M-x proof-restart-script  EFFECTS A  B  C  D  


MORE TESTS NEEDED FOR ISABELLE:
===============================

Should test assertion of theory files, and watch what happens to ML files.

Because of theory loader's odd behaviour, must watch what happens
to ML files of autoloaded children.


1) visit example.ML, example.thy       EFFECT: ML thy
2) assert .ML			       EFFECT: ML* thy*
3) retract thy			       EFFECT: ML thy


1) visit example.ML, example.thy       ML thy
2) assert thy			       ML* thy*   (reads theory too)


(* Test case for outdating a child theory *)

1) assert C.thy		        A*, B*, C*
2) retract B.thy		A*
3) edit B.thy to touch timestamp
4) assert B.thy			A*, B*, C  Message: "C out of date"
5) assert C.thy			A*, B*, C*


(* Test case for removing a dependency from a theory:
   this automatically unlocks the orphaned theory,
   is this right??
*)   

1) assert C.thy			A*, B*, C*
2) retract C.thy		A*, B*, C
3) edit C.thy to C=A, remove dependency on B
4) assert C.thy		        A*, B, C*      (B automatically unlocked)