diff options
author | Karl Berry <karl@freefriends.org> | 2023-04-18 19:40:32 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2023-04-18 19:40:32 +0000 |
commit | 421c46931938c705ca7c62437a5086ab6b0cfd8a (patch) | |
tree | 93b7c599956d37b6ca920a67e6bf8e236433b725 /Master/texmf-dist/doc/latex/prettytok/prettytok_template.html | |
parent | e63869c62873cc3e4ab1a936a91117f26ae926a3 (diff) |
prettytok (18apr23)
git-svn-id: svn://tug.org/texlive/trunk@66884 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/prettytok/prettytok_template.html')
-rw-r--r-- | Master/texmf-dist/doc/latex/prettytok/prettytok_template.html | 317 |
1 files changed, 317 insertions, 0 deletions
diff --git a/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html b/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html new file mode 100644 index 00000000000..5b0d988a4c0 --- /dev/null +++ b/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html @@ -0,0 +1,317 @@ +<!doctype html> +<html lang="en"> +<head> +<meta charset="utf-8"> +<link rel="icon" href="data:,"> +<style> +body{ + background-color: black; + color: white; +} + +/* https://stackoverflow.com/questions/7011602/stretching-iframe-in-html5 */ +#wrap_all { display: none; position:fixed; width:100%; height:100%; top: 0px; left: 0px; } + + +iframe{ + position: absolute; + width: 100%; + height: 100%; + display: none; +} +#status{ + flex: 0 0 1.3em; +} + +#display_wrap{ + flex: 1 0 auto; +} +#controller{ + flex: 0 0 50px; +} + +.control-button{ +} + + + +.tokenlist, .fileline{ + border: 1px solid gray; + padding: 2px; + line-height: 1.5em; +} + +.fileline{ + background-color: #404040; +} + +.explicit_char_target{ + background-color: #FF8080; +} +.explicit_char{ + background-color: #606060; +} + + +.cs, .active_char{ + color: #FFFF00; +} + +#popup{ + display: none; + position: absolute; + border: 1px solid gray; + background-color: #000080ff; +} + +.cmd__left_brace_cmd, .cmd__right_brace_cmd, .cmd__mac_param_cmd, .frozenrelax{ + color: #FFAAAA; +} +.cmd__out_param_cmd{ + border: 1px solid #FFAAAA; +} +.out_param_expansion{ + border: 1px solid #FFAAAA; + background-color: #000080; +} +.cmd__out_param_cmd::before{ + content: "#"; +} + +.cmd__letter_cmd{ + color: #AAFFAA; +} + +.cmd__spacer_cmd{ + color: #606060; +} + + +input[type=button]{ + color: white; + background-color: #0000ff; + border: 0; +} + +#log{ + display: flex; + flex-direction: column-reverse; + flex: 0 0 30%; + overflow: scroll; +} + +/* + hack to make it display as ␣ but copy-paste (or search) as space +*/ +.space_charcode{ + font-size: 0pt; +} + +.space_charcode::before{ + font-size: medium; + content: "␣"; +} +</style> +</head> +<body> + + <div id=output></div> + <div id=wrap_all> + <iframe id=iframe src="about:blank" frameborder=0></iframe> + <iframe id=iframe2 src="about:blank" frameborder=0></iframe> + </div> + <script> +"use strict" + +function show_html_except_space(s){ + return s + .replace(/\r|\n/g, "↵") + .replace(/\t/g, "⇥") +} + +function show_html(s){ + return show_html_except_space(s).replace(/ /g, "␣") +} + +output.innerHTML="" + +function print_tl(...tokens){ + const tl_div=document.createElement("div") + tl_div.classList.add("tokenlist") + for(let token of tokens){ + tl_div.appendChild(token) + if({13: true, 10: true}[token.data_charcode]){ + tl_div.appendChild(document.createElement("br")) + }else{ + tl_div.appendChild(document.createElement("wbr")) + } + } + output.appendChild(tl_div) +} + +function token(charcode /* int */, catcode /* single character string in hex */){ + const token_span=document.createElement("span") + const ch=String.fromCodePoint(charcode) + token_span.innerText=show_html_except_space(ch) + token_span.data_charcode=charcode + if(charcode==32){ // special handle space here + token_span.classList.add("space_charcode") + } + if(catcode==='D'){ + token_span.classList.add("active_char") + token_span.title=`active ${ch} # ${charcode}` + }else{ + const cls={ + 1: 'cmd__left_brace_cmd', + 2: 'cmd__right_brace_cmd', + 3: 'cmd__math_shift_cmd', + 4: 'cmd__tab_mark_cmd', + 6: 'cmd__mac_param_cmd', + 7: 'cmd__sup_mark_cmd', + 8: 'cmd__sub_mark_cmd', + A: 'cmd__spacer_cmd', + B: 'cmd__letter_cmd', + C: 'cmd__other_char_cmd', + }[catcode] + token_span.classList.add("token", cls) + token_span.title=`${cls} ${ch} # ${charcode}` + } + return token_span +} + +function cs(...codepoints){ + const token_span=document.createElement("span") + + const control_sequence_name=String.fromCodePoint(...codepoints) + //const meaning_str=readstr() + + /* + token_span.innerText='\\' + show_html(control_sequence_name) + ' ' + */ + + var items=control_sequence_name.split(' ') + items[0]="\\"+items[0] + items[items.length-1]+=' ' + for(var i=0; i<items.length; i++){ + if(i!=0){ // append a '␣' span that copy-paste as a space + var space_span=document.createElement("span") + space_span.innerText=' ' + space_span.classList.add("space_charcode") + token_span.appendChild(space_span) + } + + // append the text itself + if(items[i]!="") + token_span.appendChild(new Text(show_html_except_space(items[i]))) + } + + //token_span.title=`cs '${control_sequence_name}' → ${meaning_str}` + token_span.classList.add("cs") + + return token_span +} + +function csfrozenrelax(){ + const token_span=document.createElement("span") + token_span.innerText="\\relax" + token_span.title="frozen relax" + token_span.classList.add("cs", "frozenrelax") + return token_span +} + +var refresh_strategy_already_set=false +function set_refresh_strategy(strategy, duration){ + if(refresh_strategy_already_set) return + refresh_strategy_already_set=true + + switch(strategy){ + case 0: // do nothing + return + + case 1: // refresh the sub-iframe + if(window.parent===window){ + print_tl=function(...x) {} + //output.style.display="none" + iframe.src=location.href + iframe.style.display="block" + wrap_all.style.display="block" + setInterval(function(){ + iframe.src=iframe.src + }, duration) + } + return + + case 2: // refresh two sub-iframes + if(window.parent===window){ + print_tl=function(...x) {} + //output.style.display="none" + iframe.src=iframe2.src=location.href + iframe.style.display="block" + iframe2.style.display="block" + wrap_all.style.display="block" + async function sleep(ms){ + await new Promise(resolve=>setTimeout(resolve, ms)) + } + (async function(){ + while(true){ + await sleep(duration/2) + iframe.src=iframe.src + + await sleep(duration/2) + iframe2.style.zIndex=1 + iframe.style.zIndex=2 + + await sleep(duration/2) + iframe2.src=iframe2.src + + await sleep(duration/2) + iframe.style.zIndex=1 + iframe2.style.zIndex=2 + } + })() + } + return + + case 3: // refresh whole page + setTimeout(function(){ + location.reload() + }, duration) + return + + case 4: // request own file + window.addEventListener("load", async function(){ + async function get_code(){ + //let text=await (await fetch(location.href)).text() + let text=await new Promise(function(resolve){ + let request = new XMLHttpRequest(); + request.responseType = "text" + request.onload = function() { + resolve(request.responseText) + } + request.onerror = function() { + console.log("Error happened. Read documentation for more details.") + } + request.open("GET", location.href, true) + request.send() + }) + return text.replace(/.*?-end-template()-/s, "") + } + let text=await get_code() + output.innerHTML="" + try{ eval(text) }catch(e) {} + setInterval(async function(){ + let text2=await get_code() + if(text2!==text){ + output.innerHTML="" + try{ eval(text2) }catch(e) {} + text=text2 + } + }, duration) + }) + return + } +} + </script> + +<script> +// -end-template- |