-
Notifications
You must be signed in to change notification settings - Fork 479
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Change search_index to be a JSON file #2517
base: master
Are you sure you want to change the base?
Conversation
Not the best thing at the moment, because the fetch() function assumes site is served from / So it won't find search_index.json if site is project.com/docs instead of docs.project.com
Search now works from all pages in the built docs, and the basic file is a valid JSON file, which can be manipulated using standard JSON tools. |
@mortenpi @fredrikekre could you please let the CI tests run on this one? It seems quite useful to me (but I am biased, I work with @aaruni96 ;-) ). |
Sorry for the delay here. So, the reason we have it as a And I think we still want to support that Just a thought I had that we could try though is put the If that doesn't work, then I'm inclined to leave the default to generate the Last note: purely on aesthetic grounds, I agree that a JSON file would be cleaner. And would also make it much easier for anyone to consume or post-process it. But it's the |
MDN seems to suggest
That idea doesn't work for two reasons: 1) fetch still throws a CORS error, and 2) I couldn't figure out a way to have the path of the index be relative to the current page, if it was all inside the javascript.
Currently the documentation for the OSCAR project (https://docs.oscar-system.org) includes the documentation for sub projects like Nemo, Hecke, AbstractAlgebra. We do want some, but not all documentation pages from these sub projects. While we make the unwanted pages unreachable via navigation, they still show up in search, being confusing to users (functions with the same name but different method might work in Nemo, but not Oscar). If the search index were a standard json file, we could run a post process script to trim out these unwanted pages from search. This is the situation as I understand it, maybe @fingolfin can correct me. |
Local browsing anyways doesn't work well if prettyurls is true (default). Maybe a compromise can be, use a valid json file if prettyurls is true, and the current method of loading the index to a variable from within the search_index.js if prettyurls is false ? |
To uncomplicate the two codepaths, we could keep the name if prettyurls is true, add the fetch to HTML pages, and don't add the assignment to Would that be an idea worth considering ? |
I would prefer not to complicate For the OSCAR use case.. what about hooking into the search index generation in Julia, in But if you want to process the JSON file, then I'd say let's make this opt-in, configured via an option to
Uh, yea, okay, looks like things have become more strict, not less, over time. My knowledge predated CVE-2019-11730 😄 |
# convert Vector{SearchRecord} to a JSON string + do additional JS escaping | ||
println(io, JSDependencies.json_jsescape(ctx.search_index), "\n}") | ||
println(io, JSDependencies.json_jsescape(ctx.search_index)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Needs to be double checked, but JSON might need a different escaping function.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
It looks to me like json_jsescape only escapes some newline unicode, so it turns already valid JSON to also be valid javascript (also, according to comments in the source code, this is not required since 2019).
More closely looking at the function, it calls JSON.json()
, and then escapes the problematic unicode in whatever is returned, so this should be fine (at least for this change).
I'm going to need some more explanation here...
Best as I can tell, we somehow convince Documenter to build the documentation for Oscar + all the sub projects at the same time, right @fingolfin ? |
We do all kinds of crude things and hacks in https://github.com/oscar-system/Oscar.jl/blob/master/docs/make_work.jl to make it work, including using a nasty hack to workaround the fact that PR #552 here (from 2017) still hasn't been merged (perhaps I can volunteer @aaruni96 to help finish that? ;-) ) But I'll try to stay on topic: we actually copy documentation from Hecke, Nemo, AbstractAlgebra, but we do by copying (or rather: symlinking) So I assume that the index creation is after that, so hooking into the search index generation might indeed work? |
Sorry for the delay. So, the search index is just a linear list we populate while HTMLWriter goes through the document Documenter.jl/src/html/HTMLWriter.jl Line 646 in 0c55392
It then gets written out here at the end Documenter.jl/src/html/HTMLWriter.jl Lines 809 to 813 in 0c55392
We could add an interface where you e.g. pass a callback to The Documenter.jl/src/html/HTMLWriter.jl Lines 619 to 627 in 0c55392
Documenter.jl/src/html/HTMLWriter.jl Lines 703 to 714 in 0c55392
|
Not the best thing at the moment, because the fetch() function assumes index lives in "./". So search only works from /index.html.
I don't really know how to fix this.
Addresses #2516 , when its fixed.