# HG changeset patch
# User haftmann
# Date 1330853627 -3600
# Node ID a4ae06650a0a5f2249cc9579006f1d1070cb1f8c
# Parent  04f2d3c510d0c5be7731ba4c0f81852e1daaf3d9
dropped images for importer sessions

diff -r 04f2d3c510d0 -r a4ae06650a0a src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Sun Mar 04 00:29:19 2012 +0100
+++ b/src/HOL/IsaMakefile	Sun Mar 04 10:33:47 2012 +0100
@@ -11,6 +11,10 @@
   HOL-Library \
   HOL-Algebra \
   HOL-Boogie \
+  HOL-HOL4 \
+  HOL-HOL_Light \
+  HOL-HOL4-Imported \
+#  HOL-HOL_Light-Imported \  FIXME not operative at the moment \
   HOL-IMP \
   HOL-Multivariate_Analysis \
   HOL-NSA \
@@ -19,10 +23,6 @@
   HOL-SPARK \
   HOL-Word \
   HOLCF \
-  Import-HOL4 \
-  Import-HOL_Light \
-  Import-HOL4-Imported \
-#  Import-HOL_Light-Imported \  FIXME not operative at the moment \
   IOA \
   TLA \
   HOL-Base \
@@ -83,8 +83,8 @@
     # ^ this is the sort position
 
 generate: \
-  Import-HOL4-Generate \
-  Import-HOL_Light-Generate
+  HOL-HOL4-Generate \
+  HOL-HOL_Light-Generate
 
 benchmark: \
   HOL-Datatype_Benchmark \
@@ -557,35 +557,44 @@
 
 ## Import sessions
 
-Import-HOL4: $(OUT)/Import-HOL4
-
-BASIC_IMPORTER_DEPENDENCIES = Import/Importer.thy \
+IMPORTER_BASIC_DEPENDENCIES = \
+  Import/Importer.thy \
   Import/shuffler.ML \
   Import/import_rews.ML \
   Import/proof_kernel.ML \
   Import/replay.ML \
   Import/import.ML
 
-$(OUT)/Import-HOL4: $(OUT)/HOL \
-  $(BASIC_IMPORTER_DEPENDENCIES) \
+IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES = \
   Import/HOL4/ROOT.ML \
   Import/HOL4/Compatibility.thy
-	@cd Import/HOL4; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL4
 
-Import-HOL_Light: $(OUT)/Import-HOL_Light
-
-$(OUT)/Import-HOL_Light: $(OUT)/HOL \
-  $(BASIC_IMPORTER_DEPENDENCIES) \
+IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES = \
   Import/HOL_Light/ROOT.ML \
   Import/HOL_Light/HOLLightInt.thy \
   Import/HOL_Light/HOLLightList.thy \
   Import/HOL_Light/HOLLightReal.thy \
   Import/HOL_Light/Compatibility.thy
-	@cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b $(OUT)/HOL Import-HOL_Light
+
+HOL-HOL4: $(LOG)/HOL-HOL4.gz
+
+$(LOG)/HOL-HOL4.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES)
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL4
+
+HOL-HOL_Light: $(LOG)/HOL-HOL_Light.gz
 
-Import-HOL4-Imported: $(OUT)/Import-HOL4-Imported
+$(LOG)/HOL-HOL_Light.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES)
+	@$(ISABELLE_TOOL) usedir $(OUT)/HOL Import/HOL_Light
 
-$(OUT)/Import-HOL4-Imported: $(OUT)/Import-HOL4 \
+HOL-HOL4-Imported: $(LOG)/HOL-HOL4-Imported.gz
+
+$(LOG)/HOL-HOL4-Imported.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \
   Import/HOL4/imported.ML \
   Import/HOL4/Imported.thy \
   Import/HOL4/Generated/HOL4Base.thy \
@@ -641,20 +650,24 @@
   Import/HOL4/Generated/word_base.imp \
   Import/HOL4/Generated/word_bitop.imp \
   Import/HOL4/Generated/word_num.imp
-	@cd Import/HOL4; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL4 Import-HOL4-Imported
+	@$(ISABELLE_TOOL) usedir -f imported.ML -s HOL4-Imported -p 0 $(OUT)/HOL Import/HOL4
+
+HOL-HOL_Light-Imported: $(LOG)/HOL-HOL_Light-Imported.gz
 
-Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light-Imported
-
-$(OUT)/Import-HOL_Light-Imported: $(OUT)/Import-HOL_Light \
+$(LOG)/HOL-HOL_Light-Imported.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \
   Import/HOL_Light/imported.ML \
   Import/HOL_Light/Imported.thy \
   Import/HOL_Light/Generated/HOLLight.thy \
   Import/HOL_Light/Generated/hollight.imp
-	@cd Import/HOL_Light; $(ISABELLE_TOOL) usedir -b -f imported.ML -p 0 $(OUT)/Import-HOL_Light Import-HOL_Light-Imported
+	@$(ISABELLE_TOOL) usedir -f imported.ML -s HOL_Light-Imported -p 0 $(OUT)/HOL Import/HOL_Light
+
+HOL-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz
 
-Import-HOL4-Generate: $(LOG)/Import-HOL4-Generate.gz
-
-$(LOG)/Import-HOL4-Generate.gz: $(OUT)/Import-HOL4 \
+$(LOG)/Import-HOL4-Generate.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL4_COMPATIBILITY_DEDEPENDENCIES) \
   Import/HOL4/generate.ML \
   Import/HOL4/Generate.thy \
   Import/HOL4/Template/GenHOL4Base.thy \
@@ -662,15 +675,17 @@
   Import/HOL4/Template/GenHOL4Real.thy \
   Import/HOL4/Template/GenHOL4Vec.thy \
   Import/HOL4/Template/GenHOL4Word32.thy
-	@cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL4 HOL4
+	@$(ISABELLE_TOOL) usedir -f generate.ML -s HOL4-Generate -p 0 $(OUT)/HOL Import/HOL4
+
+HOL-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz
 
-Import-HOL_Light-Generate: $(LOG)/Import-HOL_Light-Generate.gz
-
-$(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/Import-HOL_Light \
+$(LOG)/Import-HOL_Light-Generate.gz: $(OUT)/HOL \
+  $(IMPORTER_BASIC_DEPENDENCIES) \
+  $(IMPORTER_HOL_LIGHT_COMPATIBILITY_DEDEPENDENCIES) \
   Import/HOL_Light/generate.ML \
   Import/HOL_Light/Generate.thy \
   Import/HOL_Light/Template/GenHOLLight.thy
-	@cd Import; $(ISABELLE_TOOL) usedir -f generate.ML -s Generate -p 0 $(OUT)/Import-HOL_Light HOL_Light
+	@$(ISABELLE_TOOL) usedir -f generate.ML -s HOL_Light-Generate -p 0 $(OUT)/HOL Import/HOL_Light
 
 
 ## HOL-Number_Theory