annotate editor.luan @ 11:538cb5ad031c

start line numbers
author Franklin Schmidt <fschmidt@gmail.com>
date Thu, 03 Apr 2025 14:34:55 -0600
parents a83c8842ca3b
children 27f2e1aaf8ff
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()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
4 local Io = require "luan:Io.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
5 local print = Io.print or error()
3
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
6 local new_file = Io.schemes.file or error()
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
7 local Math = require "luan:Math.luan"
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
8 local min = Math.min or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
9 local Swing = require "luan:swing/Swing.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
10 local new_frame = require("luan:swing/Frame.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
11 local new_label = require("luan:swing/Label.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
12 local new_text_area = require("luan:swing/Text_area.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
13 local new_scroll_pane = require("luan:swing/Scroll_pane.luan").new or error()
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
14 local List = require "luan:swing/List.luan"
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
15 local new_default_list = List.new_default_list or error()
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
16 local new_text_area_line_numbers = List.new_text_area_line_numbers or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
17 local new_menu_bar = require("luan:swing/Menu_bar.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
18 local new_menu = require("luan:swing/Menu.luan").new or error()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
19 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
20 local new_check_box_menu_item = require("luan:swing/Check_box_menu_item.luan").new or error()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
21 local Logging = require "luan:logging/Logging.luan"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
22 local logger = Logging.logger "editor"
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
23
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
24
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
25 local new_window
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
26
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
27 local function make_menu_bar(window)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
28 local menu_bar = new_menu_bar()
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
29 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
30 local file_menu = new_menu()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
31 file_menu.text = "File"
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
32 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
33 local new_file = new_menu_item()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
34 new_file.text = "New File"
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
35 new_file.accelerator = "meta N"
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
36 new_file.add_action_listener(new_window)
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
37 file_menu.add(new_file)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
38 end
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
39 do
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
40 local open = new_menu_item()
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
41 open.text = "Open..."
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
42 open.accelerator = "meta O"
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
43 open.add_action_listener(window.open)
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
44 file_menu.add(open)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
45 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
46 local revert
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
47 do
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
48 local save = new_menu_item()
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
49 save.text = "Save"
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
50 save.accelerator = "meta S"
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
51 save.add_action_listener(function()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
52 if window.save() then
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
53 revert.set_enabled(true)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
54 end
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
55 end)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
56 file_menu.add(save)
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
57 end
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
58 do
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
59 revert = new_menu_item()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
60 revert.text = "Revert"
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
61 revert.set_enabled(window.has_file)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
62 revert.add_action_listener(window.revert)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
63 file_menu.add(revert)
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
64 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
65 menu_bar.add(file_menu)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
66 end
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
67 do
6
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
68 local edit_menu = new_menu()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
69 edit_menu.text = "Edit"
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
70 local document = window.text_area.document
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
71 local undo, redo
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
72 do
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
73 undo = new_menu_item()
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
74 undo.text = "Undo"
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
75 undo.accelerator = "meta Z"
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
76 undo.add_action_listener(document.undo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
77 edit_menu.add(undo)
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
78 end
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
79 do
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
80 redo = new_menu_item()
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
81 redo.text = "Redo"
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
82 redo.accelerator = "meta shift Z"
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
83 redo.add_action_listener(document.redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
84 edit_menu.add(redo)
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
85 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
86 local function update_undo_redo()
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
87 undo.set_enabled(document.can_undo())
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
88 redo.set_enabled(document.can_redo())
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
89 end
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
90 edit_menu.dont_gc(update_undo_redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
91 update_undo_redo()
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
92 document.add_undo_listener(update_undo_redo)
9
9d8440e0aecc add undo
Franklin Schmidt <fschmidt@gmail.com>
parents: 7
diff changeset
93 edit_menu.add_separator()
6
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
94 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
95 local cut = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
96 cut.text = "Cut"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
97 cut.accelerator = "meta X"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
98 cut.add_action_listener(window.text_area.cut)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
99 edit_menu.add(cut)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
100 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
101 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
102 local copy = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
103 copy.text = "Copy"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
104 copy.accelerator = "meta C"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
105 copy.add_action_listener(window.text_area.copy)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
106 edit_menu.add(copy)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
107 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
108 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
109 local paste = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
110 paste.text = "Paste"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
111 paste.accelerator = "meta V"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
112 paste.add_action_listener(window.text_area.paste)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
113 edit_menu.add(paste)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
114 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
115 edit_menu.add_separator()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
116 do
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
117 local select_all = new_menu_item()
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
118 select_all.text = "Select All"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
119 select_all.accelerator = "meta A"
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
120 select_all.add_action_listener(window.text_area.select_all)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
121 edit_menu.add(select_all)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
122 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
123 menu_bar.add(edit_menu)
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
124 end
524d6b1c26b4 edit menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 5
diff changeset
125 do
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
126 local view_menu = new_menu()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
127 view_menu.text = "View"
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
128 do
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
129 local word_wrap = new_check_box_menu_item()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
130 word_wrap.text = "Word Wrap"
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
131 word_wrap.state = window.text_area.line_wrap
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
132 word_wrap.add_action_listener(function()
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
133 window.text_area.line_wrap = word_wrap.state
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
134 end)
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
135 view_menu.add(word_wrap)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
136 end
2
f38f6e903369 word wrap in menu
Franklin Schmidt <fschmidt@gmail.com>
parents: 1
diff changeset
137 menu_bar.add(view_menu)
4
3d6414265959 add save
Franklin Schmidt <fschmidt@gmail.com>
parents: 3
diff changeset
138 end
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
139 return menu_bar
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
140 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
141
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
142 local n_windows = 0
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
143 local documents = {}
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
144
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
145 function new_window(file)
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
146 local window = {}
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
147 window.has_file = file~=nil and file.is_file()
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
148 local frame = new_frame()
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
149 local title = file and file.canonical().to_string() or "new"
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
150 frame.add_close_listener(function()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
151 n_windows = n_windows - 1
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
152 if n_windows == 0 then
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
153 Luan.exit()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
154 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
155 end)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
156 local text_area = new_text_area()
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
157 window.text_area = text_area
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
158 if file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
159 local document = documents[title]
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
160 if document == nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
161 documents[title] = text_area.document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
162 else
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
163 text_area.document = document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
164 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
165 if file.is_file() then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
166 text_area.text = file.read_text()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
167 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
168 end
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
169 local function set_title()
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
170 local s = title
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
171 if not text_area.document.is_unedited() then
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
172 s = s.." *"
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
173 end
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
174 frame.title = s
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
175 end
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
176 set_title()
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
177 text_area.dont_gc(set_title)
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
178 text_area.document.add_undo_listener(set_title)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
179 text_area.rows = 10
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
180 text_area.columns = 20
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
181 text_area.wrap_style_word = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
182 text_area.line_wrap = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
183 text_area.tab_size = 4
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
184 text_area.set_font{ family="Monospaced", size=13 }
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
185 text_area.caret_position = 0
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
186 --print(text_area.line_count)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
187 local scroll_pane = new_scroll_pane(text_area)
11
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
188 local list = new_text_area_line_numbers(text_area)
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
189 --print(list.size)
538cb5ad031c start line numbers
Franklin Schmidt <fschmidt@gmail.com>
parents: 10
diff changeset
190 scroll_pane.set_row_header_view(list)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
191 frame.add(scroll_pane)
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
192 function window.open()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
193 local file_chooser = frame.file_chooser_load()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
194 if file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
195 file_chooser.directory = file.parent()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
196 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
197 file_chooser.visible = true
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
198 local new_file = file_chooser.file
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
199 if new_file ~= nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
200 new_window(new_file)
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
201 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
202 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
203 function window.save()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
204 if file == nil then
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
205 local file_chooser = frame.file_chooser_save()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
206 file_chooser.visible = true
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
207 file = file_chooser.file
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
208 if file == nil then
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
209 return false
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
210 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
211 title = file.canonical().to_string()
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
212 frame.title = title
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
213 documents[title] = text_area.document
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
214 end
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
215 file.write_text(text_area.text)
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
216 text_area.document.set_unedited()
7
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
217 return true
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
218 end
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
219 function window.revert()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
220 local caret_position = text_area.caret_position
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
221 local text = file.read_text()
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
222 text_area.text = text
ce4233ff5ce8 add revert
Franklin Schmidt <fschmidt@gmail.com>
parents: 6
diff changeset
223 text_area.caret_position = min(caret_position,#text)
10
a83c8842ca3b add edited
Franklin Schmidt <fschmidt@gmail.com>
parents: 9
diff changeset
224 text_area.document.set_unedited()
5
57b4c281a03e shared documents
Franklin Schmidt <fschmidt@gmail.com>
parents: 4
diff changeset
225 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
226 local menu_bar = make_menu_bar(window)
0
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
227 frame.set_menu_bar(menu_bar)
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
228 frame.pack()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
229 frame.visible = true
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
230 text_area.request_focus_in_window()
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
231 n_windows = n_windows + 1
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
232 end
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
233
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
234 Swing.run(function()
3
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
235 local args = Luan.arg
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
236 if #args == 0 then
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
237 new_window()
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
238 else
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
239 for _, arg in ipairs(args) do
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
240 local file = new_file(arg)
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
241 new_window(file)
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
242 end
a79a840691b1 handle args
Franklin Schmidt <fschmidt@gmail.com>
parents: 2
diff changeset
243 end
1
9aa38deb5883 add open
Franklin Schmidt <fschmidt@gmail.com>
parents: 0
diff changeset
244 end)