# HG changeset patch
# User kleing
# Date 1080543266 -7200
# Node ID 7b37aa726d2dfcbf63f96b0bb5fa8429844832fa
# Parent  3676def6b8b98c488b05a13bb7483e6d7e86ce37
allow sections in contents file

diff -r 3676def6b8b9 -r 7b37aa726d2d Admin/page/Contents
--- a/Admin/page/Contents	Fri Mar 26 19:58:43 2004 +0100
+++ b/Admin/page/Contents	Mon Mar 29 08:54:26 2004 +0200
@@ -1,1 +1,2 @@
-dummy	Dummy Isabelle documentation entry
+Dummy Heading
+  dummy	Dummy Isabelle documentation entry
diff -r 3676def6b8b9 -r 7b37aa726d2d Admin/page/bin/mkcontents
--- a/Admin/page/bin/mkcontents	Fri Mar 26 19:58:43 2004 +0100
+++ b/Admin/page/bin/mkcontents	Mon Mar 29 08:54:26 2004 +0200
@@ -24,25 +24,39 @@
 $infile  = $ARGV[0];
 $outfile = $ARGV[1];
 
-$fileHeader = "<ul>\n";
+$listHeader = "<ul>\n";
 $lineHeader = "  <li>";
 $lineEnd    = "</li>\n";
-$fileFooter = "</ul>\n";
+$listFooter = "</ul>\n";
+
+$topicStart = "<h2>";
+$topicEnd   = "</h2>\n";
 
 open(IN, "<$infile") || die "cannot read input file <$infile>";
 open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
 
-print OUT $fileHeader;
-
+$first = 1;
 while (<IN>) {
-  if (/[ \t]*([^ \t]+)[ \t]+(.+)\n/) {
+  if (/^([^ \t].*)\n/) {
+    if ($first == 1) {
+      $first = 0;
+    }
+    else {
+      print OUT $listFooter;
+    }
+    print OUT $topicStart;
+    print OUT $1;
+    print OUT $topicEnd;
+    print OUT $listHeader;
+  }
+  elsif (/^[ \t]+([^ \t]+)[ \t]+(.+)\n/) {
     print OUT $lineHeader;
     print OUT "<a href=\"$path$1.pdf\">$2</a>";
     print OUT $lineEnd;
   }
 }
 
-print OUT $fileFooter;
+print OUT $listFooter;
 
 close(OUT);
 close(IN);