shell/bin/editor.php


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

<?php
function main($args) {
	if (isset($_POST['stdin'])) {
		if (isset($args[1])) {
			file_put_contents($args[1],$_POST['stdin']);
		} else {
			echo $_POST['stdin'];
		}
	} else {
		if (isset($args[1]) && file_exists($args[1])) {
			$text = file_get_contents($args[1]);
		} else {
			$text = '';
		}
		echo '<div class="editor">';
		echo '<input type="hidden" name="stddest" value="'.$_POST['c'].'" />';
		echo '<textarea name="stdin">'.$text.'</textarea>'."\n";
		echo '<input type="submit" value="save" />';
		echo '</div>';
	}
}