From 69df80d1151ec718ffc44140fbd8e355c1088aea Mon Sep 17 00:00:00 2001 From: Matthew Butterick Date: Thu, 15 Nov 2018 07:30:09 -0800 Subject: [PATCH] remove scribble js --- pollen/private/ts.rktd | 2 +- pollen/scribblings/scribble-common.js | 180 -------------------------- 2 files changed, 1 insertion(+), 181 deletions(-) delete mode 100644 pollen/scribblings/scribble-common.js diff --git a/pollen/private/ts.rktd b/pollen/private/ts.rktd index 2b7b447..b4f930e 100644 --- a/pollen/private/ts.rktd +++ b/pollen/private/ts.rktd @@ -1 +1 @@ -1541194651 +1542295809 diff --git a/pollen/scribblings/scribble-common.js b/pollen/scribblings/scribble-common.js deleted file mode 100644 index 976298e..0000000 --- a/pollen/scribblings/scribble-common.js +++ /dev/null @@ -1,180 +0,0 @@ -// Common functionality for PLT documentation pages - -// Page Parameters ------------------------------------------------------------ - -var page_query_string = location.search.substring(1); - -var page_args = - ((function(){ - if (!page_query_string) return []; - var args = page_query_string.split(/[&;]/); - for (var i=0; i= 0) args[i] = [a.substring(0,p), a.substring(p+1)]; - else args[i] = [a, false]; - } - return args; - })()); - -function GetPageArg(key, def) { - for (var i=0; i= 0 && cur.substring(0,eql) == key) - return unescape(cur.substring(eql+1)); - } - return def; - } -} - -function SetCookie(key, val) { - try { - localStorage[key] = val; - } catch(e) { - var d = new Date(); - d.setTime(d.getTime()+(365*24*60*60*1000)); - try { - document.cookie = - key + "=" + escape(val) + "; expires="+ d.toGMTString() + "; path=/"; - } catch (e) {} - } -} - -// note that this always stores a directory name, ending with a "/" -function SetPLTRoot(ver, relative) { - var root = location.protocol + "//" + location.host - + NormalizePath(location.pathname.replace(/[^\/]*$/, relative)); - SetCookie("PLT_Root."+ver, root); -} - -// adding index.html works because of the above -function GotoPLTRoot(ver, relative) { - var u = GetCookie("PLT_Root."+ver, null); - if (u == null) return true; // no cookie: use plain up link - // the relative path is optional, default goes to the toplevel start page - if (!relative) relative = "index.html"; - location = u + relative; - return false; -} - -// Utilities ------------------------------------------------------------------ - -var normalize_rxs = [/\/\/+/g, /\/\.(\/|$)/, /\/[^\/]*\/\.\.(\/|$)/]; -function NormalizePath(path) { - var tmp, i; - for (i = 0; i < normalize_rxs.length; i++) - while ((tmp = path.replace(normalize_rxs[i], "/")) != path) path = tmp; - return path; -} - -// `noscript' is problematic in some browsers (always renders as a -// block), use this hack instead (does not always work!) -// document.write(""); - -// Interactions --------------------------------------------------------------- - -function DoSearchKey(event, field, ver, top_path) { - var val = field.value; - if (event && event.keyCode == 13) { - var u = GetCookie("PLT_Root."+ver, null); - if (u == null) u = top_path; // default: go to the top path - u += "search/index.html?q=" + encodeURIComponent(val); - u = MergePageArgsIntoUrl(u); - location = u; - return false; - } - return true; -} - -function TocviewToggle(glyph, id) { - var s = document.getElementById(id).style; - var expand = s.display == "none"; - s.display = expand ? "block" : "none"; - glyph.innerHTML = expand ? "▼" : "►"; -} - -// Page Init ------------------------------------------------------------------ - -// Note: could make a function that inspects and uses window.onload to chain to -// a previous one, but this file needs to be required first anyway, since it -// contains utilities for all other files. -var on_load_funcs = []; -function AddOnLoad(fun) { on_load_funcs.push(fun); } -window.onload = function() { - for (var i=0; i