Fix sensitivity to comments and whitespaces in the header

Author: augustepoiroux

REPL/Frontend.lean

@@ -78,7 +78,7 @@ def processInput (input : String) (cmdState? : Option Command.State)
   match cmdState? with
   | none => do
     let (header, parserState, messages) ← Parser.parseHeader inputCtx
-    let importKey := (input.take parserState.pos.byteIdx).trim
+    let importKey := toString header.raw -- do not contain comments and whitespace
     match headerCache.get? importKey with
     | some cachedHeaderState => do
       -- Header is cached, use it as the base command state

test/Mathlib/test/incrementality.expected.out

@@ -66,3 +66,5 @@
    "data": "9227465"}],
  "env": 1}
 
+{"env": 2}
+

test/Mathlib/test/incrementality.in

@@ -1,3 +1,5 @@
 {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo : n = n := by\n  rfl", "allTactics": true}
 
 {"cmd": "import Mathlib\ntheorem mathd_numbertheory_188 : Nat.gcd 180 168 = 12 := by norm_num\ndef fib : Nat → Nat\n  | 0 => 0\n  | 1 => 1\n  | n + 2 => fib (n + 1) + fib n\n\n#eval fib 35\ntheorem foo2 : n = n+0 := by\n  rfl", "allTactics": true}
+
+{"cmd": "import Mathlib\n-- comment to test if header is reused even when a comment is added"}