/[mojave]/metaprl/refiner/reflib/rformat.ml
ViewVC logotype

Diff of /metaprl/refiner/reflib/rformat.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3590 by nogin, Thu Apr 25 15:28:40 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 1421  Line 1421 
1421            | '_' ->            | '_' ->
1422                 collect_escape i j "\\_"                 collect_escape i j "\\_"
1423            | '^' ->            | '^' ->
1424                 collect_escape i j "\\^"                 collect_escape i j "\\makehat"
1425            | '&' ->            | '&' ->
1426                 collect_escape i j "\\&"                 collect_escape i j "\\&"
1427            | '#' ->            | '#' ->
# Line 1523  Line 1523 
1523        output_string buf.tex_out line;        output_string buf.tex_out line;
1524        if (count mod 2) = 1 then        if (count mod 2) = 1 then
1525           output_string buf.tex_out "$";           output_string buf.tex_out "$";
1526        output_string buf.tex_out "\\\\\n";        if (line <> "") && (line.[String.length line - 1] !='\n')
1527             then output_string buf.tex_out "\\\\\n";
1528        if (count mod 2) = 1 then        if (count mod 2) = 1 then
1529           buf.tex_current_line <- [false, "$ "]           buf.tex_current_line <- [false, "$ "]
1530        else        else
# Line 1544  Line 1545 
1545     if col = 0 then     if col = 0 then
1546        begin        begin
1547           tex_push_line buf;           tex_push_line buf;
1548           buf.tex_current_line <- (false, "\\\\\n") :: buf.tex_current_line;           if buf.tex_current_line <> []
1549                then buf.tex_current_line <- (false, "\\\\\n") :: buf.tex_current_line;
1550           buf.tex_prefix <- ""           buf.tex_prefix <- ""
1551        end        end
1552     else     else

Legend:
Removed from v.3590  
changed lines
  Added in v.3591

  ViewVC Help
Powered by ViewVC 1.1.26