#include <stdio.h>
main( )
{    char c;
     int newline, slashflag = 0;
     int verbatim_mode = 0, tex_mode = 0, blank_count = 0;
     int i;
     newline = 1;
     while( (c = getchar( )) != EOF) 
     {    if( c == '\n' )
          {    newline = 1;
               putchar(c);
               blank_count = 0;
               if ( verbatim_mode == 1 ) continue;
               while( (c = getchar( )) == ' ' ) blank_count++;
               ungetc(c, stdin);
               continue;    }
          if( c == ' ' )
          {    newline = 0;
               putchar(c);
               continue;    }
          if ( c == '/' && newline == 1 )
          {    newline = 0;
               c = getchar( );
               if( c == '*' )
               {    if( verbatim_mode == 1 )
                    {    /* going from verbatim mode to slash* ... stuff */
                         printf("\\end{svb}\n");
                         printf("\\par\\noindent\n");    }
                    verbatim_mode = 0;
                    tex_mode = 1;
                    continue;    }
               else 
                    slashflag = 1;    }
          if ( c == '*' )
          {    newline = 0;
               c = getchar( );
               if ( c == '/' )
               {    if( tex_mode == 1 ) 
                    {    /* completing slash* ... *slash stuff */
                         tex_mode = 0;
                         printf("\\vspace{0.12in}\n");    }
                    else printf("*/");    }
               else 
               {    putchar('*');
                    ungetc(c, stdin);    }
               continue;    }
          if( verbatim_mode == 0 && tex_mode == 0 )
          {    printf("\\begin{svb}\n");
               for ( i = 0; i < blank_count; i++ ) printf(" ");
               verbatim_mode = 1;    }
          if ( slashflag == 1 )
          {    putchar('/');
               slashflag = 0;    }
          newline = 0;
          putchar(c);    }
     if( verbatim_mode == 1 )
          printf("\\end{svb}\n");    }