fix: remove function to move cursor to correct position

EdAyers · Aug 30, 2022 · dde1ede · dde1ede
1 parent c6468e2
commit dde1ede
Show file tree

Hide file tree

Showing 4 changed files with 2 additions and 21 deletions.
diff --git a/src/Lean/Data/Lsp/Basic.lean b/src/Lean/Data/Lsp/Basic.lean
@@ -142,13 +142,6 @@ structure ApplyWorkspaceEditParams where
   edit : WorkspaceEdit
   deriving ToJson
 
-structure ShowDocumentParams where
-  uri : DocumentUri
-  external? : Option Bool
-  takeFocus? : Option Bool
-  selection? : Option Range
-  deriving ToJson
-
 structure TextDocumentItem where
   uri : DocumentUri
   languageId : String

diff --git a/src/Lean/Server/FileWorker/RequestHandling.lean b/src/Lean/Server/FileWorker/RequestHandling.lean
@@ -215,9 +215,7 @@ def getConvZoomCommands (expr: Widget.SubexprInfo) (p: Lsp.PlainGoalParams)
         (Widget.buildConvZoomCommands expr goals[0]! snap.stx hoverPos doc))
       let hOut := ctx.hOut
       let applyRequest : JsonRpc.Request ApplyWorkspaceEditParams := { id := "applyEdit", method := "workspace/applyEdit", param := ret.applyParams }
-      let _ := ←hOut.writeLspMessage applyRequest
-      let showRequest : JsonRpc.Request ShowDocumentParams := { id := "showDocument", method := "window/showDocument", param := ret.showParams }
-      let _ := ←hOut.writeLspMessage showRequest
+      hOut.writeLspMessage applyRequest
       return some ret.commands
 
 partial def handleDocumentHighlight (p : DocumentHighlightParams)

diff --git a/src/Lean/Server/Watchdog.lean b/src/Lean/Server/Watchdog.lean
@@ -644,8 +644,6 @@ section MainLoop
         mainLoop (←runClientTask)
       | Message.response "applyEdit" _ =>
         mainLoop (←runClientTask)
-      | Message.response "showDocument" _ =>
-        mainLoop (←runClientTask)
       | _ => throwServerError "Got invalid JSON-RPC message"
     | ServerEvent.clientError e => throw e
     | ServerEvent.workerEvent fw ev =>

diff --git a/src/Lean/Widget/ConvZoomCommands.lean b/src/Lean/Widget/ConvZoomCommands.lean
@@ -260,11 +260,7 @@ private def syntaxInsert (stx : Syntax) (pathBeforeConvParam : List Nat) (pathAf
       let right := value.drop 7
       newval := left ++ additionalArgs ++ ", " ++ right
       convsMerged := true
-
-
     --get whitespace from previous tactic and make new node
-
-
     /-let argNr := match pathAfterConv.head! with
       | 0 => 0
       | x => x - 1-/
@@ -320,7 +316,6 @@ private def syntaxInsert (stx : Syntax) (pathBeforeConvParam : List Nat) (pathAf
 structure ConvZoomReturn where
   commands : ConvZoomCommands
   applyParams : Lsp.ApplyWorkspaceEditParams
-  showParams : Lsp.ShowDocumentParams
 
 def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveGoal) (stx : Syntax) (p : String.Pos) (doc : Lean.Server.FileWorker.EditableDocument): MetaM ConvZoomReturn := do
   let mut list := (SubExpr.Pos.toArray subexprParam.subexprPos).toList
@@ -364,9 +359,6 @@ def buildConvZoomCommands (subexprParam : SubexprInfo) (goalParam : InteractiveG
   let edit : Lsp.WorkspaceEdit := { changes? := none, documentChanges? := [textDocumentEdit].toArray , changeAnnotations? := none }
   let applyParams : Lsp.ApplyWorkspaceEditParams := { label? := "insert `enter` tactic", edit := edit }
 
-  let showRange : Lsp.Range := { start := text.utf8PosToLspPos {byteIdx := 100}, «end» := text.utf8PosToLspPos {byteIdx := 101} }
-  let showParams : Lsp.ShowDocumentParams := { uri := doc.meta.uri, external? := none, takeFocus? := true, selection? := showRange }
-
-  return { commands := commands, applyParams := applyParams, showParams := showParams }
+  return { commands := commands, applyParams := applyParams }
 
 end Lean.Widget