traverseda
/
cpython
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Clean up the application of style to verbatim text. 

This moves styling to the stylesheet; the use of <dl> structures to control
style sometimes produced improper indentation of subsequent text in many
browsers when the text was already part of the <dl> structure (as in a
function or class description).
This commit is contained in:
Fred Drake 2002-04-15 18:41:31 +00:00
parent eeb5ec42e0
commit 8a5e6790d9
3 changed files with 10 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
Doc/html/style.css
View File

@ -65,9 +65,11 @@ var { font-family: times, serif;
.titlegraphic { vertical-align: top; }
.verbatim { color: #00008b;
.verbatim pre { color: #00008b;
font-family: lucida typewriter, lucidatypewriter,
monospace; }
monospace;
font-size: 90%; }
.verbatim { margin-left: 2em; }
.grammar { background-color: #99ccff;
margin-right: 0.5in;

2
Doc/perl/l2hinit.perl
View File

@ -577,7 +577,7 @@ sub set_depth_levels {
# initialize() is called in the main LaTeX2HTML script (which happens
# before style files are loaded).
#
%declarations = ('preform' => '<dl><dd><pre class="verbatim"></pre></dl>',
%declarations = ('preform' => '<div class="verbatim"><pre></pre></div>',
%declarations);

10
Doc/perl/python.perl
View File

@ -1915,8 +1915,8 @@ withsubitem # {} # {}
_RAW_ARG_DEFERRED_CMDS_
$alltt_start = '<dl><dd><pre class="verbatim">';
$alltt_end = '</pre></dl>';
$alltt_start = '<div class="verbatim"><pre>';
$alltt_end = '</pre></div>';
sub do_env_alltt {
local ($_) = @_;
@ -2008,12 +2008,12 @@ sub do_cmd_verbatiminput{
else {
$text = '<b>Could not locate requested file <i>$fname</i>!</b>\n';
}
return ('<dl><dd><pre class="verbatim">'
return ("<div class=\"verbatim\">\n<pre>"
. $text
. "</pre>\n<div class=\"verbatiminput-footer\">\n"
. "</pre>\n<div class=\"footer\">\n"
. "<a href=\"$srcname.txt\" type=\"text/plain\""
. ">Download as text.</a>"
. "\n</div>\n</dd></dl>"
. "\n</div></div>"
. $_);
}