Feature: Increase Input Length

[RexWzh]

Hi,

Issue report: When parsing sketch theorems using REPL, one could get stuck if the input is too long. Investigation revealed this is related to the TTY buffer limitation (e.g. 1024 characters on MacOS), as discussed here.

The current implementation handle longer inputs by concatenating multiple lines, there's a bug where the newline characters (\n) at line endings cause JSON syntax errors.

Current Implementation:

partial def getLines : IO String := do
  let line ← (← IO.getStdin).getLine
  if line.trim.isEmpty then
    return line
  else
    return line ++ (← getLines)

Proposed Fix:

    return line.trimRight ++ (← getLines)

This change allows users to break long inputs into multiple lines using line continuation.

Moveover, the File mode has no input length limitation, but ignores the env field and runs code in a fresh environment. I've updated the env field handling as well.

/-- Process a Lean file in a fresh environment if `env` is not provided. -/
structure File extends CommandOptions where
  env: Option Nat
  path : System.FilePath
deriving FromJson

def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
  try
    let cmd ← IO.FS.readFile s.path
    -- runCommand { s with env := none, cmd }
    runCommand { s with env := s.env, cmd }

All these proposed changes are backward compatible. Thanks in advance for considering these improvements.