← Back to branch summary

~azzar1/unity/add-show-desktop-key

« back to all changes in this revision

Viewing changes to www/media/browser/editor.js

  • Committer: mattgiuca
  • Date: 2008-01-20 10:03:06 UTC
  • Revision ID: svn-v3-trunk0:2b9c9e99-6f39-0410-b283-7f802c844ae2:trunk:251
setup.py: Worked the "files to copy into jail" out into a separate list
instead of being expressed as code.
Still need to add some more dependencies to get matplotlib working.

Show diffs side-by-side

added added

removed removed

Lines of Context:
www/media/browser/editor.js
4
4
{
5
5
    filename = document.getElementById("save_filename").value;
6
6
    data = editAreaLoader.getValue("editbox");
7
 
    /* Do NOT refresh the page contents (causes problems for editarea and is
8
 
     * unnecessary). */
9
 
    do_action("putfile", filename, {"path":".", "data":data}, null, true);
 
7
    do_action("putfile", filename, {"path":".", "data":data});
10
8
    saved_status.data = "Saved.";
11
9
}
12
10
 
15
13
    saved_status.data = "Not saved.";
16
14
}
17
15
 
18
 
/** Presents the "editor heading" (the part with the save box)
19
 
 * inserting it into a given element at the front.
 
16
/** Presents the text editor.
20
17
 */
21
 
function present_editorhead(elem, path, handler_type)
 
18
function handle_text(path, text, handler_type)
22
19
{
 
20
    /* Create a textarea with the text in it
 
21
     * (The makings of a primitive editor).
 
22
     */
 
23
 
 
24
    setmode(true);
 
25
    var files = document.getElementById("filesbody");
23
26
    var div = document.createElement("div");
24
 
    /* Insert as the head element */
25
 
    elem.insertBefore(div, elem.firstChild)
26
 
    div.setAttribute("id", "editorhead");
 
27
    files.appendChild(div);
 
28
    div.setAttribute("class", "padding");
27
29
 
28
30
    /* Set up minimal interface */
29
31
    var p = dom_make_text_elem("p", "Path: ");
54
56
            "you save this file, you could corrupt it.");
55
57
        div.appendChild(warn);
56
58
    }
57
 
}
58
 
 
59
 
/** Presents the text editor.
60
 
 */
61
 
function handle_text(path, text, handler_type)
62
 
{
63
 
    /* Create a textarea with the text in it
64
 
     * (The makings of a primitive editor).
65
 
     */
66
 
    var files = document.getElementById("filesbody");
67
 
    /* Put our UI at the top */
68
 
    present_editorhead(files, path, handler_type);
69
 
 
70
 
    var div = document.createElement("div");
71
 
    files.appendChild(div);
72
59
    var txt_elem = dom_make_text_elem("textarea",
73
60
        text.toString())
74
61
    div.appendChild(txt_elem);
75
62
    txt_elem.setAttribute("id", "editbox");
76
63
    txt_elem.setAttribute("onchange", "edit_text()");
77
64
    /* TODO: Make CSS height: 100% work */
78
 
    txt_elem.setAttribute("rows", "35");
 
65
    txt_elem.setAttribute("rows", "20");
79
66
 
80
67
    /* Load EditArea into the editbox */
81
68
    editAreaLoader.init({
82
69
        id : "editbox",
83
70
        syntax: "python",
84
 
        toolbar: "search, go_to_line, |, undo, redo, |, select_font, |, syntax_selection, |, highlight, |, help",
85
 
        start_highlight: true,
86
 
        allow_toggle: false,
87
 
        allow_resize: false,
88
 
        replace_tab_by_spaces: 4
 
71
        start_highlight: true
89
72
    });
90
73
}
91
74