Patch search index (#4292)

* Patch search index

This removes anything in search index that is not also present in doc.main.
That is, the search function will not return "hidden" pages, which are not
available via normal navigation.

* Move code to the right place, so its trigerred not just on interactive use

* Add JSON to docs Project.toml

* docs/search: improve doc.main parsing, use .html or / depending on local_build

---------

Co-authored-by: Benjamin Lorenz <[email protected]>

docs/Project.toml

@@ -1,7 +1,9 @@
 [deps]
 Documenter = "e30172f5-a6a5-5a46-863b-614d45cd2de4"
 DocumenterCitations = "daee34ce-89f3-4625-b898-19384cb65244"
+JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 
 [compat]
 Documenter = "1.1"
 DocumenterCitations = "~1.3.4"
+JSON = "0.21.4"

docs/make_work.jl

@@ -4,7 +4,7 @@
 #
 module BuildDoc
 
-using Documenter, DocumenterCitations
+using Documenter, DocumenterCitations, JSON
 
 include("documenter_helpers.jl")
 include("citation_style.jl")
@@ -210,6 +210,56 @@ function doit(
     dstbase = normpath(Oscar.oscardir, "docs", "src", string(nameof(pkg)))
     rm(dstbase; recursive=true, force=true)
   end
+
+  # postprocessing, for the search index
+  docspath = normpath(joinpath(Oscar.oscardir, "docs"))
+  @info "Patching search index."
+  # extract valid json from search_index.js
+  run(pipeline(`sed -n '2p;3q' $(joinpath(docspath, "build", "search_index.js"))`, stdout=(joinpath(docspath, "build", "search_index.json")))) # imperfect file, but JSON parses it
+
+  # extract paths from doc.main
+  filelist=String[]
+  docmain = include(joinpath(docspath, "doc.main"))
+  while !isempty(docmain)
+    n = pop!(docmain)
+    if n isa Pair
+      push!(docmain, last(n))
+    elseif n isa String
+      push!(filelist, n)
+    elseif n isa Array{String}
+      append!(filelist,n)
+    elseif n isa Array
+      append!(docmain,n)
+    else
+      error("err: $(typeof(n))")
+    end
+  end
+  suffix = local_build ? ".html" : "/"
+  filelist = replace.(filelist, r"\.md$"=>suffix)
+
+  # read these files
+  iosearchindex = open(joinpath(docspath, "build", "search_index.json"), "r")
+  searchindex = JSON.parse(iosearchindex)
+  close(iosearchindex)
+
+  newsearchindex = []
+
+  for item in searchindex
+    if split(item["location"], "#")[1] in filelist
+      push!(newsearchindex, item)
+    end
+  end
+
+
+  # combine this to valid javascript again, and overwrite input
+  ionewsearchindex = open(joinpath(docspath, "build", "search_index.js"), "w")
+  write(ionewsearchindex, """var documenterSearchIndex = {"docs":\n""")
+  JSON.print(ionewsearchindex, newsearchindex)
+  write(ionewsearchindex, "\n}")
+  close(ionewsearchindex)
+
+  # clean up
+  rm(joinpath(docspath, "build", "search_index.json"))
 end
 
 end # module BuildDoc