diff --git a/org.rodinp.handbook.feature/.project b/org.rodinp.handbook.feature/.project new file mode 100644 index 0000000000000000000000000000000000000000..67f84865435c1227c2ecb73d70f73d04b7bf7ea7 --- /dev/null +++ b/org.rodinp.handbook.feature/.project @@ -0,0 +1,17 @@ +<?xml version="1.0" encoding="UTF-8"?> +<projectDescription> + <name>org.rodinp.handbook.feature</name> + <comment></comment> + <projects> + </projects> + <buildSpec> + <buildCommand> + <name>org.eclipse.pde.FeatureBuilder</name> + <arguments> + </arguments> + </buildCommand> + </buildSpec> + <natures> + <nature>org.eclipse.pde.FeatureNature</nature> + </natures> +</projectDescription> diff --git a/org.rodinp.handbook.feature/README.txt b/org.rodinp.handbook.feature/README.txt new file mode 100644 index 0000000000000000000000000000000000000000..66666a3cba30c98b47517dd75a25c69e9e702f43 --- /dev/null +++ b/org.rodinp.handbook.feature/README.txt @@ -0,0 +1,22 @@ +OVERVIEW +======== + +This project holds the Rodin Handbook and the scripts to publish it. + +This feature has two purposes: + +1. A container for the content and scripts for the Rodin Handbook + +2. A feature that includes the documentation into Eclipse. + +HOW TO BUILD +============ +1. Install Plastex on your system (http://plastex.sourceforge.net/) +2. Run the build.xml ant file + +The resulting HTML and Eclipse Plugin with Eclipse help will be in the build folder. + +CONTACT +======= +Michael Jastram (michael@jastram.de) + diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html new file mode 100644 index 0000000000000000000000000000000000000000..c6484163e63721ed083d5184d8974e3644aece43 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/default-layout.html @@ -0,0 +1,53 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html tal:define="links self/links" xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> +<head> +<meta name="generator" content="plasTeX" /> +<meta http-equiv="content-type" + tal:attributes="content string:text/html;; charset=${config/files/output-encoding}" /> +<title tal:condition="python:path('self/level') > -10" tal:content="stripped string:${links/document/title}: ${self/title}">Morbi metus pede, imperdiet vitae</title> +<title tal:condition="python:path('self/level') <= -10" tal:content="stripped self/title">Morbi metus pede, imperdiet vitae</title> +<link tal:condition="links/next" rel="next" tal:attributes="href links/next/url; title links/next/title/textContent" /> +<link tal:condition="links/prev" rel="prev" tal:attributes="href links/prev/url; title links/prev/title/textContent" /> +<link tal:condition="links/up" rel="up" tal:attributes="href links/up/url; title links/up/title/textContent" /> +<link rel="stylesheet" href="styles/styles.css" /> +</head> +<body> + +<div tal:content="self">File contents</div> + +<div tal:condition="self/tableofcontents" tal:attributes="class string:contents ${self/nodeName}-contents"><!--<strong>Subsections</strong>--> +<ul> +<li tal:repeat="section self/tableofcontents"><a href="." tal:attributes="href section/url" tal:content="section/fullTocEntry">Aliquam est. Aliquam fringilla pede</a> + <ul tal:condition="section/tableofcontents"> + <li tal:repeat="subsection section/tableofcontents"><a href="." tal:attributes="href subsection/url" tal:content="subsection/fullTocEntry"></a> + <ul tal:condition="subsection/tableofcontents"> + <li tal:repeat="subsubsection subsection/tableofcontents"><a href="." tal:attributes="href subsubsection/url" tal:content="subsubsection/fullTocEntry"></a> + <ul tal:condition="subsubsection/tableofcontents"> + <li tal:repeat="paragraph subsubsection/tableofcontents"><a href="." tal:attributes="href paragraph/url" tal:content="paragraph/fullTocEntry"></a> + <ul tal:condition="paragraph/tableofcontents"> + <li tal:repeat="subparagraph paragraph/tableofcontents"><a href="." tal:attributes="href subparagraph/url" tal:content="subparagraph/fullTocEntry"></a></li> + </ul> + </li> + </ul> + </li> + </ul> + </li> + </ul> +</li> +<li tal:replace="nothing"><a href=".">Maecenas id purus</a></li> +<li tal:replace="nothing"><a href=".">Duis et eros</a></li> +<li tal:replace="nothing"><a href=".">Duis est</a></li> +</ul> +</div> + +<div id="footnotes" tal:condition="self/footnotes"> +<p><b>Footnotes</b></p> +<ol> +<li tal:repeat="footnote self/footnotes" tal:content="footnote" tal:attributes="id footnote/id">footnote text</li> +</ol> +</div> + +<script language="javascript" src="icons/imgadjust.js" type="text/javascript"></script> + +</body> +</html> diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/blank.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/blank.gif new file mode 100644 index 0000000000000000000000000000000000000000..e5b747fe417ef691e3e6f403cf647d016217bc21 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/blank.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/functionAddEvent.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/functionAddEvent.js new file mode 100644 index 0000000000000000000000000000000000000000..abddd68f8f3f9d7b663cd83c74b5fd0da1aa9cfc --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/functionAddEvent.js @@ -0,0 +1,69 @@ +function addEvent(elm, evType, fn, useCapture) { + if (elm.addEventListener) { + elm.addEventListener(evType, fn, useCapture); + return true; + } + else if (elm.attachEvent) { + var r = elm.attachEvent('on' + evType, fn); + EventCache.add(elm, evType, fn); + return r; + } + else { + elm['on' + evType] = fn; + } +} +function getEventSrc(e) { + if (!e) e = window.event; + + if (e.originalTarget) + return e.originalTarget; + else if (e.srcElement) + return e.srcElement; +} +function addLoadEvent(func) { +var oldonload = window.onload; + if (typeof window.onload != 'function') { + window.onload = func; + } else { + window.onload = + function() { + oldonload(); + func(); + } + } +} +var EventCache = function(){ + var listEvents = []; + return { + listEvents : listEvents, + + add : function(node, sEventName, fHandler, bCapture){ + listEvents.push(arguments); + }, + + flush : function(){ + var i, item; + for(i = listEvents.length - 1; i >= 0; i = i - 1){ + item = listEvents[i]; + + if(item[0].removeEventListener){ + item[0].removeEventListener(item[1], item[2], item[3]); + }; + + /* From this point on we need the event names to be prefixed with 'on" */ + if(item[1].substring(0, 2) != "on"){ + item[1] = "on" + item[1]; + }; + + if(item[0].detachEvent){ + item[0].detachEvent(item[1], item[2]); + }; + + item[0][item[1]] = null; + }; + } + }; +}(); + + +addEvent(window,'unload',EventCache.flush, false); \ No newline at end of file diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-bottom.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-bottom.gif new file mode 100644 index 0000000000000000000000000000000000000000..deb99a4ea8f5fd37d1d8f28b93fa93a4c299fe19 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-bottom.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-down.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-down.gif new file mode 100644 index 0000000000000000000000000000000000000000..af655dfca801341753a2e0d47ac7a9808835e282 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-down.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-first.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-first.gif new file mode 100644 index 0000000000000000000000000000000000000000..87faba2dd2d041b8a69f6ab81a1cf023ca3b6c36 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-first.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-home.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-home.gif new file mode 100644 index 0000000000000000000000000000000000000000..a77c59ff89fa2e941651cd94dcf69c9af1cefc6d Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-home.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-jump.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-jump.gif new file mode 100644 index 0000000000000000000000000000000000000000..b132d782a168547812a5a686ce1fd0248ecfd094 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-jump.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-last.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-last.gif new file mode 100644 index 0000000000000000000000000000000000000000..f25ca9c798520dd38e0279980936d056c6810565 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-last.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-next.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-next.gif new file mode 100644 index 0000000000000000000000000000000000000000..2ed252f656ebb957b72362dff2c1cafed1915372 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-next.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-previous.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-previous.gif new file mode 100644 index 0000000000000000000000000000000000000000..747904dc8cf3b8c16a5e57ce2de082d684e26ccf Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-previous.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-top.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-top.gif new file mode 100644 index 0000000000000000000000000000000000000000..a96e14c5786dccd8d4ff8fbe1aaa368b67b7224a Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-top.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-up.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-up.gif new file mode 100644 index 0000000000000000000000000000000000000000..f812f11a5f57fba2d72cf8de135bbb4a8e04e9ba Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/go-up.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/gohome.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/gohome.gif new file mode 100644 index 0000000000000000000000000000000000000000..a77c59ff89fa2e941651cd94dcf69c9af1cefc6d Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/gohome.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/imgadjust.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/imgadjust.js new file mode 100644 index 0000000000000000000000000000000000000000..2fce3d69ea2ffd48333976623a89a35fd09e9453 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/imgadjust.js @@ -0,0 +1,37 @@ +// +// This code fixes up the images so that MSIE doesn't truncate images +// within tables. It also adjusts the line height so that it's prettier. +// +var images = document.getElementsByTagName('img') +var adjusted = new Array(); +for ( var i = 0; i < images.length; i++ ) +{ + image = images[i]; + if ( parseInt(image.style.marginBottom) < -8 ) + { + if ( !image.height ) + continue; + + // Make sure that images in IE in tables don't get truncated + ieimgfix = document.createElement('img'); + ieimgfix.src = 'iicons/blank.gif'; + ieimgfix.style.height = image.style.height; + ieimgfix.style.width = '0px'; + + // Adjust line height to be prettier + adjust = document.createElement('span'); + adjust.style.lineHeight = (parseInt(image.style.height) - 8) + 'px'; + adjust.style.visibility = 'hidden'; + adjust.nodeValue = '&8205;'; + + // Store away the nodes for use later + adjusted[image.parentNode] = new Array(image.parentNode, image, + ieimgfix, adjust); + } +} +// Insert the adjuster nodes +for ( var n in adjusted ) +{ + adjusted[n][0].insertBefore(adjusted[n][2], adjusted[n][1]); + adjusted[n][0].insertBefore(adjusted[n][3], adjusted[n][1]); +} diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/index.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/index.gif new file mode 100644 index 0000000000000000000000000000000000000000..50838f6f1ec4fe7bf0f3b4d7e3564e28c15ca0e1 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/index.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/loading.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/loading.gif new file mode 100644 index 0000000000000000000000000000000000000000..fbe57be3c2cd761a999fcf91698963b723916e28 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/loading.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/missing.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/missing.gif new file mode 100644 index 0000000000000000000000000000000000000000..7696c539faced25decdde7c9ad83d1541adc920e Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/missing.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/modules.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/modules.gif new file mode 100644 index 0000000000000000000000000000000000000000..4951bb87588f0fe887ca49cdc70cf2897340cfda Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/modules.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/overlay.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/overlay.gif new file mode 100644 index 0000000000000000000000000000000000000000..62c546bd7323aaf8c234c89ddefdf9f4c1fa3642 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/overlay.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/toolTipLib.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/toolTipLib.js new file mode 100644 index 0000000000000000000000000000000000000000..d76d4e71c67d58b59bc0abb8416bcd7dd1f64150 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/icons/toolTipLib.js @@ -0,0 +1,107 @@ +var toolTipLib = { + xCord : 0, + yCord : 0, + obj : null, + tipElements : ['a','abbr','acronym'], + attachToolTipBehavior: function() { + if ( !document.getElementById || + !document.createElement || + !document.getElementsByTagName ) { + return; + } + var i,j; + addEvent(document,'mousemove',toolTipLib.updateXY,false); + if ( document.captureEvents ) { + document.captureEvents(Event.MOUSEMOVE); + } + for ( i=0;i<toolTipLib.tipElements.length;i++ ) { + var current = document.getElementsByTagName(toolTipLib.tipElements[i]); + for ( j=0;j<current.length;j++ ) { + addEvent(current[j],'mouseover',toolTipLib.tipOver,false); + addEvent(current[j],'mouseout',toolTipLib.tipOut,false); + current[j].setAttribute('tip',current[j].title); + current[j].removeAttribute('title'); + } + } + }, + updateXY : function(e) { + if ( document.captureEvents ) { + toolTipLib.xCord = e.pageX; + toolTipLib.yCord = e.pageY; + } else if ( window.event.clientX ) { + toolTipLib.xCord = window.event.clientX+document.documentElement.scrollLeft; + toolTipLib.yCord = window.event.clientY+document.documentElement.scrollTop; + } + }, + tipOut: function(e) { + if ( window.tID ) { + clearTimeout(tID); + } + if ( window.opacityID ) { + clearTimeout(opacityID); + } + var l = getEventSrc(e); + var div = document.getElementById('toolTip'); + if ( div ) { + div.parentNode.removeChild(div); + } + }, + checkNode : function(obj) { + var trueObj = obj; + if ( trueObj.nodeName.toLowerCase() == 'a' || trueObj.nodeName.toLowerCase() == 'acronym' || trueObj.nodeName.toLowerCase() == 'abbr' ) { + return trueObj; + } else { + return trueObj.parentNode; + } + }, + tipOver : function(e) { + toolTipLib.obj = getEventSrc(e); + tID = setTimeout("toolTipLib.tipShow()",500) + }, + tipShow : function() { + var newDiv = document.createElement('div'); + var scrX = Number(toolTipLib.xCord); + var scrY = Number(toolTipLib.yCord); + var tp = parseInt(scrY+15); + var lt = parseInt(scrX+10); + var anch = toolTipLib.checkNode(toolTipLib.obj); + var addy = ''; + var access = ''; + if ( anch.nodeName.toLowerCase() == 'a' ) { + addy = (anch.href.length > 25 ? anch.href.toString().substring(0,25)+"..." : anch.href); + var access = ( anch.accessKey ? ' <span>['+anch.accessKey+']</span> ' : '' ); + } else { + addy = anch.firstChild.nodeValue; + } + newDiv.id = 'toolTip'; + document.getElementsByTagName('body')[0].appendChild(newDiv); + newDiv.style.opacity = '.1'; + newDiv.innerHTML = "<p>"+anch.getAttribute('tip')+"<em>"+access+addy+"</em></p>"; + if ( parseInt(document.documentElement.clientWidth+document.documentElement.scrollLeft) < parseInt(newDiv.offsetWidth+lt) ) { + newDiv.style.left = parseInt(lt-(newDiv.offsetWidth+10))+'px'; + } else { + newDiv.style.left = lt+'px'; + } + if ( parseInt(document.documentElement.clientHeight+document.documentElement.scrollTop) < parseInt(newDiv.offsetHeight+tp) ) { + newDiv.style.top = parseInt(tp-(newDiv.offsetHeight+10))+'px'; + } else { + newDiv.style.top = tp+'px'; + } + toolTipLib.tipFade('toolTip',10); + }, + tipFade: function(div,opac) { + var obj = document.getElementById(div); + var passed = parseInt(opac); + var newOpac = parseInt(passed+10); + if ( newOpac < 80 ) { + obj.style.opacity = '.'+newOpac; + obj.style.filter = "alpha(opacity:"+newOpac+")"; + opacityID = setTimeout("toolTipLib.tipFade('toolTip','"+newOpac+"')",20); + } + else { + obj.style.opacity = '.80'; + obj.style.filter = "alpha(opacity:80)"; + } + } +}; +addEvent(window,'load',toolTipLib.attachToolTipBehavior,false); \ No newline at end of file diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css new file mode 100644 index 0000000000000000000000000000000000000000..ca21b8ed4d31938b78eec6a06ef0f3381058edc1 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-eclipse/styles/styles.css @@ -0,0 +1,327 @@ + +pre { + color: #004000; + width: 100%; + font-size: 90%; + background-color: #f0f0f0; + padding-top: 5px; + padding-bottom: 5px; + border: 1px #aaffaa solid; + font-family: Monaco, "Courier New", Courier, fixed; + padding-left: 4ex; +} + +.breadcrumbs { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; + font-size: small; + font-style: italic; +} + +h1, h2, h3, h4, h5, h6 { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; +} + +.navigation { clear:both } +.navigation td { background-color: #ffffff; + color: #000000; + font-weight: bold; + font-family: avantgarde, sans-serif; + font-size: 110% } + +.navigation img { border-width: 0px } +.navtitle { width: 100% } + +.contents ul { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; + list-style-type: none; + font-weight: bold; +} +.contents ul ul { + font-size: small; + font-weight: normal; +} + +hr {color: black} + +.minitoc { + border-top: 1px solid black; + border-bottom: 1px solid block; + margin-bottom: 1em; +} + +.minitoc li { + list-style-type: none; +} + +/*************/ +/* Footnotes */ +/*************/ +/* +a.footnote .footnotemark { + color: #ff8000; +} +a.footnote:hover .footnotemark { + cursor: help; +} +a.footnote .footnotetext { + display: none; +} +a.footnote:hover .footnotetext { + display: block; + position: absolute; + bottom: 0em; + left: 0em; + background-color: #F8F8CB; + color: #000; + text-align: left; + border: 7px #ff8000 solid; + padding: 10px; + margin: 0px; + z-index: 20; +} +*/ +a.footnote { + text-decoration: none; +} +#footnotes { + padding: 1em; + border-top: 1px solid black; + font-size: smaller; +} + +/*******/ +/* TeX */ +/*******/ + +/* Fonts */ +.rm { + font-family: serif; + font-style: normal; + font-weight: normal; +} +.cal { + font-family: serif; + font-style: italic; + font-weight: normal; +} +.it { + font-family: serif; + font-style: italic; + font-weight: normal; +} +.sl { + font-family: serif; + font-style: oblique; + font-weight: normal; +} +.bf { + font-family: serif; + font-style: normal; + font-weight: bold; +} +.tt { + font-family: monospace; + font-style: normal; + font-weight: normal; +} + +/* Text */ +.underbar {text-decoration: underline} + + +/*********/ +/* LaTeX */ +/*********/ + +/* Alignment */ +.center, .centering {text-align: center} +.flushleft, .raggedright {text-align: left} +.flushright, .raggedleft {text-align: right} + +/* Arrays */ +.tabular { border-collapse: collapse } +.tabular td, .tabular th { + vertical-align: top; + text-align: left; + padding-top: 0.3em; + padding-bottom: 0.3em; + padding-left: 0.6em; + padding-right: 0.6em; + empty-cells: show; +} + +/* Boxes */ +.fbox, .framebox { + border: 1px black solid; + padding-top: 1px; + padding-bottom: 1px; + padding-left: 3px; + padding-right: 3px; +} + +/* Font Selection */ +.mdseries, .textmf {font-weight: normal} +.bfseries, .textbf {font-weight: bold} +.rmfamily, .textrm {font-family: serif} +.sffamily, .textsf {font-family: sans-serif} +.ttfamily, .texttt {font-family: monospace} +.upshape, .textup {text-transform: uppercase} +.itshape, .textit {font-style: italic} +.slshape, .textsl {font-style: oblique} +.scshape, .textsc {font-variant: small-caps} + +small.tiny {font-size: x-small} +small.scriptsize {font-size: smaller} +small.footnotesize {font-size: small} +small.small {font-size: small} +.normalsize {font-size: normal} +big.large {font-size: large} +big.xlarge {font-size: x-large} +big.xxlarge {font-size: x-large} +big.huge {font-size: xx-large} +big.xhuge {font-size: xx-large} + +/* Lists */ +/*ul.itemize {}*/ +/*ol.enumerate {}*/ +dl.description dt {font-weight: bold} +table.list { + margin-left: 15px; + margin-top: 1em; + margin-bottom: 1em; +} +table.list td { + padding-right: 5px; +} + +/* Title Page */ +.titlepage {text-align: center} +.titlepage h1 {font-weight: normal} + +/* Math */ +.displaymath, .eqnarray, .equation { + margin-top: 15px; + margin-bottom: 15px; + text-align: center; +} +.eqnnum { + width: 16ex; + text-align: center; +} +.fleqn {width: 2em} + +/* Quotations and Verse */ +.quotation, .quote, .verse { + text-indent: 2em; +} +.quotation p, .quote p, .verse p { + text-indent: 2em; + margin-top: 0px; + margin-bottom: 0px; +} + +/* Rules */ +hr {color: black} + +/* Image offset classes */ +.raise15 {margin-bottom: 10px} +.raise14 {margin-bottom: 10px} +.raise13 {margin-bottom: 10px} +.raise12 {margin-bottom: 10px} +.raise11 {margin-bottom: 10px} +.raise10 {margin-bottom: 10px} +.raise9 {margin-bottom: 9px} +.raise8 {margin-bottom: 8px} +.raise7 {margin-bottom: 7px} +.raise6 {margin-bottom: 6px} +.raise5 {margin-bottom: 5px} +.raise4 {margin-bottom: 4px} +.raise3 {margin-bottom: 3px} +.raise2 {margin-bottom: 2px} +.raise1 {margin-bottom: 1px} +.raise0 {margin-bottom: 0px} +.lower0 {margin-bottom: -0px} +.lower1 {margin-bottom: -1px} +.lower2 {margin-bottom: -2px} +.lower3 {margin-bottom: -3px} +.lower4 {margin-bottom: -4px} +.lower5 {margin-bottom: -5px} +.lower6 {margin-bottom: -6px} +.lower7 {margin-bottom: -7px} +.lower8 {margin-bottom: -8px} +.lower10 {margin-bottom: -10px} +.lower11 {margin-bottom: -11px} +.lower12 {margin-bottom: -12px} +.lower13 {margin-bottom: -13px} +.lower14 {margin-bottom: -14px} +.lower15 {margin-bottom: -15px} +.lower16 {margin-bottom: -16px} +.lower17 {margin-bottom: -17px} +.lower18 {margin-bottom: -18px} +.lower19 {margin-bottom: -19px} +.lower20 {margin-bottom: -20px} +.lower21 {margin-bottom: -21px} +.lower22 {margin-bottom: -22px} +.lower23 {margin-bottom: -23px} +.lower24 {margin-bottom: -24px} +.lower25 {margin-bottom: -25px} +.lower26 {margin-bottom: -26px} +.lower27 {margin-bottom: -27px} +.lower28 {margin-bottom: -28px} +.lower29 {margin-bottom: -29px} +.lower30 {margin-bottom: -20px} +.lower20 {margin-bottom: -20px} + +td p:first-child, th p:first-child { + margin-top: 0px; + margin-bottom: 0px; +} + +td p, th p { + margin-top: 1em; + margin-bottom: 0px; +} + +p { + text-indent: 0em; + margin-top: 0px; + margin-bottom: 1em; +} + +img { + border: none; + vertical-align: baseline; +} + +img.ieimgfix { + width: 0; + visibility: hidden; + vertical-align: top; + display: none; +} + +td img.ieimgfix { + display: inline; +} + +body { + color: #000000; + background-color: #ffffff; +} + +/* Index */ +.theindex li { + list-style-type: none +} + +.changebar { + border-right: 2px solid red; + padding-right: 1em; +} + +.deletebar { + color: red; + font-size: 150%; + padding-left: 0.5ex; + padding-right: 0.5ex; +} diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html new file mode 100644 index 0000000000000000000000000000000000000000..2264cb0b1ab69d73b21304c9b0ad27ea2c04e21c --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/default-layout.html @@ -0,0 +1,114 @@ +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html tal:define="links self/links" xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en"> +<head> +<meta name="generator" content="plasTeX" /> +<meta http-equiv="content-type" + tal:attributes="content string:text/html;; charset=${config/files/output-encoding}" /> +<title tal:condition="python:path('self/level') > -10" tal:content="stripped string:${links/document/title}: ${self/title}">Morbi metus pede, imperdiet vitae</title> +<title tal:condition="python:path('self/level') <= -10" tal:content="stripped self/title">Morbi metus pede, imperdiet vitae</title> +<link tal:condition="links/next" rel="next" tal:attributes="href links/next/url; title links/next/title/textContent" /> +<link tal:condition="links/prev" rel="prev" tal:attributes="href links/prev/url; title links/prev/title/textContent" /> +<link tal:condition="links/up" rel="up" tal:attributes="href links/up/url; title links/up/title/textContent" /> +<link rel="stylesheet" href="styles/styles.css" /> +</head> +<body> + +<table width="100%" border="0"> +<tr><td valign="top" width="135px"> + +<center> +Rodin +User +Manual +</center> + +<br/> + +<div id="navcontainer"> +<ul id="navlist"> +<li><a href="index.html">Documentation Home</a> +<li><a href="http://wiki.event-b.org/">Rodin Wiki</a> +<li><a href="http://sourceforge.net/projects/rodin-b-sharp/">Rodin Download</a> +<li><a href="mailto:michael.jastram@formalmind.com">Contact</a> +</ul> +</div> + +<br/> +<br/> +<center> +<a href="http://www.deploy-project.eu/"><img src="icons/deploy.png" border="0"></a> +</center> + +</td><td valign="top" width="40"> </td><td valign="top" > + +<div class="navigation" metal:define-macro="navigation"> +<table cellspacing="2" cellpadding="0" width="100%"> +<tr> +<td tal:condition="links/prev"><a tal:attributes="href links/prev/url; title stripped:links/prev/title"><img border="0" tal:attributes="alt stripped:Previous: ${links/prev/title}" src="icons/go-previous.gif" width="16" height="16" /></a></td> +<td tal:condition="not:links/prev"><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +<td tal:condition="links/up"><a tal:attributes="href links/up/url; title stripped:links/up/title"><img border="0" tal:attributes="alt stripped:Up: ${links/up/title}" src="icons/go-up.gif" width="16" height="16" /></a></td> +<td tal:condition="not:links/up"><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +<td tal:condition="links/next"><a tal:attributes="href links/next/url; title stripped:links/next/title"><img border="0" tal:attributes="alt stripped:Next: ${links/next/title}" src="icons/go-next.gif" width="16" height="16" /></a></td> +<td tal:condition="not:links/next"><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +<td class="navtitle" align="center" tal:content="links/document/title">Section Title</td> +<td tal:condition="links/contents"><a tal:attributes="href links/contents/url" title="Table of Contents"><img border="0" alt="" src="icons/gohome.gif" width="16" height="16" /></a></td> +<td tal:condition="not:links/contents"><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +<td tal:condition="links/index"><a tal:attributes="href links/index/url" title="Index"><img border="0" alt="" src="icons/go-jump.gif" width="16" height="16" /></a></td> +<td tal:condition="not:links/index"><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +<td><img border="0" alt="" src="icons/blank.gif" width="16" height="16" /></td> +</tr> +</table> +</div> + +<div tal:content="self">File contents</div> + +<div tal:condition="self/tableofcontents" tal:attributes="class string:contents ${self/nodeName}-contents"><!--<strong>Subsections</strong>--> +<ul> +<li tal:repeat="section self/tableofcontents"><a href="." tal:attributes="href section/url" tal:content="section/fullTocEntry">Aliquam est. Aliquam fringilla pede</a> + <ul tal:condition="section/tableofcontents"> + <li tal:repeat="subsection section/tableofcontents"><a href="." tal:attributes="href subsection/url" tal:content="subsection/fullTocEntry"></a> + <ul tal:condition="subsection/tableofcontents"> + <li tal:repeat="subsubsection subsection/tableofcontents"><a href="." tal:attributes="href subsubsection/url" tal:content="subsubsection/fullTocEntry"></a> + <ul tal:condition="subsubsection/tableofcontents"> + <li tal:repeat="paragraph subsubsection/tableofcontents"><a href="." tal:attributes="href paragraph/url" tal:content="paragraph/fullTocEntry"></a> + <ul tal:condition="paragraph/tableofcontents"> + <li tal:repeat="subparagraph paragraph/tableofcontents"><a href="." tal:attributes="href subparagraph/url" tal:content="subparagraph/fullTocEntry"></a></li> + </ul> + </li> + </ul> + </li> + </ul> + </li> + </ul> +</li> +<li tal:replace="nothing"><a href=".">Maecenas id purus</a></li> +<li tal:replace="nothing"><a href=".">Duis et eros</a></li> +<li tal:replace="nothing"><a href=".">Duis est</a></li> +</ul> +</div> + +<div id="footnotes" tal:condition="self/footnotes"> +<p><b>Footnotes</b></p> +<ol> +<li tal:repeat="footnote self/footnotes" tal:content="footnote" tal:attributes="id footnote/id">footnote text</li> +</ol> +</div> + +<hr /> +<div tal:condition="python:path('self/level') > -10" class="breadcrumbs"> +<span tal:repeat="crumb links/breadcrumbs"> +<span tal:condition="not:repeat/crumb/end"> +<a href="." tal:attributes="href crumb/url" tal:content="crumb/title">Parent Section</a> <b>:</b> +</span> +<span tal:condition="repeat/crumb/end"> +<b class="current" tal:content="crumb/title">Current Section</b> +</span> +</span> +</div> + +</td></tr></table> + +<script language="javascript" src="icons/imgadjust.js" type="text/javascript"></script> + +</body> +</html> diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/background.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/background.png new file mode 100644 index 0000000000000000000000000000000000000000..9d1f6e9a0c468896e3654c6598b8a5e788d7f9ac Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/background.png differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/blank.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/blank.gif new file mode 100644 index 0000000000000000000000000000000000000000..e5b747fe417ef691e3e6f403cf647d016217bc21 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/blank.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/deploy.png b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/deploy.png new file mode 100644 index 0000000000000000000000000000000000000000..ab671fa447bbbce5d1cb2df2bdb125bede335151 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/deploy.png differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/functionAddEvent.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/functionAddEvent.js new file mode 100644 index 0000000000000000000000000000000000000000..abddd68f8f3f9d7b663cd83c74b5fd0da1aa9cfc --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/functionAddEvent.js @@ -0,0 +1,69 @@ +function addEvent(elm, evType, fn, useCapture) { + if (elm.addEventListener) { + elm.addEventListener(evType, fn, useCapture); + return true; + } + else if (elm.attachEvent) { + var r = elm.attachEvent('on' + evType, fn); + EventCache.add(elm, evType, fn); + return r; + } + else { + elm['on' + evType] = fn; + } +} +function getEventSrc(e) { + if (!e) e = window.event; + + if (e.originalTarget) + return e.originalTarget; + else if (e.srcElement) + return e.srcElement; +} +function addLoadEvent(func) { +var oldonload = window.onload; + if (typeof window.onload != 'function') { + window.onload = func; + } else { + window.onload = + function() { + oldonload(); + func(); + } + } +} +var EventCache = function(){ + var listEvents = []; + return { + listEvents : listEvents, + + add : function(node, sEventName, fHandler, bCapture){ + listEvents.push(arguments); + }, + + flush : function(){ + var i, item; + for(i = listEvents.length - 1; i >= 0; i = i - 1){ + item = listEvents[i]; + + if(item[0].removeEventListener){ + item[0].removeEventListener(item[1], item[2], item[3]); + }; + + /* From this point on we need the event names to be prefixed with 'on" */ + if(item[1].substring(0, 2) != "on"){ + item[1] = "on" + item[1]; + }; + + if(item[0].detachEvent){ + item[0].detachEvent(item[1], item[2]); + }; + + item[0][item[1]] = null; + }; + } + }; +}(); + + +addEvent(window,'unload',EventCache.flush, false); \ No newline at end of file diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-bottom.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-bottom.gif new file mode 100644 index 0000000000000000000000000000000000000000..deb99a4ea8f5fd37d1d8f28b93fa93a4c299fe19 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-bottom.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-down.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-down.gif new file mode 100644 index 0000000000000000000000000000000000000000..af655dfca801341753a2e0d47ac7a9808835e282 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-down.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-first.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-first.gif new file mode 100644 index 0000000000000000000000000000000000000000..87faba2dd2d041b8a69f6ab81a1cf023ca3b6c36 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-first.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-home.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-home.gif new file mode 100644 index 0000000000000000000000000000000000000000..a77c59ff89fa2e941651cd94dcf69c9af1cefc6d Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-home.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-jump.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-jump.gif new file mode 100644 index 0000000000000000000000000000000000000000..b132d782a168547812a5a686ce1fd0248ecfd094 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-jump.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-last.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-last.gif new file mode 100644 index 0000000000000000000000000000000000000000..f25ca9c798520dd38e0279980936d056c6810565 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-last.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-next.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-next.gif new file mode 100644 index 0000000000000000000000000000000000000000..2ed252f656ebb957b72362dff2c1cafed1915372 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-next.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-previous.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-previous.gif new file mode 100644 index 0000000000000000000000000000000000000000..747904dc8cf3b8c16a5e57ce2de082d684e26ccf Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-previous.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-top.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-top.gif new file mode 100644 index 0000000000000000000000000000000000000000..a96e14c5786dccd8d4ff8fbe1aaa368b67b7224a Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-top.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-up.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-up.gif new file mode 100644 index 0000000000000000000000000000000000000000..f812f11a5f57fba2d72cf8de135bbb4a8e04e9ba Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/go-up.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/gohome.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/gohome.gif new file mode 100644 index 0000000000000000000000000000000000000000..a77c59ff89fa2e941651cd94dcf69c9af1cefc6d Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/gohome.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/imgadjust.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/imgadjust.js new file mode 100644 index 0000000000000000000000000000000000000000..2fce3d69ea2ffd48333976623a89a35fd09e9453 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/imgadjust.js @@ -0,0 +1,37 @@ +// +// This code fixes up the images so that MSIE doesn't truncate images +// within tables. It also adjusts the line height so that it's prettier. +// +var images = document.getElementsByTagName('img') +var adjusted = new Array(); +for ( var i = 0; i < images.length; i++ ) +{ + image = images[i]; + if ( parseInt(image.style.marginBottom) < -8 ) + { + if ( !image.height ) + continue; + + // Make sure that images in IE in tables don't get truncated + ieimgfix = document.createElement('img'); + ieimgfix.src = 'iicons/blank.gif'; + ieimgfix.style.height = image.style.height; + ieimgfix.style.width = '0px'; + + // Adjust line height to be prettier + adjust = document.createElement('span'); + adjust.style.lineHeight = (parseInt(image.style.height) - 8) + 'px'; + adjust.style.visibility = 'hidden'; + adjust.nodeValue = '&8205;'; + + // Store away the nodes for use later + adjusted[image.parentNode] = new Array(image.parentNode, image, + ieimgfix, adjust); + } +} +// Insert the adjuster nodes +for ( var n in adjusted ) +{ + adjusted[n][0].insertBefore(adjusted[n][2], adjusted[n][1]); + adjusted[n][0].insertBefore(adjusted[n][3], adjusted[n][1]); +} diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/index.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/index.gif new file mode 100644 index 0000000000000000000000000000000000000000..50838f6f1ec4fe7bf0f3b4d7e3564e28c15ca0e1 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/index.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/loading.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/loading.gif new file mode 100644 index 0000000000000000000000000000000000000000..fbe57be3c2cd761a999fcf91698963b723916e28 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/loading.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/missing.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/missing.gif new file mode 100644 index 0000000000000000000000000000000000000000..7696c539faced25decdde7c9ad83d1541adc920e Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/missing.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/modules.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/modules.gif new file mode 100644 index 0000000000000000000000000000000000000000..4951bb87588f0fe887ca49cdc70cf2897340cfda Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/modules.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/overlay.gif b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/overlay.gif new file mode 100644 index 0000000000000000000000000000000000000000..62c546bd7323aaf8c234c89ddefdf9f4c1fa3642 Binary files /dev/null and b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/overlay.gif differ diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/toolTipLib.js b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/toolTipLib.js new file mode 100644 index 0000000000000000000000000000000000000000..d76d4e71c67d58b59bc0abb8416bcd7dd1f64150 --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/icons/toolTipLib.js @@ -0,0 +1,107 @@ +var toolTipLib = { + xCord : 0, + yCord : 0, + obj : null, + tipElements : ['a','abbr','acronym'], + attachToolTipBehavior: function() { + if ( !document.getElementById || + !document.createElement || + !document.getElementsByTagName ) { + return; + } + var i,j; + addEvent(document,'mousemove',toolTipLib.updateXY,false); + if ( document.captureEvents ) { + document.captureEvents(Event.MOUSEMOVE); + } + for ( i=0;i<toolTipLib.tipElements.length;i++ ) { + var current = document.getElementsByTagName(toolTipLib.tipElements[i]); + for ( j=0;j<current.length;j++ ) { + addEvent(current[j],'mouseover',toolTipLib.tipOver,false); + addEvent(current[j],'mouseout',toolTipLib.tipOut,false); + current[j].setAttribute('tip',current[j].title); + current[j].removeAttribute('title'); + } + } + }, + updateXY : function(e) { + if ( document.captureEvents ) { + toolTipLib.xCord = e.pageX; + toolTipLib.yCord = e.pageY; + } else if ( window.event.clientX ) { + toolTipLib.xCord = window.event.clientX+document.documentElement.scrollLeft; + toolTipLib.yCord = window.event.clientY+document.documentElement.scrollTop; + } + }, + tipOut: function(e) { + if ( window.tID ) { + clearTimeout(tID); + } + if ( window.opacityID ) { + clearTimeout(opacityID); + } + var l = getEventSrc(e); + var div = document.getElementById('toolTip'); + if ( div ) { + div.parentNode.removeChild(div); + } + }, + checkNode : function(obj) { + var trueObj = obj; + if ( trueObj.nodeName.toLowerCase() == 'a' || trueObj.nodeName.toLowerCase() == 'acronym' || trueObj.nodeName.toLowerCase() == 'abbr' ) { + return trueObj; + } else { + return trueObj.parentNode; + } + }, + tipOver : function(e) { + toolTipLib.obj = getEventSrc(e); + tID = setTimeout("toolTipLib.tipShow()",500) + }, + tipShow : function() { + var newDiv = document.createElement('div'); + var scrX = Number(toolTipLib.xCord); + var scrY = Number(toolTipLib.yCord); + var tp = parseInt(scrY+15); + var lt = parseInt(scrX+10); + var anch = toolTipLib.checkNode(toolTipLib.obj); + var addy = ''; + var access = ''; + if ( anch.nodeName.toLowerCase() == 'a' ) { + addy = (anch.href.length > 25 ? anch.href.toString().substring(0,25)+"..." : anch.href); + var access = ( anch.accessKey ? ' <span>['+anch.accessKey+']</span> ' : '' ); + } else { + addy = anch.firstChild.nodeValue; + } + newDiv.id = 'toolTip'; + document.getElementsByTagName('body')[0].appendChild(newDiv); + newDiv.style.opacity = '.1'; + newDiv.innerHTML = "<p>"+anch.getAttribute('tip')+"<em>"+access+addy+"</em></p>"; + if ( parseInt(document.documentElement.clientWidth+document.documentElement.scrollLeft) < parseInt(newDiv.offsetWidth+lt) ) { + newDiv.style.left = parseInt(lt-(newDiv.offsetWidth+10))+'px'; + } else { + newDiv.style.left = lt+'px'; + } + if ( parseInt(document.documentElement.clientHeight+document.documentElement.scrollTop) < parseInt(newDiv.offsetHeight+tp) ) { + newDiv.style.top = parseInt(tp-(newDiv.offsetHeight+10))+'px'; + } else { + newDiv.style.top = tp+'px'; + } + toolTipLib.tipFade('toolTip',10); + }, + tipFade: function(div,opac) { + var obj = document.getElementById(div); + var passed = parseInt(opac); + var newOpac = parseInt(passed+10); + if ( newOpac < 80 ) { + obj.style.opacity = '.'+newOpac; + obj.style.filter = "alpha(opacity:"+newOpac+")"; + opacityID = setTimeout("toolTipLib.tipFade('toolTip','"+newOpac+"')",20); + } + else { + obj.style.opacity = '.80'; + obj.style.filter = "alpha(opacity:80)"; + } + } +}; +addEvent(window,'load',toolTipLib.attachToolTipBehavior,false); \ No newline at end of file diff --git a/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/styles/styles.css b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/styles/styles.css new file mode 100644 index 0000000000000000000000000000000000000000..d3cd4f212afb2403ee87f68cff2d0a944ba27e1f --- /dev/null +++ b/org.rodinp.handbook.feature/XHTML/Themes/rodin-theme-html/styles/styles.css @@ -0,0 +1,357 @@ + +pre { + color: #004000; + width: 100%; + font-size: 90%; + background-color: #f0f0f0; + padding-top: 5px; + padding-bottom: 5px; + border: 1px #aaffaa solid; + font-family: Monaco, "Courier New", Courier, fixed; + padding-left: 4ex; +} + +.breadcrumbs { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; + font-size: small; + font-style: italic; +} + +h1, h2, h3, h4, h5, h6 { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; +} + +.navigation { clear:both } +.navigation td { background-color: #ffffff; + color: #000000; + font-weight: bold; + font-family: avantgarde, sans-serif; + font-size: 110% } + +.navigation img { border-width: 0px } +.navtitle { width: 100% } + +.contents ul { + font-family: "Lucida Grande", Arial, Helvetica, sans-serif; + list-style-type: none; + font-weight: bold; +} +.contents ul ul { + font-size: small; + font-weight: normal; +} + +hr {color: black} + +.minitoc { + border-top: 1px solid black; + border-bottom: 1px solid block; + margin-bottom: 1em; +} + +.minitoc li { + list-style-type: none; +} + +/*************/ +/* Footnotes */ +/*************/ +/* +a.footnote .footnotemark { + color: #ff8000; +} +a.footnote:hover .footnotemark { + cursor: help; +} +a.footnote .footnotetext { + display: none; +} +a.footnote:hover .footnotetext { + display: block; + position: absolute; + bottom: 0em; + left: 0em; + background-color: #F8F8CB; + color: #000; + text-align: left; + border: 7px #ff8000 solid; + padding: 10px; + margin: 0px; + z-index: 20; +} +*/ +a.footnote { + text-decoration: none; +} +#footnotes { + padding: 1em; + border-top: 1px solid black; + font-size: smaller; +} + +/*******/ +/* TeX */ +/*******/ + +/* Fonts */ +.rm { + font-family: serif; + font-style: normal; + font-weight: normal; +} +.cal { + font-family: serif; + font-style: italic; + font-weight: normal; +} +.it { + font-family: serif; + font-style: italic; + font-weight: normal; +} +.sl { + font-family: serif; + font-style: oblique; + font-weight: normal; +} +.bf { + font-family: serif; + font-style: normal; + font-weight: bold; +} +.tt { + font-family: monospace; + font-style: normal; + font-weight: normal; +} + +/* Text */ +.underbar {text-decoration: underline} + + +/*********/ +/* LaTeX */ +/*********/ + +/* Alignment */ +.center, .centering {text-align: center} +.flushleft, .raggedright {text-align: left} +.flushright, .raggedleft {text-align: right} + +/* Arrays */ +.tabular { border-collapse: collapse } +.tabular td, .tabular th { + vertical-align: top; + text-align: left; + padding-top: 0.3em; + padding-bottom: 0.3em; + padding-left: 0.6em; + padding-right: 0.6em; + empty-cells: show; + +} + +/* Boxes */ +.fbox, .framebox { + border: 1px black solid; + padding-top: 1px; + padding-bottom: 1px; + padding-left: 3px; + padding-right: 3px; +} + +/* Font Selection */ +.mdseries, .textmf {font-weight: normal} +.bfseries, .textbf {font-weight: bold} +.rmfamily, .textrm {font-family: serif} +.sffamily, .textsf {font-family: sans-serif} +.ttfamily, .texttt {font-family: monospace} +.upshape, .textup {text-transform: uppercase} +.itshape, .textit {font-style: italic} +.slshape, .textsl {font-style: oblique} +.scshape, .textsc {font-variant: small-caps} + +small.tiny {font-size: x-small} +small.scriptsize {font-size: smaller} +small.footnotesize {font-size: small} +small.small {font-size: small} +.normalsize {font-size: normal} +big.large {font-size: large} +big.xlarge {font-size: x-large} +big.xxlarge {font-size: x-large} +big.huge {font-size: xx-large} +big.xhuge {font-size: xx-large} + +/* Lists */ +/*ul.itemize {}*/ +/*ol.enumerate {}*/ +dl.description dt {font-weight: bold} +table.list { + margin-left: 15px; + margin-top: 1em; + margin-bottom: 1em; +} +table.list td { + padding-right: 5px; +} + +/* Title Page */ +.titlepage {text-align: center} +.titlepage h1 {font-weight: normal} + +/* Math */ +.displaymath, .eqnarray, .equation { + margin-top: 15px; + margin-bottom: 15px; + text-align: center; +} +.eqnnum { + width: 16ex; + text-align: center; +} +.fleqn {width: 2em} + +/* Quotations and Verse */ +.quotation, .quote, .verse { + text-indent: 2em; +} +.quotation p, .quote p, .verse p { + text-indent: 2em; + margin-top: 0px; + margin-bottom: 0px; +} + +/* Rules */ +hr {color: black} + +/* Image offset classes */ +.raise15 {margin-bottom: 10px} +.raise14 {margin-bottom: 10px} +.raise13 {margin-bottom: 10px} +.raise12 {margin-bottom: 10px} +.raise11 {margin-bottom: 10px} +.raise10 {margin-bottom: 10px} +.raise9 {margin-bottom: 9px} +.raise8 {margin-bottom: 8px} +.raise7 {margin-bottom: 7px} +.raise6 {margin-bottom: 6px} +.raise5 {margin-bottom: 5px} +.raise4 {margin-bottom: 4px} +.raise3 {margin-bottom: 3px} +.raise2 {margin-bottom: 2px} +.raise1 {margin-bottom: 1px} +.raise0 {margin-bottom: 0px} +.lower0 {margin-bottom: -0px} +.lower1 {margin-bottom: -1px} +.lower2 {margin-bottom: -2px} +.lower3 {margin-bottom: -3px} +.lower4 {margin-bottom: -4px} +.lower5 {margin-bottom: -5px} +.lower6 {margin-bottom: -6px} +.lower7 {margin-bottom: -7px} +.lower8 {margin-bottom: -8px} +.lower10 {margin-bottom: -10px} +.lower11 {margin-bottom: -11px} +.lower12 {margin-bottom: -12px} +.lower13 {margin-bottom: -13px} +.lower14 {margin-bottom: -14px} +.lower15 {margin-bottom: -15px} +.lower16 {margin-bottom: -16px} +.lower17 {margin-bottom: -17px} +.lower18 {margin-bottom: -18px} +.lower19 {margin-bottom: -19px} +.lower20 {margin-bottom: -20px} +.lower21 {margin-bottom: -21px} +.lower22 {margin-bottom: -22px} +.lower23 {margin-bottom: -23px} +.lower24 {margin-bottom: -24px} +.lower25 {margin-bottom: -25px} +.lower26 {margin-bottom: -26px} +.lower27 {margin-bottom: -27px} +.lower28 {margin-bottom: -28px} +.lower29 {margin-bottom: -29px} +.lower30 {margin-bottom: -20px} +.lower20 {margin-bottom: -20px} + +td p:first-child, th p:first-child { + margin-top: 0px; + margin-bottom: 0px; +} + +td p, th p { + margin-top: 1em; + margin-bottom: 0px; +} + +p { + text-indent: 0em; + margin-top: 0px; + margin-bottom: 1em; +} + +img { + border: none; + vertical-align: baseline; +} + +img.ieimgfix { + width: 0; + visibility: hidden; + vertical-align: top; + display: none; +} + +td img.ieimgfix { + display: inline; +} + +body { + color: #000000; + background-color: #ffffff; + background: url('../icons/background.png'); +} + +/* Index */ +.theindex li { + list-style-type: none +} + +.changebar { + border-right: 2px solid red; + padding-right: 1em; +} + +.deletebar { + color: red; + font-size: 150%; + padding-left: 0.5ex; + padding-right: 0.5ex; +} + +/* The Menu */ + +#navlist li { display: inline; +/* for IE5 and IE6 */ +} + +#navlist { +width: 135px; +/* to display the list horizontaly */ +font-family: sans-serif; +font-size: 80%; +margin: 0 0 0 0; +padding: 0; +} + +#navlist a +{ +width: 99.99%; +/* extend the sensible area to the maximum with IE5 */ +display: block; +text-decoration: none; +color: #000; +} + +#navlist a:hover { background-color: #ffffff; } +#navlist a:visited { color: #000; } + diff --git a/org.rodinp.handbook.feature/build.properties b/org.rodinp.handbook.feature/build.properties new file mode 100644 index 0000000000000000000000000000000000000000..64f93a9f0b7328eb563aa5ad6cec7f828020e124 --- /dev/null +++ b/org.rodinp.handbook.feature/build.properties @@ -0,0 +1 @@ +bin.includes = feature.xml diff --git a/org.rodinp.handbook.feature/build.xml b/org.rodinp.handbook.feature/build.xml new file mode 100644 index 0000000000000000000000000000000000000000..d0afed6bb3609642032acf4c929cd5c40127dc0c --- /dev/null +++ b/org.rodinp.handbook.feature/build.xml @@ -0,0 +1,61 @@ +<project default="generate-all"> + + <target name="generate-all"> + <antcall target="generate-html" /> + <antcall target="generate-eclipse" /> + </target> + + <target name="generate-html"> + <antcall target="generate"> + <param name="targetdir" value="${basedir}/build/html"/> + <param name="theme" value="rodin-theme-html"/> + </antcall> + <delete dir="${basedir}/build/html" includes="chm.*,*.xml,*.hs,*.jhm,*.paux"></delete> + </target> + + <target name="generate-eclipse"> + <antcall target="generate"> + <param name="targetdir" value="${basedir}/build/org.rodinp.handbook"/> + <param name="theme" value="rodin-theme-eclipse"/> + </antcall> + <delete dir="${basedir}/build/org.rodinp.handbook" includes="chm.*,*.hs,*.jhm,*.paux"></delete> + <copy todir="${basedir}/build/org.rodinp.handbook"> + <fileset dir="${basedir}/skeleton" /> + </copy> + + <replace file="${basedir}/build/org.rodinp.handbook/eclipse-toc.xml" > + <replacetoken><![CDATA[<toc ]]></replacetoken> + <replacevalue><![CDATA[<toc topic="index.html" ]]></replacevalue> + </replace> + </target> + + <target name="generate" depends="init"> + <mkdir dir="${targetdir}"/> + <exec executable="plastex" dir="${basedir}/build/latex"> + <env key="XHTMLTEMPLATES" value="${basedir}/build/XHTML"/> + <arg value="-d"/> + <arg value="${targetdir}"/> + <arg value="--theme=${theme}"/> + <arg value="${basedir}/build/latex/rodin-doc.tex"/> + </exec> + <copy todir="${targetdir}/files"> + <fileset dir="${basedir}/latex/files" /> + </copy> + </target> + + <target name="init"> + <tstamp/> + <!-- plastex cannot deal with subversion files. Thus, we create a copy --> + <copy todir="${basedir}/build/latex"> + <fileset dir="${basedir}/latex" excludes=".svn,*.sty"/> + </copy> + <!-- We tweak the Event-B Style Files for plastex --> + <copy file="${basedir}/latex/plastex-b2latex.sty" tofile="${basedir}/build/latex/b2latex.sty"/> + <copy file="${basedir}/latex/plastex-bsymb.sty" tofile="${basedir}/build/latex/bsymb.sty"/> + + <copy todir="${basedir}/build/XHTML"> + <fileset dir="${basedir}/XHTML" excludes=".svn"/> + </copy> + </target> + +</project> diff --git a/org.rodinp.handbook.feature/feature.xml b/org.rodinp.handbook.feature/feature.xml new file mode 100644 index 0000000000000000000000000000000000000000..48355a0e6971b97862e205e467918486295fa975 --- /dev/null +++ b/org.rodinp.handbook.feature/feature.xml @@ -0,0 +1,33 @@ +<?xml version="1.0" encoding="UTF-8"?> +<feature + id="org.rodinp.handbook.feature" + label="Rodin Handbook Feature" + version="1.0.0.qualifier" + provider-name="Formal Mind GmbH"> + + <description url="http://www.example.com/description"> + The Rodin Handbook. + </description> + + <copyright url="http://www.example.com/copyright"> + (c) 2011 by Formal Mind GmbH and Others + </copyright> + + <license url="http://www.example.com/license"> + This work is licensed under the Creative Commons Attribution Licens (CC BY). The full license is found at + +http://creativecommons.org/licenses/by/3.0/ + </license> + + <url> + <discovery label="Formal Mind" url="http://formalmind.com"/> + <discovery label="Rodin Website" url="http://sourceforge.net/projects/rodin-b-sharp/"/> + </url> + + <plugin + id="org.rodinp.handbook" + download-size="0" + install-size="0" + version="0.0.0"/> + +</feature> diff --git a/org.rodinp.handbook.feature/latex/.b2latex-plastex.sty.properties.xml b/org.rodinp.handbook.feature/latex/.b2latex-plastex.sty.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.b2latex-plastex.sty.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.b2latex.sty.properties.xml b/org.rodinp.handbook.feature/latex/.b2latex.sty.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.b2latex.sty.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.bsymb.sty.properties.xml b/org.rodinp.handbook.feature/latex/.bsymb.sty.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.bsymb.sty.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.cache/DVIPNG.images b/org.rodinp.handbook.feature/latex/.cache/DVIPNG.images new file mode 100644 index 0000000000000000000000000000000000000000..6747cc4f86d09b600cdc398567cf1a3c637dc403 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.cache/DVIPNG.images @@ -0,0 +1,1704 @@ +(dp0 +V\u005craisebox{4mm}{\u005cvtop {\u005cnull \u005chbox{\u005cincludegraphics[width=10mm]{img/tick_64.png}}}} +p1 +ccopy_reg +_reconstructor +p2 +(cplasTeX.Imagers +Image +p3 +c__builtin__ +object +p4 +Ntp5 +Rp6 +(dp7 +S'_depth' +p8 +g2 +(cplasTeX.Imagers +Dimension +p9 +c__builtin__ +float +p10 +F0.0 +tp11 +Rp12 +sS'depthRatio' +p13 +I0 +sS'_height' +p14 +g2 +(g9 +g10 +F1.0 +tp15 +Rp16 +sS'_width' +p17 +g2 +(g9 +g10 +F1.0 +tp18 +Rp19 +sS'filename' +p20 +Vimages/img-0001.png +p21 +sS'_cropped' +p22 +I01 +sS'checksum' +p23 +S'\xa1\xcf\t\xb5\x9eP`\xf3\xbe\xcc\xdc\xf7\xa3q\x89\xf0' +p24 +sS'path' +p25 +V/home/jastram/workspaces/rodin-src/org.rodinp.help/latex/images/img-0001.png +p26 +sS'alt' +p27 +NsS'bitmap' +p28 +g6 +sS'config' +p29 +g2 +(cplasTeX.ConfigManager +ConfigSection +p30 +g4 +Ntp31 +Rp32 +(dp33 +S'data' +p34 +(dp35 +S'save-file' +p36 +g2 +(cplasTeX.ConfigManager.Boolean +BooleanOption +p37 +g4 +Ntp38 +Rp39 +(dp40 +S'category' +p41 +(lp42 +S'images' +p43 +asS'mandatory' +p44 +I00 +sS'actual' +p45 +NsS'name' +p46 +g36 +sS'parent' +p47 +g32 +sS'source' +p48 +I2 +sS'default' +p49 +I0 +sg34 +NsS'description' +p50 +S'Should the temporary images.tex file be saved for debugging?' +p51 +sS'summary' +p52 +g51 +sS'callback' +p53 +NsS'values' +p54 +NsS'registry' +p55 +NsS'file' +p56 +NsS'error' +p57 +NsS'environ' +p58 +NsS'optional' +p59 +NsS'options' +p60 +S'--save-image-file !--delete-image-file' +p61 +sS'occurrences' +p62 +I0 +sbsS'scale-factor' +p63 +g2 +(cplasTeX.ConfigManager.Float +FloatOption +p64 +g4 +Ntp65 +Rp66 +(dp67 +g41 +(lp68 +g43 +asg44 +I00 +sg45 +Nsg46 +g63 +sg47 +g32 +sg48 +I2 +sg49 +F1.0 +sg34 +Nsg50 +S'Factor to scale externally included images by' +p69 +sg52 +g69 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--image-scale-factor' +p70 +sg62 +I0 +sbsS'cache' +p71 +g2 +(g37 +g4 +Ntp72 +Rp73 +(dp74 +g41 +(lp75 +g43 +asg44 +I00 +sg45 +Nsg46 +g71 +sg47 +g32 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Enable image caching between runs' +p76 +sg52 +g76 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--enable-image-cache !--disable-image-cache' +p77 +sg62 +I0 +sbsS'enabled' +p78 +g2 +(g37 +g4 +Ntp79 +Rp80 +(dp81 +g41 +(lp82 +g43 +asg44 +I00 +sg45 +Nsg46 +g78 +sg47 +g32 +sg48 +I2 +sg49 +I1 +sg34 +Nsg50 +S'Enable image generation' +p83 +sg52 +g83 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--enable-images !--disable-images' +p84 +sg62 +I0 +sbsS'filenames' +p85 +g2 +(cplasTeX.ConfigManager.String +StringOption +p86 +g4 +Ntp87 +Rp88 +(dp89 +g41 +(lp90 +g43 +asg44 +I00 +sg45 +Nsg46 +g85 +sg47 +g32 +sg48 +I2 +sg49 +Vimages/img-$num(4) +p91 +sg59 +Nsg50 +S'Template for image filenames' +p92 +sg52 +g92 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g91 +sg60 +S'--image-filenames' +p93 +sg62 +I0 +sbsS'vector-imager' +p94 +g2 +(g86 +g4 +Ntp95 +Rp96 +(dp97 +g41 +(lp98 +g43 +asg44 +I00 +sg45 +Nsg46 +g94 +sg47 +g32 +sg48 +I2 +sg49 +Vnone dvisvgm +p99 +sg59 +Nsg50 +S'LaTeX to vector image program' +p100 +sg52 +g100 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g99 +sg60 +S'--vector-imager' +p101 +sg62 +I0 +sbsS'baseline-padding' +p102 +g2 +(cplasTeX.ConfigManager.Integer +IntegerOption +p103 +g4 +Ntp104 +Rp105 +(dp106 +g41 +(lp107 +g43 +asg44 +I00 +sg45 +Nsg46 +g102 +sg47 +g32 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Amount to pad the image below the baseline' +p108 +sg52 +g108 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--image-baseline-padding' +p109 +sg62 +I0 +sbsS'imager' +p110 +g2 +(g86 +g4 +Ntp111 +Rp112 +(dp113 +g41 +(lp114 +g43 +asg44 +I00 +sg45 +Nsg46 +g110 +sg47 +g32 +sg48 +I2 +sg49 +Vdvipng dvi2bitmap gspdfpng gsdvipng OSXCoreGraphics +p115 +sg59 +Nsg50 +S'LaTeX to image program' +p116 +sg52 +g116 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g115 +sg60 +S'--imager' +p117 +sg62 +I0 +sbsS'base-url' +p118 +g2 +(g86 +g4 +Ntp119 +Rp120 +(dp121 +g41 +(lp122 +g43 +asg44 +I00 +sg45 +Nsg46 +g118 +sg47 +g32 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Base URL for all images' +p123 +sg52 +g123 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--image-base-url' +p124 +sg62 +I0 +sbsS'resolution' +p125 +g2 +(g103 +g4 +Ntp126 +Rp127 +(dp128 +g41 +(lp129 +g43 +asg44 +I00 +sg45 +Nsg46 +g125 +sg47 +g32 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Resolution of images document' +p130 +sg52 +g130 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--image-resolution' +p131 +sg62 +I0 +sbsS'transparent' +p132 +g2 +(g37 +g4 +Ntp133 +Rp134 +(dp135 +g41 +(lp136 +g43 +asg44 +I00 +sg45 +Nsg46 +g132 +sg47 +g32 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Specifies whether the image backgrounds should be transparent or not' +p137 +sg52 +g137 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--transparent-images !--opaque-images' +p138 +sg62 +I0 +sbsS'compiler' +p139 +g2 +(g86 +g4 +Ntp140 +Rp141 +(dp142 +g41 +(lp143 +g43 +asg44 +I00 +sg45 +Nsg46 +g139 +sg47 +g32 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'LaTeX command to use when compiling image document' +p144 +sg52 +g144 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--image-compiler' +p145 +sg62 +I0 +sbssg46 +g43 +sg47 +g2 +(cplasTeX.ConfigManager +ConfigManager +p146 +g4 +Ntp147 +Rp148 +(dp149 +S'strict' +p150 +I1 +sS'_categories' +p151 +(dp152 +S'files' +p153 +S'File Handling Options' +p154 +sg43 +S'Image Generation Options' +p155 +sS'document' +p156 +S'Document Options' +p157 +ssg34 +(dp158 +g153 +g2 +(g30 +g4 +Ntp159 +Rp160 +(dp161 +g34 +(dp162 +S'input-encoding' +p163 +g2 +(g86 +g4 +Ntp164 +Rp165 +(dp166 +g41 +(lp167 +g153 +asg44 +I00 +sg45 +Nsg46 +g163 +sg47 +g160 +sg48 +I2 +sg49 +Vutf-8 +p168 +sg59 +Nsg50 +S'Input file encoding' +p169 +sg52 +g169 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g168 +sg60 +S'--input-encoding' +p170 +sg62 +I0 +sbsS'bad-chars' +p171 +g2 +(g86 +g4 +Ntp172 +Rp173 +(dp174 +g41 +(lp175 +g153 +asg44 +I00 +sg45 +Nsg46 +g171 +sg47 +g160 +sg48 +I2 +sg49 +V: #$%^&*!~`"'=?/{}[]()|<>;\u005c,. +p176 +sg59 +Nsg50 +S'Characters that should not be allowed in a filename' +p177 +sg52 +g177 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +V: #$%^&*!~`"'=?/{}[]()|<>;\u005c,. +p178 +sg60 +S'--bad-filename-chars' +p179 +sg62 +I0 +sbsS'escape-high-chars' +p180 +g2 +(g37 +g4 +Ntp181 +Rp182 +(dp183 +g41 +(lp184 +g153 +asg44 +I00 +sg45 +Nsg46 +g180 +sg47 +g160 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Escape characters that are higher than 7-bit' +p185 +sg52 +g185 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--escape-high-chars' +p186 +sg62 +I0 +sbsg20 +g2 +(g86 +g4 +Ntp187 +Rp188 +(dp189 +g41 +(lp190 +g153 +asg44 +I00 +sg45 +Nsg46 +g20 +sg47 +g160 +sg48 +I2 +sg49 +Vindex [$id, sect$num(4)] +p191 +sg59 +Nsg50 +S'Template for output filenames' +p192 +sg52 +g192 +sg53 +cplasTeX.Config +setFilename +p193 +sg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g191 +sg60 +S'--filename' +p194 +sg62 +I0 +sbsS'output-encoding' +p195 +g2 +(g86 +g4 +Ntp196 +Rp197 +(dp198 +g41 +(lp199 +g153 +asg44 +I00 +sg45 +Nsg46 +g195 +sg47 +g160 +sg48 +I2 +sg49 +Vutf-8 +p200 +sg59 +Nsg50 +S'Output file encoding' +p201 +sg52 +g201 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g200 +sg60 +S'--output-encoding' +p202 +sg62 +I0 +sbsS'split-level' +p203 +g2 +(g103 +g4 +Ntp204 +Rp205 +(dp206 +g41 +(lp207 +g153 +asg44 +I00 +sg45 +Nsg46 +g203 +sg47 +g160 +sg48 +I2 +sg49 +I2 +sg34 +Nsg50 +S'Highest section level that generates a new file' +p208 +sg52 +g208 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--split-level' +p209 +sg62 +I0 +sbsS'directory' +p210 +g2 +(g86 +g4 +Ntp211 +Rp212 +(dp213 +g41 +(lp214 +g153 +asg44 +I00 +sg45 +S'-d' +p215 +sg46 +g210 +sg47 +g160 +sg48 +I64 +sg49 +V$jobname +p216 +sg59 +Nsg50 +S'Directory to put output files into' +p217 +sg52 +g217 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +V/home/jastram/workspaces/rodin-src/org.rodinp.help/latex +p218 +sg60 +S'--dir -d' +p219 +sg62 +I1 +sbsS'bad-chars-sub' +p220 +g2 +(g86 +g4 +Ntp221 +Rp222 +(dp223 +g41 +(lp224 +g153 +asg44 +I00 +sg45 +Nsg46 +g220 +sg47 +g160 +sg48 +I2 +sg49 +V- +p225 +sg59 +Nsg50 +S'Character that should be used instead of an illegal character' +p226 +sg52 +g226 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g225 +sg60 +S'--bad-filename-chars-sub' +p227 +sg62 +I0 +sbssg46 +g153 +sg47 +g148 +sbsS'links' +p228 +g2 +(g30 +g4 +Ntp229 +Rp230 +(dp231 +g34 +(dp232 +S';links' +p233 +g2 +(cplasTeX.ConfigManager.Compound +CompoundOption +p234 +g4 +Ntp235 +Rp236 +(dp237 +g41 +(lp238 +g156 +asg44 +I00 +sg45 +Nsg46 +g233 +sg47 +g230 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Set links for use in navigation' +p239 +sg52 +g239 +sg53 +cplasTeX.Config +setlinks +p240 +sg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--link' +p241 +sg62 +I0 +sbssg46 +g228 +sg47 +g148 +sbsS'DEFAULT' +p242 +g2 +(g30 +g4 +Ntp243 +Rp244 +(dp245 +g34 +(dp246 +sg46 +g242 +sg47 +g148 +sbsS'general' +p247 +g2 +(g30 +g4 +Ntp248 +Rp249 +(dp250 +g34 +(dp251 +S'paux-dirs' +p252 +g2 +(cplasTeX.ConfigManager.Multi +MultiOption +p253 +g4 +Ntp254 +Rp255 +(dp256 +g44 +I00 +sS'delim' +p257 +S',' +p258 +sg62 +I0 +sg56 +Nsg41 +(lp259 +sg34 +(lp260 +sg48 +I4 +sS'template' +p261 +g2 +(g86 +g4 +Ntp262 +Rp263 +(dp264 +g41 +(lp265 +sg44 +I00 +sg45 +Nsg46 +Nsg48 +I2 +sg49 +Nsg59 +Nsg50 +Nsg52 +Nsg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--paux-dirs' +p266 +sg62 +I0 +sbsg58 +Nsg50 +S'Directories where *.paux files should be loaded from.' +p267 +sg47 +g249 +sg55 +Nsg59 +(lp268 +sg45 +Nsg46 +g252 +sg49 +(lp269 +sg52 +g267 +sg53 +NsS'range' +p270 +(lp271 +I1 +aS'*' +p272 +asg54 +Nsg57 +Nsg60 +g266 +sbsS'kpsewhich' +p273 +g2 +(g86 +g4 +Ntp274 +Rp275 +(dp276 +g41 +(lp277 +sg44 +I00 +sg45 +Nsg46 +g273 +sg47 +g249 +sg48 +I2 +sg49 +Vkpsewhich +p278 +sg59 +Nsg50 +S'Program which locates LaTeX files and packages' +p279 +sg52 +g279 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g278 +sg60 +S'--kpsewhich' +p280 +sg62 +I0 +sbsS'copy-theme-extras' +p281 +g2 +(g37 +g4 +Ntp282 +Rp283 +(dp284 +g41 +(lp285 +sg44 +I00 +sg45 +Nsg46 +g281 +sg47 +g249 +sg48 +I2 +sg49 +I1 +sg34 +Nsg50 +S'Copy files associated with the theme to the output directory' +p286 +sg52 +g286 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--copy-theme-extras !--no-theme-extras' +p287 +sg62 +I0 +sbsS'theme' +p288 +g2 +(g86 +g4 +Ntp289 +Rp290 +(dp291 +g41 +(lp292 +sg44 +I00 +sg45 +S'--theme' +p293 +sg46 +g288 +sg47 +g249 +sg48 +I64 +sg49 +Vdefault +p294 +sg59 +Nsg50 +S'Theme for the renderer to use' +p295 +sg52 +g295 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Vrodin-theme-html +p296 +sg60 +S'--theme' +p297 +sg62 +I1 +sbsS'renderer' +p298 +g2 +(g86 +g4 +Ntp299 +Rp300 +(dp301 +g41 +(lp302 +sg44 +I00 +sg45 +Nsg46 +g298 +sg47 +g249 +sg48 +I2 +sg49 +VXHTML +p303 +sg59 +Nsg50 +S'Renderer to use for conversion' +p304 +sg52 +g304 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g303 +sg60 +S'--renderer' +p305 +sg62 +I0 +sbsg29 +g2 +(g86 +g4 +Ntp306 +Rp307 +(dp308 +g41 +(lp309 +sg44 +I00 +sg45 +Nsg46 +g29 +sg47 +g249 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Load additional configuration file\n\nThis configuration file will be loaded during the processing of\ncommand-line options. However, configuration files cannot override\ncommand-line options. So no matter what is in the configuration file,\nif an option is specified on the command-line, it will always win.\nTo eliminate any confusion, this should generally be the first\nargument.' +p310 +sg52 +S'Load additional configuration file' +p311 +sg53 +cplasTeX.Config +readconfig +p312 +sg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--config -c' +p313 +sg62 +I0 +sbssg46 +g247 +sg47 +g148 +sbsg43 +g32 +sg156 +g2 +(g30 +g4 +Ntp314 +Rp315 +(dp316 +g34 +(dp317 +S'toc-depth' +p318 +g2 +(g103 +g4 +Ntp319 +Rp320 +(dp321 +g41 +(lp322 +g156 +asg44 +I00 +sg45 +Nsg46 +g318 +sg47 +g315 +sg48 +I2 +sg49 +I3 +sg34 +Nsg50 +S'Number of levels to display in the table of contents' +p323 +sg52 +g323 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--toc-depth' +p324 +sg62 +I0 +sbsS'toc-non-files' +p325 +g2 +(g37 +g4 +Ntp326 +Rp327 +(dp328 +g41 +(lp329 +g156 +asg44 +I00 +sg45 +Nsg46 +g325 +sg47 +g315 +sg48 +I2 +sg49 +I0 +sg34 +Nsg50 +S'Display sections that do not create files in the table of contents' +p330 +sg52 +g330 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--toc-non-files' +p331 +sg62 +I0 +sbsS'lang-terms' +p332 +g2 +(g86 +g4 +Ntp333 +Rp334 +(dp335 +g41 +(lp336 +g156 +asg44 +I00 +sg45 +Nsg46 +g332 +sg47 +g315 +sg48 +I2 +sg49 +V +p337 +sg59 +Nsg50 +S"Specifies a ':' delimited list of files that contain language terms" +p338 +sg52 +g338 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +g337 +sg60 +S'--lang-terms' +p339 +sg62 +I0 +sbsS'title' +p340 +g2 +(g86 +g4 +Ntp341 +Rp342 +(dp343 +g41 +(lp344 +g156 +asg44 +I00 +sg45 +Nsg46 +g340 +sg47 +g315 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Title for the document\n\nThis option specifies a title to use instead of the title\nspecified in the LaTeX document.' +p345 +sg52 +S'Title for the document' +p346 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--title' +p347 +sg62 +I0 +sbsS'sec-num-depth' +p348 +g2 +(g103 +g4 +Ntp349 +Rp350 +(dp351 +g41 +(lp352 +g156 +asg44 +I00 +sg45 +Nsg46 +g348 +sg47 +g315 +sg48 +I2 +sg49 +I2 +sg34 +Nsg50 +S'Maximum section depth to display section numbers' +p353 +sg52 +g353 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--sec-num-depth' +p354 +sg62 +I0 +sbsS'index-columns' +p355 +g2 +(g103 +g4 +Ntp356 +Rp357 +(dp358 +g41 +(lp359 +g156 +asg44 +I00 +sg45 +Nsg46 +g355 +sg47 +g315 +sg48 +I2 +sg49 +I2 +sg34 +Nsg50 +S'Number of columns to split the index entries into' +p360 +sg52 +g360 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg59 +Nsg60 +S'--index-columns' +p361 +sg62 +I0 +sbsg118 +g2 +(g86 +g4 +Ntp362 +Rp363 +(dp364 +g41 +(lp365 +g156 +asg44 +I00 +sg45 +Nsg46 +g118 +sg47 +g315 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Base URL for inter-node links' +p366 +sg52 +g366 +sg53 +Nsg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--base-url' +p367 +sg62 +I0 +sbssg46 +g156 +sg47 +g148 +sbsS'counters' +p368 +g2 +(g30 +g4 +Ntp369 +Rp370 +(dp371 +g34 +(dp372 +S';counters' +p373 +g2 +(g234 +g4 +Ntp374 +Rp375 +(dp376 +g41 +(lp377 +g156 +asg44 +I00 +sg45 +Nsg46 +g373 +sg47 +g370 +sg48 +I2 +sg49 +Nsg59 +Nsg50 +S'Set initial counter values' +p378 +sg52 +g378 +sg53 +cplasTeX.Config +setcounter +p379 +sg54 +Nsg55 +Nsg56 +Nsg57 +Nsg58 +Nsg34 +Nsg60 +S'--counter' +p380 +sg62 +I0 +sbssg46 +g368 +sg47 +g148 +sbssS'unrecognized' +p381 +(lp382 +sbsbsS'longdesc' +p383 +Nsbs. \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.faq.tex.properties.xml b/org.rodinp.handbook.feature/latex/.faq.tex.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.faq.tex.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.plastex-b2latex.sty.properties.xml b/org.rodinp.handbook.feature/latex/.plastex-b2latex.sty.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.plastex-b2latex.sty.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.plastex-bsymb.sty.properties.xml b/org.rodinp.handbook.feature/latex/.plastex-bsymb.sty.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.plastex-bsymb.sty.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.reference.tex.properties.xml b/org.rodinp.handbook.feature/latex/.reference.tex.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.reference.tex.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/.tutorial.tex.properties.xml b/org.rodinp.handbook.feature/latex/.tutorial.tex.properties.xml new file mode 100644 index 0000000000000000000000000000000000000000..c24a61125fca29cdaebeed0eeecc0810575d1de2 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/.tutorial.tex.properties.xml @@ -0,0 +1 @@ +<?xml version="1.0" ?><properties><property key="MasterFilename" value="rodin-doc.tex"/></properties> \ No newline at end of file diff --git a/org.rodinp.handbook.feature/latex/b2latex.sty b/org.rodinp.handbook.feature/latex/b2latex.sty new file mode 100644 index 0000000000000000000000000000000000000000..ef66fa8d71d936a976b720bb2d55cc37ec045d9b --- /dev/null +++ b/org.rodinp.handbook.feature/latex/b2latex.sty @@ -0,0 +1,122 @@ +%------------------------------------------------------------------- +% This is b2latex.sty, generated by B2Latex plugin on Rodin +% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk +% Copyright(c)2008 ECS @ University of Southampton +%------------------------------------------------------------------- +% This style file is required for all latex files generated by the +% B2Latex plugin 0.5.x. +% Each command mentioned below, can be modified for your own style +% but command names are not allowed. +% +%------------------------------------------------------------------- +% Defined colors. +%------------------------------------------------------------------- +\usepackage{color} +\definecolor{keycolor}{rgb}{0,0,0.7} %color of key words, blue is the default +\definecolor{labelcolor}{rgb}{0,0.4,0.8} %color of labels, cyan +\definecolor{codecolor}{rgb}{0,0.2,0} %color of formulas, black +\definecolor{xcodecolor}{rgb}{0,0,0} %color of extended formulas, black +\definecolor{cmtcolor}{rgb}{0,0,0} %color of comments, black +%------------------------------------------------------------------- +\newcommand{\paraSpc} {\hspace*{\fill} \setlength{\parskip}{-2pt}} % reduce space between paras +%------------------------------------------------------------------- +\newcommand{\itemSpc} {\setlength{\itemsep}{-0pt}} % reduce space between para items +%------------------------------------------------------------------- +% Special commands for MACHINE +%------------------------------------------------------------------- +\newcommand{\MACHINE}[1] { \item[\textcolor{keycolor}{MACHINE }] #1 \paraSpc } + +\newcommand{\REFINES}[1]{ \item[\textcolor{keycolor}{REFINES }] #1 \paraSpc } + +\newcommand{\SEES}[1]{ \item[\textcolor{keycolor}{SEES }] #1 \paraSpc } + +\newcommand{\VARIABLES}{\item[\textcolor{keycolor}{VARIABLES}] \paraSpc } + +\newcommand{\INVARIANTS}{ \item[\textcolor{keycolor}{INVARIANTS}] \paraSpc } + +\newcommand{\VARIANT}{ \item[\textcolor{keycolor}{VARIANT}] \paraSpc } + +\newcommand{\EVENTS}{ \item[\textcolor{keycolor}{EVENTS}] \paraSpc } + +\newcommand{\INITIALISATION}{ \item[\textcolor{keycolor}{Initialisation}] \paraSpc } + +\newcommand{\EVT}[1]{ \item[\textcolor{keycolor}{Event }] \textit{#1} $\defi$ \paraSpc } % opt1 +% Option: deactivate above command and reactivate +% the command below to display only event name +%\newcommand{\EVT}[1]{ \item[\textit{#1}] $\defi$ \paraSpc } % opt2 + +\newcommand{\REF}[1]{ \item[\textcolor{keycolor}{refines}] \textit{#1} \paraSpc } + +\newcommand{\EXTD}[1]{ \item[\textcolor{keycolor}{extends}] \textit{#1} \paraSpc } + +\newcommand{\Status}[1]{ \item[\textcolor{keycolor}{Status}] #1 \paraSpc } + +\newcommand{\AnyPrm}{ \item[\textcolor{keycolor}{any}] \paraSpc \itemSpc } + +\newcommand{\WhereGrd}{ \item[\textcolor{keycolor}{where}] \paraSpc \itemSpc } + +\newcommand{\WhenGrd}{ \item[\textcolor{keycolor}{when}] \paraSpc \itemSpc } + +\newcommand{\Witnesses}{ \item[\textcolor{keycolor}{with}] \paraSpc \itemSpc } + +\newcommand{\ThenAct}{ \item[\textcolor{keycolor}{then}] \paraSpc \itemSpc } + +\newcommand{\BeginAct}{ \item[\textcolor{keycolor}{begin}] \paraSpc \itemSpc } + +\newcommand{\EndAct}{ \item[\textcolor{keycolor}{end}] \paraSpc } + +%------------------------------------------------------------------- +% Special commands for CONTEXT +%------------------------------------------------------------------- + +\newcommand{\CONTEXT}[1]{ \item[\textcolor{keycolor}{CONTEXT }] #1 \paraSpc } + +\newcommand{\EXTENDS}[1]{ \item[\textcolor{keycolor}{EXTENDS }] #1 \paraSpc } + +\newcommand{\SETS}{ \item[\textcolor{keycolor}{SETS}] \paraSpc } + +\newcommand{\CONSTANTS}{ \item[\textcolor{keycolor}{CONSTANTS}] \paraSpc } + +\newcommand{\THEOREMS}{ \item[\textcolor{keycolor}{THEOREMS}] \paraSpc } + +\newcommand{\AXIOMS}{ \item[\textcolor{keycolor}{AXIOMS}] \paraSpc } + +%------------------------------------------------------------------- +% General commands used in both machines and contexts +%------------------------------------------------------------------- + +% Specification Title +\newcommand{\BTitle}[3]{ +\item[\fbox{\parbox{6in}{\centering{~\\An Event-B Specification of #1 +\\Creation Date: #2 @ #3\\}}}] +} +% End of MACHINE or CONTEXT +\newcommand{\END}{ \item[\textcolor{keycolor}{END}] \hspace*{\fill} } + +% Printing non-labelled elements +% (i.e. variables, sets and constants) +\newcommand{\Item}[1]{ \item[\textcolor{codecolor}{$\tt#1$}] \itemSpc } +\newcommand{\ItemX}[1]{ \item[\textcolor{xcodecolor}{$\it#1$}] \itemSpc } + +% Printing an element with label name +% (i.e. invariants, theorems, axioms, witnesses and actions) +% parameter #1 is a label name and #2 is its content +\newcommand{\nItem}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{codecolor}{$\tt #2$} \itemSpc } % opt1 +\newcommand{\nItemX}[2]{ \item[\textcolor{labelcolor}{$\tt #1:$}] \textcolor{xcodecolor}{$\it #2$} \itemSpc } % opt1 +% Below is an alternative command for printing with no label +%\newcommand{\nItem}[2]{ \item[] $#2$} % opt2 + +% Commentations, reselect the second option for displaying asterisks +% - Newline comment +\newcommand{\cmt}[1]{ \hspace*{\fill}\\\textcolor{cmtcolor}{ #1}} %opt1 +%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2 + +% - Back Comment, for variables, sets and constants +\newcommand{\bcmt}[1]{~~~ \textcolor{cmtcolor}{#1}} %opt1 +%\newcommand{\bcmt}[1]{~~~ $/\ast$ #1 $\ast/$} %opt2 +% Select opt3 or opt4 (including asterisks) if you want to display this kind of comments +% on the newline like the newline comment +%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ #1} %opt3 +%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt4 + +%------------------------------------------------------------------- diff --git a/org.rodinp.handbook.feature/latex/bsymb.sty b/org.rodinp.handbook.feature/latex/bsymb.sty new file mode 100644 index 0000000000000000000000000000000000000000..3e446a61f1a65ebc5a56db5bfe8c37c0db390cad --- /dev/null +++ b/org.rodinp.handbook.feature/latex/bsymb.sty @@ -0,0 +1,101 @@ +%% +%% This is file `bsymb.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% bsymb.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2004 by Laurent Voisin <laurent.voisin at inf.ethz.ch> +%% +%% This file may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3 +%% of this license or (at your option) any later version. +%% The latest version of this license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.3 or later is part of all distributions of LaTeX +%% version 2003/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/06/01] +\ProvidesPackage{bsymb} + [2005/04/27 v1.5 Symbols for the B language] +\RequirePackageWithOptions{amssymb} +\newcommand\bsymb@defop[2]{ + \newcommand{#1}{\mathop{#2}\nolimits} +} +\newcommand\bsymb@deford[2]{ + \newcommand{#1}{\mathord{#2}} +} +\bsymb@deford{\bfalse}{\bot} +\bsymb@deford{\btrue}{\top} +\newcommand{\limp}{\mathbin\Rightarrow} +\newcommand{\leqv}{\mathbin\Leftrightarrow} +\bsymb@deford{\qdot}{\mkern1mu\cdot\mkern1mu} +\newcommand\defi{\mathrel{\widehat=}} + +\bsymb@defop{\pow}{\mathbb P\hbox{}} +\bsymb@defop{\pown}{\mathbb P_1} +\newcommand{\cprod}{\mathbin\times} +\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}} +\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}} +\bsymb@defop{\union}{\mathrm{union}} +\bsymb@defop{\inter}{\mathrm{inter}} +\newcommand{\Union}{\bigcup\nolimits} +\newcommand{\Inter}{\bigcap\nolimits} +\renewcommand{\emptyset}{\mathord\varnothing} +\newcommand{\rel}{\mathbin\leftrightarrow} +\newcommand{\trel}{\mathbin{\leftarrow\mkern-14mu\leftrightarrow}} +\newcommand{\srel}{\mathbin{\leftrightarrow\mkern-14mu\rightarrow}} +\newcommand{\strel}{\mathbin{\leftrightarrow\mkern-14mu\leftrightarrow}} +\bsymb@defop{\dom}{\mathrm{dom}} +\bsymb@defop{\ran}{\mathrm{ran}} +\newcommand{\fcomp}{\mathbin;} +\newcommand{\bcomp}{\circ} +\bsymb@defop{\id}{\mathrm{id}} +\newcommand{\domres}{\mathbin\lhd} +\newcommand{\domsub}{\mathbin{\lhd\mkern-14mu-}} +\newcommand{\ranres}{\mathbin\rhd} +\newcommand{\ransub}{\mathbin{\rhd\mkern-14mu-}} +\newcommand{\ovl}{\mathbin{\lhd\mkern-9mu-}} +\newcommand{\dprod}{\mathbin\otimes} +\bsymb@defop{\prjone}{\mathrm{prj}_1} +\bsymb@defop{\prjtwo}{\mathrm{prj}_2} +\newcommand{\pprod}{\mathbin\|} +\newcommand{\bsymb@partial}[2]{ + \mathbin{\mkern#2mu\mapstochar\mkern-#2mu#1} +} +\newcommand{\pfun}{\bsymb@partial\rightarrow6} +\newcommand{\tfun}{\mathbin\rightarrow} +\newcommand{\pinj}{\bsymb@partial\rightarrowtail9} +\newcommand{\tinj}{\mathbin\rightarrowtail} +\newcommand{\psur}{\bsymb@partial\twoheadrightarrow6} +\newcommand{\tsur}{\mathbin\twoheadrightarrow} +\newcommand{\tbij}{\mathbin{ + \rightarrowtail + \mkern-18mu\twoheadrightarrow} +} +\bsymb@defop{\fin}{\mathbb F\hbox{}} +\bsymb@defop{\finn}{\mathbb F_1} +\bsymb@deford{\nat}{\mathbb N} +\bsymb@deford{\natn}{\mathbb N_1} +\bsymb@deford{\intg}{\mathbb Z} +\bsymb@defop{\card}{\mathrm{card}} +\newcommand{\upto}{\mathbin{.\mkern1mu.}} +\bsymb@defop{\upred}{\mathrm{pred}} +\bsymb@defop{\usucc}{\mathrm{succ}} +\newcommand\expn{\mathbin{\widehat{\enskip}}} +\bsymb@deford{\Bool}{\mathrm{BOOL}} +\bsymb@deford{\True}{\mathrm{TRUE}} +\bsymb@deford{\False}{\mathrm{FALSE}} +\bsymb@defop{\bool}{\mathrm{bool}} +\newcommand{\bcmeq}{\mathrel{:\mkern1mu=}} +\newcommand{\bcmin}{\mathrel{:\mkern1mu\in}} +\newcommand{\bcmsuch}{\mathrel{:\mkern1mu\mid}} + +\endinput +%% +%% End of file `bsymb.sty'. diff --git a/org.rodinp.handbook.feature/latex/faq.tex b/org.rodinp.handbook.feature/latex/faq.tex new file mode 100644 index 0000000000000000000000000000000000000000..2e56b28ac4092c3ad647866232d2b567001deb68 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/faq.tex @@ -0,0 +1,30 @@ +\chapter{Frequently Asked Questions} + +\section{General Questions} + +\subsection{What is Event-B?} + +Event-B is a formal method for system-level modelling and analysis. Key features of event-B are the use of set theory as a modelling notation, the use of refinement to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. +More details are available in \url{http://www.event-b.org}. + +\subsection{What is the difference between Event-B and the B method?} + +Event-B (\ref{event-b}) is derived from the B method. Both notations have the same inventor, and share many common concepts (set-theory, refinement, proof obligations, ...) However, they are used for quite different purpose. The B method is devoted to the development of correct by construction software, while the purpose of event-B is to model full systems (including hardware, software and environment of operation). + +Both notations use a mathematical language which are quite close but do not match exactly (in particular, operator precedences are different). + +\subsection{What is Rodin?} + +The Rodin Platform is an Eclipse-based IDE for Event-B that provides effective support for refinement and mathematical proof. The platform is open source, contributes to the Eclipse framework and is further extendable with plugins. + +\subsection{Where does the Rodin name come from?} + +The Rodin Platform (\ref{rodin_platform}) was initially developed within the European Commission funded Rodin project (IST-511599 ), where Rodin is an acronym for "Rigorous Open Development Environment for Complex Systems” . Rodin is also the name of a famous French sculptor, one of his most famous work being the Thinker. + +\section{Installation Questions} + +\section{Proofer Questions} + +\section{Usage Questions} + +\section{Plug-In Questions} diff --git a/org.rodinp.handbook.feature/latex/files/sld_mth1.pdf b/org.rodinp.handbook.feature/latex/files/sld_mth1.pdf new file mode 100644 index 0000000000000000000000000000000000000000..a5dddc8c62790fa7285ac0db0008955b926fdd66 Binary files /dev/null and b/org.rodinp.handbook.feature/latex/files/sld_mth1.pdf differ diff --git a/org.rodinp.handbook.feature/latex/img/info_64.png b/org.rodinp.handbook.feature/latex/img/info_64.png new file mode 100644 index 0000000000000000000000000000000000000000..4d166f512c5aaac0b7466681c603a04159721d58 Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/info_64.png differ diff --git a/org.rodinp.handbook.feature/latex/img/pencil_64.png b/org.rodinp.handbook.feature/latex/img/pencil_64.png new file mode 100644 index 0000000000000000000000000000000000000000..85448187bd2d3075dde6589c11d84a1fb443c4ca Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/pencil_64.png differ diff --git a/org.rodinp.handbook.feature/latex/img/tick_64.png b/org.rodinp.handbook.feature/latex/img/tick_64.png new file mode 100644 index 0000000000000000000000000000000000000000..f7d4a49af4d8bacecfe6658e42b5a42a38598928 Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/tick_64.png differ diff --git a/org.rodinp.handbook.feature/latex/img/tutorial/trafficlight.png b/org.rodinp.handbook.feature/latex/img/tutorial/trafficlight.png new file mode 100644 index 0000000000000000000000000000000000000000..b9c83ca86a8fdd47dd800950c48025ff0c60504d Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/tutorial/trafficlight.png differ diff --git a/org.rodinp.handbook.feature/latex/img/warning_64.png b/org.rodinp.handbook.feature/latex/img/warning_64.png new file mode 100644 index 0000000000000000000000000000000000000000..b1b5f0acd3b8d28f499b2fcc995711ce3b1cd585 Binary files /dev/null and b/org.rodinp.handbook.feature/latex/img/warning_64.png differ diff --git a/org.rodinp.handbook.feature/latex/plastex-b2latex.sty b/org.rodinp.handbook.feature/latex/plastex-b2latex.sty new file mode 100644 index 0000000000000000000000000000000000000000..5a05e32ec166265ad94d7abec09adfcd8c3868e3 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/plastex-b2latex.sty @@ -0,0 +1,124 @@ +%------------------------------------------------------------------- +% This is b2latex.sty, generated by B2Latex plugin on Rodin +% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk +% Copyright(c)2008 ECS @ University of Southampton +%------------------------------------------------------------------- +% This style file is required for all latex files generated by the +% B2Latex plugin 0.5.x. +% Each command mentioned below, can be modified for your own style +% but command names are not allowed. +% +%------------------------------------------------------------------- +% Defined colors. +%------------------------------------------------------------------- +\usepackage{color} +\definecolor{keycolor}{rgb}{0,0,0.7} %color of key words, blue is the default +\definecolor{labelcolor}{rgb}{0,0.4,0.8} %color of labels, cyan +\definecolor{codecolor}{rgb}{0,0.2,0} %color of formulas, black +\definecolor{xcodecolor}{rgb}{0,0,0} %color of extended formulas, black +\definecolor{cmtcolor}{rgb}{0,0,0} %color of comments, black + +%------------------------------------------------------------------- +\newcommand{\paraSpc} {\hspace*{\fill} \setlength{\parskip}{-2pt}} % reduce space between paras +%------------------------------------------------------------------- +\newcommand{\itemSpc} {\setlength{\itemsep}{-0pt}} % reduce space between para items +%------------------------------------------------------------------- +% Special commands for MACHINE +%------------------------------------------------------------------- +\newcommand{\MACHINE}[1] { \item[\textcolor{keycolor}{MACHINE } #1] \paraSpc } + +\newcommand{\REFINES}[1]{ \item[\textcolor{keycolor}{REFINES }] #1 \paraSpc } + +\newcommand{\SEES}[1]{ \item[\textcolor{keycolor}{SEES }] #1 \paraSpc } + +\newcommand{\VARIABLES}{\item[\textcolor{keycolor}{VARIABLES}] \paraSpc } + +\newcommand{\INVARIANTS}{ \item[\textcolor{keycolor}{INVARIANTS}] \paraSpc } + +\newcommand{\VARIANT}{ \item[\textcolor{keycolor}{VARIANT}] \paraSpc } + +\newcommand{\EVENTS}{ \item[\textcolor{keycolor}{EVENTS}] \paraSpc } + +\newcommand{\INITIALISATION}{ \item[\textcolor{keycolor}{Initialisation}] \paraSpc } + +\newcommand{\EVT}[1]{ \item[\textcolor{keycolor}{Event} \textit{#1} $\defi$ ] \paraSpc } % opt1 +% Option: deactivate above command and reactivate +% the command below to display only event name +%\newcommand{\EVT}[1]{ \item[\textit{#1}] $\defi$ \paraSpc } % opt2 + +\newcommand{\REF}[1]{ \item[\textcolor{keycolor}{refines}] \textit{#1} \paraSpc } + +\newcommand{\EXTD}[1]{ \item[\textcolor{keycolor}{extends}] \textit{#1} \paraSpc } + +\newcommand{\Status}[1]{ \item[\textcolor{keycolor}{Status}] #1 \paraSpc } + +\newcommand{\AnyPrm}{ \item[\textcolor{keycolor}{any}] \paraSpc \itemSpc } + +\newcommand{\WhereGrd}{ \item[\textcolor{keycolor}{where}] \paraSpc \itemSpc } + +\newcommand{\WhenGrd}{ \item[\textcolor{keycolor}{when}] \paraSpc \itemSpc } + +\newcommand{\Witnesses}{ \item[\textcolor{keycolor}{with}] \paraSpc \itemSpc } + +\newcommand{\ThenAct}{ \item[\textcolor{keycolor}{then}] \paraSpc \itemSpc } + +\newcommand{\BeginAct}{ \item[\textcolor{keycolor}{begin}] \paraSpc \itemSpc } + +\newcommand{\EndAct}{ \item[\textcolor{keycolor}{end}] \paraSpc } + +%------------------------------------------------------------------- +% Special commands for CONTEXT +%------------------------------------------------------------------- + +\newcommand{\CONTEXT}[1]{ \item[\textcolor{keycolor}{CONTEXT }] #1 \paraSpc } + +\newcommand{\EXTENDS}[1]{ \item[\textcolor{keycolor}{EXTENDS }] #1 \paraSpc } + +\newcommand{\SETS}{ \item[\textcolor{keycolor}{SETS}] \paraSpc } + +\newcommand{\CONSTANTS}{ \item[\textcolor{keycolor}{CONSTANTS}] \paraSpc } + +\newcommand{\THEOREMS}{ \item[\textcolor{keycolor}{THEOREMS}] \paraSpc } + +\newcommand{\AXIOMS}{ \item[\textcolor{keycolor}{AXIOMS}] \paraSpc } + +%------------------------------------------------------------------- +% General commands used in both machines and contexts +%------------------------------------------------------------------- + +% Specification Title +\newcommand{\BTitle}[3]{ +\item[\fbox{\parbox{6in}{\centering{~\\An Event-B Specification of #1 +\\Creation Date: #2 @ #3\\}}}] +} +% End of MACHINE or CONTEXT +\newcommand{\END}{ \item[\textcolor{keycolor}{END}] \hspace*{\fill} } + +% Printing non-labelled elements +% (i.e. variables, sets and constants) +% \newcommand{\Item}[1]{ \item[\textcolor{codecolor}{$\tt#1$}] \itemSpc } +\newcommand{\Item}[1]{$\tt#1$ \itemSpc } +\newcommand{\ItemX}[1]{ $\it#1$ \itemSpc } + +% Printing an element with label name +% (i.e. invariants, theorems, axioms, witnesses and actions) +% parameter #1 is a label name and #2 is its content +\newcommand{\nItem}[2]{ $\tt #1:$ $\tt #2$ \itemSpc } % opt1 +\newcommand{\nItemX}[2]{ $\tt #1: \it #2$ \itemSpc } % opt1 +% Below is an alternative command for printing with no label +%\newcommand{\nItem}[2]{ \item[] $#2$} % opt2 + +% Commentations, reselect the second option for displaying asterisks +% - Newline comment +\newcommand{\cmt}[1]{ \hspace*{\fill}\\\textcolor{cmtcolor}{ #1}} %opt1 +%\newcommand{\cmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt2 + +% - Back Comment, for variables, sets and constants +\newcommand{\bcmt}[1]{~~~ \textcolor{cmtcolor}{#1}} %opt1 +%\newcommand{\bcmt}[1]{~~~ $/\ast$ #1 $\ast/$} %opt2 +% Select opt3 or opt4 (including asterisks) if you want to display this kind of comments +% on the newline like the newline comment +%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ #1} %opt3 +%\newcommand{\bcmt}[1]{ \hspace*{\fill}\\ $/\ast$ #1 $\ast/$} % opt4 + +%------------------------------------------------------------------- diff --git a/org.rodinp.handbook.feature/latex/plastex-bsymb.sty b/org.rodinp.handbook.feature/latex/plastex-bsymb.sty new file mode 100644 index 0000000000000000000000000000000000000000..3e446a61f1a65ebc5a56db5bfe8c37c0db390cad --- /dev/null +++ b/org.rodinp.handbook.feature/latex/plastex-bsymb.sty @@ -0,0 +1,101 @@ +%% +%% This is file `bsymb.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% bsymb.dtx (with options: `package') +%% +%% This is a generated file. +%% +%% Copyright (C) 2004 by Laurent Voisin <laurent.voisin at inf.ethz.ch> +%% +%% This file may be distributed and/or modified under the +%% conditions of the LaTeX Project Public License, either version 1.3 +%% of this license or (at your option) any later version. +%% The latest version of this license is in: +%% +%% http://www.latex-project.org/lppl.txt +%% +%% and version 1.3 or later is part of all distributions of LaTeX +%% version 2003/12/01 or later. +%% +\NeedsTeXFormat{LaTeX2e}[1999/06/01] +\ProvidesPackage{bsymb} + [2005/04/27 v1.5 Symbols for the B language] +\RequirePackageWithOptions{amssymb} +\newcommand\bsymb@defop[2]{ + \newcommand{#1}{\mathop{#2}\nolimits} +} +\newcommand\bsymb@deford[2]{ + \newcommand{#1}{\mathord{#2}} +} +\bsymb@deford{\bfalse}{\bot} +\bsymb@deford{\btrue}{\top} +\newcommand{\limp}{\mathbin\Rightarrow} +\newcommand{\leqv}{\mathbin\Leftrightarrow} +\bsymb@deford{\qdot}{\mkern1mu\cdot\mkern1mu} +\newcommand\defi{\mathrel{\widehat=}} + +\bsymb@defop{\pow}{\mathbb P\hbox{}} +\bsymb@defop{\pown}{\mathbb P_1} +\newcommand{\cprod}{\mathbin\times} +\newcommand{\bunion}{\mathbin{\mkern1mu\cup\mkern1mu}} +\newcommand{\binter}{\mathbin{\mkern1mu\cap\mkern1mu}} +\bsymb@defop{\union}{\mathrm{union}} +\bsymb@defop{\inter}{\mathrm{inter}} +\newcommand{\Union}{\bigcup\nolimits} +\newcommand{\Inter}{\bigcap\nolimits} +\renewcommand{\emptyset}{\mathord\varnothing} +\newcommand{\rel}{\mathbin\leftrightarrow} +\newcommand{\trel}{\mathbin{\leftarrow\mkern-14mu\leftrightarrow}} +\newcommand{\srel}{\mathbin{\leftrightarrow\mkern-14mu\rightarrow}} +\newcommand{\strel}{\mathbin{\leftrightarrow\mkern-14mu\leftrightarrow}} +\bsymb@defop{\dom}{\mathrm{dom}} +\bsymb@defop{\ran}{\mathrm{ran}} +\newcommand{\fcomp}{\mathbin;} +\newcommand{\bcomp}{\circ} +\bsymb@defop{\id}{\mathrm{id}} +\newcommand{\domres}{\mathbin\lhd} +\newcommand{\domsub}{\mathbin{\lhd\mkern-14mu-}} +\newcommand{\ranres}{\mathbin\rhd} +\newcommand{\ransub}{\mathbin{\rhd\mkern-14mu-}} +\newcommand{\ovl}{\mathbin{\lhd\mkern-9mu-}} +\newcommand{\dprod}{\mathbin\otimes} +\bsymb@defop{\prjone}{\mathrm{prj}_1} +\bsymb@defop{\prjtwo}{\mathrm{prj}_2} +\newcommand{\pprod}{\mathbin\|} +\newcommand{\bsymb@partial}[2]{ + \mathbin{\mkern#2mu\mapstochar\mkern-#2mu#1} +} +\newcommand{\pfun}{\bsymb@partial\rightarrow6} +\newcommand{\tfun}{\mathbin\rightarrow} +\newcommand{\pinj}{\bsymb@partial\rightarrowtail9} +\newcommand{\tinj}{\mathbin\rightarrowtail} +\newcommand{\psur}{\bsymb@partial\twoheadrightarrow6} +\newcommand{\tsur}{\mathbin\twoheadrightarrow} +\newcommand{\tbij}{\mathbin{ + \rightarrowtail + \mkern-18mu\twoheadrightarrow} +} +\bsymb@defop{\fin}{\mathbb F\hbox{}} +\bsymb@defop{\finn}{\mathbb F_1} +\bsymb@deford{\nat}{\mathbb N} +\bsymb@deford{\natn}{\mathbb N_1} +\bsymb@deford{\intg}{\mathbb Z} +\bsymb@defop{\card}{\mathrm{card}} +\newcommand{\upto}{\mathbin{.\mkern1mu.}} +\bsymb@defop{\upred}{\mathrm{pred}} +\bsymb@defop{\usucc}{\mathrm{succ}} +\newcommand\expn{\mathbin{\widehat{\enskip}}} +\bsymb@deford{\Bool}{\mathrm{BOOL}} +\bsymb@deford{\True}{\mathrm{TRUE}} +\bsymb@deford{\False}{\mathrm{FALSE}} +\bsymb@defop{\bool}{\mathrm{bool}} +\newcommand{\bcmeq}{\mathrel{:\mkern1mu=}} +\newcommand{\bcmin}{\mathrel{:\mkern1mu\in}} +\newcommand{\bcmsuch}{\mathrel{:\mkern1mu\mid}} + +\endinput +%% +%% End of file `bsymb.sty'. diff --git a/org.rodinp.handbook.feature/latex/reference.tex b/org.rodinp.handbook.feature/latex/reference.tex new file mode 100644 index 0000000000000000000000000000000000000000..49bdcd0080fa8867bd8abbb04c4ad223c5e564ea --- /dev/null +++ b/org.rodinp.handbook.feature/latex/reference.tex @@ -0,0 +1,76 @@ +\chapter{Reference} + +\section{Arithmetic} +\label{arithmetic} + +\section{Eclipse} +\label{eclipse} + +... Eclipse Definition ... + +\section{Event-B} +\label{event-b} + +Event-B is a formal method (\ref{formal_method}) for system-level modelling and analysis. Key features of Event-B are the use of set theory (\ref{set_theory}) as a modelling notation, the use of refinement (\ref{refinement}) to represent systems at different abstraction levels and the use of mathematical proof to verify consistency between refinement levels. + +\paragraph{See Also:} +\begin{itemize} +\item \url{http://www.event-b.org} +\end{itemize} + +\section{First Order Predicate Calculus} +\label{first_order_predicate_calculus} + + +\section{Formal Method} +\label{formal_method} + +\section{IDE} +\label{ide} + +... IDE Definition ... + +\section{Naming Convention} +\label{naming_convention} + +In this section we describe a recommended naming convention. Good naming conventions save time -- and nerves. + +\section{Refinement} +\label{refinement} + +... Refinement Definition ... + +\subsection{Horizontal Refinement} +\label{horizontal_refinement} + +\subsection{Vertical Refinement} +\label{vertical_refinement} + +\subsection{Data Refinement} +\label{data_refinement} + +\paragraph*{See also:} +\begin{itemize} +\item Data refinement in the trafficlight tutorial (\ref{tutorial_tl_data_refinement}) +\end{itemize} + +\section{Propositional Calculus} +\label{propositional_calculus} + +\section{Rodin} +\label{rodin} + +... Rodin Definition ... + +\section{Rodin Platform} +\label{rodin_platform} + +... Rodin Platform Definition ... + +\section{Set Theory} +\label{set_theory} + +... Set Theory Definition ... + + + diff --git a/org.rodinp.handbook.feature/latex/rodin-doc.tex b/org.rodinp.handbook.feature/latex/rodin-doc.tex new file mode 100644 index 0000000000000000000000000000000000000000..83961da9ab6fc80fabfdd511af018f94388318b3 --- /dev/null +++ b/org.rodinp.handbook.feature/latex/rodin-doc.tex @@ -0,0 +1,63 @@ +\documentclass{book} +\usepackage{hyperref} +\usepackage{graphicx} +\usepackage{bsymb} +\usepackage{b2latex} +\usepackage{fancyhdr,lastpage,color} + +\def\doculist#1#2{ + \vspace{3mm} + \noindent + \begin{tabular}{lp{0.85\textwidth}} + \includegraphics[width=10mm]{#2} & \vspace{-10mm}#1\\ + \end{tabular} +} + +\def\tick#1{\doculist{#1}{img/tick_64.png}} +\def\info#1{\doculist{#1}{img/info_64.png}} +\def\warning#1{\doculist{#1}{img/warning_64.png}} +\def\pencil#1{\doculist{\vspace{-5mm}#1}{img/pencil_64.png}} + +\title{Rodin User Manual v.2.1.1} +\author{Sample of \LaTeX-based Documentation Overhaul\\ \\ +Contact Info: Michael Jastram \href{mailto:michael.jastram@formalmind.com}{michael.jastram@formalmind.com}} + +\begin{document} + +\maketitle + +\section*{Introduction} + +The Rodin (\ref{rodin_platform}) documentation needs improvement. This has been established at the Deyploy Exec Meeting in 2010. We've been collecting background information and the requirements in the \href{http://wiki.event-b.org/index.php/User_Documentation_Overhaul}{Rodin Wiki}. + +We are currently investigating various approaches to managing the documentation. The approach shown here will work as follows: + +\begin{itemize} +\item The documentation is kept as \LaTeX. +\item We keep the source in Subversion. That way anybody with access to Subversion can contribute. +\item By keeping the documentation in Subversion, we can keep Rodin and its documentation in sync. +\item We use \href{http://plastex.sourceforge.net/}{plasTeX} to generate HTML and Eclipse Help from the \LaTeX. plasTeX supports templates, so we can use different templates for the two versions (for instance, we would not generate navigation elements for Eclipse Help, as Eclipse Help itself provides navigation). +\end{itemize} + +This document demonstrates this approach with a very small portion of the existing Rodin documentation. Obviously, it is just a proof of concept. + +\section*{Conventions} + +We use the following conventions in this manual: + +\tick{Checklists and Milestones are designated with tick.} +\info{Usegful information and tricks are designated by the information sign.} +\warning{Potential problems and warnings are designated by a warning sign.} +\pencil{\begin{description} \item Examples and Code are designated by a pencil.\end{description}} + +The Rodin (\ref{rodin_platform}) documentation needs improvement. This has been established at the Deyploy Exec Meeting in 2010. We've been collecting background information and the requirements in the \href{http://wiki.event-b.org/index.php/User_Documentation_Overhaul}{Rodin Wiki}. + + +\input{tutorial} + +\input{reference} + +\input{faq} + +\end{document} + diff --git a/org.rodinp.handbook.feature/latex/tutorial.tex b/org.rodinp.handbook.feature/latex/tutorial.tex new file mode 100644 index 0000000000000000000000000000000000000000..589721fbb150418ae07a5d94421b04d7f4ad478c --- /dev/null +++ b/org.rodinp.handbook.feature/latex/tutorial.tex @@ -0,0 +1,171 @@ +\chapter{Tutorial} +\label{tutorial} + +This tutorial should provide the user with a tour through the most important functionalities of RODIN, so that he gets a understanding of how the program works. + +The tutorial doesn't contain all the knowledge that you require. Instead, it touches upon every concept - from installation to set theory to modeling and refinement - and helps you to find gaps in your knowledge. + +Before we build a first model, we will cover some basic math. + +\section{Theory to Get You Started} +\label{tutorial_theory} + +\tick{\textbf{Goals:} The focus of this section is to briefly cover all the required theory, and to provide pointers for further reading. Specifically, this includes Propositional Calculus, First Order Predicate Calculus, Set Theory and Arithmetic} + +\paragraph{See Also:} +\begin{itemize} +\item Mathematical Notation Slides \url{files/sld_mth1.pdf} +\end{itemize} + + +\section{Getting around Rodin} +\label{tutorial_2} + +\tick{\textbf{Goals:} In this section, we cover installation, the basic features of an Eclipse application, and the Rodin-specific GUI elements.} + + +\section{Example 1: A Trafficlight Controller} +\label{tutorial_3} + +\tick{\textbf{Goals:} The focus of this section is modeling. You will learn how to model a simple system (a traffic light controller). We will use this example to introduce the concept of refinement (\ref{refinement}). The proofs in this section should all be discharged automatically. } + +The following picture visualizes the problem we are going to solve: + +\begin{center} + \includegraphics[width=0.9\textwidth]{img/tutorial/trafficlight.png} +\end{center} + +The objective is to design the software for a controller that switches the trafficlights and that reacts to pedestrian requests to cross the street. + +We tackle the problem in multiple steps: + +\begin{enumerate} + \item We will abstract the problem and develop a refinement plan (\ref{tutorial_tl_problem_abstraction}) + \item We will implement the initial model (\ref{tutorial_tl_initial_model}) + \item We will perform Data Refinement (\ref{data_refinement}) +\end{enumerate} + +\subsection{Problem Abstraction} +\label{tutorial_tl_problem_abstraction} + +\subsection{Initial Model} +\label{tutorial_tl_initial_model} + +\subsubsection{Project Setup} + +First create a new Event-B Project \textsf{File $\rangle$ New $\rangle$ Event-B Project}. Give the project the name \texttt{trafficlight}. + +Next, create a Machine. Right-click the newly created project and select \textsf{New $\rangle$ Event-B Component}. Call the component \texttt{mac0}. + +\info{A good naming convention can save a lot of work. We have a recommended naming convention (\ref{naming_convention})} + +\subsubsection{System State} + +We will now add the variables that store the traffic light value as a boolean. + +\tick{A new variable requires three elements: The variable itself, the typing invariant and the initialization. But typically, we'd also add events that change the state. And there may be further invariants constraining the state.} + + + +\pencil{ +\begin{description} +\VARIABLES + \begin{description} + \Item{ cars\_go } + \end{description} +\INVARIANTS + \begin{description} + \nItemX{ inv1 }{ cars\_go \in BOOL } + \end{description} +\EVENTS + \INITIALISATION + \begin{description} + \BeginAct + \begin{description} + \nItemX{ act1 }{ cars\_go := FALSE } + \end{description} + \EndAct + \end{description} +\END +\end{description} +} + + +\info{There are various ways to accelerate the creation of variables. The structural editor has a wizard for this purpose.} + +\pencil{ +\begin{description} +\MACHINE{mac0} +\VARIABLES + \begin{description} + \Item{ cars\_go } + \Item{ peds\_go } + \end{description} +\INVARIANTS + \begin{description} + \nItemX{ inv1 }{ cars\_go \in BOOL } + \nItemX{ inv2 }{ peds\_go \in BOOL } + \nItemX{ inv3 }{ \lnot (cars\_go = TRUE \land peds\_go = TRUE) } + \end{description} +\EVENTS + \INITIALISATION + \begin{description} + \BeginAct + \begin{description} + \nItemX{ act1 }{ cars\_go := FALSE } + \nItemX{ act2 }{ peds\_go := FALSE } + \end{description} + \EndAct + \end{description} + \EVT {cars\_light} + \begin{description} + \AnyPrm + \begin{description} + \ItemX{ new\_value } + \end{description} + \WhereGrd + \begin{description} + \nItemX{ grd1 }{ \lnot (new\_value = TRUE \land peds\_go = TRUE) } + \end{description} + \ThenAct + \begin{description} + \nItemX{ act1 }{ cars\_go := new\_value } + \end{description} + \EndAct + \end{description} + \EVT {peds\_light} + \begin{description} + \AnyPrm + \begin{description} + \ItemX{ new\_value } + \end{description} + \WhereGrd + \begin{description} + \nItemX{ grd1 }{ \lnot (cars\_go = TRUE \land new\_value = TRUE) } + \end{description} + \ThenAct + \begin{description} + \nItemX{ act1 }{ peds\_go := new\_value } + \end{description} + \EndAct + \end{description} +\END +\end{description} +} + +\subsection{Data Refinement: Introduce Trafficlight Colors} +\label{tutorial_tl_data_refinement} + + +- simple proofs +- refinement + +\section{Excurs: Data Structures} +\label{tutorial_4} + +\section{Excurs: Proofing} +\label{tutorial_5} + +\section{A more complex Example} + + diff --git a/org.rodinp.handbook.feature/org.rodinp.handbook.feature build.xml.launch b/org.rodinp.handbook.feature/org.rodinp.handbook.feature build.xml.launch new file mode 100644 index 0000000000000000000000000000000000000000..b6dc049f5fed983ee8f5d383480b712f18a54a7f --- /dev/null +++ b/org.rodinp.handbook.feature/org.rodinp.handbook.feature build.xml.launch @@ -0,0 +1,22 @@ +<?xml version="1.0" encoding="UTF-8" standalone="no"?> +<launchConfiguration type="org.eclipse.ant.AntLaunchConfigurationType"> +<booleanAttribute key="org.eclipse.ant.ui.DEFAULT_VM_INSTALL" value="true"/> +<stringAttribute key="org.eclipse.debug.core.ATTR_REFRESH_SCOPE" value="${working_set:<?xml version="1.0" encoding="UTF-8"?> <resources> <item path="/org.rodinp.help.feature" type="4"/> </resources>}"/> +<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS"> +<listEntry value="/org.rodinp.handbook.feature/build.xml"/> +</listAttribute> +<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES"> +<listEntry value="1"/> +</listAttribute> +<listAttribute key="org.eclipse.debug.ui.favoriteGroups"> +<listEntry value="org.eclipse.ui.externaltools.launchGroup"/> +</listAttribute> +<stringAttribute key="org.eclipse.jdt.launching.CLASSPATH_PROVIDER" value="org.eclipse.ant.ui.AntClasspathProvider"/> +<stringAttribute key="org.eclipse.jdt.launching.JRE_CONTAINER" value="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/java-6-openjdk"/> +<stringAttribute key="org.eclipse.jdt.launching.MAIN_TYPE" value="org.eclipse.ant.internal.launching.remote.InternalAntRunner"/> +<stringAttribute key="org.eclipse.jdt.launching.PROJECT_ATTR" value="org.rodinp.handbook.feature"/> +<stringAttribute key="org.eclipse.jdt.launching.SOURCE_PATH_PROVIDER" value="org.eclipse.ant.ui.AntClasspathProvider"/> +<stringAttribute key="org.eclipse.ui.externaltools.ATTR_LAUNCH_CONFIGURATION_BUILD_SCOPE" value="${none}"/> +<stringAttribute key="org.eclipse.ui.externaltools.ATTR_LOCATION" value="${workspace_loc:/org.rodinp.handbook.feature/build.xml}"/> +<stringAttribute key="process_factory_id" value="org.eclipse.ant.ui.remoteAntProcessFactory"/> +</launchConfiguration> diff --git a/org.rodinp.handbook.feature/skeleton/.project b/org.rodinp.handbook.feature/skeleton/.project new file mode 100644 index 0000000000000000000000000000000000000000..d60846fa4a3f1c1aa5a22ed75f14e204058c68b0 --- /dev/null +++ b/org.rodinp.handbook.feature/skeleton/.project @@ -0,0 +1,22 @@ +<?xml version="1.0" encoding="UTF-8"?> +<projectDescription> + <name>org.rodinp.handbook</name> + <comment></comment> + <projects> + </projects> + <buildSpec> + <buildCommand> + <name>org.eclipse.pde.ManifestBuilder</name> + <arguments> + </arguments> + </buildCommand> + <buildCommand> + <name>org.eclipse.pde.SchemaBuilder</name> + <arguments> + </arguments> + </buildCommand> + </buildSpec> + <natures> + <nature>org.eclipse.pde.PluginNature</nature> + </natures> +</projectDescription> diff --git a/org.rodinp.handbook.feature/skeleton/build.properties b/org.rodinp.handbook.feature/skeleton/build.properties new file mode 100644 index 0000000000000000000000000000000000000000..f750eeefb2bf2700799a2f418834e284de9c65cb --- /dev/null +++ b/org.rodinp.handbook.feature/skeleton/build.properties @@ -0,0 +1,6 @@ +bin.includes = plugin.xml,\ + *.xml,\ + *.html,\ + icons/,\ + images/,\ + styles/ diff --git a/org.rodinp.handbook.feature/skeleton/plugin.xml b/org.rodinp.handbook.feature/skeleton/plugin.xml new file mode 100644 index 0000000000000000000000000000000000000000..5ee36f5496cdca10c96b7597d0793fa0944aaede --- /dev/null +++ b/org.rodinp.handbook.feature/skeleton/plugin.xml @@ -0,0 +1,10 @@ +<?xml version='1.0' encoding='ISO-8859-1' ?> +<plugin + id="org.rodinp.handbook" + name="Rodin Handbook v.2.1.1" + version="1.0.0.qualifier" + provider-name="Formal Mind GmbH (formalmind.com)"> + <extension point="org.eclipse.help.toc"> + <toc primary="true" file="eclipse-toc.xml" /> + </extension> +</plugin>