HelpSource/Overviews/Documents.html

   1 <html>
   2 <head>
   3     <title>Documents</title>
   4     <link rel='stylesheet' href='../scdoc.css' type='text/css' />
   5     <meta http-equiv='Content-Type' content='text/html; charset=UTF-8' />
   6     <script src="../docmap.js" type="text/javascript"></script>
   7     <script src="../scdoc.js" type="text/javascript"></script>
   8 <style>
   9 #doclist {
  10     margin-top: 1em;
  11 }
  12 .result_item {
  13     margin-left: 1.5em;
  14     margin-top: 0.2em;
  15 }
  16 #search_checks {
  17     font-size: 9pt;
  18     color: #555;
  19     border-bottom: 1px solid #ddd;
  20     margin-top: 1em;
  21     padding-bottom: 1em;
  22 }
  23 #total_count {
  24     font-size: 9pt;
  25     color: #777;
  26 }
  27 </style>
  28 <noscript>
  29 <p>The document index needs JavaScript.
  30 </noscript>
  31 <script type="text/javascript">
  32 var node;
  33 var docs;
  34 var check_extensions;
  35 var filter;
  36
  37 function did_load() {
  38 //    restoreMenu();
  39     helpRoot=".."; fixTOC();
  40     node = document.getElementById("doclist");
  41     docs = docmap.sort(function(a,b) {
  42         a = a.title.toUpperCase();
  43         b = b.title.toUpperCase();
  44         if(a<b) return -1;
  45         else
  46         if(a>b) return +1;
  47         else
  48         return 0;
  49     });
  50
  51     var onChange = function() {
  52         showdocs();
  53     };
  54
  55     check_extensions = document.getElementById("check_extensions");
  56     check_extensions.onchange = onChange;
  57     filter = document.getElementById("menu_filter");
  58     filter.onchange = onChange;
  59
  60     showdocs();
  61 }
  62
  63 function showdocs() {
  64     while(node.hasChildNodes())
  65         node.removeChild(node.lastChild);
  66
  67     var count = 0;
  68     var cap = undefined;
  69     var div = document.createElement("p");
  70     var docs2 = [];
  71     div.className = "jump";
  72     div.innerHTML = "Jump to: ";
  73
  74     for(var i=0;i<docs.length;i++) {
  75         var v = docs[i];
  76         var x = v.title[0].toUpperCase();
  77
  78         if(v.installed=="extension" && !check_extensions.checked)
  79             continue;
  80
  81         if(filter.value != "all" && v.path.split("/")[0].toLowerCase() != filter.value)
  82             continue;
  83
  84         if(/Undocumented classes/.test(v.categories))
  85             continue;
  86
  87         if(cap != x) {
  88             cap = x;
  89             var a = document.createElement("a");
  90             a.setAttribute("href","#section_"+cap);
  91             a.innerHTML=cap;
  92             div.appendChild(a);
  93             div.appendChild(document.createTextNode(" "));
  94         }
  95
  96         docs2.push(v);
  97     }
  98     node.appendChild(div);
  99
 100     cap = undefined;
 101     for(var i=0;i<docs2.length;i++) {
 102         var v = docs2[i];
 103         var x = v.path.split("/");
 104         var c = v.title[0].toUpperCase();
 105
 106         if(cap != c) {
 107             var y = document.createElement("h2");
 108             var a = document.createElement("a");
 109             a.className = "anchor";
 110             a.setAttribute("name","section_"+c);
 111             a.innerHTML = cap = c;
 112             y.appendChild(a);
 113             node.appendChild(y);
 114         }
 115
 116         var div = document.createElement("div");
 117         div.className = "result_item";
 118
 119         var n = document.createElement("a");
 120         n.setAttribute("href","../"+v.path+".html");
 121         n.innerHTML = v.title;
 122         div.appendChild(n);
 123         div.appendChild(document.createTextNode(" - "+v.summary+" "));
 124
 125         n = document.createElement("span");
 126         n.className = "soft";
 127         var res = "["+x[0];
 128         if(v.installed=="extension")
 129             res += " +";
 130         else if(v.installed=="missing")
 131             res += " - missing!";
 132         n.innerHTML = res+"]";
 133         div.appendChild(n);
 134         node.appendChild(div);
 135         count++;
 136     }
 137     document.getElementById("total_count").innerHTML = count + " documents";
 138 }
 139 </script>
 140 </head>
 141 <ul id="menubar"></ul>
 142
 143 <body onload="did_load()">
 144 <div class='contents'>
 145 <div class='header'>
 146     <div id='label'>SuperCollider OVERVIEWS</div>
 147     <h1>Documents</h1>
 148     <div id='summary'>Alphabetical index of all documents</div>
 149 </div>
 150 <div id="search_checks">
 151 Filter:
 152 <select id="menu_filter">
 153 <option SELECTED value="all">All documents</option>
 154 <option value="classes">Classes only</option>
 155 <option value="reference">Reference only</option>
 156 <option value="guides">Guides only</option>
 157 <option value="tutorials">Tutorials only</option>
 158 <option value="overviews">Overviews only</option>
 159 <option value="other">Other only</option>
 160 </select>
 161 <input type="checkbox" id="check_extensions" checked="true">Include extensions</input>
 162 </div>
 163 <div id="total_count"></div>
 164 <div id='doclist'></div>
 165 </div>
 166 </body>
 167 </html>
 168