1CLINE_OPTIONS = --no_overlay
2TARGETS = $(patsubst %.sml,%.uo,$(TARGETS0))
3
4FTHM_UI = $(protect $(SIGOBJ)/FinalThm-sig.ui)
5FTHM_UID = $(dprot $(SIGOBJ)/FinalThm-sig.ui)
6FTAG_UID = $(dprot $(SIGOBJ)/FinalTag-sig.ui)
7FTAG_UI = $(protect $(SIGOBJ)/FinalTag-sig.ui)
8FTYPE_UI = $(protect $(SIGOBJ)/FinalType-sig.ui)
9FTERM_UI = $(protect $(SIGOBJ)/FinalTerm-sig.ui)
10
11TAG_UOD = $(dprot $(SIGOBJ)/Tag.uo)
12TYPE_UOD = $(dprot $(SIGOBJ)/Type.uo)
13TERM_UID = $(dprot $(SIGOBJ)/Term.ui)
14TERM_UOD = $(dprot $(SIGOBJ)/Term.uo)
15NET_UOD = $(dprot $(SIGOBJ)/Net.uo)
16
17
18.PHONY: all
19all: $(patsubst %.sml,%.uo,$(wildcard *.sml)) Thm.uo
20
21ifeq ($(KERNELID),otknl)
22Thm.sml: otknl-thm.ML
23	$(CP) $< $@
24
25Thm.sig: otknl-thmsig.ML
26	$(CP) $< $@
27
28else
29Thm.sml: std-thm.ML
30	$(CP) $< $@
31
32Thm.sig: std-thmsig.ML
33	$(CP) $< $@
34
35endif
36
37Thm.ui: Thm.sig $(FTHM_UID) $(TERM_UID) $(TAG_UOD)
38	$(HOLMOSMLC) -c $(FTHM_UI) $<
39
40Thm.uo: Thm.ui
41
42Overlay.uo: Overlay.sml $(TYPE_UOD) $(TERM_UOD) $(FTAG_UID) Thm.uo \
43            $(NET_UOD)
44	$(HOLMOSMLC) -c -toplevel $(FTYPE_UI) $(FTERM_UI) \
45	                       Thm.ui $(FTAG_UI) Net.ui  Overlay.sml
46
47
48
49EXTRA_CLEANS = Thm.sml Thm.sig
50