src/Tools/WWW_Find/IsaMakefile
author wenzelm
Sat, 09 Jul 2011 21:53:27 +0200
changeset 43721 fad8634cee62
parent 43075 6fde0c323c15
child 45026 5c0b0d67f9b1
permissions -rw-r--r--
echo prover input via raw_messages, for improved protocol tracing;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     1
#
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     2
# IsaMakefile for WWW_Find
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     3
#
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     4
# Provides static compile check for ML files only.
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     5
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
     6
## targets
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
     7
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
     8
default: Pure-WWW_Find
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
     9
images:
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    10
test: Pure-WWW_Find
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    11
all: images test
42157
99e359a9db27 added missing smlnj target
krauss
parents: 33822
diff changeset
    12
smlnj: all
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    13
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    14
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    15
## global settings
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    16
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    17
SRC = $(ISABELLE_HOME)/src
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    18
OUT = $(ISABELLE_OUTPUT)
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    19
LOG = $(OUT)/log
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    20
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    21
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    22
## Pure-WWW_Find
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    23
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    24
LOGFILE = $(LOG)/Pure-WWW_Find.gz
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    25
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    26
Pure-WWW_Find: Pure $(LOGFILE)
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    27
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    28
Pure:
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    29
	@cd $(SRC)/Pure; $(ISABELLE_TOOL) make Pure
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    30
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    31
$(LOGFILE): $(OUT)/Pure echo.ML find_theorems.ML html_unicode.ML \
43073
a4c985fe015d moved html templates to a separate module, making their awkward signatures explicit
krauss
parents: 42157
diff changeset
    32
  html_templates.ML http_status.ML http_util.ML mime.ML scgi_req.ML \
43075
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43073
diff changeset
    33
  scgi_server.ML socket_util.ML unicode_symbols.ML xhtml.ML yxml_find_theorems.ML \
6fde0c323c15 added experimental yxml_find_theorems web service (but no client yet)
krauss
parents: 43073
diff changeset
    34
  ROOT.ML
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    35
	@cd ..; $(ISABELLE_TOOL) usedir Pure WWW_Find
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    36
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    37
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    38
## clean
33817
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    39
f6a4da31f2f1 WWW_Find component: find_theorems via web browser
kleing
parents:
diff changeset
    40
clean:
33822
e332b08bf0f3 provide standard isabelle make targets;
wenzelm
parents: 33817
diff changeset
    41
	@rm -f $(LOGFILE)