Merge pull request #45 from xubaiw/better-includestr

Make include_str relative to file

DocGen4/IncludeStr.lean

@@ -7,13 +7,37 @@ import Lean
 
 namespace DocGen4
 
-open Lean System IO Lean.Elab.Term
+open Lean System IO Lean.Elab.Term FS
+
+deriving instance DecidableEq for FileType
+
+/--
+  Traverse all subdirectories fo `f` to find if one satisfies `p`.
+-/
+partial def traverseDir (f : FilePath) (p : FilePath → IO Bool) : IO (Option FilePath) := do
+  if (← p f) then
+    return f
+  for d in (← System.FilePath.readDir f) do
+    let subDir := d.path
+    let metadata ← subDir.metadata
+    if metadata.type = FileType.dir then
+      if let some p ← traverseDir subDir p then
+        return p
+  return none
 
 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
+  let str := stx[1].isStrLit?.get!
+  let srcPath := (FilePath.mk (← read).fileName)
+  let currentDir ← IO.currentDir
+  -- HACK: Currently we cannot get current file path in VSCode, we have to traversely find the matched subdirectory in the current directory.
+  if let some path ← match srcPath.parent with
+  | some p => pure $ some $ p / str
+  | none => do
+    let foundDir ← traverseDir currentDir λ p => p / str |>.pathExists 
+    pure $ foundDir.map (· / str)
+  then 
     if ←path.pathExists then
       if ←path.isDir then
         throwError s!"{str} is a directory"
@@ -21,6 +45,8 @@ syntax (name := includeStr) "include_str" str : term
         let content ← FS.readFile path
         pure $ mkStrLit content
     else
-      throwError s!"\"{str}\" does not exist as a file"
+      throwError s!"{path} does not exist as a file"
+  else
+    throwError s!"No such file in whole directory: {str}"
 
 end DocGen4

DocGen4/Output/Base.lean

@@ -46,14 +46,14 @@ def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
   basePath / parts.foldl (· / ·) (FilePath.mk ".")
 
 section Static
-  def styleCss : String := include_str "./static/style.css"
-  def siteRootJs : String := include_str "./static/site-root.js"
-  def declarationDataCenterJs : String := include_str "./static/declaration-data.js"
-  def navJs : String := include_str "./static/nav.js"
-  def howAboutJs : String := include_str "./static/how-about.js"
-  def searchJs : String := include_str "./static/search.js"
-  def findJs : String := include_str "./static/find/find.js"
-  def mathjaxConfigJs : String := include_str "./static/mathjax-config.js"
+  def styleCss : String := include_str "../../static/style.css"
+  def siteRootJs : String := include_str "../../static/site-root.js"
+  def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
+  def navJs : String := include_str "../../static/nav.js"
+  def howAboutJs : String := include_str "../../static/how-about.js"
+  def searchJs : String := include_str "../../static/search.js"
+  def findJs : String := include_str "../../static/find/find.js"
+  def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
 end Static
 
 def declNameToLink (name : Name) : HtmlM String := do