Merge branch 'main' into guests

2023-10-17 09:54:17 -06:00
parent 851701cb6f adabf0107f
commit 9cc55f895c
159 changed files with 3535 additions and 11178 deletions
@@ -206,9 +206,13 @@ export default function editor(): any {
                match_highlight: foreground(theme.middle, "accent", "active"),
                background: background(theme.middle, "active"),
            },
-            server_name_container: { padding: { left: 40 } },
-            server_name_color: text(theme.middle, "sans", "disabled", {}).color,
-            server_name_size_percent: 0.75,
+            completion_min_width: 300,
+            completion_max_width: 700,
+            inline_docs_container: { padding: { left: 40 } },
+            inline_docs_color: text(theme.middle, "sans", "disabled", {}).color,
+            inline_docs_size_percent: 0.75,
+            alongside_docs_max_width: 700,
+            alongside_docs_container: { padding: autocomplete_item.padding }
        },
        diagnostic_header: {
            background: background(theme.middle),