Stream: jsCoq

Topic: pp2DOM vs pp2HTML


view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:03):

Hi @Shachar Itzhaky , can we remove the deprecated pp2HTML/richpp2HTML methods from format-pprint.js

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:03):

?

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:04):

pretty sure the answer is yes

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:06):

Ok, great thanks!

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:06):

We are using it in the vsCode client :)

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:07):

oh nice

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:07):

I will do some cleanup then, and make sure we don't diverge

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:08):

Is there some todo you have in mind? I will for example remove old code, and put the pp2DOM specific css in their own files

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:08):

even if we don't put that code on its own npm package, I'd structure things so it could made independent

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:08):

we can maybe have subsidiary packages that expose some of the functionality but I'm not sure

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:09):

there is some maintenance overhead associated with separate packages

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:09):

Yes

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:09):

but yeah I guess it can be made standalone so that you can "steal" one file out of the jscoq package

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:10):

Yes, there are a couple of files with css etc... so I will put them in a dir

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:10):

then you can just keep the dirs in sync

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:10):

Once the new printer is more mature would make sense to have the rendered as a package tho

view this post on Zulip Shachar Itzhaky (Jan 05 2023 at 15:10):

yeah also if you are using webpack it's possible to import one file out of a package so that it does not bundle the entire package

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:10):

I think it would make sense for this one too, but I'm not planning to work a lot more on Pp.t

view this post on Zulip Emilio Jesús Gallego Arias (Jan 05 2023 at 15:15):

@Ramkumar Ramachandra wonders if we can remove the jQuery dep, I guess so right?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:36):

@Shachar Itzhaky we managed to run pp2DOM in vscode, still doesn't fully work on all cases, I guess we are not calling adjustBreaks at the right places.

Do you remember how should the pp2DOM, dom manipulation, and adjustBreaks be called so that the right magic happens?

Keep in mind that vsCode Goal view has 3 "panels", for goals, for messages (under the position) and for errors.

p.s: we are using esbuild for bundling, that's so much faster and simpler, can't wait to port jsCoq to it.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:37):

Keep in mind that vsCode Goal view has 3 "panels", for goals, for messages (under the position) and for errors.

BTW feedback on that UI choice would be much appreciated.

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 18:46):

is there a preview version of the addon?

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:46):

Yup the released version has the current UI , 0.1.3

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:47):

main branch has the same infopanel for now

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:47):

so you can install it with regular opam / vscode markeplace

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 18:47):

the thing with adjustBreaks is that it has to be called once the element knows its width. This is why it is not done by pp2DOM already; and you have to re-call it if the width changes.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:48):

You call it on the container element?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 18:48):

yes

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:52):

I see, thanks. Something I don't get well how it works in jsCoq is that pp2DOM creates a JQuery object, but then this.layout.update_goals(html) calls the JQuery .html method, is the JQuery object just html?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 18:56):

ah no. But in fact you can call $(...).html($el) where $el is another jQuery object and it will replace the entire content of the first object with the second. Perhaps more coherent would have been $(...).empty().append($el) which makes that clearer.

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 18:57):

jQuery is a wrapper for DOM elements and is rather declining because the DOM api itself has improved and also most frontends use a framework such as React or Vue to manipulate the DOM.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 18:59):

My confusion is more about the type of .html , when it takes a jquery object it will have to print it back to html before setting .innerHtml right?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 19:00):

this was not my understanding but perhaps that's what it does actually?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 19:00):

I thought that it is able to discern that it did not get a string but a jQuery object and will therefore just clone the subtree.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:10):

Yes the documentation is actually wrong, it will use append

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:10):

how do you feel about writing the panels in React?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 19:12):

personally I am more of a Vue.js person

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:15):

So indeed the documentation is outdated after this commit in jQuery:

32d81db90d6ca32ed41b43cbaea347abb1c86c6e
Author:     John Resig <jeresig@gmail.com>
AuthorDate: Mon Jan 8 02:39:10 2007 +0000
Commit: Pruned a lot of extra code out and improved how .html() works.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:17):

Shachar Itzhaky said:

personally I am more of a Vue.js person

I have not used either, but for example I heard that React bindings to CodeMirror and ProseMirror are quite better maintained, so I dunno, I was leaning into React as it seems way more popular.

But indeed we agree that either React or Vue, we want to write some parts like the panel with that, right?

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 19:26):

yes. for the document area there is probably nothing in the framework that's going to help us, so we can just manage that part directly, but the panels can benefit from some better organization.

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:29):

I'm not sure how much of a mess will integration with Curvenote be, it is also written in React

view this post on Zulip Emilio Jesús Gallego Arias (Jan 20 2023 at 19:30):

We will see indeed

view this post on Zulip Shachar Itzhaky (Jan 20 2023 at 19:30):

we need to look into what they use React for. Perhaps it's mostly for the UI around the notebook, such as toolbars and menus, and I'm not sure we want to take that as well.


Last updated: Jun 04 2023 at 23:30 UTC