# HG changeset patch
# User haftmann
# Date 1115371999 -7200
# Node ID 7f3ccb84e60d264238225ba0fabf6d648042400d
# Parent  2c351ab6c403f13a138d308dac24e1ae952323ee
added option 'tidy=' to makefile, for optional processing of results by HTML tidy

diff -r 2c351ab6c403 -r 7f3ccb84e60d Admin/page/Makefile
--- a/Admin/page/Makefile	Fri May 06 11:30:10 2005 +0200
+++ b/Admin/page/Makefile	Fri May 06 11:33:19 2005 +0200
@@ -1,6 +1,17 @@
 # -- makefile for Isabelle web pages (dist and main)
 # -- $Id$
 
+# --- force shell
+SHELL=bash
+
+# --- check parameters
+ifeq ($(tidy),)
+    TIDYCMD=:
+else
+    TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \
+                --logical-emphasis yes --gnu-emacs yes --write-back yes
+endif
+
 # --- external tools
 
 GENPAGE   = ./bin/genpage
@@ -48,6 +59,10 @@
 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
 	@env DISTNAME=`cat DISTNAME` \
 	  $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
+	-@cd $(MAIN_TARGET); \
+        for html in *.html; \
+            do $(TIDYCMD) $$html; \
+        done
 
 pub-main: main
 	@echo "Publishing main pages (*.html only)."
@@ -58,6 +73,10 @@
 	@$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
 	@env DISTNAME=`cat DISTNAME` \
 	  $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
+	-@cd $(MAIN_TARGET); \
+        for html in *.html; \
+            do $(TIDYCMD) $$html; \
+        done
 
 pub-dist: dist
 	@echo "Publishing dist pages (*.html only)."