From 568a5cea4833a3316f3741dcd32699334f770d26 Mon Sep 17 00:00:00 2001 From: xue <> Date: Sat, 28 Jan 2006 17:09:31 +0000 Subject: Rename "tools" to "buildscripts". --- buildscripts/texbuilder/build.php | 233 + buildscripts/texbuilder/prado3_quick_start.pdf | 8508 ++++++++++++++++++++++++ buildscripts/texbuilder/prado3_quick_start.tex | 115 + 3 files changed, 8856 insertions(+) create mode 100644 buildscripts/texbuilder/build.php create mode 100644 buildscripts/texbuilder/prado3_quick_start.pdf create mode 100644 buildscripts/texbuilder/prado3_quick_start.tex (limited to 'buildscripts/texbuilder') diff --git a/buildscripts/texbuilder/build.php b/buildscripts/texbuilder/build.php new file mode 100644 index 00000000..1866f868 --- /dev/null +++ b/buildscripts/texbuilder/build.php @@ -0,0 +1,233 @@ +]*>/', '', $html); + $html = preg_replace('/<\/?p>/m', '', $html); + + //escape { and } + $html = preg_replace('/([^\s]+){([^}]*)}([^\s]+)/', '$1\\\{$2\\\}$3', $html); + + //codes + $html = str_replace('$', '\$', $html); + $html = preg_replace('/]*>/', '`1`', $html); + $html = preg_replace('/<\/com:TTextHighlighter>/', '`2`', $html); + $html = preg_replace_callback('/(`1`)([^`]*)(`2`)/m', 'escape_verbatim', $html); + $html = preg_replace_callback('/(
)([^<]*)(<\/div>)/', 'escape_verbatim', $html); + + $html = preg_replace_callback('/"?[^\\/]*\/>/', 'include_image', $html); + + //runbar + $html = preg_replace('//', + 'Try, \texttt{http://../quickstart/index.php?page=$1}', $html); + + //text modifiers + $html = preg_replace('/([^<]*)<\/b>/', '\textbf{$1}', $html); + $html = preg_replace('/([^<]*)<\/i>/', '\emph{$1}', $html); + $html = preg_replace('/([^<]*)<\/tt>/', '\texttt{$1}', $html); + + //links + $html = preg_replace_callback('/]+href="([^"]*)"[^>]*>([^<]*)<\/a>/', + 'make_link', $html); + //anchor + $html = preg_replace_callback('/]+name="([^"]*)"[^>]*><\/a>/', 'anchor', $html); + + //item lists + $html = preg_replace('/
    /', '\begin{itemize}', $html); + $html = preg_replace('/<\/ol>/', '\end{itemize}', $html); + $html = preg_replace('/