From 962a4bfa7848066090209f86edce3fec482f3dd2 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Fri, 5 Aug 2022 16:32:35 -0400
Subject: [PATCH] chore: move includeStr elaborator

---
 src/Lean/Elab.lean             |  1 -
 src/Lean/Elab/BuiltinTerm.lean | 18 ++++++++++++++++++
 src/Lean/Elab/IncludeStr.lean  | 29 -----------------------------
 3 files changed, 18 insertions(+), 30 deletions(-)
 delete mode 100644 src/Lean/Elab/IncludeStr.lean

diff --git a/src/Lean/Elab.lean b/src/Lean/Elab.lean
index 06cd4d5439..62ab7fdcf9 100644
--- a/src/Lean/Elab.lean
+++ b/src/Lean/Elab.lean
@@ -43,4 +43,3 @@ import Lean.Elab.BuiltinCommand
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.Eval
 import Lean.Elab.Calc
-import Lean.Elab.IncludeStr
diff --git a/src/Lean/Elab/BuiltinTerm.lean b/src/Lean/Elab/BuiltinTerm.lean
index ca272daefe..9f7cc65eea 100644
--- a/src/Lean/Elab/BuiltinTerm.lean
+++ b/src/Lean/Elab/BuiltinTerm.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Term
+import Lean.Elab.Eval
 
 namespace Lean.Elab.Term
 open Meta
@@ -304,4 +305,21 @@ private def mkSilentAnnotationIfHole (e : Expr) : TermElabM Expr := do
     withInfoContext' stx (elabTerm e expectedType?) (mkTermInfo .anonymous (expectedType? := expectedType?) stx)
   | _ => throwUnsupportedSyntax
 
+private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=
+  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx
+
+@[implementedBy evalFilePathUnsafe]
+private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
+
+@[builtinTermElab includeStr] def elabIncludeStr : TermElab
+  | `(include_str $path:term), _ => do
+    let path ← evalFilePath path
+    let ctx ← readThe Lean.Core.Context
+    let srcPath := System.FilePath.mk ctx.fileName
+    let some srcDir := srcPath.parent
+      | throwError "cannot compute parent directory of '{srcPath}'"
+    let path := srcDir / path
+    mkStrLit <$> IO.FS.readFile path
+  | _, _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term
diff --git a/src/Lean/Elab/IncludeStr.lean b/src/Lean/Elab/IncludeStr.lean
deleted file mode 100644
index d9fc35a61c..0000000000
--- a/src/Lean/Elab/IncludeStr.lean
+++ /dev/null
@@ -1,29 +0,0 @@
-/-
-Copyright (c) 2021 Henrik Böving. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Henrik Böving, Xubai Wang, Wojciech Nawrocki
--/
-
-import Lean.Elab.Term
-import Lean.Elab.Eval
-
-namespace Lean.Elab.Term
-
-private unsafe def evalFilePathUnsafe (stx : Syntax) : TermElabM System.FilePath :=
-  evalTerm System.FilePath (Lean.mkConst ``System.FilePath) stx
-
-@[implementedBy evalFilePathUnsafe]
-private opaque evalFilePath (stx : Syntax) : TermElabM System.FilePath
-
-@[builtinTermElab includeStr] def elabIncludeStr : TermElab
-  | `(include_str $path:term), _ => do
-    let path ← evalFilePath path
-    let ctx ← readThe Lean.Core.Context
-    let srcPath := System.FilePath.mk ctx.fileName
-    let some srcDir := srcPath.parent
-      | throwError "cannot compute parent directory of '{srcPath}'"
-    let path := srcDir / path
-    mkStrLit <$> IO.FS.readFile path
-  | _, _ => throwUnsupportedSyntax
-
-end Lean.Elab.Term