Skip to content

Commit

Permalink
fix: resolveProvider?
Browse files Browse the repository at this point in the history
Recent bug fixes exposed a problem here.
The field `resolveProvider?` has a `?`, but is not an `Option`
type. The `ToJson` makes this assumption and uses the auxiliary
function `opt`. The bugs fixed today were masjing this problem.
  • Loading branch information
leodemoura committed Apr 12, 2021
1 parent f555610 commit 83b83f5
Showing 1 changed file with 58 additions and 58 deletions.
116 changes: 58 additions & 58 deletions src/Lean/Data/Lsp/LanguageFeatures.lean
Expand Up @@ -13,9 +13,9 @@ namespace Lsp
open Json

structure CompletionOptions where
triggerCharacters? : Option (Array String) := none
allCommitCharacters?: Option (Array String) := none
resolveProvider?: Bool := false
triggerCharacters? : Option (Array String) := none
allCommitCharacters? : Option (Array String) := none
resolveProvider : Bool := false
deriving FromJson, ToJson

structure CompletionItem where
Expand Down Expand Up @@ -77,9 +77,9 @@ inductive DocumentHighlightKind where

instance : ToJson DocumentHighlightKind where
toJson
| DocumentHighlightKind.text => 1
| DocumentHighlightKind.read => 2
| DocumentHighlightKind.write => 3
| DocumentHighlightKind.text => 1
| DocumentHighlightKind.read => 2
| DocumentHighlightKind.write => 3

structure DocumentHighlight where
range : Range
Expand All @@ -93,61 +93,61 @@ structure DocumentSymbolParams where
deriving FromJson, ToJson

inductive SymbolKind where
| file
| module
| «namespace»
| package
| «class»
| method
| property
| field
| constructor
| enum
| interface
| function
| «variable»
| «constant»
| string
| number
| boolean
| array
| object
| key
| null
| enumMember
| struct
| event
| operator
| typeParameter
| file
| module
| «namespace»
| package
| «class»
| method
| property
| field
| constructor
| enum
| interface
| function
| «variable»
| «constant»
| string
| number
| boolean
| array
| object
| key
| null
| enumMember
| struct
| event
| operator
| typeParameter

instance : ToJson SymbolKind where
toJson
| SymbolKind.file => 1
| SymbolKind.module => 2
| SymbolKind.namespace => 3
| SymbolKind.package => 4
| SymbolKind.class => 5
| SymbolKind.method => 6
| SymbolKind.property => 7
| SymbolKind.field => 8
| SymbolKind.constructor => 9
| SymbolKind.enum => 10
| SymbolKind.interface => 11
| SymbolKind.function => 12
| SymbolKind.variable => 13
| SymbolKind.constant => 14
| SymbolKind.string => 15
| SymbolKind.number => 16
| SymbolKind.boolean => 17
| SymbolKind.array => 18
| SymbolKind.object => 19
| SymbolKind.key => 20
| SymbolKind.null => 21
| SymbolKind.enumMember => 22
| SymbolKind.struct => 23
| SymbolKind.event => 24
| SymbolKind.operator => 25
| SymbolKind.typeParameter => 26
| SymbolKind.file => 1
| SymbolKind.module => 2
| SymbolKind.namespace => 3
| SymbolKind.package => 4
| SymbolKind.class => 5
| SymbolKind.method => 6
| SymbolKind.property => 7
| SymbolKind.field => 8
| SymbolKind.constructor => 9
| SymbolKind.enum => 10
| SymbolKind.interface => 11
| SymbolKind.function => 12
| SymbolKind.variable => 13
| SymbolKind.constant => 14
| SymbolKind.string => 15
| SymbolKind.number => 16
| SymbolKind.boolean => 17
| SymbolKind.array => 18
| SymbolKind.object => 19
| SymbolKind.key => 20
| SymbolKind.null => 21
| SymbolKind.enumMember => 22
| SymbolKind.struct => 23
| SymbolKind.event => 24
| SymbolKind.operator => 25
| SymbolKind.typeParameter => 26

structure DocumentSymbolAux (Self : Type) where
name : String
Expand Down

2 comments on commit 83b83f5

@leodemoura
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@Kha Could you please take a look at this fix? I am not familiar with the ToJon code generator, but as far as I can tell, it assumes a field containing a ? must have Option type.
BTW, I am pushing another commit to fix the indentation. I am guessing my Emacs converted tab's into spaces when I saved the file.

@Kha
Copy link
Member

@Kha Kha commented on 83b83f5 Apr 12, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, yes. The correct translation would be resolveProvider? : Option Bool, but this one works just as well (since we only send it, not parse it). And I must have accidentally copied the tabs from the LSP spec.

Please sign in to comment.