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 = [];
  42     for(var k in docmap) {
  43         if(docmap.hasOwnProperty(k))
  44             docs.push(docmap[k]);
  45     }
  46     docs = docs.sort(function(a,b) {
  47         a = a.title.toUpperCase();
  48         b = b.title.toUpperCase();
  49         if(a<b) return -1;
  50         else
  51         if(a>b) return +1;
  52         else
  53         return 0;
  54     });
  55
  56     var onChange = function() {
  57         showdocs();
  58     };
  59
  60     check_extensions = document.getElementById("check_extensions");
  61     check_extensions.onchange = onChange;
  62     filter = document.getElementById("menu_filter");
  63     filter.onchange = onChange;
  64
  65     showdocs();
  66 }
  67
  68 function showdocs() {
  69     while(node.hasChildNodes())
  70         node.removeChild(node.lastChild);
  71
  72     var count = 0;
  73     var cap = undefined;
  74     var div = document.createElement("p");
  75     var docs2 = [];
  76     div.className = "jump";
  77     div.innerHTML = "Jump to: ";
  78
  79     for(var i=0;i<docs.length;i++) {
  80         var v = docs[i];
  81         var x = v.title[0].toUpperCase();
  82
  83         if(v.installed=="extension" && !check_extensions.checked)
  84             continue;
  85
  86         if(filter.value != "all" && v.path.split("/")[0].toLowerCase() != filter.value)
  87             continue;
  88
  89         if(/Undocumented classes/.test(v.categories))
  90             continue;
  91
  92         if(cap != x) {
  93             cap = x;
  94             var a = document.createElement("a");
  95             a.setAttribute("href","#section_"+cap);
  96             a.innerHTML=cap;
  97             div.appendChild(a);
  98             div.appendChild(document.createTextNode(" "));
  99         }
 100
 101         docs2.push(v);
 102     }
 103     node.appendChild(div);
 104
 105     cap = undefined;
 106     for(var i=0;i<docs2.length;i++) {
 107         var v = docs2[i];
 108         var x = v.path.split("/");
 109         var c = v.title[0].toUpperCase();
 110
 111         if(cap != c) {
 112             var y = document.createElement("h2");
 113             var a = document.createElement("a");
 114             a.className = "anchor";
 115             a.setAttribute("name","section_"+c);
 116             a.innerHTML = cap = c;
 117             y.appendChild(a);
 118             node.appendChild(y);
 119         }
 120
 121         var div = document.createElement("div");
 122         div.className = "result_item";
 123
 124         var n = document.createElement("a");
 125         n.setAttribute("href","../"+v.path+".html");
 126         n.innerHTML = v.title;
 127         div.appendChild(n);
 128         div.appendChild(document.createTextNode(" - "+v.summary+" "));
 129
 130         n = document.createElement("span");
 131         n.className = "soft";
 132         var res = "["+x[0];
 133         if(v.installed=="extension")
 134             res += " +";
 135         else if(v.installed=="missing")
 136             res += " - missing!";
 137         n.innerHTML = res+"]";
 138         div.appendChild(n);
 139         node.appendChild(div);
 140         count++;
 141     }
 142     document.getElementById("total_count").innerHTML = count + " documents";
 143 }
 144 </script>
 145 </head>
 146 <ul id="menubar"></ul>
 147
 148 <body onload="did_load()">
 149 <div class='contents'>
 150 <div class='header'>
 151     <div id='label'>SuperCollider OVERVIEWS</div>
 152     <h1>Documents</h1>
 153     <div id='summary'>Alphabetical index of all documents</div>
 154 </div>
 155 <div id="search_checks">
 156 Filter:
 157 <select id="menu_filter">
 158 <option SELECTED value="all">All documents</option>
 159 <option value="classes">Classes only</option>
 160 <option value="reference">Reference only</option>
 161 <option value="guides">Guides only</option>
 162 <option value="tutorials">Tutorials only</option>
 163 <option value="overviews">Overviews only</option>
 164 <option value="other">Other only</option>
 165 </select>
 166 <input type="checkbox" id="check_extensions" checked="true">Include extensions</input>
 167 </div>
 168 <div id="total_count"></div>
 169 <div id='doclist'></div>
 170 </div>
 171 </body>
 172 </html>
 173