)([^<]*)(<\/div>)/', 'escape_verbatim', $html);
$html = preg_replace_callback('/(
)([^<]*)(<\/pre>)/', 'escape_verbatim', $html);
//
$html = preg_replace_callback('/([^<]*)<\/code>/', 'escape_verb', $html);
//runbar
$html = preg_replace('//',
'\href{http://www.pradosoft.com/demos/quickstart/index.php?page=$1}{$1 Demo}', $html);
//DocLink
$html = preg_replace('//',
'\href{http://www.pradosoft.com/docs/manual/$1/$2.html}{$1.$2 API Reference}', $html);
//text modifiers
$html = preg_replace('/([^<]*)<\/b>/', '\textbf{$1}', $html);
$html = preg_replace('/([^<]*)<\/i>/', '\emph{$1}', $html);
$html = preg_replace_callback('/([^<]*)<\/tt>/', 'texttt', $html);
//links
$html = preg_replace_callback('/]+href="([^"]*)"[^>]*>([^<]*)<\/a>/',
'make_link', $html);
//anchor
$html = preg_replace_callback('/]+name="([^"]*)"[^>]*><\/a>/', 'anchor', $html);
//description
$html = preg_replace('/- ([^<]*)<\/dt>/', '\item[$1]', $html);
$html = preg_replace('/<\/?dd>/', '', $html);
$html = preg_replace('/
/', '\begin{description}', $html);
$html = preg_replace('/<\/dl>/', '\end{description}', $html);
//item lists
$html = preg_replace('//', '\begin{itemize}', $html);
$html = preg_replace('/<\/ul>/', '\end{itemize}', $html);
$html = preg_replace('//', '\begin{enumerate}', $html);
$html = preg_replace('/<\/ol>/', '\end{enumerate}', $html);
$html = preg_replace('/- /', '\item ', $html);
$html = preg_replace('/<\/li>/', '', $html);
//headings
$html = preg_replace('/
([^<]+)<\/h1>/', '\section{$1}', $html);
$html = preg_replace('/([^<]+)<\/h2>/', '\subsection{$1}', $html);
$html = preg_replace('/([^<]+)<\/h3>/', '\subsubsection{$1}', $html);
$html = html_entity_decode($html);
return $html;
}
function get_chapter_label($chapter)
{
return '\hypertarget{'.str_replace(' ', '', $chapter).'}{}';
}
function get_section_label($section)
{
$section = str_replace('.page', '', $section);
return '\hypertarget{'.str_replace('/', '.', $section).'}{}';
}
function set_header_id($content, $count)
{
global $header_count;
$header_count = $count*100;
$content = preg_replace_callback('//', "h1", $content);
$content = preg_replace_callback('//', "h2", $content);
$content = preg_replace_callback('//', "h3", $content);
return $content;
}
function h1($matches)
{
global $header_count;
return "