Haskell Artificial Neural Networking library
Vous ne pouvez pas sélectionner plus de 25 sujets Les noms de sujets doivent commencer par une lettre ou un nombre, peuvent contenir des tirets ('-') et peuvent comporter jusqu'à 35 caractères.

345 lignes
8.0KB

  1. // Haddock JavaScript utilities
  2. var rspace = /\s\s+/g,
  3. rtrim = /^\s+|\s+$/g;
  4. function spaced(s) { return (" " + s + " ").replace(rspace, " "); }
  5. function trim(s) { return s.replace(rtrim, ""); }
  6. function hasClass(elem, value) {
  7. var className = spaced(elem.className || "");
  8. return className.indexOf( " " + value + " " ) >= 0;
  9. }
  10. function addClass(elem, value) {
  11. var className = spaced(elem.className || "");
  12. if ( className.indexOf( " " + value + " " ) < 0 ) {
  13. elem.className = trim(className + " " + value);
  14. }
  15. }
  16. function removeClass(elem, value) {
  17. var className = spaced(elem.className || "");
  18. className = className.replace(" " + value + " ", " ");
  19. elem.className = trim(className);
  20. }
  21. function toggleClass(elem, valueOn, valueOff, bool) {
  22. if (bool == null) { bool = ! hasClass(elem, valueOn); }
  23. if (bool) {
  24. removeClass(elem, valueOff);
  25. addClass(elem, valueOn);
  26. }
  27. else {
  28. removeClass(elem, valueOn);
  29. addClass(elem, valueOff);
  30. }
  31. return bool;
  32. }
  33. function makeClassToggle(valueOn, valueOff)
  34. {
  35. return function(elem, bool) {
  36. return toggleClass(elem, valueOn, valueOff, bool);
  37. }
  38. }
  39. toggleShow = makeClassToggle("show", "hide");
  40. toggleCollapser = makeClassToggle("collapser", "expander");
  41. function toggleSection(id)
  42. {
  43. var b = toggleShow(document.getElementById("section." + id));
  44. toggleCollapser(document.getElementById("control." + id), b);
  45. rememberCollapsed(id, b);
  46. return b;
  47. }
  48. var collapsed = {};
  49. function rememberCollapsed(id, b)
  50. {
  51. if(b)
  52. delete collapsed[id]
  53. else
  54. collapsed[id] = null;
  55. var sections = [];
  56. for(var i in collapsed)
  57. {
  58. if(collapsed.hasOwnProperty(i))
  59. sections.push(i);
  60. }
  61. // cookie specific to this page; don't use setCookie which sets path=/
  62. document.cookie = "collapsed=" + escape(sections.join('+'));
  63. }
  64. function restoreCollapsed()
  65. {
  66. var cookie = getCookie("collapsed");
  67. if(!cookie)
  68. return;
  69. var ids = cookie.split('+');
  70. for(var i in ids)
  71. {
  72. if(document.getElementById("section." + ids[i]))
  73. toggleSection(ids[i]);
  74. }
  75. }
  76. function setCookie(name, value) {
  77. document.cookie = name + "=" + escape(value) + ";path=/;";
  78. }
  79. function clearCookie(name) {
  80. document.cookie = name + "=;path=/;expires=Thu, 01-Jan-1970 00:00:01 GMT;";
  81. }
  82. function getCookie(name) {
  83. var nameEQ = name + "=";
  84. var ca = document.cookie.split(';');
  85. for(var i=0;i < ca.length;i++) {
  86. var c = ca[i];
  87. while (c.charAt(0)==' ') c = c.substring(1,c.length);
  88. if (c.indexOf(nameEQ) == 0) {
  89. return unescape(c.substring(nameEQ.length,c.length));
  90. }
  91. }
  92. return null;
  93. }
  94. var max_results = 75; // 50 is not enough to search for map in the base libraries
  95. var shown_range = null;
  96. var last_search = null;
  97. function quick_search()
  98. {
  99. perform_search(false);
  100. }
  101. function full_search()
  102. {
  103. perform_search(true);
  104. }
  105. function perform_search(full)
  106. {
  107. var text = document.getElementById("searchbox").value.toLowerCase();
  108. if (text == last_search && !full) return;
  109. last_search = text;
  110. var table = document.getElementById("indexlist");
  111. var status = document.getElementById("searchmsg");
  112. var children = table.firstChild.childNodes;
  113. // first figure out the first node with the prefix
  114. var first = bisect(-1);
  115. var last = (first == -1 ? -1 : bisect(1));
  116. if (first == -1)
  117. {
  118. table.className = "";
  119. status.innerHTML = "No results found, displaying all";
  120. }
  121. else if (first == 0 && last == children.length - 1)
  122. {
  123. table.className = "";
  124. status.innerHTML = "";
  125. }
  126. else if (last - first >= max_results && !full)
  127. {
  128. table.className = "";
  129. status.innerHTML = "More than " + max_results + ", press Search to display";
  130. }
  131. else
  132. {
  133. // decide what you need to clear/show
  134. if (shown_range)
  135. setclass(shown_range[0], shown_range[1], "indexrow");
  136. setclass(first, last, "indexshow");
  137. shown_range = [first, last];
  138. table.className = "indexsearch";
  139. status.innerHTML = "";
  140. }
  141. function setclass(first, last, status)
  142. {
  143. for (var i = first; i <= last; i++)
  144. {
  145. children[i].className = status;
  146. }
  147. }
  148. // do a binary search, treating 0 as ...
  149. // return either -1 (no 0's found) or location of most far match
  150. function bisect(dir)
  151. {
  152. var first = 0, finish = children.length - 1;
  153. var mid, success = false;
  154. while (finish - first > 3)
  155. {
  156. mid = Math.floor((finish + first) / 2);
  157. var i = checkitem(mid);
  158. if (i == 0) i = dir;
  159. if (i == -1)
  160. finish = mid;
  161. else
  162. first = mid;
  163. }
  164. var a = (dir == 1 ? first : finish);
  165. var b = (dir == 1 ? finish : first);
  166. for (var i = b; i != a - dir; i -= dir)
  167. {
  168. if (checkitem(i) == 0) return i;
  169. }
  170. return -1;
  171. }
  172. // from an index, decide what the result is
  173. // 0 = match, -1 is lower, 1 is higher
  174. function checkitem(i)
  175. {
  176. var s = getitem(i).toLowerCase().substr(0, text.length);
  177. if (s == text) return 0;
  178. else return (s > text ? -1 : 1);
  179. }
  180. // from an index, get its string
  181. // this abstracts over alternates
  182. function getitem(i)
  183. {
  184. for ( ; i >= 0; i--)
  185. {
  186. var s = children[i].firstChild.firstChild.data;
  187. if (s.indexOf(' ') == -1)
  188. return s;
  189. }
  190. return ""; // should never be reached
  191. }
  192. }
  193. function setSynopsis(filename) {
  194. if (parent.window.synopsis) {
  195. if (parent.window.synopsis.location.replace) {
  196. // In Firefox this avoids adding the change to the history.
  197. parent.window.synopsis.location.replace(filename);
  198. } else {
  199. parent.window.synopsis.location = filename;
  200. }
  201. }
  202. }
  203. function addMenuItem(html) {
  204. var menu = document.getElementById("page-menu");
  205. if (menu) {
  206. var btn = menu.firstChild.cloneNode(false);
  207. btn.innerHTML = html;
  208. menu.appendChild(btn);
  209. }
  210. }
  211. function adjustForFrames() {
  212. var bodyCls;
  213. if (parent.location.href == window.location.href) {
  214. // not in frames, so add Frames button
  215. addMenuItem("<a href='#' onclick='reframe();return true;'>Frames</a>");
  216. bodyCls = "no-frame";
  217. }
  218. else {
  219. bodyCls = "in-frame";
  220. }
  221. addClass(document.body, bodyCls);
  222. }
  223. function reframe() {
  224. setCookie("haddock-reframe", document.URL);
  225. window.location = "frames.html";
  226. }
  227. function postReframe() {
  228. var s = getCookie("haddock-reframe");
  229. if (s) {
  230. parent.window.main.location = s;
  231. clearCookie("haddock-reframe");
  232. }
  233. }
  234. function styles() {
  235. var i, a, es = document.getElementsByTagName("link"), rs = [];
  236. for (i = 0; a = es[i]; i++) {
  237. if(a.rel.indexOf("style") != -1 && a.title) {
  238. rs.push(a);
  239. }
  240. }
  241. return rs;
  242. }
  243. function addStyleMenu() {
  244. var as = styles();
  245. var i, a, btns = "";
  246. for(i=0; a = as[i]; i++) {
  247. btns += "<li><a href='#' onclick=\"setActiveStyleSheet('"
  248. + a.title + "'); return false;\">"
  249. + a.title + "</a></li>"
  250. }
  251. if (as.length > 1) {
  252. var h = "<div id='style-menu-holder'>"
  253. + "<a href='#' onclick='styleMenu(); return false;'>Style &#9662;</a>"
  254. + "<ul id='style-menu' class='hide'>" + btns + "</ul>"
  255. + "</div>";
  256. addMenuItem(h);
  257. }
  258. }
  259. function setActiveStyleSheet(title) {
  260. var as = styles();
  261. var i, a, found;
  262. for(i=0; a = as[i]; i++) {
  263. a.disabled = true;
  264. // need to do this always, some browsers are edge triggered
  265. if(a.title == title) {
  266. found = a;
  267. }
  268. }
  269. if (found) {
  270. found.disabled = false;
  271. setCookie("haddock-style", title);
  272. }
  273. else {
  274. as[0].disabled = false;
  275. clearCookie("haddock-style");
  276. }
  277. styleMenu(false);
  278. }
  279. function resetStyle() {
  280. var s = getCookie("haddock-style");
  281. if (s) setActiveStyleSheet(s);
  282. }
  283. function styleMenu(show) {
  284. var m = document.getElementById('style-menu');
  285. if (m) toggleShow(m, show);
  286. }
  287. function pageLoad() {
  288. addStyleMenu();
  289. adjustForFrames();
  290. resetStyle();
  291. restoreCollapsed();
  292. }