Hello! I ran into an issue a while ago, where trying to elaborate/give expressions in holes that contain strings resulted in lexical errors. These errors did not occur in agda-mode for Emacs.
Screenshot
Demo code in the screenshot
```agda
open import Agda.Builtin.List
open import Agda.Builtin.Nat
open import Agda.Builtin.String
open import Agda.Builtin.Reflection
open import Agda.Builtin.Unit
macro
doAThing : String → Term → TC ⊤
doAThing s h = typeError (strErr "Finished" ∷ [])
thing : Nat
thing = {! doAThing "x" !}
thing2 : String
thing2 = {! "x" !}
```
This only happens when the expression from the hole in the source code is used. If the hole is empty, agda-mode-vscode will prompt for an expression, and the same expression will work.
The error occurs because expressions that are obtained from holes in the source code are quoted twice, using Parser.userInput. The quoting happens in Goal.getContent and again in the request encoding. This results in string values such as "x" being turned into "\\\"x\\\"", and then into "\\\\\\\"x\\\\\\\"" in the second phase.
This pull request makes the following changes:
Replaces ->Parser.userInput with JS.String.trim in Goal.getContent. This means that getContent is no longer escaped properly. The reason trim is introduced is so that the matches on the empty string (such as this one) continue to work well.
Most applications of getContent have gotten an additional ->Parser.userInput. Notable exceptions are:
The call in pointed. This one should be fine, since it's mostly used to find the selected goal and its contents. In these cases, we explicitly do not want quoting to occur.
The call in modify. I believe this one should be mostly fine, as the content is used as the argument to the f function. It is only used in GiveParen and in the input methods. ⚠️ I am not sure how to test these cases myself, although I do not believe they would run into problems because of this change.
banacorn
commented
2 years ago
Hello! I ran into an issue a while ago, where trying to elaborate/give expressions in holes that contain strings resulted in lexical errors. These errors did not occur in
agda-modefor Emacs.Screenshot
Demo code in the screenshot
```agda open import Agda.Builtin.List open import Agda.Builtin.Nat open import Agda.Builtin.String open import Agda.Builtin.Reflection open import Agda.Builtin.Unit macro doAThing : String → Term → TC ⊤ doAThing s h = typeError (strErr "Finished" ∷ []) thing : Nat thing = {! doAThing "x" !} thing2 : String thing2 = {! "x" !} ```This only happens when the expression from the hole in the source code is used. If the hole is empty,
agda-mode-vscodewill prompt for an expression, and the same expression will work.The error occurs because expressions that are obtained from holes in the source code are quoted twice, using
Parser.userInput. The quoting happens inGoal.getContentand again in the request encoding. This results in string values such as"x"being turned into"\\\"x\\\"", and then into"\\\\\\\"x\\\\\\\""in the second phase.This pull request makes the following changes:
->Parser.userInputwithJS.String.triminGoal.getContent. This means thatgetContentis no longer escaped properly. The reasontrimis introduced is so that the matches on the empty string (such as this one) continue to work well.getContenthave gotten an additional->Parser.userInput. Notable exceptions are:pointed. This one should be fine, since it's mostly used to find the selected goal and its contents. In these cases, we explicitly do not want quoting to occur.modify. I believe this one should be mostly fine, as the content is used as the argument to theffunction. It is only used inGiveParenand in theinput methods. ⚠️ I am not sure how to test these cases myself, although I do not believe they would run into problems because of this change.