/[mojave]/metaprl/theories/tactic/comment.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/comment.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 195  Line 195 
195     `""     `""
196    
197  dform tex_comment_item_df4 : tex_comment_item{comment_term{docoff}} =  dform tex_comment_item_df4 : tex_comment_item{comment_term{docoff}} =
198     izone `"\\kill\\end{tabbing}\n\\fi\\texoff{}\n\\iftex\\begin{tabbing}%" ezone     izone slot["raw", "\n\\end{tabbing}\\fi\\texoff{}\n\\iftex\\begin{tabbing}\n"] ezone
199    
200  dform tex_comment_item_df5 : tex_comment_item{comment_term{doc{'t}}} =  dform tex_comment_item_df5 : tex_comment_item{comment_term{doc{'t}}} =
201     izone slot["raw", "\\kill\\end{tabbing}\n\\fi\\textrue\n"] ezone     izone slot["raw", "\n\\end{tabbing}\\fi\\textrue\n\n"] ezone
202     't     't
203     izone `"\\iftex\\begin{tabbing}%" ezone     izone slot["raw","\\iftex\\begin{tabbing}\n"] ezone
204    
205  dform tex_comment_white_df1 : mode[tex] :: comment_white =  dform tex_comment_white_df1 : mode[tex] :: comment_white =
206     izone slot["raw", "\n"] ezone     izone slot["raw", " "] ezone
207    
208    dform tex_comment_white_df2 : mode[tex] :: cons{comment_white; cons{comment_white; 't}} =
209       izone slot["raw", "\n\n"] ezone slot{'t}
210    
211  (*  (*
212   * Plain version.   * Plain version.
# Line 211  Line 214 
214  dform normal_comment_white_df1 : except_mode[tex] :: comment_white =  dform normal_comment_white_df1 : except_mode[tex] :: comment_white =
215     com_cbreak     com_cbreak
216    
217    dform normal_comment_white_df2 : except_mode[tex] :: cons{comment_white; cons{comment_white; 't}} =
218       com_hbreak slot{'t}
219    
220  dform normal_doc_df2 : except_mode[tex] :: doc{'t} =  dform normal_doc_df2 : except_mode[tex] :: doc{'t} =
221     `"@begin[doc]" com_hbreak 't com_hbreak `"@end[doc]"     `"@begin[doc]" com_hbreak 't com_hbreak `"@end[doc]"
222    

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

  ViewVC Help
Powered by ViewVC 1.1.26