chore: empty port of the Data.Buffer.Parser in core (#5864)

Komyyy · Komyyy · commit 4d8f5b5cb6e3 · 2023-07-13T14:30:53.000Z
addition to #5848
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -2017,6 +2017,7 @@ import Mathlib.Init.Control.Lawful
 import Mathlib.Init.Core
 import Mathlib.Init.Data.Bool.Basic
 import Mathlib.Init.Data.Bool.Lemmas
+import Mathlib.Init.Data.Buffer.Parser
 import Mathlib.Init.Data.Fin.Basic
 import Mathlib.Init.Data.Int.Basic
 import Mathlib.Init.Data.Int.Bitwise
diff --git a/Mathlib/Init/Data/Buffer/Parser.lean b/Mathlib/Init/Data/Buffer/Parser.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Gabriel Ebner
+
+! This file was ported from Lean 3 source module data.buffer.parser
+! leanprover-community/lean commit 549e2fed50b361d0d49a3dd1e7ccb6de9440059b
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+
+Porting note:
+As the parsing framework has completely changed in Lean 4
+there is no point porting these files directly.
+They can be rewritten from scratch as needed, just as for tactics.
+-/
