On Sat, 22 Jun 2019 08:55:43 -0700 (PDT), Jon P <[email protected]> wrote: > Re results we are using ElasticSearch and so we should have a good amount > of leeway to optimise the results. I guess the best result for 2+2 is > 2p2e4. We're still experimenting with how much to search the comments and > theorem names and how much to search the assertions. There may need to be > some way for people to specify they are searching the assertions, such as > using |- maybe.
Sounds reasonable. I think if a conclusion matches exactly it should rank high, but tweaking sort results is complicated :-). > Re fonts we are a little confused (we don't have so much frontend > experience). Is this the font you mean that could be hosted? > https://github.com/alif-type/xits On Metamath.org it seems to call that > font at the beginning however it also seems to be commented out which is a > little confusing. I suggest looking here for an example: http://us.metamath.org/mpeuni/2p2e4.html The key is this in the style: @font-face { font-family: XITSMath-Regular; src: url(xits-math.woff); } .math { font-family: XITSMath-Regular } Of course, now you need the file xits-math.woff at that directory. You can get a copy from the Metamath site. More details here: https://developer.mozilla.org/en-US/docs/Web/CSS/@font-face I suggest testing with Firefox; Firefox is pickier about font locations (for security), so if it works with Firefox it'll work with anything. Setting up the fonts takes a few minutes, but it'll mean that the text will work almost everywhere. I just noticed that we *only* specify a url source in Metamath. We might want to add a local(...) to the src options, so that people who already have XITSMath-Regular installed will just use that. It's a minor optimization, but it'd be nice for first-timers with poor bandwidth. I'll have to track that down later. --- David A. Wheeler P.S., here it is in a larger context: <STYLE TYPE="text/css"> <!-- img { margin-bottom: -4px } .r { font-family: "Arial Narrow"; font-size: x-small; } .i { font-family: "Arial Narrow"; font-size: x-small; color: gray; } --> </STYLE> <STYLE TYPE="text/css"> <!-- .setvar { color: red; } .wff { color: blue; } .class { color: #C3C; } .symvar { border-bottom:1px dotted;color:#C3C} .typecode { color: gray } .hidden { color: gray } @font-face { font-family: XITSMath-Regular; src: url(xits-math.woff); } .math { font-family: XITSMath-Regular } --> </STYLE> -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E1hekxm-00079X-8m%40rmmprod05.runbox.
