No longer need to drop messages and trees in proccessCommandsWithInfo…

…Trees

Signed-off-by: Andrew Wells <andrewmw94@gmail.com>

REPL/Frontend.lean

@@ -20,10 +20,7 @@ def processCommandsWithInfoTrees
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  let msgs := s.messages.toList.drop commandState.messages.toList.length
-  let trees := s.infoState.trees.toList.drop commandState.infoState.trees.size
-
-  pure (s, msgs, trees)
+  pure (s, s.messages.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.

REPL/Main.lean

@@ -205,8 +205,6 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let tactics ← match s.allTactics with
   | some true => tactics trees
   | _ => pure []
-  -- The list is repeated, so we only keep the second half.
-  let tactics := tactics.drop (tactics.length / 2)
   let cmdSnapshot :=
   { cmdState
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD