<?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;
}

?>