Skip to content
Snippets Groups Projects
Commit 9689433f authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[feature] jscoqdoc. 

A useful utility for injecting jsCoq into documents generated by `coqdoc`.
Adapted from a hack I used for Software Foundations.

To demonstrate its use, `nahas_tutorial.v` is used as an example.
parent c7095b35
No related branches found
No related tags found
No related merge requests found
Expand all Hide whitespace changes
Inline Side-by-side
examples/.gitignore 0 → 100644
+ 2
− 0
View file @ 9689433f
_build
nahas_tutorial.html
examples/Makefile 0 → 100644
+ 9
− 0
View file @ 9689433f
.PHONY: all
all: nahas_tutorial.html
nahas_tutorial.html: nahas_tutorial.v
mkdir -p _build && cp $< _build/
coqc _build/$<
JSCOQ_URL=.. ../ui-js/jscoqdoc.js --no-index --no-lib-name --parse-comments _build/$<
@rm coqdoc.css # urghh
examples/nahas_tutorial.v 0 → 100644
+ 2903
− 0
View file @ 9689433f
This diff is collapsed.
ui-css/jscoq.css deleted 100644 → 0
+ 0
− 183
View file @ c7095b35
code, kbd, pre, samp {
font-family: Menlo,Monaco,Consolas,monospace;
}
body,html {
height: 100%;
background-color:#eee;
}
#toplevel-container {
width: 50%;
background-color: black;
color: #ccc;
overflow: auto;
overflow-x: hidden;
height: 100%;
float:left;
padding:10px;
padding-top: 20px;
}
#toplevel-container pre#output {
padding: 0px;
}
#toplevel-container #output {
background-color:transparent;
color: #ccc;
border: none;
line-height:18px;
font-size: 12px;
margin-bottom: 0px;
}
#toplevel-container textarea {
width:90%;
line-height:18px;
font-size: 12px;
background-color: transparent;
color: #fff;
border: 0;
resize: none;
outline: none;
font-family: Menlo,Monaco,Consolas,monospace;
font-weight: bold;
float:left;
margin: 0px;
padding:0px;
}
#toplevel-container #sharp {
float: left;
line-height:18px;
font-size: 12px;
font-family: Menlo,Monaco,Consolas,monospace;
white-space: pre;
}
.sharp:before{
content:"# ";
line-height:18px;
font-size: 12px;
font-family: Menlo,Monaco,Consolas,monospace;
}
.caml{
color:rgb(110, 110, 201);
}
#toplevel-side {
position:relative;
width:45%;
height: 100%;
overflow: auto;
text-align:justify;
float:left;
margin-left:30px;
}
.stderr {
color: #d9534f;
}
.stdout {
}
#goal-info-area {
overflow: auto;
height: 30%;
float: left;
margin-bottom: 0.2em;
}
#toplevel-info ul{
padding: 0px;
list-style-type: none;
}
div.msg-area {
padding-top: 0.2em;
border-top: 2px solid black;
overflow: auto;
resize: vertical;
float: left;
width: 100%;
}
.msg-area span {
display: block;
padding: 2px;
margin-top: 2px;
margin-bottom: 0px;
border-left: 2px solid red;
border-top: 1px dashed red;
/* border-bottom: 1px solid red; */
border-right: 1px solid red;
width: 100%;
}
#goal-info-area {
height: 50%;
}
#goal-info-area span {
border: 0px;
}
#query-info-area {
height: 13%;
}
#jscoq-log-area {
height: 30%;
}
.errorloc{
border-bottom-width: 3px;
border-bottom-style: solid;
border-bottom-color: red;
}
canvas {
border: 1px dashed black;
float: left;
margin: 7px;
}
#output canvas {
background-color: #464646;
float: none;
display: block;
border: 1px dashed while;
margin: 7px;
}
#output img {
display:block;
}
#toplevel-examples {
width: 270px;
float: left;
}
#toplevel-examples .list-group-item{
padding: 5px 15px;
}
#btn-share {
float:right;
margin-top:-20px;
background-color:rgb(92, 129, 184);
border-color: rgb(70, 75, 128);
padding: 1px 5px;
display:none;
}
.clear { clear:both; }
.sharp .id { color: #59B65C ; font-style: italic }
.sharp .kw0 { color: rgb(64, 75, 190); font-weight: bold ;}
.sharp .kw1 { color: rgb(150, 0, 108); font-weight: bold ;}
.sharp .kw2 { color: rgb(23, 100, 42); font-weight: bold ;}
.sharp .kw3 { color: #59B65C; font-weight: bold ;}
.sharp .kw4 { color: #59B65C; font-weight: bold ;}
.sharp .comment { color: green ; font-style: italic ; }
.sharp .string { color: #6B6B6B; font-weight: bold ; }
.sharp .text { }
.sharp .numeric { color: #729AAF; }
.sharp .directive { font-style: italic ; color : #EB00FF; } ;
.sharp .escape { color: #409290 ; }
.sharp .symbol0 { color: orange ; font-weight: bold ; }
.sharp .symbol1 { color: #993300 ; font-weight: bold ; }
.sharp .constant { color: rgb(0, 152, 255); }
ui-css/jscoqdoc.css 0 → 100644
+ 632
− 0
View file @ 9689433f
body {
overscroll-behavior-y: none;
--header-bg: #4b525f87;
--heading-bg: #91a1d1;
}
@media (max-width: 1564px) { /* 860 / 0.55 */
/* this is a hack that's needed because changing padding causes reflow */
/* and loses the current scroll position */
.terse#ide-wrapper #main {
padding-right: 10px;
padding-left: 10px;
}
.terse#ide-wrapper #page {
padding-left: 80px;
transition: padding 0.1s ease;
transition-delay: 0.5s;
}
.terse#ide-wrapper:not(.toggled) #page {
padding-left: 0;
}
#ide-wrapper #main {
transition: padding 0.1s ease;
transition-delay: 0.3s;
}
.full#ide-wrapper:not(.toggled) #main {
padding-right: 10px;
transition: padding 0.1s ease;
}
#ide-wrapper:not(.toggled) #page {
transition-delay: 0s;
}
.terse#ide-wrapper #panel-wrapper {
transition-delay: 0.1s;
}
}
#ide-wrapper.layout-flex #panel-wrapper {
max-width: 38em !important; /* jsCoq's default is 48em */
}
.doc div.code {
display: block;
overflow-x: auto;
}
*:focus {
outline: none;
}
#jscoq-plug {
position: absolute;
height: 32px;
right: 0;
top: 40px;
width: 40px !important;
background: url(../ui-images/jscoq-splash.png);
background-size: cover;
cursor: pointer;
/*transition: visibility 0s linear 1s, width 0.2s ease; */
transition: width 0.2s ease;
}
#jscoq-plug:hover {
width: 60px !important;
}
body.goals-active #jscoq-plug {
width: 0 !important;
}
#panel-wrapper button.close {
position: absolute;
padding: 0;
border: none;
top: 0; left: 0;
width: 15px; height: 15px;
font-size: 16px; line-height: 10px;
}
#panel-wrapper button.close:hover {
background: #ccc;
}
#panel-wrapper #toolbar {
padding-left: 15px;
}
/*
* Larger fonts in presentation mode (SF's `terse`)
*/
body.terse #panel-wrapper .flex-panel {
font-size: 125%;
}
body.terse #panel-wrapper .exits.right {
display: none;
}
body.terse .CodeMirror.jscoq {
font-size: 22px;
line-height: 34px;
}
body.terse #goal-panel div.contextual-info {
font-size: 100%; /* overrides jsCoq's style */
}
body.terse #query-panel .Error,
body.terse #query-panel .Warning,
body.terse #query-panel .Notice,
body.terse #query-panel .Info,
body.terse #query-panel .Debug {
background-size: 18px;
background-position-y: 3px;
padding-left: 22px;
}
#footer hr {
border-top: 1px solid black;
opacity: 0.2;
}
/* ---------------------------------------------------------------- */
/**
* Document body styles;
* Based on Software Foundations
*/
body {
padding: 0px 0px;
margin: 0px 0px;
padding-left: 1em;
background-color: white;
font-family: Arial, Helvetica, sans-serif;
background-repeat: no-repeat;
background-size: 100%;
}
#page {
display: block;
padding: 0px;
margin: 0px;
}
#header {
min-height: 30px;
max-width: 760px;
margin: 0 auto;
padding-left: 80px;
padding-right: 80px;
padding-top: 30px;
background-color: var(--header-bg);
}
#header h1 {
padding: 0;
margin: 0;
}
/* Menu */
ul#menu {
padding: 0;
display: block;
margin: auto;
}
ul#menu li, div.button {
display: inline-block;
background-color: white;
padding: 5px;
font-size: .70em;
text-transform: uppercase;
width: 30%;
text-align: center;
font-weight: 600;
}
div.button {
margin-top:5px;
width: 40%;
}
#button_block {margin-top:50px;}
ul#menu a.hover li {
background-color: red;
}
/* Contents */
#main, #main_home {
display: block;
padding: 80px;
padding-top: 60px; /* BCP */
font-size: 100%;
line-height: 100%;
max-width: 760px;
background-color: #ffffff;
margin: 0 auto;
}
#main_home {
background-color: rgba(255, 255, 255, 0.5);
}
#index_content div.intro p {
font-size: 12px;
}
#main h1 {
/* line-height: 80%; */
line-height: normal;
padding-top: 3px;
padding-bottom: 4px;
/* Demitri: font-size: 22pt; */
font-size: 200%; /* BCP */
}
/* allow for multi-line headers */
#main a.idref:visited {color : #416DFF; text-decoration : none; }
#main a.idref:link {color : #416DFF; text-decoration : none; }
#main a.idref:hover {text-decoration : none; }
#main a.idref:active {text-decoration : none; }
#main a.modref:visited {color : #416DFF; text-decoration : none; }
#main a.modref:link {color : #416DFF; text-decoration : none; }
#main a.modref:hover {text-decoration : none; }
#main a.modref:active {text-decoration : none; }
#main .keyword { color : #697f2f }
#main { color: black }
/* General section class - applies to all .section IDs */
.section {
padding-top: 12px;
padding-bottom: 11px;
padding-left: 8px;
margin-top: 5px;
margin-bottom: 3px;
margin-top: 18px;
font-size : 125%;
color: #ffffff;
}
.section, ul#menu li.section_name, div.button, td.logical_tab, .ui-state-active {
background-color: var(--heading-bg);
}
/* Book title in header */
.booktitleinheader {
color: #000000;
text-transform: uppercase;
font-weight: 300;
letter-spacing: 1px;
font-size: 125%;
margin-left: 0px;
margin-bottom: 22px;
}
/* Chapter titles */
.libtitle {
max-width: 860px;
text-transform: uppercase;
margin: 5px auto;
font-weight: 500;
padding-bottom: 2px;
font-size: 120%;
letter-spacing: 3px;
}
.subtitle {
display: block;
padding-top: 10px;
font-size: 70%;
line-height: normal;
}
h2.section {
color: #2a2c71;
background-color: transparent;
padding-left: 0px;
padding-top: 0px;
padding-bottom: 0px;
/* margin-top: 0px; */
margin-top: 9px; /* BCP 2/20 */
font-size : 135%; }
h3.section {
/* background-color: rgb(90%,90%,100%); */
background-color: white;
/* padding-left: 8px; */
padding-left: 0px;
/* padding-top: 7px; */
padding-top: 0px;
/* padding-bottom: 0px; */
padding-bottom: 0.5em;
/* margin-top: 9px; */
/* margin-top: 4px; (BCP 2/20) */
margin-top: 9px; /* BCP 2/20 */
font-size : 115%;
color:black;
}
h4.section {
margin-top: .2em;
background-color: white;
color: #2a2c71;
padding-left: 0px;
padding-top: 0px;
padding-bottom: 0.5em; /* 0px; */
font-size : 100%;
font-style : bold;
text-decoration : underline;
}
#header p {
font-size: 13px;
}
/* Sets up Main ID and margins */
#main .doc {
margin: 0px auto;
font-size: 14px;
line-height: 22px;
/* max-width: 570px; */
color: black;
/* text-align: justify; */
border-style: plain;
/* This might work better after changing back to standard coqdoc: */
padding-top: 10px;
/* padding-top: 18px; */
}
.quote {
margin-left: auto;
margin-right: auto;
width: 40em;
color: darkred;
}
.loud {
color: darkred;
}
pre {
margin-top: 0px;
margin-bottom: 0px;
}
.inlinecode {
display: inline;
/* font-size: 125%; */
color: #444444;
font-family: monospace }
.doc .inlinecode {
display: inline;
font-size: 105%;
color: rgb(35%,35%,70%);
font-family: monospace }
h1 .inlinecode .id, h1.section span.inlinecode {
color: #ffffff;
}
.inlinecodenm {
display: inline;
/* font-size: 125%; */
color: #444444;
}
.doc .inlinecodenm {
display: inline;
color: rgb(35%,35%,70%);
}
.doc .inlinecodenm .id {
color: rgb(35%,35%,70%);
}
.doc .code {
display: inline;
font-size: 110%;
color: rgb(35%,35%,70%);
font-family: monospace;
padding-left: 0px;
}
.comment {
display: inline;
font-family: monospace;
color: rgb(50%,50%,80%);
}
.inlineref {
display: inline;
/* font-family: monospace; */
color: rgb(50%,50%,80%);
}
.show::before {
/* content: "more"; */
content: "+";
}
.show {
background-color: rgb(93%,93%,93%);
display: inline;
font-family: monospace;
font-size: 60%;
padding-top: 1px;
padding-bottom: 2px;
padding-left: 4px;
padding-right: 4px;
color: rgb(60%,60%,60%);
}
/*
.show {
display: inline;
font-family: monospace;
font-size: 60%;
padding-top: 0px;
padding-bottom: 0px;
padding-left: 10px;
border: 1px;
border-style: solid;
color: rgb(75%,75%,85%);
}
*/
.proofbox {
font-size: 90%;
color: rgb(75%,75%,75%);
}
#main .less-space {
margin-top: -12px;
}
/* Inline quizzes */
.quiz:before {
color: rgb(40%,40%,40%);
/* content: "- Quick Check -" ; */
display: block;
text-align: center;
margin-bottom: 5px;
}
.quiz {
border: 4px;
border-color: rgb(80%,80%,80%);
/*
margin-left: 40px;
margin-right: 100px;
*/
padding: 5px;
padding-left: 8px;
padding-right: 8px;
margin-top: 10px;
margin-bottom: 15px;
border-style: solid;
}
/* For textual ones... */
.show-old {
display: inline;
font-family: monospace;
font-size: 80%;
padding-top: 0px;
padding-bottom: 0px;
padding-left: 3px;
padding-right: 3px;
border: 1px;
margin-top: 5px; /* doesn't work?! */
border-style: solid;
color: rgb(75%,75%,85%);
}
.largebr {
margin-top: 10px;
}
.code {
padding-left: 20px;
font-size: 14px;
font-family: monospace;
line-height: 17px;
margin-top: 9px;
}
/* Working:
.code {
display: block;
padding-left: 0px;
font-size: 110%;
font-family: monospace;
}
*/
.code-space {
max-width: 50em;
margin-top: 0em;
/* margin-bottom: -.5em; */
margin-left: auto;
margin-right: auto;
}
.code-tight {
max-width: 50em;
margin-top: .6em;
/* margin-bottom: -.7em; */
margin-left: auto;
margin-right: auto;
}
hr.doublespaceincode {
height: 1pt;
visibility: hidden;
font-size: 10px;
}
/*
code.br {
height: 5em;
}
*/
#main .citation {
color: rgb(70%,0%,0%);
text-decoration: underline;
}
table.infrule {
border: 0px;
margin-left: 50px;
margin-top: .5em;
margin-bottom: 1.2em;
}
td.infrule {
font-family: monospace;
text-align: center;
/* color: rgb(35%,35%,70%); */
padding: 0px;
line-height: 100%;
}
tr.infrulemiddle hr {
margin: 1px 0 1px 0;
}
.infrulenamecol {
color: rgb(60%,60%,60%);
font-size: 80%;
padding-left: 1em;
padding-bottom: 0.1em
}
#footer {
font-size: 65%;
font-family: sans-serif;
}
.id { display: inline; }
.id[title="constructor"] {
color: #697f2f;
}
.id[title="var"],
.id[title="variable"] {
color: rgb(40%,0%,40%);
}
.id[title="definition"] {
color: rgb(0%,40%,0%);
}
.id[title="abbreviation"] {
color: rgb(0%,40%,0%);
}
.id[title="lemma"] {
color: rgb(0%,40%,0%);
}
.id[title="instance"] {
color: rgb(0%,40%,0%);
}
.id[title="projection"] {
color: rgb(0%,40%,0%);
}
.id[title="method"] {
color: rgb(0%,40%,0%);
}
.id[title="inductive"] {
color: #034764;
}
.id[title="record"] {
color: rgb(0%,0%,80%);
}
.id[title="class"] {
color: rgb(0%,0%,80%);
}
.id[title="keyword"] {
color : #697f2f;
/* color: black; */
}
.inlinecode .id {
color: rgb(0%,0%,0%);
}
.nowrap {
white-space: nowrap;
}
.HIDEFROMHTML {
display: none;
}
ui-js/jscoq-agent.js 0 → 100644
+ 83
− 0
View file @ 9689433f
/**
* Injects jsCoq into an existing page.
* This script has to be at the end of the body so that it runs after
* the page DOM has loaded.
*/
function jsCoqInject() {
b = document.body;
b.setAttribute('id', 'ide-wrapper');
b.classList.add('toggled');
b.classList.add(isTerse() ? 'terse' : 'full');
var plug = document.createElement('div');
plug.setAttribute('id', 'jscoq-plug');
plug.addEventListener('click', jsCoqStart);
b.append(plug);
}
var jsCoqShow = location.search === '?jscoq=on' ||
location.search !== '?jscoq=off' && localStorage.jsCoqShow === 'true';
var jscoq_ids = ['#main > div.code, #main > div.HIDEFROMHTML > div.code'];
var jscoq_opts = {
layout: 'flex',
show: jsCoqShow,
focus: false,
replace: true,
editor: { mode: { 'company-coq': true }, className: 'jscoq code-tight' },
init_pkgs: ['init'],
all_pkgs: { '+': ['coq'] },
init_import: ['utf8'],
implicit_libs: true
};
async function jsCoqLoad() {
// - remove empty code fragments (coqdoc generates some spurious ones)
for (let code of document.querySelectorAll('#main > div.code')) {
if (code.textContent.match(/^\s*$/)) code.remove();
}
// - make page div focusable so that keyboard scrolling works
var page = document.querySelector('#page');
page.setAttribute('tabindex', -1);
page.focus();
// - set presenter keyboard bindings to page-up/page-down to allow editing
if (typeof KEYS !== 'undefined')
Object.assign(KEYS, {
next: 34, // PageDown
prev: 33 // PageUp
});
// - load and start jsCoq
await JsCoq.load(jscoq_opts.base_path);
Deprettify.REPLACES.push( // LF,PLF define their own versions (for Imp)
[/∨/g, '\\/'], [/∧/g, '/\\'], [/↔/g, '<->'], [/≤/g, '<='], [/≠/g, '<>'],
[/∈/g, '\\in']);
var coq = await JsCoq.start(jscoq_ids, jscoq_opts);
window.coq = coq;
window.addEventListener('beforeunload', () => { localStorage.jsCoqShow = coq.layout.isVisible(); })
// - close button (replaces jsCoq's bulky power button)
//$('#panel-wrapper #toolbar').prepend($('<button>').addClass('close').text('×')
// .on('click', () => coq.layout.hide()));
}
function jsCoqStart() {
coq.layout.show();
}
/** SF-style terse mode */
function isTerse() {
return !!document.querySelector('[src$="/slides.js"]');
}
if (location.search !== '?jscoq=no') {
window.addEventListener('DOMContentLoaded', () => {
jsCoqInject();
jsCoqLoad();
});
}
ui-js/jscoqdoc.js 0 → 100755
+ 54
− 0
View file @ 9689433f
#!/usr/bin/env node
const fs = require('fs'),
path = require('path'),
chld = require('child-process-promise');
const JSCOQ_URL = process.env['JSCOQ_URL'] || '.',
SCRIPTS = ["ui-js/jscoq-loader.js", "ui-js/jscoq-agent.js"],
STYLES = ["ui-css/jscoqdoc.css"];
function treatText(text) {
return text
.replace(/(<link href=")coqdoc[.]css(".*>)/, (_, pref, suf) =>
[...SCRIPTS.map(mkScript), ...STYLES.map(mkStyle)].join('\n'));
}
function treatFile(fn) {
var text = fs.readFileSync(fn, 'utf-8');
fs.writeFileSync(fn, treatText(text));
}
function url(fn) {
return `${JSCOQ_URL}/${fn}`;
}
function mkScript(fn) {
return `<script src="${url(fn)}"></script>`;
}
function mkStyle(fn) {
return `<link href="${url(fn)}" rel="stylesheet" type="text/css" />`;
}
async function main() {
var args = process.argv.slice(2),
coqdocArgs = args.filter(x => !x.endsWith('.html')),
html = args.map(a => {
if (a.endsWith('.html')) return a;
else if (a.endsWith('.v'))
return path.basename(a).replace(/[.]v$/, '.html')
}).filter(x => x);
if (coqdocArgs.length > 0) {
await chld.spawn('coqdoc', coqdocArgs, {stdio: 'inherit'});
}
for (let fn of html)
treatFile(fn);
}
main().catch(e => {
console.log(`error: ${e.message}`);
process.exit(1);
})
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment