fixed URLs;
authorwenzelm
Mon May 10 15:17:14 1999 +0200 (1999-05-10)
changeset 6619010dfaf75064
parent 6618 13293a7d4a57
child 6620 fc991461c7b9
fixed URLs;
doc-src/manual.bib
doc-src/url.sty
     1.1 --- a/doc-src/manual.bib	Mon May 10 15:16:49 1999 +0200
     1.2 +++ b/doc-src/manual.bib	Mon May 10 15:17:14 1999 +0200
     1.3 @@ -547,7 +547,7 @@
     1.4    note		= {Beta release},
     1.5    year		= 1993,
     1.6    month		= apr,
     1.7 -  url		= {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}}
     1.8 +  url		= {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}}
     1.9  
    1.10  %P
    1.11  
    1.12 @@ -572,7 +572,7 @@
    1.13  		 {Isabelle})}, 
    1.14    pages		= {246-274},
    1.15    crossref	= {colog88},
    1.16 -  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}
    1.17 +  url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}}
    1.18  
    1.19  @Article{paulson-coind,
    1.20    author	= {Lawrence C. Paulson},
    1.21 @@ -603,7 +603,7 @@
    1.22    number	= 3,
    1.23    pages		= {363-397},
    1.24    year		= 1989,
    1.25 -  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}
    1.26 +  url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}}
    1.27  
    1.28  %replaces paulson-final
    1.29  @Article{paulson-mscs,
    1.30 @@ -670,7 +670,7 @@
    1.31    volume	= 3,
    1.32    pages		= {237-258},
    1.33    year		= 1986,
    1.34 -  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}
    1.35 +  url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}}
    1.36  
    1.37  @Article{paulson-set-I,
    1.38    author	= {Lawrence C. Paulson},
    1.39 @@ -692,7 +692,7 @@
    1.40    number	= 2,
    1.41    pages		= {167-215},
    1.42    year		= 1995,
    1.43 -  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}
    1.44 +  url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}}
    1.45  
    1.46  @article{paulson85,
    1.47    author	= {Lawrence C. Paulson},
    1.48 @@ -715,7 +715,7 @@
    1.49    title		= {{Isabelle}: The Next 700 Theorem Provers},
    1.50    crossref	= {odifreddi90},
    1.51    pages		= {361-386},
    1.52 -  url		= {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}
    1.53 +  url		= {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}}
    1.54  
    1.55  % replaces paulson-ns and paulson-security
    1.56  @Article{paulson-jcs,
    1.57 @@ -776,7 +776,7 @@
    1.58    year		= 1995,
    1.59    number	= 364,
    1.60    month		= may,
    1.61 -  url		= {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}
    1.62 +  url		= {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}}
    1.63  
    1.64  @Book{reeves90,
    1.65    author	= {Steve Reeves and Michael Clarke},
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/url.sty	Mon May 10 15:17:14 1999 +0200
     2.3 @@ -0,0 +1,268 @@
     2.4 +% url.sty  ver 1.1    6-Feb-1996   Donald Arseneau   asnd@triumf.ca
     2.5 +%
     2.6 +% A form of \verb that allows linebreaks at certain characters or 
     2.7 +% combinations of characters, accepts reconfiguration, and can usually
     2.8 +% be used in the argument to another command.  It is intended for email
     2.9 +% addresses, hypertext links, directories/paths, etc., which normally 
    2.10 +% have no spaces.  The font may be selected using the \urlstyle command, 
    2.11 +% and new url-like commands can be defined using \urldef.
    2.12 +%
    2.13 +% Usage:    Conditions:
    2.14 +% \url{ }   If the argument contains any "%", "#", or "^^", or ends with
    2.15 +%           "\", it can't be used in the argument to another command.  
    2.16 +%           The argument must not contain unbalanced braces.
    2.17 +% \url|  |  ...where "|" is any character not used in the argument and not 
    2.18 +%           "{".  The same restrictions as above except that the argument
    2.19 +%           may contain unbalanced braces.
    2.20 +% \xyz      for "\xyz" a defined-url;  this can be used anywhere, no matter
    2.21 +%           what characters it contains.
    2.22 +% 
    2.23 +% See further instructions after "\endinput"
    2.24 +
    2.25 +\def\url@ttstyle{%
    2.26 +\@ifundefined{selectfont}{\def\UrlFont{\tt}}{\def\UrlFont{\ttfamily}}% 
    2.27 +\def\UrlBreaks{\do\.\do\@\do\\\do\/\do\!\do\_\do\|\do\%\do\;\do\>\do\]%
    2.28 + \do\)\do\,\do\?\do\'\do\+\do\=\do@url@hyp}%
    2.29 +\def\UrlBigBreaks{\do\:}%
    2.30 +\def\UrlNoBreaks{\do\(\do\[\do\{\do\<}% (unnecessary)
    2.31 +\def\UrlSpecials{\do\ {\ }}%
    2.32 +\def\UrlOrds{\do\*\do\-}% any ordinary characters that aren't usually
    2.33 +}
    2.34 +\def\url@rmstyle{%
    2.35 +\@ifundefined{selectfont}{\def\UrlFont{\rm}}{\def\UrlFont{\rmfamily}}% 
    2.36 +\def\UrlBreaks{\do\.\do\@\do\/\do\!\do\%\do\;\do\]\do\)\do\,\do\?\do@url@hyp
    2.37 +  \do\+\do\=}%
    2.38 +\def\UrlBigBreaks{\do\:}%
    2.39 +\def\UrlNoBreaks{\do\(\do\[\do\{}% prevents breaks after *next* character
    2.40 +\def\UrlSpecials{\do\<{\langle}\do\>{\rangle\penalty\relpenalty}\do\_{\_%
    2.41 + \penalty\@m}\do\|{\mid}\do\{{\lbrace}\do\}{\rbrace\penalty\relpenalty}\do
    2.42 + \\{\mathbin{\backslash}}\do\~{\mathord{{}^{\textstyle\sim}}}\do\ {\ }}%
    2.43 +\def\UrlOrds{\do\'\do\"\do\-}%
    2.44 +}
    2.45 +\def\url@sfstyle{\url@rmstyle 
    2.46 +\@ifundefined{selectfont}{\def\UrlFont{\sf}}{\def\UrlFont{\sffamily}}% 
    2.47 +}
    2.48 +\def\url@samestyle{\ifdim\fontdimen\thr@@\font=\z@ \url@ttstyle \else
    2.49 +  \url@rmstyle \fi \def\UrlFont{}}
    2.50 +
    2.51 +\def\do@url@hyp{}% by default, no breaks after hyphens
    2.52 +
    2.53 +\@ifundefined{strip@prefix}{\def\strip@prefix#1>{}}{}
    2.54 +\@ifundefined{verbatim@nolig@list}{\def\verbatim@nolig@list{\do\`}}{}
    2.55 +
    2.56 +\def\Url{\relax\ifmmode\@nomatherr$\fi 
    2.57 + \UrlFont $\fam\z@ \textfont\z@\font 
    2.58 + \let\do\@makeother \dospecials % verbatim catcodes
    2.59 + \catcode`{\@ne \catcode`}\tw@ % except braces 
    2.60 + \medmuskip0mu \thickmuskip\medmuskip \thinmuskip\medmuskip
    2.61 + \@tempcnta\fam\multiply\@tempcnta\@cclvi 
    2.62 + \let\do\set@mathcode \UrlOrds % ordinary characters that were special
    2.63 + \advance\@tempcnta 8192 \UrlBreaks % bin
    2.64 + \advance\@tempcnta 4096 \UrlBigBreaks % rel
    2.65 + \advance\@tempcnta 4096 \UrlNoBreaks % open
    2.66 + \let\do\set@mathact \UrlSpecials % active
    2.67 + \let\do\set@mathnolig \verbatim@nolig@list % prevent ligatures 
    2.68 + \@ifnextchar\bgroup\Url@z\Url@y}
    2.69 +
    2.70 +\def\Url@y#1{\catcode`{11 \catcode`}11
    2.71 +  \def\@tempa##1#1{\Url@z{##1}}\@tempa}
    2.72 +\def\Url@z#1{\def\@tempa{#1}\expandafter\expandafter\expandafter\Url@use
    2.73 +  \expandafter\strip@prefix\meaning\@tempa\, \relax\m@th$\endgroup}
    2.74 +\let\Url@use\@empty
    2.75 +
    2.76 +\def\set@mathcode#1{\count@`#1\advance\count@\@tempcnta\mathcode`#1\count@}
    2.77 +\def\set@mathact#1#2{\mathcode`#132768 \lccode`\~`#1\lowercase{\def~{#2}}}
    2.78 +\def\set@mathnolig#1{\ifnum\mathcode`#1<32768
    2.79 +   \lccode`\~`#1\lowercase{\edef~{\mathchar\number\mathcode`#1_{\/}}}%
    2.80 +   \mathcode`#132768 \fi}
    2.81 +
    2.82 +\def\urldef#1#2{\begingroup \setbox\z@\hbox\bgroup
    2.83 +  \def\Url@z{\Url@def{#1}{#2}}#2}
    2.84 +\expandafter\ifx\csname DeclareRobustCommand\endcsname\relax
    2.85 +  \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup
    2.86 +    \def#1{#2{#3}}}
    2.87 +\else
    2.88 +  \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup
    2.89 +    \DeclareRobustCommand{#1}{#2{#3}}}
    2.90 +\fi
    2.91 +
    2.92 +\def\urlstyle#1{\csname url@#1style\endcsname}
    2.93 +
    2.94 +% Sample (and default) configuration:
    2.95 +%
    2.96 +\newcommand\url{\begingroup \Url}
    2.97 +%
    2.98 +\newcommand\path{\begingroup \urlstyle{tt}\Url}
    2.99 +%
   2.100 +% too many styles define \email like \address, so I will not define it.
   2.101 +% \newcommand\email{\begingroup \urlstyle{rm}\Url}
   2.102 +
   2.103 +% Process LaTeX \package options
   2.104 +%
   2.105 +\urlstyle{tt}
   2.106 +\@ifundefined{ProvidesPackage}{}{
   2.107 +  \ProvidesPackage{url}[1996/02/06 \space ver 1.1 \space 
   2.108 +       Verb mode for urls, email addresses, and file names]
   2.109 +  \DeclareOption{hyphens}{\def\do@url@hyp{\do\-}}% allow breaks after hyphens
   2.110 +  \DeclareOption{obeyspaces}{\let\Url@use\relax}
   2.111 +  \ProcessOptions
   2.112 +\ifx\Url@use\relax \def\Url@use#1 #2{#1\ifx\relax#2\@empty\else
   2.113 +  \penalty\relpenalty\ #2\expandafter\Url@use\fi}\fi
   2.114 +}
   2.115 +
   2.116 +\endinput
   2.117 +%
   2.118 +% url.sty  ver 1.1    6-Feb-1996   Donald Arseneau   asnd@reg.triumf.ca
   2.119 +%
   2.120 +% This package defines "\url", a form of "\verb" that allows linebreaks,
   2.121 +% and can often be used in the argument to another command.  It can be
   2.122 +% configured to print in different formats, and is particularly useful for 
   2.123 +% hypertext links, email addresses, directories/paths, etc.  The font may 
   2.124 +% be selected using the "\urlstyle" command and pre-defined text can be 
   2.125 +% stored with the "\urldef" command. New url-like commands can be defined, 
   2.126 +% and a "\path" command is provided this way. 
   2.127 +%
   2.128 +% Usage:    Conditions:
   2.129 +% \url{ }   If the argument contains any "%", "#", or "^^", or ends with 
   2.130 +%           "\", it can't be used in the argument to another command.  
   2.131 +%           The argument must not contain unbalanced braces.
   2.132 +% \url|  |  ...where "|" is any character not used in the argument and not 
   2.133 +%           "{".  The same restrictions as above except that the argument
   2.134 +%           may contain unbalanced braces.
   2.135 +% \xyz      for "\xyz" a defined-url;  this can be used anywhere, no matter
   2.136 +%           what characters it contains.
   2.137 +% 
   2.138 +% The "\url" command is fragile, and its argument is likely to be very
   2.139 +% fragile, but a defined-url is robust.
   2.140 +%
   2.141 +% Package Option:  obeyspaces
   2.142 +% Ordinarily, all spaces are ignored in the url-text.  The "[obeyspaces]" 
   2.143 +% option allows spaces, but may introduce spurious spaces when a url
   2.144 +% containing "\" characters is given in the argument to another command.  
   2.145 +% So if you need to obey spaces should say "\usepackage[obeyspaces]{url}",
   2.146 +% and if you need both spaces and backslashes, use a `defined-url' for 
   2.147 +% anything with "\".
   2.148 +%
   2.149 +% Package Option:  hyphens
   2.150 +% Ordinarily, breaks are not allowed after "-" characters because this 
   2.151 +% leads to confusion. (Is the "-" part of the address or just a hyphen?)  
   2.152 +% The package option "[hyphens]" allows breaks after explicit hyphen 
   2.153 +% characters.  The "\url" command will *never ever* hyphenate words.
   2.154 +% 
   2.155 +% Defining a defined-url:
   2.156 +% Take for example the email address "myself%node@gateway.net" which could
   2.157 +% not be given (using "\url" or "\verb") in a caption or parbox due to the
   2.158 +% percent sign.  This address can be predefined with 
   2.159 +%    \urldef{\myself}\url{myself%node@gateway.net}   or
   2.160 +%    \urldef{\myself}\url|myself%node@gateway.net|
   2.161 +% and then you may use "\myself" instead of "\url{myself%node@gateway.net}"
   2.162 +% in an argument, and even in a moving argument like a caption because a
   2.163 +% defined-url is robust.
   2.164 +%
   2.165 +% Style: 
   2.166 +% You can switch the style of printing using "\urlstyle{tt}", where "tt"
   2.167 +% can be any defined style.  The pre-defined styles are "tt", "rm", "sf", 
   2.168 +% and "same" which all allow the same linebreaks but different fonts -- 
   2.169 +% the first three select a specific font and the "same" style uses the
   2.170 +% current text font.  You can define your own styles with different fonts 
   2.171 +% and/or line-breaking by following the explanations below.  The "\url" 
   2.172 +% command follows whatever the currently-set style dictates.
   2.173 +%
   2.174 +% Alternate commands:
   2.175 +% It may be desireable to have different things treated differently, each
   2.176 +% in a predefined style; e.g., if you want directory paths to always be 
   2.177 +% in tt and email addresses to be rm, then you would define new url-like
   2.178 +% commands as follows:
   2.179 +%
   2.180 +%    \newcommand\email{\begingroup \urlstyle{rm}\Url}
   2.181 +%    \newcommand\directory{\begingroup \urlstyle{tt}\Url}
   2.182 +%
   2.183 +% You must follow this format closely, and NOTE that the final command is 
   2.184 +% "\Url", not "\url".  In fact, the "\directory" example is exactly the 
   2.185 +% "\path" definition which is pre-defined in the package.  If you look 
   2.186 +% above, you will see that "\url" is defined with
   2.187 +%    \newcommand\url{\begingroup \Url}
   2.188 +% I.e., using whatever url-style has been selected.
   2.189 +%
   2.190 +% You can make a defined-url for these other styles, using the usual 
   2.191 +% "\urldef" command as in this example:
   2.192 +%
   2.193 +%    \urldef{\myself}{\email}{myself%node.domain@gateway.net}
   2.194 +%
   2.195 +% which makes "\myself" act like "\email{myself%node.domain@gateway.net}",
   2.196 +% if the "\email" command is defined as above.  The "\myself" command is
   2.197 +% robust.
   2.198 +%
   2.199 +% Defining styles:
   2.200 +% Before describing how to customize the printing style, it is best to 
   2.201 +% mention something about the unusual implementation of "\url".  Although
   2.202 +% the material is textual in nature, and the font specification required
   2.203 +% is a text-font command, the text is actually typeset in *math* mode.
   2.204 +% This allows the context-sensitive linebreaking, but also accounts for
   2.205 +% the default behavior of ignoring spaces.  Now on to defining styles.
   2.206 +%
   2.207 +% To change the font or the list of characters that allow linebreaks, you
   2.208 +% could redefine the commands "\UrlFont", "\UrlBreaks", "\UrlSpecials" etc.
   2.209 +% directly in the document, but it is better to define a new `url-style' 
   2.210 +% (following the example of "\url@ttstyle" and "\url@rmstyle") which defines 
   2.211 +% all of "\UrlBigbreaks", "\UrlNoBreaks", "\UrlBreaks", "\UrlSpecials", and 
   2.212 +% "\UrlFont".
   2.213 +%
   2.214 +% Changing font:
   2.215 +% The "\UrlFont" command selects the font.  The definition of "\UrlFont"
   2.216 +% done by the pre-defined styles varies to cope with a variety of LaTeX
   2.217 +% font selection schemes, but it could be as simple as "\def\UrlFont{\tt}".
   2.218 +% In addition to setting "\UrlFont", some characters will probably need 
   2.219 +% to be defined in the "\UrlSpecials" list because most fonts don't have 
   2.220 +% all the standard input characters.  See the definition of "\url@rmstyle", 
   2.221 +% which implements "\urlstyle{rm}".  Or even better, follow the definition
   2.222 +% of "\url@sfstyle", which executes "\url@rmstyle" and then redefines
   2.223 +% just "\UrlFont".  The nominal format for each special character "c" 
   2.224 +% in the "\UrlSpecials" list is: "\do\c{<definition>}", but you can 
   2.225 +% include other definitions too.
   2.226 +%
   2.227 +% Changing linebreaks:
   2.228 +% The list of characters that allow line-breaks is given by "\UrlBreaks" 
   2.229 +% and "\UrlBigBreaks", which have the format "\do\c" for character "c". 
   2.230 +% The differences are that `BigBreaks' have a lower penalty and have 
   2.231 +% different breakpoints when in sequence (as in "http://"): `BigBreaks' 
   2.232 +% are treated as mathrels while `Breaks' are mathbins (see The TeXbook, 
   2.233 +% p.170). In particular, a series of `BigBreak' characters will break at 
   2.234 +% the end and only at the end; a series of `Break' characters will break 
   2.235 +% after the first and after every following *pair*; there will be no 
   2.236 +% break after a `Break' character if a `BigBreak' follows.  In the case 
   2.237 +% of "http://" it doesn't matter whether ":" is a `Break' or `BigBreak' --
   2.238 +% the breaks are the same in either case; but for DECnet nodes with "::"
   2.239 +% it is important to prevent breaks *between* the colons, and that is why 
   2.240 +% colons are `BigBreaks'.
   2.241 +%
   2.242 +% It is possible for characters to prevent breaks after the next following 
   2.243 +% character (I use this for parentheses).  Specify these in "\UrlNoBreaks". 
   2.244 +%
   2.245 +% You can do arbitrarily complex things with characters by making them 
   2.246 +% active in math mode (mathcode hex-8000) and specifying the definition(s)
   2.247 +% in "\UrlSpecials".  This is used in the rm and sf styles to handle 
   2.248 +% several characters that are not present in fonts.
   2.249 +%
   2.250 +% If all this sounds confusing ... well, it is!  But I hope you won't need 
   2.251 +% to redefine breakpoints -- the default assignments seem to work well for 
   2.252 +% a wide variety of applications.  If you do need to make changes, you can 
   2.253 +% test for breakpoints using regular math mode and the characters "+=(a".
   2.254 +%
   2.255 +% Yet more flexibility:
   2.256 +% You can also set up url.sty to do multiple things with the verbatim text
   2.257 +% by defining "\Url@use", but the format of the definition is special:
   2.258 +%
   2.259 +%    \def\Url@use#1\,{ ... do things with #1 ... }
   2.260 +%
   2.261 +% Yes, that is "#1" followed by "\," then the definition.  For example, 
   2.262 +% to put a hypertext link in the DVI file:
   2.263 +%
   2.264 +%    \def\Url@use#1\,{\special{html:<a href="#1">}#1\special{html:</a>}}
   2.265 +%
   2.266 +% The End
   2.267 +% ver 1.1 6-Feb-1996:  
   2.268 +% Fix hyphens that wouldn't break and ligatures that weren't suppressed.
   2.269 +
   2.270 +Test file integrity:  ASCII 32-57, 58-126:  !"#$%&'()*+,-./0123456789
   2.271 +:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~