[r2003-01-16 20:50:09 by cvscast] Petites modifs au web/index2.xml et web/macros2.xml - Beppe

Original author: cvscast Date: 2003-01-16 20:50:09+00:00

[r2003-01-16 20:50:09 by cvscast] Petites modifs au web/index2.xml et web/macros2.xml - Beppe
Original author: cvscast Date: 2003-01-16 20:50:09+00:00
ebd3d147 · Pietro Abate · 83d31a86 · ebd3d147
Commit ebd3d147 authored Oct 05, 2007 by Pietro Abate
--- a/web/macros2.cd
+++ b/web/macros2.cd
@@ -19,7 +19,7 @@ let fun box (title : Any, subtitle : Any, name : Any, content : XML) : XML =
 ]];;

 let fun convert (XML_elem | Char | XML | PHP -> XML)
- | <php> s -> "<?php" @ s @ "?>"
+ | (<php>_) & x -> [ x ]
 | <box ({ title=t } 
         & ({ subtitle=st } | (st := `nil))
         & ({ link=name } | (name := `nil)) )>x -> 
@@ -44,7 +44,9 @@ let out : String =
  [ '<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">' ]
  @
-  (transform convert src with x -> print_xml x);;
+  (transform convert src with
+       x -> print_xml x);;
+

 dump_to_file "index.php" out;;