<?php

// $Date: 2004/01/01 15:27:44 $
// $Revision: 1.6 $
// $Author: jcrocholl $

function indent($extra 0) {
    global 
$indent_chars$indent_level;
    for (
$i $indent_level*$indent_chars $extra$i 0$i--) 
        
$result .= ' ';
    return 
$result;
}

function 
length($text) {
    return 
strlen($text);
}

function 
fill($text$length) {
    while (
length($text) < $length$text .= ' ';
    return 
$text;
}

function 
newline() {
    return 
"\n";
}

function 
span($class$text) {
    return 
$text;
}

?>