/*************************************************************************** * File: hyperpf.c * * Last modified on Thu Feb 19 15:32:06 PST 1998 by lamport * * * * Compile this file with: * * * * cc -lcurses -ltermlib -o hyper hyperpf.c * * * * to produce the executable file hyper. * * * * * * hyperpf [-o out_file] [-l latex_cmd] [-d dvi_cmd] [-n lines] in_file * * * * in_file : The name of a .tex file file containing a single proof * * constructed with the LaTeX pf package commands. See the * * documentation for restrictions on this file. (The * * .tex extension may be omitted.) * * * * out_file : The output file. The default is DEFAULT_OUT_FILE. * * It is a .tex file, but the .tex extension may be omitted. * * * * lines : The number of lines hyperpf will assume is in the * * window where it is running. Default is DEFAULT_LINES. * * * * latex_cmd : To LaTeX the file, hyperpf will execute the command * * latex_cmd with "%s" replaced by out_file. * * Default is DEFAULT_LATEX_COMMAND. * * * * dvi_cmd : To display the dvi file, on startup the command dvi_cmd * * with "%s" replaced by out_file (minus its .tex extension). * * Default is DEFAULT_DVI_COMMMAD. * ***************************************************************************/ #include #include #include /*************************************************************************** * SYSTEM-DEPENDENT CONSTANTS * ***************************************************************************/ #define DEFAULT_OUT_FILE "hyper" /************************************************************************* * The default output file name. * *************************************************************************/ #define DEFAULT_LATEX_COMMAND "latex %s.tex > /dev/null; xrefresh" /************************************************************************* * Command to LaTeX out_file and cause the dvi previewer to refresh. It * * is run with %s replaced with out_file (without the .tex extension). * *************************************************************************/ #define DEFAULT_DVI_COMMAND "xdvi %s.dvi > /dev/null &" /************************************************************************* * Command executed on startup to launch a dvi previewer to display the * * LaTeX output. It is run with %s replaced with out_file (without the * * .tex extension). * *************************************************************************/ #define DEFAULT_LINES 60 /************************************************************************* * In its user interface, hyperpf assumes that the display window (the * * one in which the hyperpf command is executed) has at least this many * * lines. * *************************************************************************/ #define HOW_TO_KILL_PGM "typing Control-C or Control-Z" /************************************************************************* * Instructions for killing hyperpf if it's hung calling a program that * * won't terminate. On my system, Control-C works when first running * * LaTeX and launching the dvi previewer; Control-Z is needed when * * rerunning LaTeX. * *************************************************************************/ #define MAX_LINE_LENGTH 1000 /************************************************************************* * Maximum number of characters in a single line of in_file. * *************************************************************************/ #define MAX_PROOF_DEPTH 30 /************************************************************************* * Maximum nesting nepth of proof environments in in_file. * *************************************************************************/ #define MAX_ITEMS 29999 /************************************************************************* * The maximum allowed total number of \step, \qedstep, \begin{proof} * * and \end{proof} commands in in_file. * *************************************************************************/ #define MAX_ARG_LEN 300 /************************************************************************* * A number bigger than the maximum number of characters in any * * argument. * *************************************************************************/ /*************************************************************************** * SYSTEM-DEPENDENT INPUT CHARACTERS * * * * The following constants define the numeric value of keyboard input * * characters that may be system dependent. * * * * In an xterm on my system, an arrow key generates a string of three * * characters. The first two are ignored and the third is treated as the * * real input character. * ***************************************************************************/ #define ENTER_CHAR 10 /* */ #define CONTROL_C_CHAR 3 /* Control-C */ #define BACKSPACE_CHAR 127 /* */ #define SPACE_CHAR 32 /* */ #define IGNORE_CHAR_1 27 /* arrow prefix character */ #define IGNORE_CHAR_2 91 /* arrow prefix character */ #define LEFT_ARROW_CHAR 'D' /* final character */ #define RIGHT_ARROW_CHAR 'C' /* final character */ #define UP_ARROW_CHAR 'A' /* final character */ #define DOWN_ARROW_CHAR 'B' /* final character */ /*************************************************************************** * SYSTEM-DEPENDENT PROCEDURES * ***************************************************************************/ void clear_display() /************************************************************************* * A command that clears the display window--the one in which hyperpf is * * being run. * *************************************************************************/ {system("clear"); } void initialize_display() /************************************************************************* * Called on startup. It initializes the keyboard to suppress echoing * * and cause getchar() to get characters immediately rather than waiting * * for the user to type . This should also perform any other * * system-dependent intialization needed for the display window. * *************************************************************************/ { initscr(); raw (); noecho (); } void ring_bell() /************************************************************************* * Called when the user types an illegal character. * *************************************************************************/ { putchar(007); } char hpf_getchar() /************************************************************************* * Called to get the next input character typed by the user. It waits * * until that character is typed. * *************************************************************************/ { return(getchar()); } /**************** END OF SYSTEM DEPENDENT CODE (I hope) ******************/ /*************************************************************************** * GLOBAL VARIABLES * ***************************************************************************/ /*************************************************************************** * Arguments to Hyperpf * ***************************************************************************/ char in_file_arg [MAX_ARG_LEN]; char out_file_arg [MAX_ARG_LEN]; char latex_cmd_arg[MAX_ARG_LEN]; char dvi_cmd_arg [MAX_ARG_LEN]; int num_lines_arg; /*************************************************************************** * File Names and Handles * ***************************************************************************/ char ipf_name[MAX_ARG_LEN]; /* input file name with .tex extension. */ char opf_name[MAX_ARG_LEN]; /* output file name with .tex extension. */ char opf_root[MAX_ARG_LEN]; /* output file name without .tex extension. */ FILE *ipf; /* input file handle. */ FILE *opf; /* output file handle. */ /*************************************************************************** * PROCEDURES TO RUN PROGRAMS * ***************************************************************************/ void latex_out_file() { char cmd[MAX_ARG_LEN]; printf("LaTeXing %s.\n", opf_name); printf("If this doesn't complete in a few seconds, stop hyperpf by\n"); printf("%s and try LaTeXing %s yourself.\n", HOW_TO_KILL_PGM, opf_name); sprintf(cmd, latex_cmd_arg, opf_root); system(cmd); return; } void start_dvi_previewer() { char cmd[MAX_ARG_LEN]; printf("\nStarting dvi previewer on %s.dvi.\n", opf_root); printf("If this doesn't complete in a few seconds, stop hyperpf by\n"); printf("%s and try previewing %s.dvi yourself.\n", HOW_TO_KILL_PGM, opf_name); sprintf(cmd, dvi_cmd_arg, opf_root); system(cmd); return; } /*************************************************************************** * MISC GLOBAL VARIABLES * * * * step_level : The depth of the currently chosen step. * * Must be <= MAX_PROOF_DEPTH * * step[lev] : The currently chosen step is * * step[1].step[1]...step[step_level] * * * * pf_depth : The depth of proof to be output. * * * * parsed_file : array of BEGIN_PROOF, END_PROOF, STEP, and QEDSTEP * * values, corresponding to commands in the input file. * * * * parsed_file_len : number of entries in parsed_file * **************************************************************************/ int parsed_file_len; /*************************************************************************** * LINE LOOP VARIABLES * * line : line currently being processed. * * line_num : number of lines preceding the current one * * in the input file * * * * level : The number of proof environments that the input is * * currently within. Assumed to be <= MAX_PROOF_DEPTH * * * * label_num[lev] : The number of the last step encountered at level lev, * * for lev <= level. Must be <= MAX_LABEL_NUM. * * * * equal_upto : The largest number such that * * * * = * * * * writing_output : TRUE iff currently writing input lines to output * * lines * * * * initialize_line_loop_variables() * * Initializes the line loop variables * **************************************************************************/ #define BEGIN_PROOF 1 #define BEGIN_NOPROOF 2 #define STEP 3 #define NOSTEP 4 #define STEPREF 5 #define LEVELREF 6 #define END_PROOF 7 #define END_NOPROOF 8 #define QEDSTEP 9 #define NOCOMMAND 10 char line[MAX_LINE_LENGTH]; int line_num; int level; int label_num[MAX_PROOF_DEPTH+1]; int equal_upto; int writing_output; int step_level; int step[MAX_PROOF_DEPTH]; int pf_depth; char argument[MAX_LINE_LENGTH]; char parsed_file[MAX_ITEMS]; /* type char to save space; should be int */ void initialize_line_loop_variables() { line_num = 0; level = 0; equal_upto = 0; label_num[level] = 0; writing_output = TRUE; } /*************************************************************************** * GETTING THE ARGUMENTS * ***************************************************************************/ void print_usage() /************************************************************************* * Prints the following message on stderr: * * * * Usage: hyperpf [-o out_file] [-l latex_cmd] [-d dvi_cmd] [-n lines] in_file * * * * in_file : The name of a .tex file file containing a single proof * * constructed with the LaTeX pf package commands. See the * * documentation for restrictions on this file. (The * * .tex extension may be omitted.) * * * * out_file : The output file. The default is DEFAULT_OUT_FILE. * * It is a .tex file, but the .tex extension may be omitted. * * * * lines : hyperpf will assume that window where it is running can * * display at least this many lines of text. * * Default is DEFAULT_LINES. * * * * latex_cmd : To LaTeX the file, hyperpf will execute the command * * latex_cmd with %s replaced by out_file. * * Default is DEFAULT_LATEX_COMMAND. * * * * dvi_cmd : To display the dvi file, on startup the command dvi_cmd * * with %s replaced by out_file (minus its .tex extension). * * Default is DEFAULT_DVI_COMMAND. * *************************************************************************/ { fprintf(stderr, "Usage: hyperpf [-o out_file] [-l latex_cmd] [-d dvi_cmd] [-n lines] in_file\n"); fprintf(stderr, "\n"); fprintf(stderr, " in_file : The name of a .tex file file containing a single proof\n"); fprintf(stderr, " constructed with the LaTeX pf package commands. See the\n"); fprintf(stderr, " documentation for restrictions on this file. (The\n"); fprintf(stderr, " .tex extension may be omitted.)\n"); fprintf(stderr, "\n"); fprintf(stderr, " out_file : The output file. The default is %s.\n", DEFAULT_OUT_FILE); fprintf(stderr, " It is a .tex file, but the .tex extension may be omitted.\n"); fprintf(stderr, "\n"); fprintf(stderr, " lines : hyperpf will assume that window where it is running can\n"); fprintf(stderr, " display at least this many lines of text\n"); fprintf(stderr, " Default is %d.\n", DEFAULT_LINES); fprintf(stderr, "\n"); fprintf(stderr, " latex_cmd : To LaTeX the file, hyperpf will execute the command\n"); fprintf(stderr, " latex_cmd with %%s replaced by out_file.\n"); fprintf(stderr, " Default is %s.\n", DEFAULT_LATEX_COMMAND); fprintf(stderr, "\n"); fprintf(stderr, " dvi_cmd : To display the dvi file, on startup the command dvi_cmd\n"); fprintf(stderr, " with %%s replaced by out_file (minus its .tex extension).\n"); fprintf(stderr, " Default is %s.\n", DEFAULT_DVI_COMMAND); } /*************************************************************************** * FILE HANDLING PROCEDURES * * * * Defines the following procedures that are used elsewhere: * * * * open_input_file read_input_line * * close_input_file write_output_line * * open_files get_file_names * * close_files * ***************************************************************************/ void get_file_names() /************************************************************************* * Sets the global variables ipf_name, opf_name, and opf_root. * *************************************************************************/ { char *temp_str ; /* Set ipf_name */ strcpy(ipf_name, in_file_arg); if (strstr(ipf_name, ".tex") == NULL) { strcat(ipf_name, ".tex"); } else { if ( ((int) (strstr(ipf_name, ".tex")) - (int)(ipf_name) + 4) != strlen(ipf_name)) { fprintf(stderr, "Bad input file name '%s'\n", ipf_name); exit(-1); } } ; /* Set opf_name */ strcpy(opf_name, out_file_arg); if (strstr(opf_name, ".tex") == NULL) { strcat(opf_name, ".tex"); } else { if ( ((int) (strstr(opf_name, ".tex")) - (int)(opf_name) + 4) != strlen(opf_name)) { fprintf(stderr, "Bad file name '%s'\n", opf_name); exit(-1); } } ; /* Set opf_root */ strcpy(opf_root, opf_name); temp_str = (char *) strstr(opf_root, ".tex") ; temp_str[0] = '\0'; } void open_input_file() { if ((ipf = fopen(ipf_name, "r")) == NULL) { fprintf(stderr, "Couldn't open input file '%s'\n", ipf_name); exit(-1); } } void close_input_file() { fclose(ipf); } void open_files() { open_input_file(); if ((opf = fopen(opf_name, "w")) == NULL) { fprintf(stderr, "Couldn't open output file '%s'\n", opf_name); exit(-1); } } void close_files() { close_input_file(); fclose(opf); } int read_input_line() { if (fgets(line, MAX_LINE_LENGTH, ipf) == NULL) { return(0); } else { return(1); } } void write_output_line() { if (fputs(line, opf) == NULL) { fprintf(stderr, "Error writing output file\n"); exit(-1); } } /*************************************************************************** * DEBUGGING * ***************************************************************************/ void debug_print_args() { printf("in_file_arg = %s\n", in_file_arg); printf("out_file_arg = %s\n", out_file_arg); printf("latex_cmd_arg = %s\n", latex_cmd_arg); printf("dvi_cmd_arg = %s\n", dvi_cmd_arg); printf("num_lines_arg = %d\n", num_lines_arg); printf("ipf_name = %s\n", ipf_name); printf("opf_name = %s\n", opf_name); printf("opf_root = %s\n", opf_root); return; } void print_step() { int lev; printf("step_level = %d, pf_depth = %d\n", step_level, pf_depth); lev = 1 ; while (lev <= step_level) { printf("step[%d] = %d, ", lev, step[lev]); lev++; }; printf("\n\n"); } void print_state() { int lev; printf( "line %d: %s ", line_num, line); printf("level = %d, ", level); lev = 1 ; while (lev <= level) { printf("label_num[%d] = %d, ", lev, label_num[lev]); lev++; }; printf("\n equal_upto = %d, ", equal_upto); if(writing_output) {printf("writing_output = TRUE\n\n");} else {printf("writing_output = FALSE\n\n");} } void print_parsed_file() { int pos; pos = 0; while (pos < parsed_file_len) { switch (parsed_file[pos]) { case BEGIN_PROOF : printf("BEGIN_PROOF\n"); break; case END_PROOF : printf("END_PROOF\n"); break; case STEP : printf("STEP\n"); break; case QEDSTEP : printf("QEDSTEP\n"); break; default : printf("?????\n"); exit(-1); }; pos++; } } /*************************************************************************** * UTILITY COMMANDS FOR PARSING INPUT * * * * find_next_command() * * Searches for a command in line, and * * - sets command to the number of the command (an integer) * * or to NOCOMMAND if there is none. * * - For a \step command, it sets argument to its argument. * **************************************************************************/ int command; void look_for(char *cmd_str, /* command string */ int cmd /* command number */ ) /************************************************************************* * Looks for first instance of cmd_str starting from line[0]. If it * * finds one, then it sets command to cmd. * *************************************************************************/ { /* DEBUG ******************************************** printf("lookfor, line %d\n", line_num); printf("cmd_str = %s\n", cmd_str); printf("line = %s\n", line); *********************************************/ if (strstr(line, cmd_str) == NULL) { return; } command = cmd; } void arg_look_for(char *cmd_str, /* command string */ int cmd /* command number */ ) /************************************************************************* * Assumes cmd_str is a string of the form "\command{". Looks for an * * instance of cmd_str starting from line[0]. If it finds one, then it * * sets command to cmd, and sets argument to the string immediately * * following it up to the next "}". * *************************************************************************/ { char *fnd_cmd_str ; char *rbrace_pos; int arg_len; /* DEBUG ******************************************** printf("line %d, arg_look_for %s\n", line_num, cmd_str); printf("lookfor, line %d, pos %d\n", line_num, pos); printf("cmd_str = %s\n", cmd_str); printf("line[pos] = %s\n", line + pos); *********************************************/ if ((fnd_cmd_str = (char*) strstr(line, cmd_str)) == NULL) { return; } /* DEBUG ******************************************** printf("found\n"); printf("line = %d, fnd_cmd_str = %d\n", line, fnd_cmd_str); printf("\n"); printf("line = %s\n", line); printf("fnd_cmd_str = %s\n", fnd_cmd_str); printf("\n"); *********************************************/ command = cmd; if ((rbrace_pos = (char*) strchr(fnd_cmd_str, '}')) == NULL) { fprintf(stderr, "Missing '}' on line %d\n", line_num+1); return; }; arg_len = rbrace_pos - fnd_cmd_str - strlen(cmd_str); strncpy(argument, fnd_cmd_str+strlen(cmd_str), arg_len); argument[arg_len] = '\0'; /* DEBUG ******************************************** printf("from: %s", line); printf("argument: ->%s<-\n", argument); printf("fnd_cmd_str = %s\n", fnd_cmd_str); printf("rbrace_pos = %s\n", rbrace_pos); printf("as numbers: line = %d, fnd_cmd_str = %d, rbrace_pos = %d\n\n", line, fnd_cmd_str, rbrace_pos); *********************************************/ } void find_next_command() { command = NOCOMMAND; look_for("\\begin{proof}", BEGIN_PROOF); if (command != NOCOMMAND) {return;}; look_for("\\end{proof}", END_PROOF); if (command != NOCOMMAND) {return;}; arg_look_for("\\step{", STEP); if (command != NOCOMMAND) {return;}; look_for("\\qedstep", QEDSTEP); /* look_for("\\end{noproof}", END_NOPROOF, pos, 0); */ /* look_for("\\begin{noproof}", BEGIN_NOPROOF, pos, 0); */ /* look_for("\\nostep{", NOSTEP, pos, 1); */ /* look_for("\\stepref{", STEPREF, pos, 1); */ /* look_for("\\levelref{", LEVELREF, pos, 1); */ /* if (no_comments == 0) */ /* { look_for("%", -2, pos, 0); */ /* } */ /* else */ /* { look_for("%%%{", STEPREF, pos, 1); */ /* } */ return; } /*************************************************************************** * fix_step() * * * * Changes the values of step_level and step as follows: * * * * k := Max { k \leq step_level : * * \A 1 \leq i \leq k : there is a step with long * * number step[1]. ... . step[k] } * * IF k = step_level * * THEN leave unchanged * * ELSE IF step step[1]. ... .step[k] has a proof * * THEN step_level := k+1 * * step[k+1] := number of steps in step * * step[1]. ... .step[k]'s proof * * ELSE step_level := k * ***************************************************************************/ void fix_step() { int pos ; int not_done; if (step_level == 0) {return;} /* level0 */ pos = 0; not_done = TRUE; initialize_line_loop_variables(); while (not_done && (pos < parsed_file_len)) { /********************************************************************* * LOOP INVARIANT : * * /\ level = number of \begin{proof}'s - number of \end{proof}'s * * in parsed_file[0], ... , parsed_file[pos - 1] * * * * /\ \A i \leq level : label_num[i] = number of \step's and * * \qedstep's encountered at * * current proof level i * * * * /\ equal_upto = Max {n \leq step_level : * * \A 0 < i \leq n : label_num[i] = step[i]} * *********************************************************************/ switch (parsed_file[pos]) { case BEGIN_PROOF : level++; label_num[level] = 0; break; case END_PROOF : if (equal_upto == level) { step_level = level; not_done = FALSE; } else { if ( (equal_upto == level-1) && (step_level >= level) ) { step_level = level; step[level] = label_num[level]; not_done = FALSE; } } ; level--; break; case STEP : case QEDSTEP : label_num[level]++; if (equal_upto == level) { step_level = level; not_done = FALSE; } else { if ( (equal_upto == (level-1)) && (step[level] == label_num[level]) ) { equal_upto = level; if (level == step_level) { not_done = FALSE; } } }; break; default : fprintf(stderr, "Program bug: bad parsed_file entry.\n"); exit(-1); }; pos++; }; } /*************************************************************************** * DISPLAY * ***************************************************************************/ void display_text_pf() /************************************************************************* * step selects a text proof, which is now displayed. * *************************************************************************/ { int pos; pos=0; while (pos < step_level) { printf(">"); pos++; }; printf(" text proof\n"); return; } void display_step() /************************************************************************* * Displays the proof step indicated by label_num and level, if * * level \geq start_level. * *************************************************************************/ { int pos; pos=0; while (pos < level) { printf(" "); pos++; }; printf(" <%d>%d\n", level, label_num[level]); return; } void display_selected_step() /************************************************************************* * Displays the proof step indicated step and step_level, as the * * selected step. * *************************************************************************/ { int pos; pos=0; while (pos < step_level) { printf(">"); pos++; }; printf(" <%d>%d\n", step_level, step[step_level]); return; } void print_help() /************************************************************************* * Prints the following message: * * * * hyperpf * * * * This is a hypertext reader that displays a selected portion of the * * proof. You can display and navigate through the proof with the * * following commands, where [num] is an optional number with default * * value of 1. * * * * - To select a different proof step in this window: * * * * [num] n : Move num steps forward at the current level. * * [num] p : Move num steps backwards at the current level. * * d : Move to the next level down in the proof structure. * * [num] u : Move num levels up in the proof structure. * * * * - To refresh the xdvi display with a new part of the proof: * * * * [num] x : LaTeX the portion of the proof displayed, plus the first * * num levels in the proof of the selected statement. * * * * - Miscellaneous: * * r : Re-read the input file. * * h : Type this message. * * q : Exit. * * * * - The following aliases can be used for the commands listed above: * * n : f > (arrows may not * * p : b < work on all systems) * * u : ^ * * d : _ * * x : * * * * TYPE ANY CHARACTER TO CONTINUE. * *************************************************************************/ { clear_display(); printf(" hyperpf\n"); printf("\n"); printf("This is a hypertext reader that displays a selected portion of the\n"); printf("proof. You can display and navigate through the proof with the\n"); printf("following commands, where [num] is an optional number with default\n"); printf("value of 1.\n"); printf("\n"); printf("- To select a different proof step in this window:\n"); printf("\n"); printf(" [num] n : Move num steps forward at the current level. \n"); printf(" [num] p : Move num steps backwards at the current level.\n"); printf(" d : Move to the next level down in the proof structure.\n"); printf(" [num] u : Move num levels up in the proof structure.\n"); printf("\n"); printf("- To refresh the xdvi display with a new part of the proof:\n"); printf("\n"); printf(" [num] x : LaTeX the portion of the proof displayed, plus the first\n"); printf(" num levels in the proof of the selected statement.\n"); printf("\n"); printf("- Miscellaneous: \n"); printf(" r : Re-read the input file.\n"); printf(" h : Type this message.\n"); printf(" q : Exit.\n"); printf("\n"); printf("- The following aliases can be used for the commands listed above:\n"); printf(" n : f > (arrows may not \n"); printf(" p : b < work on all systems)\n"); printf(" u : ^ \n"); printf(" d : _ \n"); printf(" x : \n"); printf("\n"); printf("TYPE ANY CHARACTER TO CONTINUE.\n"); hpf_getchar(); return; } int internal_display_pf(int start_level, int disp) /************************************************************************* * IF disp = TRUE * * THEN Displays all proof steps with level \geq start_level that * * will be displayed by pfshow for the current value of with pf_level <- 0, and indicates the current * * value of , and returns 0. * * ELSE Returns the number of lines that it would have displayed * *************************************************************************/ { int pos ; int cnt; pos = 0; cnt = 0; if (disp) { /******************************************************************** * Clear the screen. * ********************************************************************/ clear_display(); /******************************************************************** * Print top of screen. * ********************************************************************/ printf("Type h for help.\n\n"); }; /************************************************************************ * Process the proof display. * ************************************************************************/ initialize_line_loop_variables(); while (pos < parsed_file_len) { /********************************************************************* * LOOP INVARIANT : * * /\ level = number of \begin{proof}'s - number of \end{proof}'s * * in parsed_file[0], ... , parsed_file[pos - 1] * * * * /\ \A i \leq level : label_num[i] = number of \step's and * * \qedstep's encountered at * * current proof level i * * * * /\ equal_upto = Max {n \leq step_level : * * \A 0 < i \leq n : label_num[i] = step[i]} * *********************************************************************/ switch (parsed_file[pos]) { case BEGIN_PROOF : level++; label_num[level] = 0; if ( (equal_upto == level-1) && (step_level == level) && (step[level] == 0) ) { /* step selects a text proof */ if (disp) {display_text_pf();} else {cnt++;}; } break; case END_PROOF : if (equal_upto == level) { equal_upto--; } level--; break; case STEP : case QEDSTEP : label_num[level]++; if (equal_upto == level) { equal_upto--; if (level >= start_level) { if (disp) {display_step(start_level);} else {cnt++;}; }; } else { if ( (equal_upto == (level-1)) && (level <= step_level) ) { if (step[level] == label_num[level]) { equal_upto = level; if (level == step_level) { if (disp) {display_selected_step();} else {cnt++;}; } else { if (level >= start_level) { if (disp) {display_step();} else {cnt++;}; }; }; } else { if (level >= start_level) { if (disp) {display_step();} else {cnt++;}; }; } } }; break; default : fprintf(stderr, "Program bug: bad parsed_file entry.\n"); exit(-1); }; pos++; }; return(cnt); } void display_pf(int scrn_ht) { int dpth = 1; if (step_level == 0) { clear_display(); printf("Type h for help.\n\nentire proof\n"); return;} while ( (dpth <= step_level+3) && (internal_display_pf(dpth, FALSE) > scrn_ht - 2) ) { dpth++; }; if (dpth > step_level) { clear_display(); printf("Screen to short to show proof\n"); } else { internal_display_pf(dpth, TRUE); }; return; } /*************************************************************************** * INPUT PROCESSING FOR parse_input() * * * * ip_process_begin_proof() * * ip_process_end_proof() * * ip_process_step() * * Process a single command, with the variable command having the * * values set by find_next_command. Makes any necessary changes to * * line. * **************************************************************************/ void add_parsed_file_entry() /************************************************************************* * Adds value of command as net parsed_file entry. * *************************************************************************/ { parsed_file[parsed_file_len] = command; parsed_file_len++; if (parsed_file_len >= MAX_ITEMS) { fprintf(stderr, "Too many items.\n"); exit(-1); }; return; } void ip_process_begin_proof() { level++; if (level > MAX_PROOF_DEPTH) { fprintf(stderr, "proofs too deeply nested\n"); exit(-1); } label_num[level] = 0; add_parsed_file_entry(); return; } void ip_process_end_proof() { level--; if (level < 0) { fprintf(stderr, "Extra \\end{proof} on line %d\n", line_num+1); level++; }; add_parsed_file_entry(); return; } void ip_process_step() { add_parsed_file_entry(); return; } void parse_input() { open_input_file(); parsed_file_len = 0; while (read_input_line() != 0) { find_next_command(); switch (command) { case BEGIN_PROOF : ip_process_begin_proof(); break; case END_PROOF : ip_process_end_proof(); break; case STEP : case QEDSTEP : ip_process_step(); break; case NOCOMMAND : break; default : fprintf(stderr, "This program has a bug\n"); exit(-1); } /* End switch */ }; close_input_file(); return; } /*************************************************************************** * INPUT PROCESSING FOR produce_output_file() * * * * po_process_begin_proof() * * po_process_end_proof() * * po_process_step() * * Process a single command, with the variable command having the * * values set by find_next_command. Makes any necessary changes to * * line. * **************************************************************************/ void po_process_begin_proof() { level++; if (level > MAX_PROOF_DEPTH) { fprintf(stderr, "proofs too deeply nested\n"); exit(-1); } label_num[level] = 0; /* if ( (equal_upto < level-1) || (level > step_level + pf_depth) ) { writing_output = FALSE; }; */ /************************************************************************* * Sets writing_output to value that preserves loop invariant. * *************************************************************************/ writing_output = ( ( (equal_upto >= level-1) || (equal_upto == step_level) ) && (level <= step_level + pf_depth) ); if (writing_output) {write_output_line();}; } void po_process_end_proof() { if (writing_output) {write_output_line();}; if (equal_upto == level) { equal_upto--; }; level--; if (level < 0) { fprintf(stderr, "Extra \\end{proof} on line %d\n", line_num+1); level++; }; /* DEBUG printf("end(proof) at level %d\n", level+1); */ /************************************************************************* * Sets writing_output to value that preserves loop invariant. * *************************************************************************/ writing_output = ( ( (equal_upto >= level-1) || (equal_upto == step_level) ) && (level <= step_level + pf_depth) ); return; } void po_process_step() { label_num[level]++; if (equal_upto == level) { equal_upto--; } else { if ( (equal_upto == (level-1)) && (equal_upto < step_level) && (step[level] == label_num[level]) ) {equal_upto = level; } }; if (writing_output) {write_output_line();}; } void produce_output_file() /************************************************************************* * Reads input file and produces output file, based on the values of * * step_level, step, and pf_depth. * *************************************************************************/ {open_files(); initialize_line_loop_variables(); /* main loop */ while (read_input_line() != 0) { /********************************************************************** * LOOP INVARIANT : * * /\ level = number of \begin{proof}'s - number of \end{proof}'s * * up to line number line. * * * * /\ \A i \leq level : label_num[i] = number of \step's encountered * * at current proof level i * * * * /\ equal_upto = Max { Max {n : \A i < n : * * label_num[i] = step[i]}, * * step_level } * * * * /\ writing_output = /\ \/ equal_upto \geq level-1 * * \/ equal_upto = step_level * * /\ level \leq step_level + pf_depth * **********************************************************************/ /* DEBUG printf("line = %d\n", line); */ find_next_command(); /********************************************************************** * ASSERTION: command has the appropriate value * **********************************************************************/ switch (command) { case BEGIN_PROOF : po_process_begin_proof(); break; case END_PROOF : po_process_end_proof(); break; case STEP : case QEDSTEP : /* DEBUG printf("po_process_step at line %d\n", line_num+1); */ po_process_step(); break; case NOCOMMAND : /* DEBUG printf("NOCOMMAND\n"); */ if (writing_output) {write_output_line();}; break; default : fprintf(stderr, "This program has a bug\n"); exit(-1); } /* End switch */ /********************************************************************** * ASSERTION: Any command in the current line has been processed, and * * the output line has been written iff it should be. * **********************************************************************/ /* Debug if (command != NOCOMMAND) {print_state();}; */ line_num++; } /* END while (read_input_line() != 0) */ /* have reached the end of file */ close_files(); while (level > 0) { fprintf(stderr, "unmatched \\begin{proof}\n"); level--; } } main(int argc, char *argv[]) { int pos; char *ptr; char ip_char; int no_prefix; /* TRUE iff no prefix number has been typed. */ int prefix_num; char cmd[MAX_ARG_LEN]; /************************************************************************* * Get arguments. * *************************************************************************/ /* Set defaults. */ strcpy(out_file_arg, DEFAULT_OUT_FILE); strcpy(latex_cmd_arg, DEFAULT_LATEX_COMMAND); strcpy(dvi_cmd_arg, DEFAULT_DVI_COMMAND); num_lines_arg = DEFAULT_LINES; /* Check for legal of arguments. */ if ( (argc < 2) || ((argc % 2) != 0) ) { print_usage(); exit(-1); } /* Get mandatory argument. */ strcpy(in_file_arg, argv[argc-1]); /* Get switches. */ pos = 3; while (pos < argc) { strcpy(cmd, argv[argc-pos]); switch (cmd[1]) { case 'n' : sscanf(argv[argc-pos+1], "%d", &num_lines_arg); break; case 'o' : strcpy(out_file_arg, argv[argc-pos+1]); break; case 'l' : strcpy(latex_cmd_arg, argv[argc-pos+1]); break; case 'd' : strcpy(dvi_cmd_arg, argv[argc-pos+1]); break; default : print_usage(); exit(-1); } pos = pos+2; }; get_file_names(); /************************************************************************* * Initialize step_level and step. * *************************************************************************/ step_level = 1; step[1] = 1; pf_depth = 0; /************************************************************************* * Run LaTeX and launch dvi previewer. * *************************************************************************/ parse_input(); fix_step(); produce_output_file(); latex_out_file(); start_dvi_previewer(); initialize_display(); print_help(); display_pf(num_lines_arg); no_prefix = TRUE; /************************************************************************* * Main Loop * *************************************************************************/ while ((ip_char = hpf_getchar()) != 'q') { if ( ('0' <= ip_char) && (ip_char <= '9') ) { /* numeric prefix entered */ if (no_prefix) { prefix_num = ip_char - '0'; no_prefix = FALSE; } else { prefix_num = (10 * prefix_num) + (ip_char - '0'); } } else { /* command entered */ if (no_prefix) { prefix_num = 1; }; no_prefix = TRUE; switch (ip_char) { case 'u' : case '^' : case UP_ARROW_CHAR : /************************************************************ * Go up in the tree prefix_num times. * ************************************************************/ pos = 0; while (pos < prefix_num) { step_level-- ; pos++; }; if (step_level <= 0) {step_level=0;}; fix_step(); display_pf(num_lines_arg); break; case 'd' : case '_' : case DOWN_ARROW_CHAR : /************************************************************ * Go down in the tree one level. * ************************************************************/ step_level++; step[step_level] = 1; fix_step(); display_pf(num_lines_arg); break; case 'n' : case 'f' : case '>' : case SPACE_CHAR : case RIGHT_ARROW_CHAR : /************************************************************ * Go forward prefix_num steps. * ************************************************************/ step[step_level] = step[step_level] + prefix_num; fix_step(); display_pf(num_lines_arg); break; case 'p' : case 'b' : case '<' : case BACKSPACE_CHAR : case LEFT_ARROW_CHAR : /************************************************************ * Go backwards prefix_num steps. * ************************************************************/ step[step_level] = step[step_level] - prefix_num; if (step[step_level] < 1) {step[step_level] = 1;}; fix_step(); display_pf(num_lines_arg); break; case 'x' : case ENTER_CHAR : pf_depth = prefix_num; produce_output_file(); latex_out_file(); display_pf(num_lines_arg); break; case 'r' : /************************************************************ * Re-parse input file and redisplay. * ************************************************************/ parse_input(); fix_step(); display_pf(num_lines_arg); break; case 'h' : print_help(); display_pf(num_lines_arg); break; case CONTROL_C_CHAR : /* Control-C */ exit(-1); break; case 'q' : break; case IGNORE_CHAR_1 : /* Hack to make arrows work on DEC term */ case IGNORE_CHAR_2 : if (prefix_num != 1) { no_prefix = FALSE;}; break; default : ring_bell(); }; /* switch */ } /* else */ } /* while */ }