Topic: documentation view
Patrick Massot (Jan 15 2019 at 08:05):
@Gabriel Ebner What happened to the documentation view feature of vscode-lean?
Gabriel Ebner (Jan 15 2019 at 08:38):
@Patrick Massot I'm a bit busy at the moment so there's nothing new (though it's available in the released version now). In the other thread you suggested that the documentation view should have back/forward buttons and a way to input your own url. I completely agree. (The webview api in vscode is unfortunately really, really stripped down... Not even hyperlinks work by default, we are changing them to vscode commands on the fly....)
@Edward Ayers if you want to look at this, I can give you pointers.
Gabriel Ebner (Jan 15 2019 at 08:39):
In case anybody has too much free time and wants to give feedback, run "ctrl+shift+p open documentation view" and post your complaints here.
Patrick Massot (Jan 15 2019 at 08:42):
Thanks Gabriel! Did you intend to ping Bryan instead of Ed?
Patrick Massot (Jan 15 2019 at 08:43):
@Jeremy Avigad Did you see that feature?
Gabriel Ebner (Jan 15 2019 at 08:44):
No, Ed asked me in Amsterdam to please give him work on the vscode extension. But I'm happy about contributions from all sides.
Patrick Massot (Jan 15 2019 at 08:47):
By the way, am I correct in thinking that this was not in the previous release? If not then please forgive me for asking today
Gabriel Ebner (Jan 15 2019 at 08:50):
I made a release for Ed's translations PR yesterday, that's the first release with the documentation view.
Patrick Massot (Jan 15 2019 at 08:53):
Weird... I did try to check before posting. Sorry
Jeremy Avigad (Jan 16 2019 at 02:51):
I just tried documentation view. It's great! Here are two comments.
The bigger one: once we move from the table of contents to a specific chapter, as far as I can tell it is impossible to go back to the table of contents without pressing ctrl-shift-P and choosing "open documentation view" again. That makes it less convenient to browse. I don't know the ideal solution here. Maybe the best solution is to assign a keystroke to "open documentation view", so that pressing that would return to the TOC.
The smaller issue: the natural way to play with the text and examples is to split the screen, put the text in the left, and then run the examples in the right. But even when I have a split screen, when I click on the "try it" button, the window opens on the left, and I have to manually move it to the right. Would it be possible to have the window open on the right?
Patrick Massot (Jan 31 2019 at 10:47):
I just tried to use the VScode Lean documentation view in our computer rooms, with no success. Could it be that it tries to access TPIL without using the system-wide proxy setup?
Patrick Massot (Jan 31 2019 at 10:48):
@Edward Ayers @Gabriel Ebner
Gabriel Ebner (Jan 31 2019 at 10:48):
Yes, I'm pretty sure it doesn't look at proxy settings.
Patrick Massot (Jan 31 2019 at 10:48):
Note that VScode does successfully use the proxy when downloading the Lean extension
Patrick Massot (Jan 31 2019 at 10:49):
Fixing this would be a nice improvement
Edward Ayers (Jan 31 2019 at 11:01):
Did you have to set the
http.proxy in the vscode settings for the extension downloading to work?
Gabriel Ebner (Jan 31 2019 at 11:02):
Ideally, we could use the system proxy settings that vscode uses itself, but it looks like this is not possible yet: https://github.com/Microsoft/vscode/issues/12588
Gabriel Ebner (Jan 31 2019 at 11:03):
http.proxy* settings are the older (now deprecated) way to set the proxy in vscode (and it is ignored by most of vscode). We could use this setting (but Patrick needs to set it).
Patrick Massot (Jan 31 2019 at 11:05):
I didn't have to set anything to get the extension
Gabriel Ebner (Jan 31 2019 at 11:06):
@Patrick Massot vscode has two settings for proxies: one is taken directly from the system settings and is used for extension fetching, etc. But this is unfortunately not accessible to extensions (i.e., us).
Kevin Buzzard (Jan 31 2019 at 11:35):
issues/12588. Wow -- and I thought we had issues.
Kevin Buzzard (Jan 31 2019 at 11:37):
When there are 4621 open issues, how do you get people to work on the one you want to be fixed?
Mario Carneiro (Jan 31 2019 at 11:41):
in big companies the issues process has to be a lot more formal. There is triage and tagging, periodic review of priorities, and work is often aimed for milestones. Quite often the issues system is the force behind all work - i.e. if you want to change something you should make an issue first, so that the intent is logged and prioritized
Mario Carneiro (Jan 31 2019 at 11:42):
so you have people working on the most important things and other people adding and organizing new issues
Mario Carneiro (Jan 31 2019 at 11:44):
For a big github project, you can vote on your favorite issues by adding a thumbs up reaction to it; this sometimes helps, depending on the team, but it's just a suggestion
Mario Carneiro (Jan 31 2019 at 11:46):
apparently people really want floating windows https://github.com/Microsoft/vscode/issues?q=is%3Aopen+is%3Aissue+sort%3Areactions-%2B1-desc
Last updated: May 10 2021 at 00:31 UTC