r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

doc: IncludeStr

main
Henrik Böving 2022-05-19 20:41:45 +02:00
parent 279df92555
commit 5fd076530e
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
DocGen4/IncludeStr.lean
View File

@ -27,6 +27,11 @@ partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option F
syntax (name := includeStr) "include_str" str : term syntax (name := includeStr) "include_str" str : term
/--
Provides a way to include the contents of a file at compile time as a String.
This is used to include things like the CSS and JS in the binary so we
don't have to carry them around as files.
-/
@[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do @[termElab includeStr] def includeStrImpl : TermElab := λ stx expectedType? => do
let str := stx[1].isStrLit?.get! let str := stx[1].isStrLit?.get!
let srcPath := (FilePath.mk (← read).fileName) let srcPath := (FilePath.mk (← read).fileName)