5
filename = document.getElementById("save_filename").value;
6
data = editAreaLoader.getValue("editbox");
7
/* Do NOT refresh the page contents (causes problems for editarea and is
9
do_action("putfile", filename, {"path":".", "data":data}, null, true);
10
saved_status.data = "Saved.";
15
saved_status.data = "Not saved.";
18
/** Presents the "editor heading" (the part with the save box)
19
* inserting it into a given element at the front.
21
function present_editorhead(elem, path, handler_type)
23
var div = document.createElement("div");
24
/* Insert as the head element */
25
elem.insertBefore(div, elem.firstChild)
26
div.setAttribute("id", "editorhead");
28
/* Set up minimal interface */
29
var p = dom_make_text_elem("p", "Path: ");
30
var pathname = document.createElement("input");
31
pathname.setAttribute("type", "text");
32
pathname.setAttribute("size", "30");
33
pathname.setAttribute("id", "save_filename");
34
pathname.setAttribute("value", path);
35
p.appendChild(pathname);
36
var savebutton = document.createElement("input");
37
savebutton.setAttribute("type", "button");
38
savebutton.setAttribute("value", "Save");
39
savebutton.setAttribute("onclick", "save_file()");
40
p.appendChild(savebutton);
41
var t = document.createTextNode(" ");
43
saved_status = document.createTextNode("Saved.");
44
//p.appendChild(saved_status);
47
/* Print a warning message if this is not actually a text file.
49
if (handler_type != "text")
51
var warn = dom_make_text_elem("p",
52
"Warning: You are editing a binary " +
53
"file, which explains any strange characters you may see. If " +
54
"you save this file, you could corrupt it.");
55
div.appendChild(warn);
59
/** Presents the text editor.
61
function handle_text(path, text, handler_type)
63
/* Create a textarea with the text in it
64
* (The makings of a primitive editor).
66
var files = document.getElementById("filesbody");
67
/* Put our UI at the top */
68
present_editorhead(files, path, handler_type);
70
var div = document.createElement("div");
71
files.appendChild(div);
72
var txt_elem = dom_make_text_elem("textarea",
74
div.appendChild(txt_elem);
75
txt_elem.setAttribute("id", "editbox");
76
txt_elem.setAttribute("onchange", "edit_text()");
77
/* TODO: Make CSS height: 100% work */
78
txt_elem.setAttribute("rows", "35");
80
/* Load EditArea into the editbox */
84
toolbar: "search, go_to_line, |, undo, redo, |, select_font, |, syntax_selection, |, highlight, |, help",
85
start_highlight: true,
88
replace_tab_by_spaces: 4