DrRacket/advanced_files/scribble-common.js

   1 // Common functionality for PLT documentation pages
   2
   3 // Page Parameters ------------------------------------------------------------
   4
   5 var page_query_string =
   6   (location.href.search(/\?([^#]+)(?:#|$)/) >= 0) && RegExp.$1;
   7
   8 var page_args =
   9   ((function(){
  10       if (!page_query_string) return [];
  11       var args = page_query_string.split(/[&;]/);
  12       for (var i=0; i<args.length; i++) {
  13         var a = args[i];
  14         var p = a.indexOf('=');
  15         if (p >= 0) args[i] = [a.substring(0,p), a.substring(p+1)];
  16         else args[i] = [a, false];
  17       }
  18       return args;
  19     })());
  20
  21 function GetPageArg(key, def) {
  22   for (var i=0; i<page_args.length; i++)
  23     if (page_args[i][0] == key) return unescape(page_args[i][1]);
  24   return def;
  25 }
  26
  27 function MergePageArgsIntoLink(a) {
  28   if (page_args.length == 0 ||
  29       (!a.attributes["pltdoc"]) || (a.attributes["pltdoc"].value == ""))
  30     return;
  31   a.href.search(/^([^?#]*)(?:\?([^#]*))?(#.*)?$/);
  32   if (RegExp.$2.length == 0) {
  33     a.href = RegExp.$1 + "?" + page_query_string + RegExp.$3;
  34   } else {
  35     // need to merge here, precedence to arguments that exist in `a'
  36     var i, j;
  37     var prefix = RegExp.$1, str = RegExp.$2, suffix = RegExp.$3;
  38     var args = str.split(/[&;]/);
  39     for (i=0; i<args.length; i++) {
  40       j = args[i].indexOf('=');
  41       if (j) args[i] = args[i].substring(0,j);
  42     }
  43     var additions = "";
  44     for (i=0; i<page_args.length; i++) {
  45       var exists = false;
  46       for (j=0; j<args.length; j++)
  47         if (args[j] == page_args[i][0]) { exists = true; break; }
  48       if (!exists) str += "&" + page_args[i][0] + "=" + page_args[i][1];
  49     }
  50     a.href = prefix + "?" + str + suffix;
  51   }
  52 }
  53
  54 // Cookies --------------------------------------------------------------------
  55
  56 function GetCookie(key, def) {
  57   var i, cookiestrs;
  58   try {
  59     if (document.cookie.length <= 0) return def;
  60     cookiestrs = document.cookie.split(/; */);
  61   } catch (e) { return def; }
  62   for (i = 0; i < cookiestrs.length; i++) {
  63     var cur = cookiestrs[i];
  64     var eql = cur.indexOf('=');
  65     if (eql >= 0 && cur.substring(0,eql) == key)
  66       return unescape(cur.substring(eql+1));
  67   }
  68   return def;
  69 }
  70
  71 function SetCookie(key, val) {
  72   var d = new Date();
  73   d.setTime(d.getTime()+(365*24*60*60*1000));
  74   try {
  75     document.cookie =
  76       key + "=" + escape(val) + "; expires="+ d.toGMTString() + "; path=/";
  77   } catch (e) {}
  78 }
  79
  80 // note that this always stores a directory name, ending with a "/"
  81 function SetPLTRoot(ver, relative) {
  82   var root = location.protocol + "//" + location.host
  83            + NormalizePath(location.pathname.replace(/[^\/]*$/, relative));
  84   SetCookie("PLT_Root."+ver, root);
  85 }
  86
  87 // adding index.html works because of the above
  88 function GotoPLTRoot(ver, relative) {
  89   var u = GetCookie("PLT_Root."+ver, null);
  90   if (u == null) return true; // no cookie: use plain up link
  91   // the relative path is optional, default goes to the toplevel start page
  92   if (!relative) relative = "index.html";
  93   location = u + relative;
  94   return false;
  95 }
  96
  97 // Utilities ------------------------------------------------------------------
  98
  99 normalize_rxs = [/\/\/+/g, /\/\.(\/|$)/, /\/[^\/]*\/\.\.(\/|$)/];
 100 function NormalizePath(path) {
 101   var tmp, i;
 102   for (i = 0; i < normalize_rxs.length; i++)
 103     while ((tmp = path.replace(normalize_rxs[i], "/")) != path) path = tmp;
 104   return path;
 105 }
 106
 107 // `noscript' is problematic in some browsers (always renders as a
 108 // block), use this hack instead (does not always work!)
 109 // document.write("<style>mynoscript { display:none; }</style>");
 110
 111 // Interactions ---------------------------------------------------------------
 112
 113 function DoSearchKey(event, field, ver, top_path) {
 114   var val = field.value;
 115   if (event && event.keyCode == 13) {
 116     var u = GetCookie("PLT_Root."+ver, null);
 117     if (u == null) u = top_path; // default: go to the top path
 118     u += "search/index.html?q=" + escape(val);
 119     if (page_query_string) u += "&" + page_query_string;
 120     location = u;
 121     return false;
 122   }
 123   return true;
 124 }
 125
 126 function TocviewToggle(glyph, id) {
 127   var s = document.getElementById(id).style;
 128   var expand = s.display == "none";
 129   s.display = expand ? "block" : "none";
 130   glyph.innerHTML = expand ? "&#9660;" : "&#9658;";
 131 }
 132
 133 // Page Init ------------------------------------------------------------------
 134
 135 // Note: could make a function that inspects and uses window.onload to chain to
 136 // a previous one, but this file needs to be required first anyway, since it
 137 // contains utilities for all other files.
 138 var on_load_funcs = [];
 139 function AddOnLoad(fun) { on_load_funcs.push(fun); }
 140 window.onload = function() {
 141   for (var i=0; i<on_load_funcs.length; i++) on_load_funcs[i]();
 142 };
 143
 144 AddOnLoad(function(){
 145     var links = document.getElementsByTagName("a");
 146     for (var i=0; i<links.length; i++) MergePageArgsIntoLink(links[i]);
 147     var label = GetPageArg("ctxtname",false);
 148     if (!label) return;
 149     var indicator = document.getElementById("contextindicator");
 150     if (!indicator) return;
 151     indicator.innerHTML = label;
 152     indicator.style.display = "block";
 153   });