mirror of
https://github.com/lollipopkit/flutter_server_box.git
synced 2025-12-17 23:34:24 +01:00
new & opt.
opt.: input field auto focus opt.: snippet page top padding new: setting of editor font size
This commit is contained in:
@@ -27,6 +27,7 @@ const roundRectCardPadding = EdgeInsets.symmetric(horizontal: 17, vertical: 13);
|
||||
|
||||
const placeholder = SizedBox();
|
||||
const height13 = SizedBox(height: 13);
|
||||
const height77 = SizedBox(height: 77);
|
||||
const width13 = SizedBox(width: 13);
|
||||
const width7 = SizedBox(width: 7);
|
||||
|
||||
|
||||
@@ -71,6 +71,9 @@ class SettingStore extends PersistentStore {
|
||||
StoreProperty<bool> get sshVirtualKeyAutoOff =>
|
||||
property('sshVirtualKeyAutoOff', defaultValue: true);
|
||||
|
||||
StoreProperty<double> get editorFontSize =>
|
||||
property('editorFontSize', defaultValue: 13);
|
||||
|
||||
// Editor theme
|
||||
StoreProperty<String> get editorTheme =>
|
||||
property('editorTheme', defaultValue: defaultEditorTheme);
|
||||
|
||||
Reference in New Issue
Block a user