3
var savebutton = document.getElementById("save_button");
4
var filename = document.getElementById("save_filename").value;
5
data = editAreaLoader.getValue("editbox");
6
/* Do NOT refresh the page contents (causes problems for editarea and is
8
do_action("putfile", filename,
9
{"path":".", "data":data, "overwrite":"true"}, null, true);
10
savebutton.setAttribute("value", "Saved");
11
// XXX Do not disable for now; there is a problem getting the callback
13
//savebutton.setAttribute("disabled", "disabled");
18
var savebutton = document.getElementById("save_button");
19
savebutton.setAttribute("value", "Save");
20
savebutton.removeAttribute("disabled");
23
/** Presents the "editor heading" (the part with the save box)
24
* inserting it into a given element at the front.
26
function present_editorhead(elem, path, handler_type)
28
var div = document.getElementById("actions2");
30
/* Set up minimal interface */
31
var p = dom_make_text_elem("p", "Save as: ");
32
var pathname = document.createElement("input");
33
pathname.setAttribute("type", "text");
34
pathname.setAttribute("size", "30");
35
pathname.setAttribute("id", "save_filename");
36
pathname.setAttribute("value", path);
37
p.appendChild(pathname);
38
var savebutton = document.createElement("input");
39
savebutton.setAttribute("id", "save_button");
40
savebutton.setAttribute("type", "button");
41
savebutton.setAttribute("value", "Saved");
42
savebutton.setAttribute("disabled", "disabled");
43
savebutton.setAttribute("onclick", "save_file()");
44
p.appendChild(savebutton);
45
var t = document.createTextNode(" ");
49
/* Print a warning message if this is not actually a text file.
51
if (handler_type != "text")
53
var warn = dom_make_text_elem("p",
54
"Warning: You are editing a binary " +
55
"file, which explains any strange characters you may see. If " +
56
"you save this file, you could corrupt it.");
57
div.appendChild(warn);
61
/** Presents the text editor.
63
function handle_text(path, text, handler_type)
65
/* Create a textarea with the text in it
66
* (The makings of a primitive editor).
68
var files = document.getElementById("filesbody");
69
/* Put our UI at the top */
70
present_editorhead(files, path, handler_type);
72
var div = document.createElement("div");
73
files.appendChild(div);
74
var txt_elem = dom_make_text_elem("textarea",
76
div.appendChild(txt_elem);
77
txt_elem.setAttribute("id", "editbox");
78
txt_elem.setAttribute("onchange", "edit_text()");
79
/* TODO: Make CSS height: 100% work */
80
txt_elem.setAttribute("rows", "35");
82
/* Load EditArea into the editbox */
86
toolbar: "search, go_to_line, |, undo, redo, |, select_font, |, syntax_selection, |, highlight, |, help",
87
start_highlight: true,
90
replace_tab_by_spaces: 4,
91
change_callback: "edit_text"