aboutsummaryrefslogtreecommitdiff
path: root/docs/htmldoc/libgraph.html
diff options
context:
space:
mode:
Diffstat (limited to 'docs/htmldoc/libgraph.html')
-rw-r--r--docs/htmldoc/libgraph.html245
1 files changed, 245 insertions, 0 deletions
diff --git a/docs/htmldoc/libgraph.html b/docs/htmldoc/libgraph.html
new file mode 100644
index 0000000..dbcda1f
--- /dev/null
+++ b/docs/htmldoc/libgraph.html
@@ -0,0 +1,245 @@
+<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>
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:03:02 +0000