summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/prettytok
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2022-07-08 21:52:25 +0000
committerKarl Berry <karl@freefriends.org>2022-07-08 21:52:25 +0000
commit136fa6ccfd2eea815bf528abe6635d5d1ef401d7 (patch)
tree4614673397627b232d832332f017497159ec924f /Master/texmf-dist/doc/latex/prettytok
parent54afcfc581b829cbba8702ccecc339a65942a6ea (diff)
prettytok_template.html in runtime
git-svn-id: svn://tug.org/texlive/trunk@63842 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/prettytok')
-rw-r--r--Master/texmf-dist/doc/latex/prettytok/prettytok_template.html283
1 files changed, 0 insertions, 283 deletions
diff --git a/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html b/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html
deleted file mode 100644
index 8764d498095..00000000000
--- a/Master/texmf-dist/doc/latex/prettytok/prettytok_template.html
+++ /dev/null
@@ -1,283 +0,0 @@
-<!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;
- overflow: scroll;
- white-space: nowrap;
-}
-.tokenlist::-webkit-scrollbar, .fileline::-webkit-scrollbar { width: 0 !important }
-
-.fileline{
- background-color: #404040;
-}
-
-.explicit_char_target{
- background-color: #FF8080;
-}
-.explicit_char{
- background-color: #606060;
-}
-
-
-.cs, .active_char{
- color: #FFFF00;
-}
-.cs::before{
- content: "\\";
-}
-.cs::after{
- content: " ";
-}
-
-#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;
-}
-</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(s){
- return s.replace(/ /g, "␣")
- .replace(/\r|\n/g, "↵")
- .replace(/\t/g, "⇥")
-}
-
-output.innerHTML=""
-
-function print_tl(...tokens){
- const tl_div=document.createElement("div")
- tl_div.className="tokenlist"
- for(let token of tokens){
- tl_div.appendChild(token)
- if({13: true, 10: true}[token.data_charcode]){
- tl_div.appendChild(document.createElement("br"))
- }
- }
- 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(ch)
- token_span.data_charcode=charcode
- if(catcode==='D'){
- token_span.className="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.className="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)
- //token_span.title=`cs '${control_sequence_name}' → ${meaning_str}`
- token_span.className="cs"
-
- return token_span
-}
-
-function csfrozenrelax(){
- const token_span=document.createElement("span")
- token_span.innerText="relax"
- token_span.title="frozen relax"
- token_span.className="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-