2
/** Presents the text editor.
4
function handle_text(path, text, handler_type)
6
/* Create a textarea with the text in it
7
* (The makings of a primitive editor).
11
var files = document.getElementById("filesbody");
12
var div = document.createElement("div");
13
files.appendChild(div);
14
div.setAttribute("class", "padding");
15
/* First, print a warning message if this is not actually a text file.
17
if (handler_type != "text")
19
var warn = dom_make_text_elem("p",
20
"Warning: You are editing a binary " +
21
"file, which explains any strange characters you may see. If " +
22
"you save this file, you could corrupt it.");
23
div.appendChild(warn);
25
var txt_elem = dom_make_text_elem("textarea",
27
div.appendChild(txt_elem);
28
txt_elem.setAttribute("id", "editbox");
29
/* TODO: Make CSS height: 100% work */
30
txt_elem.setAttribute("rows", "20");