replaced exit_use by exit_use_dir for subdirectories
authorclasohm
Tue Nov 21 12:41:52 1995 +0100 (1995-11-21)
changeset 13505bf4a54ba25f
parent 1349 ef26adb4e5b6
child 1351 4a960c012383
replaced exit_use by exit_use_dir for subdirectories
src/CCL/Makefile
src/FOL/Makefile
src/FOLP/Makefile
src/HOL/Makefile
src/HOLCF/Makefile
src/ZF/Makefile
     1.1 --- a/src/CCL/Makefile	Tue Nov 21 12:40:04 1995 +0100
     1.2 +++ b/src/CCL/Makefile	Tue Nov 21 12:41:52 1995 +0100
     1.3 @@ -55,8 +55,9 @@
     1.4  
     1.5  test:   ex/ROOT.ML  $(BIN)/CCL  $(EX_FILES)
     1.6  	case "$(COMP)" in \
     1.7 -	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/CCL ;;\
     1.8 -	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/CCL;;\
     1.9 +	poly*)	echo 'exit_use_dir"ex"; quit();' \
    1.10 +                  | $(COMP) $(BIN)/CCL ;;\
    1.11 +	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/CCL;;\
    1.12  	*)	echo Bad value for ISABELLECOMP: \
    1.13                  	$(COMP) is not poly or sml;;\
    1.14  	esac
     2.1 --- a/src/FOL/Makefile	Tue Nov 21 12:40:04 1995 +0100
     2.2 +++ b/src/FOL/Makefile	Tue Nov 21 12:41:52 1995 +0100
     2.3 @@ -58,8 +58,8 @@
     2.4  
     2.5  test:   ex/ROOT.ML  $(BIN)/FOL  $(EX_FILES) 
     2.6  	case "$(COMP)" in \
     2.7 -	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOL ;;\
     2.8 -	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/FOL;;\
     2.9 +	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOL ;;\
    2.10 +	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOL;;\
    2.11  	*)	echo Bad value for ISABELLECOMP: \
    2.12                  	$(COMP) is not poly or sml;;\
    2.13  	esac
     3.1 --- a/src/FOLP/Makefile	Tue Nov 21 12:40:04 1995 +0100
     3.2 +++ b/src/FOLP/Makefile	Tue Nov 21 12:41:52 1995 +0100
     3.3 @@ -52,8 +52,8 @@
     3.4  
     3.5  test:   ex/ROOT.ML  $(BIN)/FOLP  $(EX_FILES) 
     3.6  	case "$(COMP)" in \
     3.7 -	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/FOLP ;;\
     3.8 -	sml*)	echo 'exit_use"ex/ROOT.ML";' | $(BIN)/FOLP;;\
     3.9 +	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/FOLP ;;\
    3.10 +	sml*)	echo 'exit_use_dir"ex";' | $(BIN)/FOLP;;\
    3.11  	*)	echo Bad value for ISABELLECOMP: \
    3.12                  	$(COMP) is not poly or sml;;\
    3.13  	esac
     4.1 --- a/src/HOL/Makefile	Tue Nov 21 12:40:04 1995 +0100
     4.2 +++ b/src/HOL/Makefile	Tue Nov 21 12:41:52 1995 +0100
     4.3 @@ -72,14 +72,14 @@
     4.4  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
     4.5  
     4.6  IMP:    $(BIN)/HOL  $(IMP_FILES)
     4.7 -	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
     4.8 +	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
     4.9  
    4.10  ##Hoare logic
    4.11  Hoare_NAMES = Hoare Arith2 Examples
    4.12  Hoare_FILES = Hoare/ROOT.ML $(Hoare_NAMES:%=Hoare/%.thy) $(Hoare_NAMES:%=Hoare/%.ML)
    4.13  
    4.14  Hoare:  $(BIN)/HOL  $(Hoare_FILES)
    4.15 -	echo 'exit_use"Hoare/ROOT.ML";quit();' | $(LOGIC)
    4.16 +	echo 'exit_use_dir"Hoare";quit();' | $(LOGIC)
    4.17  
    4.18  ##The integers in HOL
    4.19  INTEG_NAMES = Equiv Integ 
    4.20 @@ -88,7 +88,7 @@
    4.21                $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
    4.22  
    4.23  Integ:  $(BIN)/HOL  $(INTEG_FILES)
    4.24 -	echo 'exit_use"Integ/ROOT.ML";quit();' | $(LOGIC)
    4.25 +	echo 'exit_use_dir"Integ";quit();' | $(LOGIC)
    4.26  
    4.27  ##I/O Automata
    4.28  IOA_NTP_NAMES = Abschannel Action Correctness Impl Lemmas Multiset Packet\
    4.29 @@ -96,7 +96,7 @@
    4.30  IOA_ABP_NAMES = Action Correctness Lemmas
    4.31  IOA_MT_NAMES = Asig IOA Option Solve
    4.32  
    4.33 -IOA_FILES = IOA/ROOT_NTP.ML IOA/ROOT_ABP.ML IOA/NTP/Spec.thy\
    4.34 +IOA_FILES = IOA/NTP/ROOT.ML IOA/ABP/ROOT.ML IOA/NTP/Spec.thy\
    4.35   $(IOA_NTP_NAMES:%=IOA/NTP/%.thy) $(IOA_NTP_NAMES:%=IOA/NTP/%.ML)\
    4.36   IOA/ABP/Abschannel.thy IOA/ABP/Abschannel_finite.thy IOA/ABP/Env.thy\
    4.37   IOA/ABP/Impl.thy IOA/ABP/Impl_finite.thy IOA/ABP/Packet.thy\
    4.38 @@ -105,8 +105,8 @@
    4.39   $(IOA_MT_NAMES:%=IOA/meta_theory/%.thy) $(IOA_MT_NAMES:%=IOA/meta_theory/%.ML)
    4.40  
    4.41  IOA:    $(BIN)/HOL  $(IOA_FILES)
    4.42 -	echo 'exit_use"IOA/ROOT_NTP.ML";quit();' | $(LOGIC)
    4.43 -#	echo 'exit_use"IOA/ROOT_ABP.ML";quit();' | $(LOGIC)
    4.44 +	echo 'exit_use_dir"IOA/NTP";quit();' | $(LOGIC)
    4.45 +	echo 'exit_use_dir"IOA/ABP";quit();' | $(LOGIC)
    4.46  
    4.47  ##Properties of substitutions
    4.48  SUBST_NAMES = AList Setplus Subst Unifier UTerm UTLemmas
    4.49 @@ -115,7 +115,7 @@
    4.50                $(SUBST_NAMES:%=Subst/%.thy) $(SUBST_NAMES:%=Subst/%.ML)
    4.51  
    4.52  Subst:  $(BIN)/HOL  $(SUBST_FILES)
    4.53 -	echo 'exit_use"Subst/ROOT.ML";quit();' | $(LOGIC)
    4.54 +	echo 'exit_use_dir"Subst";quit();' | $(LOGIC)
    4.55  
    4.56  ##Confluence of Lambda-calculus
    4.57  LAMBDA_NAMES = Lambda ParRed Commutation Eta
    4.58 @@ -123,8 +123,8 @@
    4.59  LAMBDA_FILES = Lambda/ROOT.ML \
    4.60                $(LAMBDA_NAMES:%=Lambda/%.thy) $(LAMBDA_NAMES:%=Lambda/%.ML)
    4.61  
    4.62 -Lambda:	$(BIN)/HOL  $(LAMBDA_FILES)
    4.63 -	echo 'exit_use"Lambda/ROOT.ML";quit();' | $(LOGIC)
    4.64 +Lambda:  $(BIN)/HOL $(LAMBDA_FILES)
    4.65 +	echo 'exit_use_dir"Lambda";quit();' | $(LOGIC)
    4.66  
    4.67  ##Type inference for MiniML
    4.68  MINIML_NAMES = I Maybe MiniML Type W
    4.69 @@ -132,8 +132,8 @@
    4.70  MINIML_FILES = MiniML/ROOT.ML \
    4.71                $(MINIML_NAMES:%=MiniML/%.thy) $(MINIML_NAMES:%=MiniML/%.ML)
    4.72  
    4.73 -MiniML:	$(BIN)/HOL  $(MINIML_FILES)
    4.74 -	echo 'exit_use"MiniML/ROOT.ML";quit();' | $(LOGIC)
    4.75 +MiniML: $(BIN)/HOL  $(MINIML_FILES)
    4.76 +	echo 'exit_use_dir"MiniML";quit();' | $(LOGIC)
    4.77  
    4.78  ##Lexical analysis
    4.79  LEX_FILES = Auto AutoChopper Chopper Prefix
    4.80 @@ -142,7 +142,7 @@
    4.81              $(LEX_NAMES:%=Lex/%.thy) $(LEX_NAMES:%=Lex/%.ML)
    4.82  
    4.83  Lex:	$(BIN)/HOL  $(LEX_FILES)
    4.84 -	echo 'exit_use"Lex/ROOT.ML";quit();' | $(LOGIC)
    4.85 +	echo 'exit_use_dir"Lex";quit();' | $(LOGIC)
    4.86  
    4.87  ##Miscellaneous examples
    4.88  EX_NAMES = LexProd MT Acc PropLog Puzzle Qsort LList Rec Simult Term String \
    4.89 @@ -152,7 +152,7 @@
    4.90             ex/set.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
    4.91  
    4.92  ex:     $(BIN)/HOL  $(EX_FILES)
    4.93 -	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    4.94 +	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
    4.95  
    4.96  #Full test.
    4.97  test:   $(BIN)/HOL IMP Hoare Lex Integ Subst Lambda MiniML IOA ex
     5.1 --- a/src/HOLCF/Makefile	Tue Nov 21 12:40:04 1995 +0100
     5.2 +++ b/src/HOLCF/Makefile	Tue Nov 21 12:41:52 1995 +0100
     5.3 @@ -61,8 +61,8 @@
     5.4  
     5.5  test:   ex/ROOT.ML  $(BIN)/HOLCF  $(EX_FILES) 
     5.6  	case "$(COMP)" in \
     5.7 -	poly*)	echo 'exit_use"ex/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
     5.8 -	sml*)	echo 'exit_use"ex/ROOT.ML"' | $(BIN)/HOLCF;;\
     5.9 +	poly*)	echo 'exit_use_dir"ex"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
    5.10 +	sml*)	echo 'exit_use_dir"ex"' | $(BIN)/HOLCF;;\
    5.11  	*)	echo Bad value for ISABELLECOMP: \
    5.12                  	$(COMP) is not poly or sml;;\
    5.13  	esac
    5.14 @@ -77,8 +77,9 @@
    5.15  
    5.16  test2:	explicit_domains/ROOT.ML  $(BIN)/HOLCF  $(EXPLICIT_DOMAINS_FILES) 
    5.17  	case "$(COMP)" in \
    5.18 -	poly*)	echo 'exit_use"explicit_domains/ROOT.ML"; quit();' | $(COMP) $(BIN)/HOLCF ;;\
    5.19 -	sml*)	echo 'exit_use"explicit_domains/ROOT.ML"' | $(BIN)/HOLCF;;\
    5.20 +	poly*)	echo 'exit_use_dir"explicit_domains"; quit();' \
    5.21 +                  | $(COMP) $(BIN)/HOLCF ;;\
    5.22 +	sml*)	echo 'exit_use_dir"explicit_domains"' | $(BIN)/HOLCF;;\
    5.23  	*)	echo Bad value for ISABELLECOMP: \
    5.24                  	$(COMP) is not poly or sml;;\
    5.25  	esac
     6.1 --- a/src/ZF/Makefile	Tue Nov 21 12:40:04 1995 +0100
     6.2 +++ b/src/ZF/Makefile	Tue Nov 21 12:41:52 1995 +0100
     6.3 @@ -69,7 +69,7 @@
     6.4  IMP_FILES = IMP/ROOT.ML $(IMP_NAMES:%=IMP/%.thy) $(IMP_NAMES:%=IMP/%.ML)
     6.5  
     6.6  IMP:   $(BIN)/ZF  $(IMP_FILES)
     6.7 -	echo 'exit_use"IMP/ROOT.ML";quit();' | $(LOGIC)
     6.8 +	echo 'exit_use_dir"IMP";quit();' | $(LOGIC)
     6.9  
    6.10  ##Coinduction example
    6.11  COIND_NAMES = ECR Language MT Map Static Types Values 
    6.12 @@ -78,7 +78,7 @@
    6.13                $(COIND_NAMES:%=Coind/%.thy) $(COIND_NAMES:%=Coind/%.ML)
    6.14  
    6.15  Coind:  $(BIN)/ZF  $(COIND_FILES)
    6.16 -	echo 'exit_use"Coind/ROOT.ML";quit();' | $(LOGIC)
    6.17 +	echo 'exit_use_dir"Coind";quit();' | $(LOGIC)
    6.18  
    6.19  ##AC examples
    6.20  AC_NAMES = AC_Equiv OrdQuant Transrec2 Cardinal_aux \
    6.21 @@ -92,7 +92,7 @@
    6.22             $(AC_NAMES:%=AC/%.thy) $(AC_NAMES:%=AC/%.ML)
    6.23  
    6.24  AC:  $(BIN)/ZF  $(AC_FILES)
    6.25 -	echo 'exit_use"AC/ROOT.ML";quit();' | $(LOGIC)
    6.26 +	echo 'exit_use_dir"AC";quit();' | $(LOGIC)
    6.27  
    6.28  ##Residuals example
    6.29  
    6.30 @@ -103,7 +103,7 @@
    6.31                              $(RESID_NAMES:%=Resid/%.ML)
    6.32  
    6.33  Resid:  $(BIN)/ZF  $(RESID_FILES)
    6.34 -	echo 'exit_use"Resid/ROOT.ML";quit();' | $(LOGIC)
    6.35 +	echo 'exit_use_dir"Resid";quit();' | $(LOGIC)
    6.36  
    6.37  ##Miscellaneous examples
    6.38  EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
    6.39 @@ -113,7 +113,7 @@
    6.40  
    6.41  #Test ZF by loading the examples in directory ex
    6.42  ex:     $(BIN)/ZF  $(EX_FILES)
    6.43 -	echo 'exit_use"ex/ROOT.ML";quit();' | $(LOGIC)
    6.44 +	echo 'exit_use_dir"ex";quit();' | $(LOGIC)
    6.45  
    6.46  #Full test.
    6.47  test:   $(BIN)/ZF IMP Coind AC Resid ex