3
function showfile($filename, $lang, $interestingrows = array()) {
4
echo "<strong>".$filename."</strong>";
5
echo '<div id="ace_'.str_replace(".", "", $filename).'" class="ace">';
6
$handle = @fopen($filename, "r");
9
while (($buffer = fgets($handle, 4096)) !== false) {
11
$buffer = str_replace("&", "&", $buffer);
12
$buffer = str_replace("<", "<", $buffer);
13
$buffer = str_replace(">", ">", $buffer);
18
echo "Error: unexpected fgets() fail\n";
24
echo '<script type="text/javascript">
25
var Range = require("ace/range").Range;
26
var editor = ace.edit("ace_'.str_replace(".", "", $filename).'");
27
editor.setTheme("ace/theme/merbivore");
28
editor.getSession().setMode("ace/mode/'.$lang.'");
29
editor.setReadOnly(true);
30
editor.setShowPrintMargin(false);
31
editor.setDisplayIndentGuides(false);
32
editor.setHighlightSelectedWord(true);
33
lines = editor.getSession().getLength();
34
$("#ace_'.str_replace(".", "", $filename).'").height(Math.min(500,lines*16));
35
aceeditors.push("ace_'.str_replace(".", "", $filename).'");';
36
for($i = 0; $i < count($interestingrows); $i++) {
37
echo 'editor.getSession().addMarker(new Range('.$interestingrows[$i][0].', 0, '
38
.$interestingrows[$i][1].', Number.POSITIVE_INFINITY), "interesting", "text",false);';
b'\\ No newline at end of file'