Issues while executing tactics with `;` in them.

I was trying to execute the following theorem via REPL:

theorem ftaylorSeriesWithin_univ : ftaylorSeriesWithin 𝕜 f univ = ftaylorSeries 𝕜 f := by sorry

.This theorem can be found in Mathlib in the file mathlib/Mathlib/Analysis/Calculus/ContDiff/Defs.lean (https://github.com/leanprover-community/mathlib4/blob/ae43e7f0dda4b24139e98b5033268fa1d7b09374/Mathlib/Analysis/Calculus/ContDiff/Defs.lean#L1642). I made a copy of this file by copying its contents till this theorem and replacing the proof with a sorry and removed the subsequent content of the file. I successfully loaded the theorems and definitions in this copied file via the command {"path": <path-to-copied-file> } using REPL, however, when I start running the proof line by line interactively in tactic mode via the command {'tactic': 'ext1 x; ext1 n', 'proofState': 0} (which is a valid tactic as used in the proof and works on VS Code IDE), I keep getting error: 'Lean error:\n<input>:1:6: expected end of input'. I have noticed that whenever I have ; used in the command I keep getting the same error (even in some other proofs). The error specifically points to the character ; (in this case Lean error:\n:1:6:)

Note: Everything works fine as soon as I run {'tactic': 'ext1 x', 'proofState': 0}.

Reproduce the failure through the REPL command using the tactic entry point, comparing ext1 x; ext1 n with ext1 x. Use the copied Mathlib/Analysis/Calculus/ContDiff/Defs.lean context as the reproduction case; done when tactics containing ; are accepted and the reported end-of-input error is gone.