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{|}~