Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • hamelin/jscoq-light
  • rousselin/jscoq-light
2 results
Show changes
Showing
with 909 additions and 42 deletions
......@@ -8,7 +8,7 @@ type Block_type =
| ['Pp_hvbox', number]
| ['Pp_hovbox', number];
export type Pp =
export type Pp =
['Pp_empty']
| ['Pp_string', string]
| ['Pp_glue', Pp[]]
......
"""
Coqdoclight
A script to turn coq files into worksheets
"""
import sys, html, pathlib
def err(x):
print("####### ERROR ########")
print(x, file=sys.stderr)
print("######################")
exit(1)
def dbg(x):
print(x, file=sys.stderr)
def out(x):
print(x, end="")
def out_rw_snippet():
out('<textarea class="snippet">')
def out_ro_snippet():
out('<textarea class="snippet read-only">')
out_snippet = out_rw_snippet
def trimout(x):
out(x.strip())
def html_out(x):
out(html.escape(x))
out("\n")
"""
Token interface
"""
class Token:
"""
Eat a character, return None if there is no match yet,
or the length of the match
"""
def eat(self, c):
pass
"""
Reset the internal state of the tokenizer
"""
def reset(self):
pass
class Char(Token):
def __init__(self,c):
self.c = c
def eat(self, x):
if x == self.c:
return 1
class Stars(Token):
def __init__(self):
self.reset()
def reset(self):
self.newline = True
self.stars = 0
def eat(self,c):
if c == '\n':
self.newline = True
self.stars = 0
elif self.newline:
if c == '*':
self.stars += 1
elif c == ' ' and self.stars > 0:
ret=self.stars+1
self.stars=0
self.newline=False
return ret
elif not c.isspace():
self.newline = False
self.stars = 0
class Leading(Token):
def __init__(self,lit):
self.lit = lit
self.idx = 0
self.newline = True
def reset(self):
self.newline = True
self.idx = 0
def eat(self,c):
if c == '\n':
self.newline = True
if self.newline:
if c == self.lit[self.idx]:
self.idx += 1
if self.idx == len(self.lit):
self.idx = 0
self.newline = c == '\n'
return len(self.lit)
else:
self.newline = c.isspace()
self.idx = 0
else:
self.newline = c.isspace()
self.idx = 0
class Lit(Token):
def __init__(self,lit):
self.idx = 0
self.lit = lit
self.len = len(lit)
def reset(self):
self.idx = 0
def eat(self, x):
if self.lit[self.idx] == x:
self.idx += 1
if self.idx == self.len:
self.reset()
return self.len
else:
self.idx = 0
class Scanner:
def __init__(self,src):
self.rules = []
self.i = 0
self.process = err
self.src = src
self.stack = []
self.cleanup = []
def prev(self):
if self.i > 0:
return self.src[self.i-1]
def push(self,rules,process):
self.stack.append((self.rules, self.process, self.cleanup))
self.rules = rules
self.process = process
self.cleanup = []
def pop(self):
for c in list(self.cleanup):
c.action(sc,self.i,self.i)
(self.rules, self.process, self.cleanup) = self.stack[-1]
self.stack.pop()
def consecutive(self):
c = self.src[self.i]
i = self.i+1
for i in range(i,len(self.src)):
if self.src[i] != c:
i-=1
break
return (i+1)-self.i
def eat(self,c):
for ru in self.rules:
r = ru.token.eat(c)
if r:
self.reset()
return (ru, r)
def reset(self):
for ru in self.rules:
ru.token.reset()
def find_next(self):
comments=0
first_comment=0
while self.i < len(self.src):
c = self.src[self.i]
r = self.eat(c)
if c == '*' and self.prev() == '(':
if comments == 0:
first_comment = self.i-1
comments += 1
if comments > 0 and c == ')' and self.prev() == '*':
comments -= 1
self.reset()
if r:
(ru,l) = r
tokstart=self.i-l+1
tokend=self.i+1
if comments == 0 or tokstart <= first_comment: # if the token includes the comment, we accept it
return (ru,tokstart,tokend)
self.i += 1
def scan(self):
cstart = 0
cend = 0
alive = True
while alive:
r = self.find_next()
if not r:
alive=False
cend=len(self.src)
else:
# Set the cursor end to the start of the token
(_,cend,_) = r
buf=self.src[cstart:cend]
if buf and not buf.isspace():
#dbg(f"PR:{self.process.__name__}:@@@{buf}@@@")
self.process(buf)
if r:
(ru,s,e) = r
#dbg(f"RU:{type(ru).__name__}:{type(ru.token).__name__}:@@@{self.src[s:e]}@@@")
ru.action(self,s,e)
self.i+=1
cstart=self.i
class Rule:
# sc = scanner
# s = beginning index of the match
# e = end index of the match
def action(self,sc,s,e):
pass
# Coqdoc
TOK_BEGIN_CODE = Char('[')
TOK_END_CODE_COQ = Char(']')
TOK_END_CODE = Lit(']]')
TOK_BEGIN_VERBATIM = Leading("<<\n")
TOK_END_VERBATIM = Leading(">>\n")
TOK_BEGIN_COM = Lit("(*")
TOK_END_COM = Lit("*)")
TOK_DASH = Leading("-")
TOK_STARS = Stars()
TOK_ENDLINE = Char('\n')
TOK_BLANKLINE = Lit("\n\n")
TOK_UNDERSCORE = Char('_')
TOK_SHARP = Char('#')
class Code(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_CODE
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
sc.push([self], trimout)
if sc.consecutive() < 2: # coq code
out('<code class="cm-s-default coq-highlight">')
self.token = TOK_END_CODE_COQ
else: # non-coq code
out('<code>')
self.token = TOK_END_CODE
sc.i += 1 # skip second [
def end_action(self,sc,s,e):
out('</code>')
sc.pop()
self.set_start()
class Html(Rule):
def __init__(self):
self.token = TOK_SHARP
self.set_start()
def set_start(self):
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
sc.push([self], trimout)
def end_action(self,sc,s,e):
sc.pop()
self.set_start()
class Comment(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_COM
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
sc.push([self], trimout)
out('<code class="cm-s-default coq-highlight">(*')
self.token = TOK_END_COM
def end_action(self,sc,s,e):
sc.pop()
self.set_start()
out('*)</code>')
class Title(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_STARS
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
self.hlevel = e-s-1 # the blank space
out(f'<h{self.hlevel}>')
self.token = TOK_ENDLINE
sc.cleanup.append(self)
def end_action(self,sc,s,e):
self.set_start()
sc.cleanup.remove(self)
out(f'</h{self.hlevel}>\n')
class ListEnd(Rule):
def __init__(self,start_rule):
self.start_rule = start_rule
self.token = TOK_BLANKLINE
def action(self,sc,s,e):
sc.cleanup.remove(self)
sc.rules.remove(self)
self.start_rule.action = self.start_rule.start_action
out("</li>")
for _ in range(0,self.start_rule.deepness):
out("</ul>")
out("\n")
class ListStart(Rule):
def __init__(self):
self.token = TOK_DASH
self.action = self.start_action
def start_action(self,sc,s,e):
cons=sc.consecutive()
if cons >= 4: # this is a horizontal rule
out("<hr />\n")
sc.i+=cons-1
return
self.action = self.in_action
self.deepness = 0
listend = ListEnd(self)
sc.rules.append(listend)
sc.cleanup.append(listend)
self.in_action(sc,s,e)
def in_action(self,sc,s,e):
level=sc.consecutive()
sc.i += level-1
if level > self.deepness:
for _ in range(0,level-self.deepness):
out("<ul>")
elif level < self.deepness:
for _ in range(0,self.deepness-level):
out("</ul>")
elif self.deepness != 0:
out("</li>")
self.deepness = level
out("<li>\n")
class Italic(Rule):
def __init__(self):
self.token = TOK_UNDERSCORE
self.set_start()
def set_start(self):
self.action = self.start_action
def start_action(self,sc,s,e):
out("<i>")
self.action = self.end_action
def end_action(self,sc,s,e):
out("</i>")
self.set_start()
class Verbatim(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_VERBATIM
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
self.token = TOK_END_VERBATIM
sc.push([self], trimout)
out('<pre>')
def end_action(self,sc,s,e):
sc.pop()
self.set_start()
out('</pre>\n')
class Ignore(Rule):
def __init__(self,token):
self.token = token
self.set_start()
def set_start(self):
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
sc.push([self], len)
def end_action(self,sc,s,e):
sc.pop()
self.set_start()
class EndCoqdoc(Rule):
def __init__(self):
self.token = TOK_END_COM
def action(self,sc,s,e):
sc.pop()
out("</p>\n")
# Top tokens
TOK_BEGIN_HIDE = Lit("(* begin hide *)")
TOK_END_HIDE = Lit("(* end hide *)")
TOK_BEGIN_SHOW = Lit("(* begin show *)")
TOK_END_SHOW = Lit("(* end show *)")
TOK_BEGIN_DETAILS=Lit("(* begin details ")
TOK_END_DETAILS=Lit("(* end details *)")
TOK_BEGIN_READ_ONLY=Lit("(* begin read-only *)")
TOK_END_READ_ONLY=Lit("(* end read-only *)")
TOK_BEGIN_DOC = Lit("(**")
class Show(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_SHOW
self.action = self.start_action
def start_action(self,sc,s,e):
out('</textarea>')
self.token = TOK_END_SHOW
self.action = self.end_action
push_top(sc)
sc.rules.append(self)
def end_action(self,sc,s,e):
out('<textarea style="display:none;" class="snippet">\n')
self.set_start()
sc.pop()
class Hide(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_HIDE
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.end_action
self.token = TOK_END_HIDE
out('<textarea style="display:none;" class="snippet">\n')
sc.push([self, Show()], trimout)
def end_action(self,sc,s,e):
out('</textarea>')
sc.pop()
self.set_start()
class Details(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_DETAILS
self.action = self.start_action
def start_action(self,sc,s,e):
self.action = self.com_action
self.token = TOK_END_COM
self.details_name = None
def set_details_name(x):
self.details_name = x[1:]
sc.push([self], set_details_name)
def com_action(self,sc,s,e):
self.action = self.end_action
self.token = TOK_END_DETAILS
sc.process = trimout
out('<details>\n')
if self.details_name:
out(f'<summary>{self.details_name}</summary>\n')
out_snippet()
def end_action(self,sc,s,e):
out('</textarea>\n</details>')
sc.pop()
self.set_start()
class ReadOnly(Rule):
def __init__(self):
self.set_start()
def set_start(self):
self.token = TOK_BEGIN_READ_ONLY
self.action = self.start_action
def start_action(self,sc,s,e):
global out_snippet
self.action = self.end_action
self.token = TOK_END_READ_ONLY
out_snippet = out_ro_snippet
def end_action(self,sc,s,e):
global out_snippet
self.set_start()
out_snippet = out_rw_snippet
class Coqdoc(Rule):
def __init__(self):
self.token = TOK_BEGIN_DOC
def action(self,sc,s,e):
out("<p>\n")
rules=[
Code (),
Verbatim (),
EndCoqdoc (),
Title (),
Italic (),
Comment (),
ListStart (),
Html (),
Ignore (Char('$')), # Ignore latex
Ignore (Char('%')), # idem
]
sc.push(rules, html_out)
def push_top(sc):
def snippet_out(x):
out_snippet()
out(x.strip())
out('</textarea>\n')
sc.push([Hide (), Coqdoc (), Details (), ReadOnly ()], snippet_out)
if len(sys.argv) < 2:
err("moulinette expect one argument: the path of the coq file")
with open(sys.argv[1], 'r') as file:
global sc
sc = Scanner(file.read())
filename=pathlib.Path(sys.argv[1]).name
out("""
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<title>jsCoq – Use Coq in Your Browser</title>
<meta http-equiv="content-type" content="text/html;charset=utf-8" />
<meta name="description" content="An Online IDE for the Coq Theorem Prover" />
<!-- Move to copy with the bundle -->
<link rel="icon" href="frontend/classic/images/favicon.png">
<style>body { visibility: hidden; } /* FOUC avoidance */</style>
<link rel="stylesheet" type="text/css" href="./dist/frontend/index.css">
</head>
<body class="jscoq-main">
<div id="ide-wrapper" class="toggled">
<div id="code-wrapper">
<div id="document-wrapper">
""")
out(f'<div id="document" data-filename="{filename}">')
push_top(sc)
sc.scan()
# TODO: Options for addons
out("""
</div> <!-- /#document -->
</div> <!-- /#document-wrapper -->
</div> <!-- /#code-wrapper -->
</div> <!-- /#ide-wrapper -->
<script type="module">
import { JsCoq } from './jscoq.js';
var sp = new URLSearchParams(location.search),
ifHas = x => sp.has(x) ? x : undefined;
if (!localStorage['scratchpad.last_filename'])
setTimeout(() => document.body.classList.add('welcome'), 1500);
var jscoq_ids = ['.snippet'];
var jscoq_opts = {
backend: sp.get('backend') ?? ifHas('wa'),
implicit_libs: false,
focus: false,
editor: { mode: { 'company-coq': true } },
all_pkgs: {'./coq-pkgs': ['coq'], './addons/teach/coq-pkgs': ['teach']}
};
JsCoq.start(jscoq_ids, jscoq_opts).then(res => {
/* Global reference */
window.coq = res;
});
</script>
</body>
</html>
""")
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -27,7 +27,7 @@
package.json
package-lock.json)
(action
(run npm install --no-save)))
(run npm install --no-progress --no-save)))
(alias
(name jscoq)
......@@ -48,6 +48,8 @@
(source_tree examples)
(source_tree docs) ; for `quick-help.html`
dist
jscoq.js
dist-webpack
index.html
coq-pkgs))
......
......@@ -57,7 +57,7 @@ var frontend = esbuild
format: "esm",
loader: {
'.png': 'binary',
'.svg': 'binary'
'.svg': 'dataurl'
},
outdir: "dist/frontend",
minify,
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.