diff --git a/DocGen4/IncludeStr.lean b/DocGen4/IncludeStr.lean new file mode 100644 index 0000000..335365a --- /dev/null +++ b/DocGen4/IncludeStr.lean @@ -0,0 +1,21 @@ +import Lean + +namespace DocGen4 + +open Lean System IO Lean.Elab.Term + +syntax (name := includeStr) "include_str" str : term + +@[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do + let str := stx[1].isStrLit?.get! + let path := FilePath.mk str + if ←path.pathExists then + if ←path.isDir then + throwError s!"{str} is a directory" + else + let content ← FS.readFile path + return mkStrLit content + else + throwError s!"\"{str}\" does not exist as a file" + +end DocGen4