OK. You have a marvelous looking webpage. On this you want to share some nice proofs. Maybe you have used BoxProver as assistant. Now it sounds like the app you need is this.
I have made some changes to the grammar - these are described in the "Syntax" section. A line can be followed by a line, no naming are needed. Name tokens can be created using "" - that is anything that is not " goes in here. I have made it so that implication can be written both as => or ->.
Now this put together you can make proofs either by copying the whole boxproof from BoxProver apart from the head, that is the
%abbrev d : {S}{Q}{x_1} proof ( S => exi ([x] Q x) , |- exi ([x] S => Q x) ) = [S][Q][x_1]part. Or you can create arbitrary proofs in a simpler way:
"I <3 deduction" premise p premise q \/ ~q by lem ( q assumption ( q assumption p by copy 1 ) p -> q by imp_i "5 - 7" ) ( ~q assumption ( q assumption bot by neg_e 10 11 p by bot_e 12 ) q => p by imp_i "10 - 14" ) q -> p by dis_e 2 "10-14" "13-17"Note that keywords like "lem" must be followed by a space for the lexer to recognize it.
Back to your nice looking homepage. You can find the git repo here. Grap the file boxproofs.js. Insert the code of stack.js into somewhere reachable. boxproofs.js is a 8000 loc file. This can be a bit overwhelming. However, in order to change the appearance of the boxes you have to change within the object var html found near line 7572. In this you can style the container, the lines and even the error messages.
Finally create spans with boxproves, say you name the class "boxproof". Now run:
var bproofs = new BoxProofs(); bproofs.createBoxesHtml(document.getElementsByClassName("boxproof"));Feel free to tinker around. As goes for most of these projects, this isn't copyrighted.
And if you find any errors - that is proofs accepted by boxprover, but not this app, please make a comment below on the problem.