author | wenzelm |
Sat, 09 Jul 2011 21:53:27 +0200 | |
changeset 43721 | fad8634cee62 |
parent 43075 | 6fde0c323c15 |
child 43948 | 8f5add916a99 |
permissions | -rw-r--r-- |
33817 | 1 |
if String.isPrefix "polyml" ml_system |
2 |
then |
|
3 |
(use "unicode_symbols.ML"; |
|
4 |
use "html_unicode.ML"; |
|
5 |
use "mime.ML"; |
|
6 |
use "http_status.ML"; |
|
7 |
use "http_util.ML"; |
|
8 |
use "xhtml.ML"; |
|
9 |
use "socket_util.ML"; |
|
10 |
use "scgi_req.ML"; |
|
11 |
use "scgi_server.ML"; |
|
12 |
use "echo.ML"; |
|
43073
a4c985fe015d
moved html templates to a separate module, making their awkward signatures explicit
krauss
parents:
33817
diff
changeset
|
13 |
use "html_templates.ML"; |
43075
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43073
diff
changeset
|
14 |
use "find_theorems.ML"; |
6fde0c323c15
added experimental yxml_find_theorems web service (but no client yet)
krauss
parents:
43073
diff
changeset
|
15 |
use "yxml_find_theorems.ML") |
33817 | 16 |
else () |