Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Fri, 4 Feb 1994 21:47:25 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA10923;
          Fri, 4 Feb 1994 14:18:41 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA10919;
          Fri, 4 Feb 1994 14:16:39 -0700
Received: from pdxgate.cs.pdx.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA29466;
          Fri, 4 Feb 1994 13:14:11 -0800
Received: from draco.cs.pdx.edu 
          by pdxgate.cs.pdx.edu (4.1/pdx-gateway-evision: 1.31 id AA11761;
          Fri, 4 Feb 94 13:13:54 PST
Received: from draco.cs.pdx.edu 
          by draco.cs.pdx.edu (4.1/pdx-client-evision: 1.21 id AA02022;
          Fri, 4 Feb 94 13:13:52 PST
Message-Id: <9402042113.AA02022@draco.cs.pdx.edu>
To: Wai Wong <Wai.Wong@cl.cam.ac.uk>
Cc: info-hol@cs.uidaho.edu (info-hol mailing list)
Subject: Re: Finding a theorem whose name I know
In-Reply-To: Your message of Fri, 04 Feb 94 08:57:50 +0000. <"swan.cl.cam.:270340:940204085801"@cl.cam.ac.uk>
Date: Fri, 04 Feb 94 13:13:52 PST
From: schubert@cs.pdx.edu


Following up on Wai's suggestion, I've made a couple very simple changes to
xholhelp that others may find useful.  Frequently, I want to provide xholhelp
with more than one string to limit the theorem search.

For example, I might begin by asking for all theorms about "LESS." Discovering
that there are 80 such theorems, I might wish to restrict my search so that I
only see those that also match with "ADD."  Additionally, the order of the two
strings shouldn't matter.  That is, I want to find all theorems that match the
patterns:

         *LESS*ADD*
    and  *ADD*LESS*

for which, there are 17 matches.

The first change below permits the entry of multiple (blank separated) strings
in the xholhelp dialog box.  The second change replaces the hol_thm script to
allow searches with up to three string parameters.  Similar changes could be
made for apropos...  Unfortunately, there are sometimes duplications
(e.g. LESS_SUB_ADD_LESS matches twice).

-Tom

---------------------------------------------------------------
CHANGES:

 1) In xholhelp.c, procedure doT()
      Change line 287 from   strcat(callsed, "hol_thm \""); 
                      to     strcat(callsed, "hol_thm ");

      Delete line 289        strcat(callsed, "\"");

    With this change, xholhelp passes multiple arguments to hol_thm, rather
    than a single argument.
      
 2) Replace hol_thm with the following (modifying ORIG_DIR and ORIG_HELP_PATH
    appropriately):


THMSED=ORIG_DIR/h_thm.sed
DEFTHMHELPPATH=ORIG_HELP_PATH/THEOREMS/*
CUR_HELP_PATH=`echo ${THM_HELP_PATH} ${DEFTHMHELPPATH} |sed 's/ /:/g'`
CUR_HELP_PATH=`echo ${THM_HELP_PATH} ${DEFTHMHELPPATH} |sed 's/ /:/g'`

for i in `echo $CUR_HELP_PATH | sed 's/^:/.:/
				s/::/:.:/g
				s/:$/:./
				s/:/ /g'`
do
     if /bin/test $# -eq 1
        then
	for j in $i/*${1}*.doc
	do
	if test -f $j
	then
		sed -f $THMSED $j
		echo ""
	fi
	done
     else 
        if /bin/test $# -eq 2
	then
	for j in $i/*${1}*${2}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${2}*${1}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
     else 
        if /bin/test $# -ge 3
	then
	for j in $i/*${1}*${2}*${3}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${2}*${1}*${3}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${3}*${1}*${2}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${3}*${2}*${1}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${1}*${3}*${2}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
	for j in $i/*${2}*${3}*${1}*.doc
	  do  if test -f $j; then sed -f $THMSED $j;echo "" ;fi; done
     fi
   fi
 fi
done