From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 17 Jun 2004 13:48:56 +0000 (+0000)
Subject: - moogle replaces the old search engine
X-Git-Tag: pre_subst_in_kernel~26
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1063eca1bcf978717317356f493ef2a5e456b458;p=helm.git

- moogle replaces the old search engine
---

diff --git a/helm/on-line/xslt/resolve_topurl.xsl b/helm/on-line/xslt/resolve_topurl.xsl
index 4f794af39..695047108 100644
--- a/helm/on-line/xslt/resolve_topurl.xsl
+++ b/helm/on-line/xslt/resolve_topurl.xsl
@@ -1,6 +1,7 @@
 <?xml version="1.0"?>
 
 <xsl:stylesheet version="1.0" xmlns:xsl="http://www.w3.org/1999/XSL/Transform"
+                              xmlns:helm="http://www.cs.unibo.it/helm"
                               xmlns:subst="http://www.cs.unibo.it/helm/subst">
 
 <xsl:import href="links_library.xsl"/>
@@ -217,6 +218,58 @@
   </xsl:call-template>
 </xsl:template>
 
+<!-- used by moogle -->
+
+<xsl:template match="helm:uwobo_form">
+ <form action="{concat($processorURL,'apply?')}" method="get">
+  <xsl:apply-templates select="*"/>
+ </form>
+</xsl:template>
+
+<xsl:template match = "helm:hidden_params">
+ <xsl:call-template name="hidden_params"/>
+</xsl:template>
+
+<xsl:template match = "helm:j_params">
+ <xsl:call-template name="j_params"/>
+</xsl:template>
+
+<xsl:template name="hidden_params">
+ <input type="hidden" name="xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="param.profile" value="{$profile}"/>
+ <input type="hidden" name="profile" value="{$profile}"/>
+ <input type="hidden" name="param.keys" value="{$keys}"/>
+ <input type="hidden" name="param.embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="param.thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="param.prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="param.media-type" value="{$media-type}"/>
+ <input type="hidden" name="param.thmedia-type" select="{$thmedia-type}"/>
+ <input type="hidden" name="prooftreemedia-type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="param.doctype-public" select="{$doctype-public}"/>
+ <input type="hidden" name="param.encoding" select="{$encoding}"/>
+ <input type="hidden" name="param.thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="param.prooftreeencoding" select="{$prooftreeencoding}"/>
+</xsl:template>
+
+<xsl:template name="j_params">
+ <input type="hidden" name="j_xmluri" value="{concat($getterURL,'getempty')}"/>
+ <input type="hidden" name="j_processorURL" value="{$processorURL}"/> 
+ <input type="hidden" name="j_profile" value="{$profile}"/>
+ <input type="hidden" name="j_keys" value="{$keys}"/>
+ <input type="hidden" name="j_embedkeys" value="{$embedkeys}"/>
+ <input type="hidden" name="j_thkeys" value="{$thkeys}"/>
+ <input type="hidden" name="j_prooftreekeys" value="{$prooftreekeys}"/>
+
+ <input type="hidden" name="j_media_type" value="{$media-type}"/>
+ <input type="hidden" name="j_thmedia_type" select="{$thmedia-type}"/>
+ <input type="hidden" name="j_prooftreemedia_type" select="{$prooftreemedia-type}"/>
+ <input type="hidden" name="j_doctype_public" select="{$doctype-public}"/>
+ <input type="hidden" name="j_encoding" select="{$encoding}"/>
+ <input type="hidden" name="j_thencoding" select="{$thencoding}"/>
+ <input type="hidden" name="j_prooftreeencoding" select="{$prooftreeencoding}"/>
+</xsl:template>
+
 <xsl:template match="/|*">
  <xsl:copy>
   <xsl:copy-of select="@*"/>
diff --git a/helm/on-line/xslt/search.xsl b/helm/on-line/xslt/search.xsl
index 226b7d069..17fbee744 100644
--- a/helm/on-line/xslt/search.xsl
+++ b/helm/on-line/xslt/search.xsl
@@ -37,10 +37,12 @@
 
 <xsl:param name="action" select="''"/>
 <xsl:param name="expression" select="''"/>
+<xsl:param name="advanced" select="no"/>
 <xsl:param name="choices" select="''"/>
 <xsl:param name="interp" select="''"/>
 <xsl:param name="constraints" select="''"/>
 <xsl:param name="searchengineURL" select="''"/>
+<xsl:param name="url" select="''"/>
 
 <xsl:include href="links_library.xsl"/>
 
@@ -50,6 +52,12 @@
  </xsl:call-template>
 </xsl:variable>
 
+<xsl:variable name="quoted_url">
+ <xsl:call-template name="quote">
+  <xsl:with-param name="s" select="$url"/>
+ </xsl:call-template>
+</xsl:variable>
+
 <xsl:variable name="quoted_choices">
  <xsl:call-template name="quote">
   <xsl:with-param name="s" select="$choices"/>
@@ -74,7 +82,7 @@
 </xsl:variable>
 
 <xsl:template match="/">
- <xsl:copy-of select="document(concat($searchengineURL,$action,'?expression=',$quoted_expression,'&amp;choices=',$quoted_choices,'&amp;interpretation_choices=',$interp,$param_constraints))"/> 
+ <xsl:copy-of select="document(concat($searchengineURL,$action,'?expression=',$quoted_expression,'&amp;advanced=',$advanced,'&amp;choices=',$quoted_choices,'&amp;interpretation_choices=',$interp,$param_constraints,'&amp;url=',$quoted_url,'&amp;preprocess=true'))"/> 
 </xsl:template>
 
 </xsl:stylesheet> 
diff --git a/helm/on-line/xslt/toplevel_header.xsl b/helm/on-line/xslt/toplevel_header.xsl
index d8fdb2f42..88650a5a7 100644
--- a/helm/on-line/xslt/toplevel_header.xsl
+++ b/helm/on-line/xslt/toplevel_header.xsl
@@ -5,6 +5,8 @@
   xmlns:helm="http://www.cs.unibo.it/helm"
   xmlns:html="http://www.w3.org/1999/xhtml">
 
+<xsl:include href="links_library.xsl" />
+
 <!-- add theory's breadcrumb trail -->
 <xsl:template name="breadcrumb_trail">
   <xsl:param name="path" select="''" />
@@ -68,7 +70,10 @@
       <html:td style="text-align:right"><xsl:text>
 	</xsl:text>
 	<html:span style="font-family:sans-serif">
-	  [<html:a href="http://mowgli.cs.unibo.it:58085/getpage?url=index.html&amp;preprocess=true&amp;param.keys=d_c%2CC1%2CHC2%2CL&amp;param.thkeys=T1%2CT2%2CL%2CE&amp;param.embedkeys=d_c%2CTC1%2CHC2%2CL&amp;param.doctype-public=-//W3C//DTD%20XHTML%201.0%20Transitional//EN&amp;param.encoding=iso-8859-1&amp;param.thencoding=iso-8859-1&amp;param.media-type=text/html&amp;param.thmedia-type=text/html&amp;param.CICURI=dummy:query_result&amp;param.naturalLanguage=yes&amp;param.annotations=no&amp;param.processorURL=http://mowgli.cs.unibo.it:58080/" target="_top">search</html:a>]
+	  <xsl:variable name="searchLinkURL">
+	    <xsl:call-template name="makeSearchLinkURL" />
+	  </xsl:variable>
+	  [<html:a href="{$searchLinkURL}" target="_top">search</html:a>]
 	</html:span><xsl:text>
       </xsl:text>
       </html:td><xsl:text>