comparison src/luan_editor/Window.luan @ 76:1beb4c57c269 default tip

monospaced sans-serif
author Franklin Schmidt <fschmidt@gmail.com>
date Wed, 18 Jun 2025 20:20:21 -0600
parents 7f5b3824f4d4
children
comparison
equal deleted inserted replaced
75:7f5b3824f4d4 76:1beb4c57c269
35 local Option_pane = require "luan:swing/Option_pane.luan" 35 local Option_pane = require "luan:swing/Option_pane.luan"
36 local show_message_dialog = Option_pane.show_message_dialog or error() 36 local show_message_dialog = Option_pane.show_message_dialog or error()
37 local Clipboard = require "luan:swing/Clipboard.luan" 37 local Clipboard = require "luan:swing/Clipboard.luan"
38 local Swing_runner = require "luan:swing/Swing_runner.luan" 38 local Swing_runner = require "luan:swing/Swing_runner.luan"
39 local swing_run = Swing_runner.run or error() 39 local swing_run = Swing_runner.run or error()
40 local Font = require "luan:swing/Font.luan"
40 local Java = require "classpath:luan_editor/Java.luan" 41 local Java = require "classpath:luan_editor/Java.luan"
41 local Logging = require "luan:logging/Logging.luan" 42 local Logging = require "luan:logging/Logging.luan"
42 local logger = Logging.logger "editor/Window" 43 local logger = Logging.logger "editor/Window"
43 44
44 45
45 local Window = {} 46 local Window = {}
47
48 local fonts = {}
49 for _, font in ipairs( Font.get_available_font_family_names() ) do
50 fonts[font] = font
51 end
52 local monospaced = fonts["Lucida Console"] or fonts["Monospaced"] or error()
53 -- logger.info(monospaced)
46 54
47 local n_windows = 0 55 local n_windows = 0
48 local documents = {} 56 local documents = {}
49 57
50 local function bool(val,default) 58 local function bool(val,default)
144 wrap_style_word = true 152 wrap_style_word = true
145 line_wrap = config.line_wrap 153 line_wrap = config.line_wrap
146 whitespace_visible = config.whitespace_visible 154 whitespace_visible = config.whitespace_visible
147 tab_size = config.tab_size 155 tab_size = config.tab_size
148 --font = { family="Monospaced", size=13 } 156 --font = { family="Monospaced", size=13 }
149 font_changes = { family="Monospaced" } 157 font_changes = { family=monospaced }
150 } 158 }
151 window.text_area = text_area 159 window.text_area = text_area
152 local title = file and file.canonical().to_string() or "new" 160 local title = file and file.canonical().to_string() or "new"
153 if document ~= nil then 161 if document ~= nil then
154 text_area.document = document 162 text_area.document = document