diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 13:34:29 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-03 13:34:29 +0000 |
| commit | 94bb3e91c134e09e194be2f8778ff5def909674d (patch) | |
| tree | 31d5f8ca2c602db7c9d8378d22402943f32c556f /etc/proviola | |
| parent | 9f8a026e13f358bb5565f21afe23f449c801d259 (diff) | |
Support files for Movie output
Diffstat (limited to 'etc/proviola')
| -rw-r--r-- | etc/proviola/README | 13 | ||||
| -rw-r--r-- | etc/proviola/movie-pp.rnc | 21 | ||||
| -rw-r--r-- | etc/proviola/movie.rnc | 12 | ||||
| -rw-r--r-- | etc/proviola/proviola-pp.xsl | 145 | ||||
| -rw-r--r-- | etc/proviola/proviola-spp.xsl | 158 | ||||
| -rw-r--r-- | etc/proviola/proviola.xsl | 151 |
6 files changed, 500 insertions, 0 deletions
diff --git a/etc/proviola/README b/etc/proviola/README new file mode 100644 index 00000000..81ba50eb --- /dev/null +++ b/etc/proviola/README @@ -0,0 +1,13 @@ +Experimental work-in-progress on "Movie" output from +annotated Proof General buffers. + +The XSL files here are due to Carst Tankink, copied from the Proviola +project. See http://mws.cs.ru.nl/proviola and these papers: + +Carst Tankink, Herman Geuvers, James McKinna, Freek Wiedijk +Proviola: a Tool for Proof Re-animation +MKM 2010. + +Carst Tankink, Herman Geuvers and James McKinna. +Narrating Formal Proof (Work in Progress) +UITP 2010. diff --git a/etc/proviola/movie-pp.rnc b/etc/proviola/movie-pp.rnc new file mode 100644 index 00000000..86ee33eb --- /dev/null +++ b/etc/proviola/movie-pp.rnc @@ -0,0 +1,21 @@ +default namespace = "" + +start = + element movie { + element film { + element frame { + attribute frameNumber { xsd:integer }, + element command { text }, + element response { text }, + element command-pp { part+ }, + element response-pp { part* } + }+ + } + } +part = + element part { + attribute class { classname }, + text + } + +classname = "plain" | "comment" | "obligation" | "label" diff --git a/etc/proviola/movie.rnc b/etc/proviola/movie.rnc new file mode 100644 index 00000000..685ae6fe --- /dev/null +++ b/etc/proviola/movie.rnc @@ -0,0 +1,12 @@ +default namespace = "" + +start = + element movie { + element film { + element frame { + attribute frameNumber { xsd:integer }, + element command { text }, + element response { text } + } + }+ + } diff --git a/etc/proviola/proviola-pp.xsl b/etc/proviola/proviola-pp.xsl new file mode 100644 index 00000000..24ca7839 --- /dev/null +++ b/etc/proviola/proviola-pp.xsl @@ -0,0 +1,145 @@ +<?xml version="1.0" encoding="ISO-8859-1"?> + +<xsl:stylesheet version="1.0" + xmlns:xsl="http://www.w3.org/1999/XSL/Transform"> + +<xsl:template match="/"> + <html> + <head> + <style type="text/css"> + body { + margin: 0px; + padding: 0px; + } + + div.commands { + margin: 0px; + padding: 0px; + width: 50%; + /* border-right: 1px solid #777; */ + } + + span.command:hover { + background-color: #ccc; + } + + div.goal { + position: fixed; + left: 50%; + bottom: 0px; + width: 50%; + margin: 0px; + padding-top: 100%; + border-left: 1px solid #777; + background-color: #fff; + } + + div.hidden { + display: none; + } + + pre { + padding: 4px 8px 4px 8px; + margin: 0px; + background-color: #fff; + } + + span.label { + color: #f00; + } + + span.comment { + color: #090; + } + + span.lemma { + color: #00f; + } + + span.obligation { + /* color: #c40; */ + color: #a0f; + } + </style> + <script type = "text/javascript"> + var plains = new Array(); + var obligations = new Array(); + + function mouseover(id) { + plain = getPlain(id); + obligation = getObligation(id); + setResponse(plain, obligation); + }; + + function set_array() { + <xsl:for-each select="movie/film/frame"> + i = <xsl:value-of select="@frameNumber"/>; + plains[i] =""; + obligations[i] = ""; + <xsl:for-each select="response-pp/part"> + <xsl:if test="@class = 'plain'"> + plains[i] = "<xsl:value-of select="translate(., '
', '	')"/>"; + </xsl:if> + <xsl:if test="@class = 'obligation'"> + + obligations[i] ="<xsl:value-of select="translate(., '
', '	')"/>"; + </xsl:if> + </xsl:for-each> + </xsl:for-each> + }; + + function getPlain(id) { + return plains[id]; + }; + + function getObligation(id) { + return obligations[id]; + }; + + function setResponse(plain, obligation) { + + goalSpans = document.getElementById("goal").getElementsByTagName("span"); + + goalSpans[0].innerHTML = plain.replace(/	/g, '\n'); + goalSpans[1].innerHTML = obligation.replace(/	/g, '\n'); + }; + </script> + </head> + + <body onload="set_array()"> + <div class = "commands"> + <pre> + <xsl:for-each select="movie/film/frame"> + <span class ="command"> + <xsl:attribute name="onmouseover"> + mouseover( + <xsl:value-of select="@frameNumber"/> + ) + </xsl:attribute> + + <xsl:for-each select="command-pp/part"> + <span> + <xsl:attribute name="class"> + <xsl:value-of select="@class"/> + </xsl:attribute> + <xsl:value-of select="."/> + </span> + </xsl:for-each> + + </span> + </xsl:for-each> + </pre> + </div> + + <div id="goal" class="goal"> + <pre> + <span class="context"> + </span> + <span class="obligation"> + </span> + </pre> + </div> + </body> + </html> +</xsl:template> +</xsl:stylesheet> diff --git a/etc/proviola/proviola-spp.xsl b/etc/proviola/proviola-spp.xsl new file mode 100644 index 00000000..29560167 --- /dev/null +++ b/etc/proviola/proviola-spp.xsl @@ -0,0 +1,158 @@ +<?xml version="1.0" encoding="ISO-8859-1"?> +<!-- Modified form of proviola.xsl, taken from + http://mws.cs.ru.nl/proviola 2/8/10. --> + +<xsl:stylesheet version="1.0" + xmlns:xsl="http://www.w3.org/1999/XSL/Transform"> + + +<xsl:template match="/"> + <html> + <head> + <style type="text/css"> + body { + margin: 0px; + padding: 0px; + } + + div.commands { + margin: 0px; + padding: 0px; + width: 50%; + /* border-right: 1px solid #777; */ + } + + span.command:hover { + background-color: #ccc; + } + + div.goal { + position: fixed; + left: 50%; + bottom: 0px; + width: 50%; + margin: 0px; + padding-top: 100%; + border-left: 1px solid #777; + background-color: #fff; + } + + div.hidden { + display: none; + } + + pre { + padding: 4px 8px 4px 8px; + margin: 0px; + background-color: #fff; + } + + span.label { + color: #f00; + } + + span.comment { + color: #090; + } + + span.lemma { + color: #00f; + } + + span.obligation { + /* color: #c40; */ + color: #a0f; + } + </style> + <script type = "text/javascript"> + var responses = new Array(); + + function mouseover(id) { + response = get_response(id); + set_response(response); + }; + + function set_array() { + <xsl:for-each select="movie/film/frame"> + <xsl:variable name="data"> + <xsl:call-template name="replace"> + <xsl:with-param name="string"> + <xsl:value-of + select="translate(response, '
', '	') "/> + </xsl:with-param> + <xsl:with-param name="from">"</xsl:with-param> + <xsl:with-param name="to">\"</xsl:with-param> + </xsl:call-template> + </xsl:variable> + + i = <xsl:value-of select="@frameNumber"/>; + data = "<xsl:value-of select="$data"/>"; + responses[i]=data; + </xsl:for-each> + }; + + function get_response(id) { + return responses[id]; + }; + + function set_response(response) { + goalSpan = document.getElementById("goal").getElementsByTagName("span")[0]; + goalSpan.innerHTML = response.replace(/	/g, '\n'); + }; + </script> + </head> + + <body onload="set_array()"> + <div class = "commands"> + <pre> + <xsl:for-each select="movie/film/frame"> + <span class ="command"> + <xsl:attribute name="onmouseover"> + mouseover( + <xsl:value-of select="@frameNumber"/> + ) + </xsl:attribute> + <span> + <xsl:attribute name="class"> + <xsl:value-of select="command/@class"/> + </xsl:attribute> + <xsl:value-of select="command"/> + </span> + </span> + </xsl:for-each> + </pre> + </div> + + <div id="goal" class="goal"> + <pre> + <span> + </span> + </pre> + </div> + </body> + </html> +</xsl:template> + +<xsl:template name="replace"> +<xsl:param name="string"/> + <xsl:param name="from"/> + <xsl:param name="to"/> + <xsl:choose> + <xsl:when test= "contains($string, $from)"> + <xsl:value-of select="substring-before($string, $from)"/> + <xsl:value-of select="$to"/> + <xsl:call-template name="replace"> + <xsl:with-param name="string" + select="substring-after($string, $from)"/> + <xsl:with-param name="from" select="$from"/> + <xsl:with-param name="to" select="$to"/> + </xsl:call-template> + </xsl:when> + <xsl:otherwise> + <xsl:value-of select="$string"/> + </xsl:otherwise> + </xsl:choose> +</xsl:template> + + +</xsl:stylesheet> diff --git a/etc/proviola/proviola.xsl b/etc/proviola/proviola.xsl new file mode 100644 index 00000000..1b6d1359 --- /dev/null +++ b/etc/proviola/proviola.xsl @@ -0,0 +1,151 @@ +<?xml version="1.0" encoding="ISO-8859-1"?> + +<xsl:stylesheet version="1.0" + xmlns:xsl="http://www.w3.org/1999/XSL/Transform"> + + +<xsl:template match="/"> + <html> + <head> + <style type="text/css"> + body { + margin: 0px; + padding: 0px; + } + + div.commands { + margin: 0px; + padding: 0px; + width: 50%; + /* border-right: 1px solid #777; */ + } + + span.command:hover { + background-color: #ccc; + } + + div.goal { + position: fixed; + left: 50%; + bottom: 0px; + width: 50%; + margin: 0px; + padding-top: 100%; + border-left: 1px solid #777; + background-color: #fff; + } + + div.hidden { + display: none; + } + + pre { + padding: 4px 8px 4px 8px; + margin: 0px; + background-color: #fff; + } + + span.label { + color: #f00; + } + + span.comment { + color: #090; + } + + span.lemma { + color: #00f; + } + + span.obligation { + /* color: #c40; */ + color: #a0f; + } + </style> + <script type = "text/javascript"> + var responses = new Array(); + + function mouseover(id) { + response = get_response(id); + set_response(response); + }; + + function set_array() { + <xsl:for-each select="movie/film/frame"> + <xsl:variable name="data"> + <xsl:call-template name="replace"> + <xsl:with-param name="string"> + <xsl:value-of + select="translate(response, '
', '	') "/> + </xsl:with-param> + <xsl:with-param name="from">"</xsl:with-param> + <xsl:with-param name="to">\"</xsl:with-param> + </xsl:call-template> + </xsl:variable> + + i = <xsl:value-of select="@frameNumber"/>; + data = "<xsl:value-of select="$data"/>"; + responses[i]=data; + </xsl:for-each> + }; + + function get_response(id) { + return responses[id]; + }; + + function set_response(response) { + goalSpan = document.getElementById("goal").getElementsByTagName("span")[0]; + goalSpan.innerHTML = response.replace(/	/g, '\n'); + }; + </script> + </head> + + <body onload="set_array()"> + <div class = "commands"> + <pre> + <xsl:for-each select="movie/film/frame"> + <span class ="command"> + <xsl:attribute name="onmouseover"> + mouseover( + <xsl:value-of select="@frameNumber"/> + ) + </xsl:attribute> + <xsl:value-of select="command"/> + </span> + </xsl:for-each> + </pre> + </div> + + <div id="goal" class="goal"> + <pre> + <span> + </span> + </pre> + </div> + </body> + </html> +</xsl:template> + +<xsl:template name="replace"> +<xsl:param name="string"/> + <xsl:param name="from"/> + <xsl:param name="to"/> + <xsl:choose> + <xsl:when test= "contains($string, $from)"> + <xsl:value-of select="substring-before($string, $from)"/> + <xsl:value-of select="$to"/> + <xsl:call-template name="replace"> + <xsl:with-param name="string" + select="substring-after($string, $from)"/> + <xsl:with-param name="from" select="$from"/> + <xsl:with-param name="to" select="$to"/> + </xsl:call-template> + </xsl:when> + <xsl:otherwise> + <xsl:value-of select="$string"/> + </xsl:otherwise> + </xsl:choose> +</xsl:template> + + +</xsl:stylesheet> |