1 /* 2 * formed.h -- FormEd (Formula Editor) X Windows program. 3 * 4 */ 5 6 /* C Includes */ 7 8 #include <stdio.h> 9 #include <string.h> 10 11 /* X Includes */ 12 13 #include <X11/Intrinsic.h> 14 #include <X11/StringDefs.h> 15 #include <X11/Shell.h> 16 #include <X11/Xaw/Form.h> 17 #include <X11/Xaw/Command.h> 18 #include <X11/Xaw/Box.h> 19 #include <X11/Xaw/Viewport.h> 20 #include <X11/Xaw/Label.h> 21 #include <X11/Xaw/AsciiText.h> 22 #include <X11/Xaw/TextSrc.h> 23 #include <X11/Xaw/List.h> 24 25 /* bitmaps */ 26 27 #define all_lg_width 16 28 #define all_lg_height 16 29 static char all_lg_bits[] = { 30 0x03, 0xc0, 0x03, 0xc0, 0x06, 0x60, 0x06, 0x60, 0x0c, 0x30, 0x0c, 0x30, 31 0xf8, 0x1f, 0xf8, 0x1f, 0x30, 0x0c, 0x30, 0x0c, 0x60, 0x06, 0x60, 0x06, 32 0xc0, 0x03, 0xc0, 0x03, 0x80, 0x01, 0x80, 0x01}; 33 #define all_md_width 12 34 #define all_md_height 12 35 static char all_md_bits[] = { 36 0x03, 0x0c, 0x03, 0x0c, 0x06, 0x06, 0x06, 0x06, 0xfc, 0x03, 0xfc, 0x03, 37 0x98, 0x01, 0x98, 0x01, 0xf0, 0x00, 0xf0, 0x00, 0x60, 0x00, 0x60, 0x00}; 38 #define all_sm_width 8 39 #define all_sm_height 8 40 static char all_sm_bits[] = { 41 0x81, 0x81, 0x42, 0x7e, 0x24, 0x24, 0x18, 0x18}; 42 #define and_lg_width 16 43 #define and_lg_height 16 44 static char and_lg_bits[] = { 45 0xc0, 0x01, 0x60, 0x03, 0x60, 0x03, 0x60, 0x03, 0x40, 0x01, 0xc0, 0x00, 46 0xc0, 0x00, 0xe0, 0x01, 0x30, 0x33, 0x18, 0x33, 0x0c, 0x26, 0x0c, 0x1c, 47 0x0c, 0x0c, 0x0c, 0x1c, 0xf8, 0x37, 0xf0, 0x33}; 48 #define and_md_width 12 49 #define and_md_height 12 50 static char and_md_bits[] = { 51 0x70, 0x00, 0x58, 0x00, 0x58, 0x00, 0x30, 0x00, 0x30, 0x00, 0x68, 0x00, 52 0xcc, 0x06, 0x86, 0x04, 0x86, 0x03, 0x86, 0x01, 0xc6, 0x02, 0x7c, 0x06}; 53 #define and_sm_width 8 54 #define and_sm_height 8 55 static char and_sm_bits[] = { 56 0x08, 0x14, 0x14, 0x08, 0x14, 0x52, 0x22, 0x5c}; 57 #define exists_lg_width 14 58 #define exists_lg_height 18 59 static char exists_lg_bits[] = { 60 0x00, 0x00, 0xfe, 0x1f, 0xfe, 0x1f, 0x00, 0x18, 0x00, 0x18, 0x00, 0x18, 61 0x00, 0x18, 0x00, 0x18, 0xf8, 0x1f, 0xf8, 0x1f, 0x00, 0x18, 0x00, 0x18, 62 0x00, 0x18, 0x00, 0x18, 0x00, 0x18, 0xfe, 0x1f, 0xfe, 0x1f, 0x00, 0x00}; 63 #define exists_md_width 12 64 #define exists_md_height 14 65 static char exists_md_bits[] = { 66 0x00, 0x00, 0xfe, 0x07, 0xfe, 0x07, 0x00, 0x04, 0x00, 0x04, 0x00, 0x04, 67 0xf8, 0x07, 0xf8, 0x07, 0x00, 0x04, 0x00, 0x04, 0x00, 0x04, 0xfe, 0x07, 68 0xfe, 0x07, 0x00, 0x00}; 69 #define exists_sm_width 8 70 #define exists_sm_height 11 71 static char exists_sm_bits[] = { 72 0x00, 0x7e, 0x40, 0x40, 0x40, 0x7c, 0x40, 0x40, 0x40, 0x7e, 0x00}; 73 #define iff_lg_width 16 74 #define iff_lg_height 16 75 static char iff_lg_bits[] = { 76 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x08, 0x10, 0x0c, 0x30, 77 0xfe, 0x7f, 0xff, 0xff, 0xfe, 0x7f, 0x0c, 0x30, 0x08, 0x10, 0x00, 0x00, 78 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 79 #define iff_md_width 12 80 #define iff_md_height 12 81 static char iff_md_bits[] = { 82 0x00, 0x00, 0x00, 0x00, 0x04, 0x02, 0x06, 0x06, 0xff, 0x0f, 0xff, 0x0f, 83 0x06, 0x06, 0x04, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 84 #define iff_sm_width 8 85 #define iff_sm_height 8 86 static char iff_sm_bits[] = { 87 0x00, 0x24, 0x42, 0xff, 0x42, 0x24, 0x00, 0x00}; 88 #define imp_lg_width 16 89 #define imp_lg_height 16 90 static char imp_lg_bits[] = { 91 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x08, 0x00, 0x18, 0x00, 0x38, 92 0xff, 0x7f, 0xff, 0xff, 0xff, 0x7f, 0x00, 0x38, 0x00, 0x18, 0x00, 0x08, 93 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 94 #define imp_md_width 12 95 #define imp_md_height 12 96 static char imp_md_bits[] = { 97 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x02, 0x00, 0x06, 0xff, 0x0f, 98 0xff, 0x0f, 0x00, 0x06, 0x00, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 99 #define imp_sm_width 8 100 #define imp_sm_height 8 101 static char imp_sm_bits[] = { 102 0x00, 0x20, 0x40, 0xff, 0x40, 0x20, 0x00, 0x00}; 103 #define not_lg_width 16 104 #define not_lg_height 16 105 static char not_lg_bits[] = { 106 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 107 0x00, 0x00, 0xff, 0xff, 0xff, 0xff, 0x00, 0xc0, 0x00, 0xc0, 0x00, 0xc0, 108 0x00, 0xc0, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 109 #define not_md_width 12 110 #define not_md_height 12 111 static char not_md_bits[] = { 112 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xff, 0x0f, 113 0xff, 0x0f, 0x00, 0x0c, 0x00, 0x0c, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00}; 114 #define not_sm_width 8 115 #define not_sm_height 8 116 static char not_sm_bits[] = { 117 0x00, 0x00, 0x00, 0xff, 0x80, 0x80, 0x00, 0x00}; 118 #define or_lg_width 16 119 #define or_lg_height 16 120 static char or_lg_bits[] = { 121 0x03, 0xc0, 0x03, 0xc0, 0x06, 0x60, 0x06, 0x60, 0x0c, 0x30, 0x0c, 0x30, 122 0x18, 0x18, 0x18, 0x18, 0x30, 0x0c, 0x30, 0x0c, 0x60, 0x06, 0x60, 0x06, 123 0xc0, 0x03, 0xc0, 0x03, 0x80, 0x01, 0x80, 0x01}; 124 #define or_md_width 12 125 #define or_md_height 12 126 static char or_md_bits[] = { 127 0x03, 0x0c, 0x03, 0x0c, 0x06, 0x06, 0x06, 0x06, 0x0c, 0x03, 0x0c, 0x03, 128 0x98, 0x01, 0x98, 0x01, 0xf0, 0x00, 0xf0, 0x00, 0x60, 0x00, 0x60, 0x00}; 129 #define or_sm_width 8 130 #define or_sm_height 8 131 static char or_sm_bits[] = { 132 0x81, 0x81, 0x42, 0x42, 0x24, 0x24, 0x18, 0x18}; 133 #define pattern_width 4 134 #define pattern_height 4 135 static char pattern_bits[] = { 136 0x05, 0x0a, 0x05, 0x0a}; 137 138 139 #define LABELFONT "-*-helvetica-*-r-*-*-*-120-*-*-*-*-*-*" 140 #define LARGEFONT "-*-helvetica-*-r-*-*-*-240-*-*-*-*-*-*" 141 #define MEDFONT "-*-helvetica-*-r-*-*-*-140-*-*-*-*-*-*" 142 #define SMALLFONT "-*-helvetica-medium-r-*-*-*-100-*-*-*-*-*-*" 143 144 #define SMALLFONT_DIM 8 145 #define MEDFONT_DIM 12 146 #define LARGEFONT_DIM 16 147 148 #define SMALL_SPACING 3 149 #define MED_SPACING 5 150 #define LARGE_SPACING 7 151 152 #define VIEWPORT_HEIGHT 600 153 #define VIEWPORT_WIDTH 1000 154 155 #define CANVAS_HEIGHT 1000 156 #define CANVAS_WIDTH 1000 157 158 #define FORMULA 1 159 #define OPERATOR 2 160 161 #define OR_OP 1 /* subtypes of operator */ 162 #define AND_OP 2 163 #define NOT_OP 3 164 #define EXISTS_OP 4 165 #define ALL_OP 5 166 #define IFF_OP 6 167 #define IMP_OP 7 168 169 #define TEXT_LENGTH 500 170 171 #define PLACE_HOLDER 0 172 #define LOGIC_MENU 1 173 #define EDIT_MENU 2 174 175 #define NUM_LOGIC_BUTTONS 10 176 #define NUM_EDIT_BUTTONS 10 177 178 #define ADD 1 /* for use in accum_size */ 179 #define IGNORE 0 180 181 /* The rest of this file is communal (global) variables. */ 182 /* Names of global variables have first letter capitalized. */ 183 184 #ifdef IN_MAIN 185 #define CLASS /* empty string if included by main program */ 186 #else 187 #define CLASS extern /* extern if included by anything else */ 188 #endif 189 190 CLASS XtAppContext App_con; 191 192 CLASS Display *Dpy; /* variables for window setup */ 193 CLASS Window Win; 194 CLASS XSetWindowAttributes W_attr; 195 CLASS GC Gc; 196 CLASS int Def_screen; 197 CLASS int Frame_depth; 198 CLASS Colormap Cmap; 199 CLASS int Foreground, Background; 200 CLASS int Display_setup; /* flag for if display has been initialized */ 201 202 CLASS int Fore_set, Back_set, Load_file; /* command line options */ 203 CLASS char User_fore[25], User_back[25]; 204 CLASS char Crnt_file[25]; /* the current filename in use */ 205 206 CLASS int Have_message; /* for if have a message widget displayed */ 207 CLASS char Error_string[50]; /* for building error messages */ 208 209 CLASS XFontStruct *Font_struct; /* structure holding font information */ 210 CLASS int Font_char_ht; /* max height for characters in the font */ 211 CLASS int Font_ascent; /* max baseline to top edge of character */ 212 213 /* pixel maps for operators and inversions */ 214 CLASS Pixmap And, Or, Not, All, Exists, Imp, Iff; 215 CLASS Pixmap And_invert, Or_invert, Not_invert, All_invert, Exists_invert, Imp_invert, Iff_invert; 216 217 CLASS Pixmap Pattern; 218 219 /* when font size is selected, following are set */ 220 CLASS int Spacing; 221 CLASS char *Or_bits, *And_bits, *Not_bits, *Imp_bits, *Iff_bits, *Exists_bits, *All_bits; 222 CLASS int Or_width, And_width, Not_width, Imp_width, Iff_width, Exists_width, All_width; 223 CLASS int Or_height, And_height, Not_height, Imp_height, Iff_height, Exists_height, All_height; 224 225 CLASS struct formula_ptr_2 *Crnt_formula; /* the top level formula */ 226 CLASS struct formula_ptr_2 *Top_formula; /* the head of the formula list */ 227 CLASS struct formula_ptr_2 *Crnt_transform; /*the current formula displayed*/ 228 229 CLASS struct formula_box *B; /* the top level formula box */ 230 CLASS int Highlighted; /* is a formula currently highlighted? */ 231 CLASS struct formula_box *Sel_area; /* the currently selected formula box */ 232 233 CLASS Widget Outline; /* widgets referenced in callbacks */ 234 CLASS Widget Canvas; 235 CLASS Widget Popup, Edit_popup, Font_popup, Message; /* popups */ 236 CLASS Widget Place_holder; 237 CLASS Widget Edit_text; 238 CLASS Widget Help_text; 239 240 CLASS char Edit_str[TEXT_LENGTH*2]; /* for conjoining, disjoining of */ 241 /* formulas */ 242 243 CLASS int Crnt_button_menu; /* the child(ren) currently displayed in the */ 244 /* button menu */ 245 246 /* the list of children to manage in button_menu */ 247 CLASS WidgetList Logic_buttons; 248 CLASS WidgetList Edit_buttons; 249 250 /* space needed for logic & edit buttons */ 251 CLASS int Logic_area_width, Logic_area_height; 252 CLASS int Edit_area_width, Edit_area_height; 253 254 CLASS String Str; /* string in the edit window */ 255 CLASS String File_str; /* string in the file window */ 256 CLASS char Help_str[500]; /* string in the help window */ 257 258 CLASS Widget Help_popup; /* help widgets */ 259 /* these need to be global so can reset sensitivities */ 260 CLASS Widget Help_info, Edit_help, Logic_help, 261 Formula_control_help, Select_area_help, 262 Cancel; 263 264 /**** function prototypes for formed.c, display.c, and callbacks.c. ****/ 265 266 /* formed.c */ 267 268 void proc_command_line(); 269 int sprint_formula(); 270 void select_area(); 271 void draw_formula_box_inverted(); 272 void display_formula(); 273 struct formula_box *do_box_geometry(); 274 struct formula_box *arrange_box(); 275 void draw_formula_box(); 276 void draw_inverted_operators(); 277 struct formula_box *find_point(); 278 void install_up_pointers(); 279 void free_formula_box_tree(); 280 void transform(); 281 struct formula_box *find_sub_box(); 282 void free_formulas(); 283 284 /* display.c */ 285 286 void setup_display(); 287 int convert_color(); 288 void user_error(); 289 void setup_font(); 290 void kill_message(); 291 void accum_size(); 292 293 /* callbacks.c */ 294 295 void edit_menu_callback(); 296 void logic_menu_callback(); 297 void comp_redo_callback(); 298 void comp_undo_callback(); 299 void next_callback(); 300 void previous_callback(); 301 void font_callback(); 302 void quit_callback(); 303 void help_callback(); 304 void help_info_callback(); 305 void return_help_menu(); 306 void set_help_string(); 307 void destroy_popup(); 308 void load_callback(); 309 void set_load_file(); 310 int load_formula_list(); 311 void save_callback(); 312 void set_save_file(); 313 int save_formula_list(); 314 void clausify_callback(); 315 void operate_callback(); 316 void nnf_callback(); 317 void skolemize_callback(); 318 void cnf_callback(); 319 void cnf_simp_callback(); 320 void rms_cnf_callback(); 321 void rms_dnf_callback(); 322 void dnf_callback(); 323 void dnf_simp_callback(); 324 void redo_callback(); 325 void undo_callback(); 326 void expandConj_callback(); 327 void expandDisj_callback(); 328 void edit_callback(); 329 void abbreviate_callback(); 330 void replace_callback(); 331 void edit_transform(); 332 struct formula *str_to_formula(); 333 struct formula *replace_text(); 334 struct formula *make_deleted(); 335 struct formula *join_formulas(); 336 struct formula_ptr_2 *find_end(); 337 void clear_text_callback(); 338 void conjoin_callback(); 339 void conjoin_with_callback(); 340 void disjoin_callback(); 341 void disjoin_with_callback(); 342 void quantify_callback(); 343 void add_quantify_callback(); 344 void negate_callback(); 345 void new_formula_callback(); 346 void insert_formula_callback(); 347 void delete_formula_callback(); 348 void unedit_callback(); 349 void reedit_callback(); 350 void font_menu_callback(); 351 void create_menu_popup(); 352 void create_edit_popup(); 353