annotate src/luan/modules/swing/Text_area.luan @ 1992:ac02e07f09de default tip

add config
author Franklin Schmidt <fschmidt@gmail.com>
date Tue, 01 Jul 2025 15:14:26 -0600
parents bb12d502b72e
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
1 local Luan = require "luan:Luan.luan"
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
2 local error = Luan.error
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
3 local set_metatable = Luan.set_metatable or error()
1912
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
4 local ipairs = Luan.ipairs or error()
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
5 local Utils = require "luan:swing/Utils.luan"
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
6 local fail = Utils.fail or error()
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
7 local make_metatable = Utils.make_metatable or error()
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
8 local remove = Utils.remove or error()
1885
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
9 local check_empty = Utils.check_empty or error()
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
10 local Text_component = require("luan:swing/Text_component.luan")
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
11 local super__index = Text_component.__index or error()
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
12 local super__new_index = Text_component.__new_index or error()
1885
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
13 local super_construct = Text_component.construct or error()
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
14 require "java"
1874
Franklin Schmidt <fschmidt@gmail.com>
parents: 1868
diff changeset
15 local TextAreaLuan = require "java:luan.modules.swing.TextAreaLuan"
1893
0170d482b5d5 add FlatLaf
Franklin Schmidt <fschmidt@gmail.com>
parents: 1887
diff changeset
16 local Logging = require "luan:logging/Logging.luan"
0170d482b5d5 add FlatLaf
Franklin Schmidt <fschmidt@gmail.com>
parents: 1887
diff changeset
17 local logger = Logging.logger "swing/Text_area"
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
18
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
19
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
20 local Text_area = {}
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
21
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
22 function Text_area.__index(text_area,key)
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
23 local rtn = super__index(text_area,key)
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
24 if rtn ~= fail then return rtn end
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
25 local jtext_area = text_area.java
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
26 if key == "line_wrap" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
27 return jtext_area.getLineWrap()
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
28 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
29 if key == "wrap_style_word" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
30 return jtext_area.getWrapStyleWord()
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
31 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
32 if key == "tab_size" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
33 return jtext_area.getTabSize()
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
34 end
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
35 if key == "rows" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
36 return jtext_area.getRows()
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
37 end
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
38 if key == "columns" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
39 return jtext_area.getColumns()
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
40 end
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
41 if key == "line_count" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
42 return jtext_area.getLineCount()
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
43 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
44 if key == "whitespace_visible" then
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
45 return jtext_area.isWhitespaceVisible()
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
46 end
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
47 return fail
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
48 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
49
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
50 function Text_area.__new_index(text_area,key,value)
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
51 local rtn = super__new_index(text_area,key,value)
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
52 if rtn ~= fail then return end
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
53 local jtext_area = text_area.java
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
54 if key == "line_wrap" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
55 jtext_area.setLineWrap(value)
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
56 return
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
57 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
58 if key == "wrap_style_word" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
59 jtext_area.setWrapStyleWord(value)
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
60 return
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
61 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
62 if key == "tab_size" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
63 jtext_area.setTabSize(value)
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
64 return
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
65 end
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
66 if key == "rows" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
67 jtext_area.setRows(value)
1862
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
68 return
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
69 end
d59d4ef5ca46 swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1616
diff changeset
70 if key == "columns" then
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
71 jtext_area.setColumns(value)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
72 return
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
73 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
74 if key == "whitespace_visible" then
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
75 jtext_area.setWhitespaceVisible(value)
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
76 return
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
77 end
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
78 return fail
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
79 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
80
1863
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
81 local mt = make_metatable(Text_area)
928e73bfe7ea swing work
Franklin Schmidt <fschmidt@gmail.com>
parents: 1862
diff changeset
82
1885
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
83 function Text_area.new(props)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
84 local jtext_area = TextAreaLuan.new()
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
85 local text_area = { java = jtext_area }
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
86 super_construct(text_area,props)
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
87 local rows = remove(props,"rows")
1887
Franklin Schmidt <fschmidt@gmail.com>
parents: 1885
diff changeset
88 if rows~=nil then jtext_area.setRows(rows) end
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
89 local columns = remove(props,"columns")
1887
Franklin Schmidt <fschmidt@gmail.com>
parents: 1885
diff changeset
90 if columns~=nil then jtext_area.setColumns(columns) end
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
91 local wrap_style_word = remove(props,"wrap_style_word")
1887
Franklin Schmidt <fschmidt@gmail.com>
parents: 1885
diff changeset
92 if wrap_style_word~=nil then jtext_area.setWrapStyleWord(wrap_style_word) end
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
93 local line_wrap = remove(props,"line_wrap")
1887
Franklin Schmidt <fschmidt@gmail.com>
parents: 1885
diff changeset
94 if line_wrap~=nil then jtext_area.setLineWrap(line_wrap) end
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
95 local tab_size = remove(props,"tab_size")
1887
Franklin Schmidt <fschmidt@gmail.com>
parents: 1885
diff changeset
96 if tab_size~=nil then jtext_area.setTabSize(tab_size) end
1944
Franklin Schmidt <fschmidt@gmail.com>
parents: 1914
diff changeset
97 local whitespace_visible = remove(props,"whitespace_visible")
1914
Franklin Schmidt <fschmidt@gmail.com>
parents: 1912
diff changeset
98 if whitespace_visible~=nil then jtext_area.setWhitespaceVisible(whitespace_visible) end
1885
Franklin Schmidt <fschmidt@gmail.com>
parents: 1878
diff changeset
99 check_empty(props)
1878
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
100 function text_area.get_line_from_position(pos)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
101 return jtext_area.getLineOfOffset(pos-1) + 1
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
102 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
103 function text_area.get_line_start_position(line)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
104 return jtext_area.getLineStartOffset(line-1) + 1
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
105 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
106 function text_area.get_line_end_position(line)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
107 return jtext_area.getLineEndOffset(line-1) + 1
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
108 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
109 function text_area.insert(text,pos)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
110 return jtext_area.insert(text,pos-1)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
111 end
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
112 function text_area.replace(start_pos,length,text)
1909
Franklin Schmidt <fschmidt@gmail.com>
parents: 1908
diff changeset
113 text_area._document.run_in_transaction(function()
Franklin Schmidt <fschmidt@gmail.com>
parents: 1908
diff changeset
114 return jtext_area.getDocument().replace(start_pos-1,length,text)
Franklin Schmidt <fschmidt@gmail.com>
parents: 1908
diff changeset
115 end)
1878
Franklin Schmidt <fschmidt@gmail.com>
parents: 1877
diff changeset
116 end
1912
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
117 function text_area.set_hightlights(hightlights)
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
118 local list = {}
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
119 for _, hightlight in ipairs(hightlights) do
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
120 list[#list+1] = TextAreaLuan.Range.new(hightlight.start-1,hightlight.end_-1)
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
121 end
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
122 jtext_area.setHightlights(list)
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
123 end
9fa922236aff highlights
Franklin Schmidt <fschmidt@gmail.com>
parents: 1909
diff changeset
124 text_area.clear_hightlights = jtext_area.clearHighlights
1616
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
125 set_metatable(text_area,mt)
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
126 return text_area
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
127 end
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
128
915cb538e2a3 start swing
Franklin Schmidt <fschmidt@gmail.com>
parents:
diff changeset
129 return Text_area