annotate editor.luan @ 17:273aebbcf90b

add goto
author Franklin Schmidt <fschmidt@gmail.com>
date Sun, 06 Apr 2025 19:21:25 -0600
parents 90abee9e07d5
children fd6d0162e924
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
1 local Luan = require "luan:Luan.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
2 local error = Luan.error
3
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
3 local ipairs = Luan.ipairs or error()
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
4 local stringify = Luan.stringify or error()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
5 local String = require "luan:String.luan"
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
6 local sub_string = String.sub or error()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
7 local replace = String.replace or error()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
8 local starts_with = String.starts_with or error()
17
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
9 local to_number = String.to_number or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
10 local Io = require "luan:Io.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
11 local print = Io.print or error()
3
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
12 local new_file = Io.schemes.file or error()
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
13 local Math = require "luan:Math.luan"
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
14 local min = Math.min or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
15 local Swing = require "luan:swing/Swing.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
16 local new_frame = require("luan:swing/Frame.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
17 local new_label = require("luan:swing/Label.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
18 local new_text_area = require("luan:swing/Text_area.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
19 local new_scroll_pane = require("luan:swing/Scroll_pane.luan").new or error()
13
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
20 local new_text_area_line_numbers = require("luan:swing/TextAreaLineNumbers.luan").new or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
21 local new_menu_bar = require("luan:swing/Menu_bar.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
22 local new_menu = require("luan:swing/Menu.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
23 local new_menu_item = require("luan:swing/Menu_item.luan").new or error()
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
24 local new_check_box_menu_item = require("luan:swing/Check_box_menu_item.luan").new or error()
12
Franklin Schmidt <fschmidt@gmail.com>
parents: 11
diff changeset
25 local int_to_color = require("luan:swing/Color.luan").int_to_color or error()
13
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
26 local create_empty_border = require("luan:swing/Border.luan").create_empty_border or error()
16
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
27 local Option_pane = require "luan:swing/Option_pane.luan"
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
28 local show_message_dialog = Option_pane.show_message_dialog or error()
17
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
29 local show_input_dialog = Option_pane.show_input_dialog or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
30 local Logging = require "luan:logging/Logging.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
31 local logger = Logging.logger "editor"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
32
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
33
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
34 local new_window
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
35
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
36 local function make_menu_bar(window)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
37 local menu_bar = new_menu_bar()
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
38 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
39 local file_menu = new_menu()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
40 file_menu.text = "File"
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
41 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
42 local new_file = new_menu_item()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
43 new_file.text = "New File"
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
44 new_file.accelerator = "meta N"
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
45 new_file.add_action_listener(new_window)
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
46 file_menu.add(new_file)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
47 end
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
48 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
49 local open = new_menu_item()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
50 open.text = "Open..."
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
51 open.accelerator = "meta O"
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
52 open.add_action_listener(window.open)
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
53 file_menu.add(open)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
54 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
55 local revert
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
56 do
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
57 local save = new_menu_item()
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
58 save.text = "Save"
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
59 save.accelerator = "meta S"
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
60 save.add_action_listener(function()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
61 if window.save() then
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
62 revert.set_enabled(true)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
63 end
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
64 end)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
65 file_menu.add(save)
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
66 end
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
67 do
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
68 revert = new_menu_item()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
69 revert.text = "Revert"
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
70 revert.set_enabled(window.has_file)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
71 revert.add_action_listener(window.revert)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
72 file_menu.add(revert)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
73 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
74 menu_bar.add(file_menu)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
75 end
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
76 do
6
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
77 local edit_menu = new_menu()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
78 edit_menu.text = "Edit"
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
79 local document = window.text_area.document
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
80 local undo, redo
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
81 do
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
82 undo = new_menu_item()
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
83 undo.text = "Undo"
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
84 undo.accelerator = "meta Z"
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
85 undo.add_action_listener(document.undo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
86 edit_menu.add(undo)
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
87 end
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
88 do
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
89 redo = new_menu_item()
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
90 redo.text = "Redo"
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
91 redo.accelerator = "meta shift Z"
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
92 redo.add_action_listener(document.redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
93 edit_menu.add(redo)
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
94 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
95 local function update_undo_redo()
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
96 undo.set_enabled(document.can_undo())
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
97 redo.set_enabled(document.can_redo())
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
98 end
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
99 edit_menu.dont_gc(update_undo_redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
100 update_undo_redo()
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
101 document.add_undo_listener(update_undo_redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
102 edit_menu.add_separator()
6
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
103 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
104 local cut = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
105 cut.text = "Cut"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
106 cut.accelerator = "meta X"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
107 cut.add_action_listener(window.text_area.cut)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
108 edit_menu.add(cut)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
109 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
110 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
111 local copy = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
112 copy.text = "Copy"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
113 copy.accelerator = "meta C"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
114 copy.add_action_listener(window.text_area.copy)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
115 edit_menu.add(copy)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
116 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
117 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
118 local paste = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
119 paste.text = "Paste"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
120 paste.accelerator = "meta V"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
121 paste.add_action_listener(window.text_area.paste)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
122 edit_menu.add(paste)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
123 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
124 edit_menu.add_separator()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
125 do
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
126 local indent = new_menu_item()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
127 indent.text = "Indent"
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
128 indent.accelerator = "meta CLOSE_BRACKET"
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
129 indent.add_action_listener(window.indent)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
130 edit_menu.add(indent)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
131 end
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
132 do
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
133 local unindent = new_menu_item()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
134 unindent.text = "Unindent"
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
135 unindent.accelerator = "meta OPEN_BRACKET"
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
136 unindent.add_action_listener(window.unindent)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
137 edit_menu.add(unindent)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
138 end
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
139 edit_menu.add_separator()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
140 do
6
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
141 local select_all = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
142 select_all.text = "Select All"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
143 select_all.accelerator = "meta A"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
144 select_all.add_action_listener(window.text_area.select_all)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
145 edit_menu.add(select_all)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
146 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
147 menu_bar.add(edit_menu)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
148 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
149 do
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
150 local view_menu = new_menu()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
151 view_menu.text = "View"
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
152 do
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
153 local word_wrap = new_check_box_menu_item()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
154 word_wrap.text = "Word Wrap"
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
155 word_wrap.state = window.text_area.line_wrap
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
156 word_wrap.add_action_listener(function()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
157 window.text_area.line_wrap = word_wrap.state
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
158 end)
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
159 view_menu.add(word_wrap)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
160 end
14
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
161 do
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
162 local show_whitespace = new_check_box_menu_item()
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
163 show_whitespace.text = "Show Whitespace"
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
164 show_whitespace.add_action_listener(function()
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
165 window.text_area.show_whitespace(show_whitespace.state)
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
166 end)
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
167 view_menu.add(show_whitespace)
357fdbf446cb add show_whitespace
Franklin Schmidt <fschmidt@gmail.com>
parents: 13
diff changeset
168 end
16
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
169 do
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
170 local show_column = new_menu_item()
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
171 show_column.text = "Show Cursor Column"
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
172 show_column.add_action_listener(function()
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
173 show_message_dialog( window.frame, "Cursor Column: "..window.cursor_column() )
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
174 end)
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
175 view_menu.add(show_column)
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
176 end
17
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
177 do
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
178 local goto = new_menu_item()
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
179 goto.text = "Goto Line"
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
180 goto.accelerator = "meta G"
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
181 goto.add_action_listener(function()
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
182 local input = show_input_dialog( window.frame, "Cursor Column: "..window.cursor_column() )
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
183 --logger.info("input "..input)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
184 local line = input and to_number(input)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
185 if line ~= nil then
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
186 window.goto(line)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
187 end
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
188 end)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
189 view_menu.add(goto)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
190 end
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
191 menu_bar.add(view_menu)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
192 end
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
193 return menu_bar
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
194 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
195
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
196 local n_windows = 0
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
197 local documents = {}
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
198
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
199 function new_window(file)
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
200 local window = {}
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
201 window.has_file = file~=nil and file.is_file()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
202 local frame = new_frame()
16
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
203 window.frame = frame
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
204 local title = file and file.canonical().to_string() or "new"
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
205 frame.add_close_listener(function()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
206 n_windows = n_windows - 1
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
207 if n_windows == 0 then
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
208 Luan.exit()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
209 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
210 end)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
211 local text_area = new_text_area()
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
212 window.text_area = text_area
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
213 if file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
214 local document = documents[title]
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
215 if document == nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
216 documents[title] = text_area.document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
217 else
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
218 text_area.document = document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
219 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
220 if file.is_file() then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
221 text_area.text = file.read_text()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
222 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
223 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
224 local function set_title()
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
225 local s = title
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
226 if not text_area.document.is_unedited() then
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
227 s = s.." *"
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
228 end
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
229 frame.title = s
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
230 end
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
231 set_title()
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
232 text_area.dont_gc(set_title)
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
233 text_area.document.add_undo_listener(set_title)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
234 text_area.rows = 10
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
235 text_area.columns = 20
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
236 text_area.wrap_style_word = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
237 text_area.line_wrap = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
238 text_area.tab_size = 4
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
239 text_area.set_font{ family="Monospaced", size=13 }
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
240 text_area.set_selection(0)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
241 --print(text_area.line_count)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
242 local scroll_pane = new_scroll_pane(text_area)
13
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
243 local line_numbers = new_text_area_line_numbers(text_area)
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
244 line_numbers.foreground_color = int_to_color(0x888888)
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
245 line_numbers.border = create_empty_border(0,8,0,8)
2baecd73d6bb line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 12
diff changeset
246 scroll_pane.set_row_header_view(line_numbers)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
247 frame.add(scroll_pane)
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
248 function window.open()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
249 local file_chooser = frame.file_chooser_load()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
250 if file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
251 file_chooser.directory = file.parent()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
252 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
253 file_chooser.visible = true
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
254 local new_file = file_chooser.file
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
255 if new_file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
256 new_window(new_file)
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
257 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
258 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
259 function window.save()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
260 if file == nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
261 local file_chooser = frame.file_chooser_save()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
262 file_chooser.visible = true
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
263 file = file_chooser.file
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
264 if file == nil then
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
265 return false
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
266 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
267 title = file.canonical().to_string()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
268 frame.title = title
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
269 documents[title] = text_area.document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
270 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
271 file.write_text(text_area.text)
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
272 text_area.document.set_unedited()
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
273 return true
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
274 end
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
275 function window.revert()
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
276 local selection = text_area.get_selection()
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
277 local text = file.read_text()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
278 text_area.text = text
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
279 text_area.set_selection(min(selection,#text+1))
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
280 text_area.document.set_unedited()
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
281 end
15
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
282 local function selection_lines()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
283 local start_seletion, end_selection = text_area.get_selection()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
284 local end_ = end_selection == start_seletion and end_selection or end_selection - 1
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
285 local start_line = text_area.get_line_from_position(start_seletion)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
286 local end_line = text_area.get_line_from_position(end_)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
287 local start_pos = text_area.get_line_start_position(start_line)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
288 local end_pos = text_area.get_line_end_position(end_line)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
289 local text = text_area.text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
290 text = sub_string(text,start_pos,end_pos-2)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
291 return {
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
292 text = text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
293 start_pos = start_pos
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
294 length = #text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
295 lines = end_line - start_line + 1
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
296 start_seletion = start_seletion
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
297 end_selection = end_selection
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
298 }
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
299 end
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
300 function window.indent()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
301 local r = selection_lines()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
302 local text = r.text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
303 local start_pos = r.start_pos
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
304 text = "\t"..replace(text,"\n","\n\t")
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
305 text_area.replace(start_pos,r.length,text)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
306 --logger.info(stringify{text_area.get_selection()})
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
307 text_area.set_selection( r.start_seletion+1, r.end_selection+r.lines )
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
308 end
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
309 function window.unindent()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
310 local r = selection_lines()
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
311 local text = r.text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
312 text = "\n"..text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
313 local start_seletion = r.start_seletion
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
314 if starts_with(text,"\n\t") then
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
315 start_seletion = start_seletion - 1
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
316 end
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
317 local len1 = #text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
318 text = replace(text,"\n\t","\n")
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
319 local len2 = #text
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
320 local end_selection = r.end_selection - (len1 - len2)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
321 text = sub_string(text,2)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
322 text_area.replace(r.start_pos,r.length,text)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
323 text_area.set_selection(start_seletion,end_selection)
93e46dadb694 add indent
Franklin Schmidt <fschmidt@gmail.com>
parents: 14
diff changeset
324 end
16
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
325 function window.cursor_column()
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
326 local cursor_pos = text_area.get_selection()
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
327 local line = text_area.get_line_from_position(cursor_pos)
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
328 local start_line_pos = text_area.get_line_start_position(line)
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
329 return cursor_pos - start_line_pos + 1
90abee9e07d5 add show_column
Franklin Schmidt <fschmidt@gmail.com>
parents: 15
diff changeset
330 end
17
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
331 function window.goto(line)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
332 local pos = text_area.get_line_start_position(line)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
333 text_area.set_selection(pos)
273aebbcf90b add goto
Franklin Schmidt <fschmidt@gmail.com>
parents: 16
diff changeset
334 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
335 local menu_bar = make_menu_bar(window)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
336 frame.set_menu_bar(menu_bar)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
337 frame.pack()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
338 frame.visible = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
339 text_area.request_focus_in_window()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
340 n_windows = n_windows + 1
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
341 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
342
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
343 Swing.run(function()
3
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
344 local args = Luan.arg
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
345 if #args == 0 then
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
346 new_window()
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
347 else
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
348 for _, arg in ipairs(args) do
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
349 local file = new_file(arg)
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
350 new_window(file)
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
351 end
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
352 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
353 end)