filter/tex/displaytex.php

   1 <?php // $Id$
   2       // This script displays tex source code.
   3
   4     $texexp = urldecode($_SERVER['QUERY_STRING']);
   5     // entities are usually encoded twice, first in HTML editor then in tex/filter.php
   6     $texexp = html_entity_decode(html_entity_decode($texexp));
   7     // encode all entities
   8     $texexp = htmlentities($texexp);
   9 ?>
  10 <html>
  11   <head>
  12     <title>TeX Source</title>
  13     <meta http-equiv="content-type" content="text/html; charset=iso-8859-1" />
  14   </head>
  15   <body bgcolor="#FFFFFF">
  16     <?php echo $texexp; ?>
  17   </body>
  18 </html>