Skip to content

Commit

Permalink
[ fix banacorn#178 ] Replace canonicalizeEscape with `Parser.unesca…
Browse files Browse the repository at this point in the history
…peEOL` and handle it upstream in the S-expression parser instead
  • Loading branch information
banacorn committed Nov 15, 2024
1 parent f81bd62 commit bb1b20e
Show file tree
Hide file tree
Showing 6 changed files with 29 additions and 38 deletions.
4 changes: 2 additions & 2 deletions lib/js/src/Response.bs.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

24 changes: 9 additions & 15 deletions lib/js/src/State/State__Response.bs.js

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

4 changes: 2 additions & 2 deletions src/Response.res
Original file line number Diff line number Diff line change
Expand Up @@ -285,7 +285,7 @@ let parse = (tokens: Token.t): result<t, Parser.Error.t> => {
switch xs[3] {
| Some(A("t")) =>
switch xs[2] {
| Some(A(message)) => Ok(RunningInfo(1, message))
| Some(A(message)) => Ok(RunningInfo(1, Parser.unescapeEOL(message)))
| _ => err(11)
}
| _ => Ok(ClearRunningInfo)
Expand All @@ -298,7 +298,7 @@ let parse = (tokens: Token.t): result<t, Parser.Error.t> => {
}
| Some(A("agda2-verbose")) =>
switch xs[1] {
| Some(A(message)) => Ok(RunningInfo(2, message))
| Some(A(message)) => Ok(RunningInfo(2, Parser.unescapeEOL(message)))
| _ => err(13)
}
// NOTE: now there are 2 kinds of "agda2-highlight-clear", "TokenBased" and "NotOnlyTokenBased"
Expand Down
29 changes: 12 additions & 17 deletions src/State/State__Response.res
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
// from Agda Response to Tasks
let canonicalizeEscape = content => content->String.replaceRegExp(%re("/\\n|\\r\\n/g"), "\n")
let insertBeforeNewline = (prefix, content) =>
content->String.replaceRegExp(%re("/\n/g"), "\n" ++ prefix)

// adds indentation to a multiline string
let indent = (content, indent) => {
let indentation = String.repeat(" ", indent)
content->String.replaceRegExp(%re("/\n/g"), "\n" ++ indentation) // should also handles CR LF on Windows
}
// does this function really do anything?
let removeNewlines = string => string->String.split("\n")->Array.join("\n")

open Response
Expand Down Expand Up @@ -153,20 +157,17 @@ let rec handle = async (
// do nothing
await State__Goal.removeBoundaryAndDestroy(state, goal)
| GiveString(content) =>
let (indent, _text, _) = State__Goal.indentationWidth(state.document, goal)
let (indentationWidth, _text, _) = State__Goal.indentationWidth(state.document, goal)
// 1. ideally, we want to add a "\t" or equivalent spaces before the indent based on
// "editor.tabSize" and "editor.insertSpaces"
// but we cannot load the "editor.tabSize" here
// so as a workaround we use a default value of 2
// maybe consider storing these attributed in the state
// 2. the Emacs plugin seems to use len(text) as the indent, which could be a
// safet choice
let defaultIndent = 2
let defaultIndentation = 2
await State__Goal.modify(state, goal, _ =>
insertBeforeNewline(
String.repeat(" ", defaultIndent + indent),
canonicalizeEscape(content),
)
Parser.unescapeEOL(content)->indent(defaultIndentation + indentationWidth)
)
await State__Goal.removeBoundaryAndDestroy(state, goal)
}
Expand Down Expand Up @@ -206,20 +207,14 @@ let rec handle = async (
}
| DisplayInfo(info) => await DisplayInfo.handle(state, info)
| RunningInfo(1, message) =>
Js.log(
"Type-checking:\n " ++
message ++
"\n => " ++
removeNewlines(canonicalizeEscape(message)),
)
let message = removeNewlines(canonicalizeEscape(message))
let message = removeNewlines(message)
await State.View.Panel.displayInAppendMode(
state,
Plain("Type-checking"),
[Item.plainText(message)],
)
| RunningInfo(verbosity, message) =>
let message = removeNewlines(canonicalizeEscape(message))
let message = removeNewlines(message)
state.runningInfoLog->Array.push((verbosity, message))->ignore
await State.View.DebugBuffer.displayInAppendMode([(verbosity, message)])
| CompleteHighlightingAndMakePromptReappear =>
Expand Down
3 changes: 2 additions & 1 deletion test/tests/Parser/Response/Issue95-2.6.1-Unix.out
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
NonLast Status: implicit arguments not displayed, module not type checked
NonLast ClearRunningInfo
NonLast ClearHighlighting
NonLast RunningInfo 1 Checking Issue95 (/Users/omega/github/agda-mode/test/ManualTests/Issue95.agda).\n
NonLast RunningInfo 1 Checking Issue95 (/Users/omega/github/agda-mode/test/ManualTests/Issue95.agda).

NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-0
NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-1
NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode39869-2
Expand Down
3 changes: 2 additions & 1 deletion test/tests/Parser/Response/QuotationMark-2.6.0-Unix.out
Original file line number Diff line number Diff line change
@@ -1,7 +1,8 @@
NonLast Status: implicit arguments not displayed, module not type checked
NonLast ClearRunningInfo
NonLast ClearHighlighting
NonLast RunningInfo 1 Checking QuotationMark (/Users/omega/github/agda-mode/test/ManualTests/QuotationMark.agda).\n
NonLast RunningInfo 1 Checking QuotationMark (/Users/omega/github/agda-mode/test/ManualTests/QuotationMark.agda).

NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-0
NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-1
NonLast HighlightingInfoIndirect /var/folders/r2/lx4mzz2x1kn940m7lhnv0b_h0000gn/T/agda2-mode19020-2
Expand Down

0 comments on commit bb1b20e

Please sign in to comment.