@@ -48,6 +48,11 @@ function isJSONProperty(obj: unknown): obj is IJSONProperty {
4848 */
4949type LanguageServerSettings = Record < string , ServerSchemaWrapper > ;
5050
51+ /**
52+ * Default server priority; this should match the value defined in `plugin.json` schema.
53+ */
54+ const DEAULT_SERVER_PRIORITY = 50 ;
55+
5156/**
5257 * Get default values from JSON Schema properties field.
5358 */
@@ -396,7 +401,7 @@ export class SettingsSchemaManager {
396401 composite . language_servers
397402 ) ;
398403
399- composite . language_servers = this . _mergeByServer (
404+ composite . language_servers = SettingsSchemaManager . mergeByServer (
400405 collapsedDefaults . settings ,
401406 collapsedUser . settings
402407 ) ;
@@ -552,7 +557,7 @@ export class SettingsSchemaManager {
552557 } ;
553558 }
554559
555- private _mergeByServer (
560+ static mergeByServer (
556561 defaults : LanguageServerSettings ,
557562 userSettings : LanguageServerSettings
558563 ) : LanguageServerSettings {
@@ -565,9 +570,19 @@ export class SettingsSchemaManager {
565570 // nothing to merge with
566571 result [ serverKey ] = JSONExt . deepCopy ( serverSettingsGroup ) ;
567572 } else {
573+ // priority should come from (a) user (b) overrides (c) fallback default;
574+ // unfortunately the user and default values get merged in the form so we
575+ // cannot distinguish (a) from (c); as a workaround we can compare its value
576+ // with the default value.
577+ const userOrDefaultPriority = serverSettingsGroup . priority ;
578+ const isPriorityUserSet =
579+ typeof userOrDefaultPriority !== 'undefined' &&
580+ userOrDefaultPriority !== DEAULT_SERVER_PRIORITY ;
581+ const priority = isPriorityUserSet
582+ ? userOrDefaultPriority
583+ : result [ serverKey ] . priority ?? DEAULT_SERVER_PRIORITY ;
568584 const merged : Required < ServerSchemaWrapper > = {
569- priority : ( result [ serverKey ] . priority ||
570- serverSettingsGroup . priority ) as any ,
585+ priority,
571586 // `serverSettings` entries are expected to be flattened to dot notation here.
572587 serverSettings : {
573588 ...( result [ serverKey ] . serverSettings || { } ) ,
0 commit comments