aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/libgraph.html
diff options
context:
space:
mode:
authorCyril Cohen2019-10-16 11:26:43 +0200
committerCyril Cohen2019-10-16 11:26:43 +0200
commit6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch)
tree1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/htmldoc/libgraph.html
parentdd82aaeae7e9478efc178ce8430986649555b032 (diff)
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/htmldoc/libgraph.html')
-rw-r--r--docs/htmldoc/libgraph.html245
1 files changed, 0 insertions, 245 deletions
diff --git a/docs/htmldoc/libgraph.html b/docs/htmldoc/libgraph.html
deleted file mode 100644
index dbcda1f..0000000
--- a/docs/htmldoc/libgraph.html
+++ /dev/null
@@ -1,245 +0,0 @@
-<html>
-<head>
-<style>
-#cy {
- width: 100%;
- height: -moz-calc(100% - 2em);
- height: -webkit-calc(100% - 2em);
- height: -o-calc(100% - 2em);
- height: 95%;
- display: block;
-}
-
-.button {
- -moz-box-shadow:inset 0px 1px 0px 0px #ffffff;
- -webkit-box-shadow:inset 0px 1px 0px 0px #ffffff;
- box-shadow:inset 0px 1px 0px 0px #ffffff;
- background:-webkit-gradient(linear, left top, left bottom, color-stop(0.05, #f9f9f9), color-stop(1, #e9e9e9));
- background:-moz-linear-gradient(top, #f9f9f9 5%, #e9e9e9 100%);
- background:-webkit-linear-gradient(top, #f9f9f9 5%, #e9e9e9 100%);
- background:-o-linear-gradient(top, #f9f9f9 5%, #e9e9e9 100%);
- background:-ms-linear-gradient(top, #f9f9f9 5%, #e9e9e9 100%);
- background:linear-gradient(to bottom, #f9f9f9 5%, #e9e9e9 100%);
- filter:progid:DXImageTransform.Microsoft.gradient(startColorstr='#f9f9f9', endColorstr='#e9e9e9',GradientType=0);
- background-color:#f9f9f9;
- -moz-border-radius:6px;
- -webkit-border-radius:6px;
- border-radius:6px;
- border:1px solid #dcdcdc;
- display:inline-block;
- cursor:pointer;
- color:#666666;
- font-family:Arial;
- font-size:15px;
- font-weight:bold;
- padding:6px 24px;
- text-decoration:none;
- text-shadow:0px 1px 0px #ffffff;
-}
-.button:hover {
- background:-webkit-gradient(linear, left top, left bottom, color-stop(0.05, #e9e9e9), color-stop(1, #f9f9f9));
- background:-moz-linear-gradient(top, #e9e9e9 5%, #f9f9f9 100%);
- background:-webkit-linear-gradient(top, #e9e9e9 5%, #f9f9f9 100%);
- background:-o-linear-gradient(top, #e9e9e9 5%, #f9f9f9 100%);
- background:-ms-linear-gradient(top, #e9e9e9 5%, #f9f9f9 100%);
- background:linear-gradient(to bottom, #e9e9e9 5%, #f9f9f9 100%);
- filter:progid:DXImageTransform.Microsoft.gradient(startColorstr='#e9e9e9', endColorstr='#f9f9f9',GradientType=0);
- background-color:#e9e9e9;
-}
-.button:active {
- position:relative;
- top:1px;
-}
-.button-bar {
- margin-left:auto;
- width: auto;
- position: absolute;
- right: 10px;
-}
-.zoom-in:before { font-size:12pt; content: "+" }
-.zoom-out:before { font-size:12pt; content: "-" }
-.zoom-expand:before { font-size:12pt; content: "fit" }
-</style>
-<link href="js/jquery.qtip.min.css" rel="stylesheet" type="text/css" />
-<link href="js/cytoscape.js-panzoom.css" rel="stylesheet" type="text/css" />
-
-<script src="js/jquery-2.0.3.min.js"></script>
-<script src="js/cytoscape.min.js"></script>
-<script src="js/dagre.min.js"></script>
-<script src="js/cytoscape-dagre.js"></script>
-<script src="js/jquery.qtip.min.js"></script>
-<script src="js/cytoscape-qtip.js"></script>
-<script src="js/cytoscape-panzoom.js"></script>
-
-<script src="depend.js"></script>
-
-<script type="text/javascript">
-$(document).ready(function(){
- var cy = window.cy = cytoscape({
- container: document.getElementById('cy'), // container to render in
- elements: depends,
- style: [
- { selector: '.hidden',
- style: {
- 'display': 'none',
- }},
- { selector: "node",
- style: {
- 'width': 'mapData(score, 0, 0.006769776522008331, 20, 60)',
- 'height': 'mapData(score, 0, 0.006769776522008331, 20, 60)',
- 'content':'data(name)',
- 'font-size':'18pt',
- 'font-weight':'bold',
- 'text-valign':'center',
- 'text-halign':'center',
- 'text-outline-color': 'white',
- 'border-color': function(e) {
- if (e.data('released') === 'yes') {return 'green'}
- else {return '#ccc'}
- },
- 'border-width': '2px',
- 'border-style': 'dashed',
- 'background-color': 'white',
- 'text-outline-width':'1px',
- 'color':'#555',
- 'overlay-padding':'6px',
- 'z-index':'10',
- }},
- { selector: '$node > node',
- style: {
- 'background-color': 'rgba(255,255,255,0.5)',
- 'border-style' : 'dotted',
- 'border-width' : '1',
- 'border-color' : 'blue',
- 'padding' : '1em',
- 'label': 'data(name)',
- 'text-valign':'top',
- 'text-halign':'center',
- 'z-index': 99,
- }},
- { selector: 'edge',
- style: {
- 'width': 3,
- 'line-color': '#ccc',
- 'target-arrow-color': '#ccc',
- 'target-arrow-shape': 'triangle',
- }},
- { selector: '.red',
- style: {
- 'line-color': 'red',
- 'target-arrow-color': 'red',
- 'target-arrow-shape': 'triangle',
- 'z-index': 100,
- }},
- ],
- ready: function(){ window.cy = this; },
- layout: {
- name: 'dagre',
- fit: false,
- edgeSep: 10,
- padding: 5,
- animate: false,
- },
- textureOnViewport: true,
- }); // end: var cy = cytoscape(...
-
- cy.on('tap', 'node', function(evt){
- var node = evt.cyTarget;
- var g = node.data('name');
- node.connectedEdges().forEach(function(e){ e.toggleClass('red') });
- if (g == '+') { collapse_this('#' + node.parent().id()); }
- });
-
- cy.nodes().forEach(function(n){
- var g = n.data('name');
-
- if (g == '+') {
- n.addClass('hidden');
- n.relativePosition({ x: 0, y:0 });
- };
- if (g == '-') {
- var x = n.relativePosition('x');
- var y = n.relativePosition('y');
- n.relativePosition({ x: -x, y: -y });
- };
-
- if (n.isChild() && g != '+' && g !='-') {
- n.qtip({
- content: [
- { name: 'View coqdoc',
- url: 'mathcomp.' + n.parent().data('name') + '.' + g + '.html'
- },
- ].map(function( link ){
- return '<a target="_blank" href="' + link.url + '">' +
- link.name + '</a>';
- }).join('<br />\n'),
- position: { my: 'top center', at: 'bottom center' },
- style: { classes: 'qtip-bootstrap', tip: { width: 16, height: 8 } },
- });
- } else if (n.isParent()) {
- n.qtip({
- content: [
- { name: 'Collapse',
- url: n.id(),
- },
- ].map(function( link ){
- return '<a href="#" onclick="collapse_this(\'#' + link.url +
- '\');">' + link.name + '</a>';
- }).join('<br />\n'),
- position: { my: 'top center', at: 'bottom center' },
- style: { classes: 'qtip-bootstrap', tip: { width: 16, height: 8 } },
- });
-
- }
- });
-
- cy.center();
-
- cy.panzoom({
- // icon class names
- sliderHandleIcon: 'zoom-slide',
- zoomInIcon: 'zoom-in',
- zoomOutIcon: 'zoom-out',
- resetIcon: 'zoom-expand'
-});
-});
-
-
-function collapse_this(id) {
- cy.$(id).children().forEach(function(e) {
- e.toggleClass('hidden');
- if (e.data('name') == '+' && !e.hasClass('hidden')) {
- e.relativePosition({ x: 0, y:0 });
- }
- });
-}
-
-function collapse() {
- cy.nodes().forEach(function(n){
- if (n.isParent()) { collapse_this('#' + n.id()) }
- });
- cy.layout();
- cy.fit();
- cy.center();
- cy.reset();
-}
-
-function no_red() {
- cy.edges().forEach(function(e) { e.removeClass('red'); });
-}
-</script>
-</head>
-<body>
- <div id="cy">
- </div>
- <div>
- Nodes and clusters can be dragged around and clicked.
- When a node/cluster is clicked its links are highlighted
- and a contextual menu pops up. Clusters can be collapsed.
- </div>
- <div class="button-bar">
- <div class="button" onclick="collapse()">collapse all</div>
- <div class="button" onclick="no_red()">clear red edges</div>
- </div>
-</body>
-</html>