# HG changeset patch # User wenzelm # Date 926342234 -7200 # Node ID 010dfaf75064094a862f991c7119d297f10715d2 # Parent 13293a7d4a57ee24a403441ae2b02a5d21d678a9 fixed URLs; diff -r 13293a7d4a57 -r 010dfaf75064 doc-src/manual.bib --- a/doc-src/manual.bib Mon May 10 15:16:49 1999 +0200 +++ b/doc-src/manual.bib Mon May 10 15:17:14 1999 +0200 @@ -547,7 +547,7 @@ note = {Beta release}, year = 1993, month = apr, - url = {\verb|http://www.csl.sri.com/reports/pvs-language.dvi.Z|}} + url = {\url{http://www.csl.sri.com/reports/pvs-language.dvi.Z}}} %P @@ -572,7 +572,7 @@ {Isabelle})}, pages = {246-274}, crossref = {colog88}, - url = {http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}} + url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR175-lcp-simple.dvi.gz}}} @Article{paulson-coind, author = {Lawrence C. Paulson}, @@ -603,7 +603,7 @@ number = 3, pages = {363-397}, year = 1989, - url = {http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}} + url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR130-lcp-generic-theorem-prover.dvi.gz}}} %replaces paulson-final @Article{paulson-mscs, @@ -670,7 +670,7 @@ volume = 3, pages = {237-258}, year = 1986, - url = {http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}} + url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR82-lcp-higher-order-resolution.dvi.gz}}} @Article{paulson-set-I, author = {Lawrence C. Paulson}, @@ -692,7 +692,7 @@ number = 2, pages = {167-215}, year = 1995, - url = {http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}} + url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz}}} @article{paulson85, author = {Lawrence C. Paulson}, @@ -715,7 +715,7 @@ title = {{Isabelle}: The Next 700 Theorem Provers}, crossref = {odifreddi90}, pages = {361-386}, - url = {http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}} + url = {\url{http://www.cl.cam.ac.uk/Research/Reports/TR143-lcp-experience.dvi.gz}}} % replaces paulson-ns and paulson-security @Article{paulson-jcs, @@ -776,7 +776,7 @@ year = 1995, number = 364, month = may, - url = {http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}} + url = {\url{http://www.cl.cam.ac.uk:80/ftp/papers/reports/TR364-or200-church-rosser-isabelle.ps.gz}}} @Book{reeves90, author = {Steve Reeves and Michael Clarke}, diff -r 13293a7d4a57 -r 010dfaf75064 doc-src/url.sty --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/url.sty Mon May 10 15:17:14 1999 +0200 @@ -0,0 +1,268 @@ +% url.sty ver 1.1 6-Feb-1996 Donald Arseneau asnd@triumf.ca +% +% A form of \verb that allows linebreaks at certain characters or +% combinations of characters, accepts reconfiguration, and can usually +% be used in the argument to another command. It is intended for email +% addresses, hypertext links, directories/paths, etc., which normally +% have no spaces. The font may be selected using the \urlstyle command, +% and new url-like commands can be defined using \urldef. +% +% Usage: Conditions: +% \url{ } If the argument contains any "%", "#", or "^^", or ends with +% "\", it can't be used in the argument to another command. +% The argument must not contain unbalanced braces. +% \url| | ...where "|" is any character not used in the argument and not +% "{". The same restrictions as above except that the argument +% may contain unbalanced braces. +% \xyz for "\xyz" a defined-url; this can be used anywhere, no matter +% what characters it contains. +% +% See further instructions after "\endinput" + +\def\url@ttstyle{% +\@ifundefined{selectfont}{\def\UrlFont{\tt}}{\def\UrlFont{\ttfamily}}% +\def\UrlBreaks{\do\.\do\@\do\\\do\/\do\!\do\_\do\|\do\%\do\;\do\>\do\]% + \do\)\do\,\do\?\do\'\do\+\do\=\do@url@hyp}% +\def\UrlBigBreaks{\do\:}% +\def\UrlNoBreaks{\do\(\do\[\do\{\do\<}% (unnecessary) +\def\UrlSpecials{\do\ {\ }}% +\def\UrlOrds{\do\*\do\-}% any ordinary characters that aren't usually +} +\def\url@rmstyle{% +\@ifundefined{selectfont}{\def\UrlFont{\rm}}{\def\UrlFont{\rmfamily}}% +\def\UrlBreaks{\do\.\do\@\do\/\do\!\do\%\do\;\do\]\do\)\do\,\do\?\do@url@hyp + \do\+\do\=}% +\def\UrlBigBreaks{\do\:}% +\def\UrlNoBreaks{\do\(\do\[\do\{}% prevents breaks after *next* character +\def\UrlSpecials{\do\<{\langle}\do\>{\rangle\penalty\relpenalty}\do\_{\_% + \penalty\@m}\do\|{\mid}\do\{{\lbrace}\do\}{\rbrace\penalty\relpenalty}\do + \\{\mathbin{\backslash}}\do\~{\mathord{{}^{\textstyle\sim}}}\do\ {\ }}% +\def\UrlOrds{\do\'\do\"\do\-}% +} +\def\url@sfstyle{\url@rmstyle +\@ifundefined{selectfont}{\def\UrlFont{\sf}}{\def\UrlFont{\sffamily}}% +} +\def\url@samestyle{\ifdim\fontdimen\thr@@\font=\z@ \url@ttstyle \else + \url@rmstyle \fi \def\UrlFont{}} + +\def\do@url@hyp{}% by default, no breaks after hyphens + +\@ifundefined{strip@prefix}{\def\strip@prefix#1>{}}{} +\@ifundefined{verbatim@nolig@list}{\def\verbatim@nolig@list{\do\`}}{} + +\def\Url{\relax\ifmmode\@nomatherr$\fi + \UrlFont $\fam\z@ \textfont\z@\font + \let\do\@makeother \dospecials % verbatim catcodes + \catcode`{\@ne \catcode`}\tw@ % except braces + \medmuskip0mu \thickmuskip\medmuskip \thinmuskip\medmuskip + \@tempcnta\fam\multiply\@tempcnta\@cclvi + \let\do\set@mathcode \UrlOrds % ordinary characters that were special + \advance\@tempcnta 8192 \UrlBreaks % bin + \advance\@tempcnta 4096 \UrlBigBreaks % rel + \advance\@tempcnta 4096 \UrlNoBreaks % open + \let\do\set@mathact \UrlSpecials % active + \let\do\set@mathnolig \verbatim@nolig@list % prevent ligatures + \@ifnextchar\bgroup\Url@z\Url@y} + +\def\Url@y#1{\catcode`{11 \catcode`}11 + \def\@tempa##1#1{\Url@z{##1}}\@tempa} +\def\Url@z#1{\def\@tempa{#1}\expandafter\expandafter\expandafter\Url@use + \expandafter\strip@prefix\meaning\@tempa\, \relax\m@th$\endgroup} +\let\Url@use\@empty + +\def\set@mathcode#1{\count@`#1\advance\count@\@tempcnta\mathcode`#1\count@} +\def\set@mathact#1#2{\mathcode`#132768 \lccode`\~`#1\lowercase{\def~{#2}}} +\def\set@mathnolig#1{\ifnum\mathcode`#1<32768 + \lccode`\~`#1\lowercase{\edef~{\mathchar\number\mathcode`#1_{\/}}}% + \mathcode`#132768 \fi} + +\def\urldef#1#2{\begingroup \setbox\z@\hbox\bgroup + \def\Url@z{\Url@def{#1}{#2}}#2} +\expandafter\ifx\csname DeclareRobustCommand\endcsname\relax + \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup + \def#1{#2{#3}}} +\else + \def\Url@def#1#2#3{\m@th$\endgroup\egroup\endgroup + \DeclareRobustCommand{#1}{#2{#3}}} +\fi + +\def\urlstyle#1{\csname url@#1style\endcsname} + +% Sample (and default) configuration: +% +\newcommand\url{\begingroup \Url} +% +\newcommand\path{\begingroup \urlstyle{tt}\Url} +% +% too many styles define \email like \address, so I will not define it. +% \newcommand\email{\begingroup \urlstyle{rm}\Url} + +% Process LaTeX \package options +% +\urlstyle{tt} +\@ifundefined{ProvidesPackage}{}{ + \ProvidesPackage{url}[1996/02/06 \space ver 1.1 \space + Verb mode for urls, email addresses, and file names] + \DeclareOption{hyphens}{\def\do@url@hyp{\do\-}}% allow breaks after hyphens + \DeclareOption{obeyspaces}{\let\Url@use\relax} + \ProcessOptions +\ifx\Url@use\relax \def\Url@use#1 #2{#1\ifx\relax#2\@empty\else + \penalty\relpenalty\ #2\expandafter\Url@use\fi}\fi +} + +\endinput +% +% url.sty ver 1.1 6-Feb-1996 Donald Arseneau asnd@reg.triumf.ca +% +% This package defines "\url", a form of "\verb" that allows linebreaks, +% and can often be used in the argument to another command. It can be +% configured to print in different formats, and is particularly useful for +% hypertext links, email addresses, directories/paths, etc. The font may +% be selected using the "\urlstyle" command and pre-defined text can be +% stored with the "\urldef" command. New url-like commands can be defined, +% and a "\path" command is provided this way. +% +% Usage: Conditions: +% \url{ } If the argument contains any "%", "#", or "^^", or ends with +% "\", it can't be used in the argument to another command. +% The argument must not contain unbalanced braces. +% \url| | ...where "|" is any character not used in the argument and not +% "{". The same restrictions as above except that the argument +% may contain unbalanced braces. +% \xyz for "\xyz" a defined-url; this can be used anywhere, no matter +% what characters it contains. +% +% The "\url" command is fragile, and its argument is likely to be very +% fragile, but a defined-url is robust. +% +% Package Option: obeyspaces +% Ordinarily, all spaces are ignored in the url-text. The "[obeyspaces]" +% option allows spaces, but may introduce spurious spaces when a url +% containing "\" characters is given in the argument to another command. +% So if you need to obey spaces should say "\usepackage[obeyspaces]{url}", +% and if you need both spaces and backslashes, use a `defined-url' for +% anything with "\". +% +% Package Option: hyphens +% Ordinarily, breaks are not allowed after "-" characters because this +% leads to confusion. (Is the "-" part of the address or just a hyphen?) +% The package option "[hyphens]" allows breaks after explicit hyphen +% characters. The "\url" command will *never ever* hyphenate words. +% +% Defining a defined-url: +% Take for example the email address "myself%node@gateway.net" which could +% not be given (using "\url" or "\verb") in a caption or parbox due to the +% percent sign. This address can be predefined with +% \urldef{\myself}\url{myself%node@gateway.net} or +% \urldef{\myself}\url|myself%node@gateway.net| +% and then you may use "\myself" instead of "\url{myself%node@gateway.net}" +% in an argument, and even in a moving argument like a caption because a +% defined-url is robust. +% +% Style: +% You can switch the style of printing using "\urlstyle{tt}", where "tt" +% can be any defined style. The pre-defined styles are "tt", "rm", "sf", +% and "same" which all allow the same linebreaks but different fonts -- +% the first three select a specific font and the "same" style uses the +% current text font. You can define your own styles with different fonts +% and/or line-breaking by following the explanations below. The "\url" +% command follows whatever the currently-set style dictates. +% +% Alternate commands: +% It may be desireable to have different things treated differently, each +% in a predefined style; e.g., if you want directory paths to always be +% in tt and email addresses to be rm, then you would define new url-like +% commands as follows: +% +% \newcommand\email{\begingroup \urlstyle{rm}\Url} +% \newcommand\directory{\begingroup \urlstyle{tt}\Url} +% +% You must follow this format closely, and NOTE that the final command is +% "\Url", not "\url". In fact, the "\directory" example is exactly the +% "\path" definition which is pre-defined in the package. If you look +% above, you will see that "\url" is defined with +% \newcommand\url{\begingroup \Url} +% I.e., using whatever url-style has been selected. +% +% You can make a defined-url for these other styles, using the usual +% "\urldef" command as in this example: +% +% \urldef{\myself}{\email}{myself%node.domain@gateway.net} +% +% which makes "\myself" act like "\email{myself%node.domain@gateway.net}", +% if the "\email" command is defined as above. The "\myself" command is +% robust. +% +% Defining styles: +% Before describing how to customize the printing style, it is best to +% mention something about the unusual implementation of "\url". Although +% the material is textual in nature, and the font specification required +% is a text-font command, the text is actually typeset in *math* mode. +% This allows the context-sensitive linebreaking, but also accounts for +% the default behavior of ignoring spaces. Now on to defining styles. +% +% To change the font or the list of characters that allow linebreaks, you +% could redefine the commands "\UrlFont", "\UrlBreaks", "\UrlSpecials" etc. +% directly in the document, but it is better to define a new `url-style' +% (following the example of "\url@ttstyle" and "\url@rmstyle") which defines +% all of "\UrlBigbreaks", "\UrlNoBreaks", "\UrlBreaks", "\UrlSpecials", and +% "\UrlFont". +% +% Changing font: +% The "\UrlFont" command selects the font. The definition of "\UrlFont" +% done by the pre-defined styles varies to cope with a variety of LaTeX +% font selection schemes, but it could be as simple as "\def\UrlFont{\tt}". +% In addition to setting "\UrlFont", some characters will probably need +% to be defined in the "\UrlSpecials" list because most fonts don't have +% all the standard input characters. See the definition of "\url@rmstyle", +% which implements "\urlstyle{rm}". Or even better, follow the definition +% of "\url@sfstyle", which executes "\url@rmstyle" and then redefines +% just "\UrlFont". The nominal format for each special character "c" +% in the "\UrlSpecials" list is: "\do\c{}", but you can +% include other definitions too. +% +% Changing linebreaks: +% The list of characters that allow line-breaks is given by "\UrlBreaks" +% and "\UrlBigBreaks", which have the format "\do\c" for character "c". +% The differences are that `BigBreaks' have a lower penalty and have +% different breakpoints when in sequence (as in "http://"): `BigBreaks' +% are treated as mathrels while `Breaks' are mathbins (see The TeXbook, +% p.170). In particular, a series of `BigBreak' characters will break at +% the end and only at the end; a series of `Break' characters will break +% after the first and after every following *pair*; there will be no +% break after a `Break' character if a `BigBreak' follows. In the case +% of "http://" it doesn't matter whether ":" is a `Break' or `BigBreak' -- +% the breaks are the same in either case; but for DECnet nodes with "::" +% it is important to prevent breaks *between* the colons, and that is why +% colons are `BigBreaks'. +% +% It is possible for characters to prevent breaks after the next following +% character (I use this for parentheses). Specify these in "\UrlNoBreaks". +% +% You can do arbitrarily complex things with characters by making them +% active in math mode (mathcode hex-8000) and specifying the definition(s) +% in "\UrlSpecials". This is used in the rm and sf styles to handle +% several characters that are not present in fonts. +% +% If all this sounds confusing ... well, it is! But I hope you won't need +% to redefine breakpoints -- the default assignments seem to work well for +% a wide variety of applications. If you do need to make changes, you can +% test for breakpoints using regular math mode and the characters "+=(a". +% +% Yet more flexibility: +% You can also set up url.sty to do multiple things with the verbatim text +% by defining "\Url@use", but the format of the definition is special: +% +% \def\Url@use#1\,{ ... do things with #1 ... } +% +% Yes, that is "#1" followed by "\," then the definition. For example, +% to put a hypertext link in the DVI file: +% +% \def\Url@use#1\,{\special{html:}#1\special{html:}} +% +% The End +% ver 1.1 6-Feb-1996: +% Fix hyphens that wouldn't break and ligatures that weren't suppressed. + +Test file integrity: ASCII 32-57, 58-126: !"#$%&'()*+,-./0123456789 +:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~