1 /*
2 * callbacks.c -- Callbacks for the FormEd program.
3 *
4 */
5
6 #include "../header.h"
7 #include "formed.h"
8
9 #include "help_str.h"
10
11 Widget replace_button();
12 Widget conjoin_button();
13 Widget disjoin_button();
14 Widget add_quantifiers_button();
15 Widget insert_button();
16 Widget create_one_line_text_widget();
17
18 /*************************
19 *
20 * void edit_menu_callback(w, client_data, call_data)
21 *
22 *****************************/
23
edit_menu_callback(w,client_data,call_data)24 void edit_menu_callback(w, client_data, call_data)
25 Widget w;
26 XtPointer client_data;
27 XtPointer call_data;
28 {
29
30 int same_display;
31
32 same_display = 0;
33
34 /* unmanage the current child, or list of children if not the placeholder */
35 switch(Crnt_button_menu) {
36 case PLACE_HOLDER:
37 XtUnmanageChild(Place_holder);
38 break;
39 case EDIT_MENU:
40 user_error("Edit panel already displayed.\n");
41 same_display = 1;
42 break;
43 case LOGIC_MENU:
44 XtUnmanageChildren(Logic_buttons, NUM_LOGIC_BUTTONS);
45 break;
46 }
47
48 if (!same_display) {
49 XtManageChildren(Edit_buttons, NUM_EDIT_BUTTONS);
50 Crnt_button_menu = EDIT_MENU;
51 }
52
53 } /* edit_menu_callback */
54
55
56 /*************************
57 *
58 * void logic_menu_callback(w, client_data, call_data)
59 *
60 *****************************/
61
logic_menu_callback(w,client_data,call_data)62 void logic_menu_callback(w, client_data, call_data)
63 Widget w;
64 XtPointer client_data;
65 XtPointer call_data;
66 {
67 int same_display;
68
69 same_display = 0;
70
71 /* unmanage the current child, or list of children if not the placeholder */
72 switch(Crnt_button_menu) {
73 case PLACE_HOLDER:
74 XtUnmanageChild(Place_holder);
75 break;
76 case LOGIC_MENU:
77 user_error("Logic panel already displayed.\n");
78 same_display = 1;
79 break;
80 case EDIT_MENU:
81 XtUnmanageChildren(Edit_buttons, NUM_EDIT_BUTTONS);
82 break;
83 }
84
85 if (!same_display) {
86 XtManageChildren(Logic_buttons, NUM_LOGIC_BUTTONS);
87 Crnt_button_menu = LOGIC_MENU;
88 }
89
90 } /* logic_menu_callback */
91
92 /*************************
93 *
94 * void comp_redo_callback(w, client_data, call_data)
95 *
96 *****************************/
97
comp_redo_callback(w,client_data,call_data)98 void comp_redo_callback(w,client_data, call_data)
99 Widget w;
100 XtPointer client_data;
101 XtPointer call_data;
102 {
103
104 if (Crnt_formula) {
105 if (Crnt_formula->right == NULL && Crnt_formula->up == NULL)
106 user_error("Nothing exists to be redone.\n");
107 else {
108 Crnt_transform = find_end(Crnt_formula);
109 display_formula(Crnt_transform);
110 }
111 }
112 else
113 user_error("No formulas are currently loaded.\n");
114
115 } /* end comp_redo_callback */
116
117 /*************************
118 *
119 * void comp_undo_callback(w, client_data, call_data)
120 *
121 *****************************/
122
comp_undo_callback(w,client_data,call_data)123 void comp_undo_callback(w,client_data, call_data)
124 Widget w;
125 XtPointer client_data;
126 XtPointer call_data;
127 {
128
129 if (Crnt_formula) {
130 Crnt_transform = Crnt_formula;
131 display_formula(Crnt_transform);
132 }
133 else
134 user_error("No formulas are currently loaded.\n");
135
136 } /* end comp_undo_callback */
137
138 /*************************
139 *
140 * void next_callback(w, client_data, call_data)
141 *
142 *****************************/
143
next_callback(w,client_data,call_data)144 void next_callback(w,client_data, call_data)
145 Widget w;
146 XtPointer client_data;
147 XtPointer call_data;
148 {
149
150
151 if (Crnt_formula) {
152 /* display next formula, if have one */
153
154 if (Crnt_formula->next) {
155 Crnt_formula = Crnt_formula->next;
156 Crnt_transform = find_end(Crnt_formula);
157 display_formula(Crnt_transform);
158 }
159 else
160 user_error("End of formula list.\n");
161 }
162 else
163 user_error("No formulas are currently loaded.\n");
164
165 } /* next_callback */
166
167 /*************************
168 *
169 * void previous_callback(w, client_data, call_data)
170 *
171 *****************************/
172
previous_callback(w,client_data,call_data)173 void previous_callback(w,client_data, call_data)
174 Widget w;
175 XtPointer client_data;
176 XtPointer call_data;
177 {
178
179
180 if (Crnt_formula) {
181
182 /* display previous formula, if have one */
183
184 if (Crnt_formula->prev) {
185 Crnt_formula = Crnt_formula->prev;
186 Crnt_transform = find_end(Crnt_formula);
187 display_formula(Crnt_transform);
188 }
189 else
190 user_error("Beginning of formula list.\n");
191 }
192 else
193 user_error("No formulas are currently loaded.\n");
194
195 } /* end previous_callback */
196
197 /*************************
198 *
199 * void font_callback(w, client_data, call_data)
200 *
201 *****************************/
202
font_callback(w,client_data,call_data)203 void font_callback(w,client_data, call_data)
204 Widget w;
205 XtPointer client_data;
206 XtPointer call_data;
207 {
208
209
210 XtDestroyWidget(Popup);
211
212 /* redisplay formula if have one */
213
214 setup_font((char *) client_data);
215
216 if (Crnt_formula)
217 display_formula(Crnt_transform);
218
219 } /* end font_callback */
220
221
222 /*************************
223 *
224 * void quit_callback(w, client_data, call_data)
225 *
226 *****************************/
227
quit_callback(w,client_data,call_data)228 void quit_callback(w,client_data, call_data)
229 Widget w;
230 XtPointer client_data;
231 XtPointer call_data;
232 {
233 print_mem(stdout);
234 exit(0);
235
236 } /* end quit_callback */
237
238 /*************************
239 *
240 * void help_callback(w, client_data, call_data)
241 *
242 *****************************/
243
help_callback(w,client_data,call_data)244 void help_callback(w,client_data, call_data)
245 Widget w;
246 XtPointer client_data;
247 XtPointer call_data;
248 {
249 Widget help_menu_form;
250 int n;
251 Arg arg[10];
252
253
254 create_menu_popup("Help", w); /* create the popup shell */
255
256 n = 0;
257 XtSetArg(arg[n], XtNbackground, Background); n++;
258 help_menu_form = XtCreateManagedWidget("help_menu_form", formWidgetClass,
259 Popup, arg, n);
260
261
262 /* command buttons */
263
264 /* how to use help */
265 n = 0;
266 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
267 XtSetArg(arg[n], XtNlabel, "How to use Help");n++;
268 Help_info = XtCreateManagedWidget("help_info",commandWidgetClass,
269 help_menu_form,arg,n);
270 XtAddCallback(Help_info, XtNcallback, help_info_callback, Help_info);
271
272 /* Edit buttons */
273 n = 0;
274 XtSetArg(arg[n], XtNfromVert, Help_info); n++;
275 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
276 XtSetArg(arg[n], XtNlabel, "Edit Menu Buttons");n++;
277 Edit_help = XtCreateManagedWidget("edit_help", commandWidgetClass,
278 help_menu_form, arg, n);
279 XtAddCallback(Edit_help, XtNcallback, help_info_callback, Edit_help);
280
281 /* Logic buttons */
282 n = 0;
283 XtSetArg(arg[n], XtNfromVert, Edit_help); n++;
284 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
285 XtSetArg(arg[n], XtNlabel, "Logic Menu Buttons");n++;
286 Logic_help = XtCreateManagedWidget("logic_help", commandWidgetClass,
287 help_menu_form, arg, n);
288 XtAddCallback(Logic_help, XtNcallback, help_info_callback, Logic_help);
289
290 /* formula control buttons */
291 n = 0;
292 XtSetArg(arg[n], XtNfromVert, Logic_help); n++;
293 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
294 XtSetArg(arg[n], XtNlabel, "Formula Control Buttons");n++;
295 Formula_control_help = XtCreateManagedWidget("formula_control_help",
296 commandWidgetClass,
297 help_menu_form, arg, n);
298 XtAddCallback(Formula_control_help, XtNcallback, help_info_callback,
299 Formula_control_help);
300
301 /* selecting formula area information */
302 n = 0;
303 XtSetArg(arg[n], XtNfromVert, Formula_control_help); n++;
304 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
305 XtSetArg(arg[n], XtNlabel, "Selecting Formula Areas");n++;
306 Select_area_help = XtCreateManagedWidget("select_area_help",
307 commandWidgetClass,
308 help_menu_form, arg, n);
309 XtAddCallback(Select_area_help, XtNcallback, help_info_callback,
310 Select_area_help);
311
312 /* cancel */
313 n = 0;
314 XtSetArg(arg[n], XtNfromVert, Select_area_help); n++;
315 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
316 XtSetArg(arg[n], XtNlabel, "Cancel"); n++;
317 Cancel = XtCreateManagedWidget("cancel",commandWidgetClass,
318 help_menu_form, arg, n);
319 XtAddCallback(Cancel, XtNcallback, destroy_popup, Popup);
320
321 XtPopup(Popup, XtGrabNone);
322
323 } /* end help_callback */
324
325
326 /*************************
327 *
328 * void help_info_callback(entry, client_data, call_data)
329 *
330 *****************************/
331
help_info_callback(entry,client_data,call_data)332 void help_info_callback(entry,client_data, call_data)
333 Widget entry;
334 XtPointer client_data;
335 XtPointer call_data;
336 {
337 Widget selected_help = (Widget) client_data;
338 int n;
339 Arg arg[10];
340 Dimension width, height;
341 Position x, y;
342 Widget help_label, help_form, help_return, help_list;
343
344 /* make the buttons in the main menu insensitive */
345 /* until a return to menu has been issued */
346
347 XtSetArg(arg[0], XtNsensitive, False);
348 XtSetValues(Help_info, arg, 1);
349
350 XtSetArg(arg[0], XtNsensitive, False);
351 XtSetValues(Edit_help, arg, 1);
352
353 XtSetArg(arg[0], XtNsensitive, False);
354 XtSetValues(Logic_help, arg, 1);
355
356 XtSetArg(arg[0], XtNsensitive, False);
357 XtSetValues(Formula_control_help, arg, 1);
358
359 XtSetArg(arg[0], XtNsensitive, False);
360 XtSetValues(Select_area_help, arg, 1);
361
362 XtSetArg(arg[0], XtNsensitive, False);
363 XtSetValues(Cancel, arg, 1);
364
365 /* create the shell */
366 n = 0;
367 XtSetArg(arg[n], XtNwidth, &width); n++;
368 XtSetArg(arg[n], XtNheight, &height); n++;
369 XtGetValues(Outline, arg, n);
370 XtTranslateCoords(Outline, (Position)((width/2)-200),
371 (Position)(height/2-150), &x, &y);
372
373 n = 0;
374 XtSetArg(arg[n], XtNx, x); n++;
375 XtSetArg(arg[n], XtNy, y); n++;
376 Help_popup = XtCreatePopupShell("Help_popup", transientShellWidgetClass,
377 Outline, arg, n);
378
379 /* form widget to hold buttons & text */
380 n = 0;
381 XtSetArg(arg[n], XtNforeground, Foreground); n++;
382 help_form = XtCreateManagedWidget("help_form", formWidgetClass,
383 Help_popup, arg, n);
384
385 /* help label */
386 n = 0;
387 XtSetArg(arg[n], XtNlabel, "Help"); n++;
388 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
389 XtSetArg(arg[n], XtNbackground, Background); n++;
390 XtSetArg(arg[n], XtNwidth, 300); n++;
391 XtSetArg(arg[n], XtNborderWidth, 0); n++;
392 help_label = XtCreateManagedWidget("help_label", labelWidgetClass,
393 help_form, arg, n);
394
395 /* return to help menu selection */
396 n = 0;
397 XtSetArg(arg[n], XtNfromVert, help_label); n++;
398 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
399 XtSetArg(arg[n], XtNlabel, "Return to Help Menu"); n++;
400 help_return = XtCreateManagedWidget("help_return", commandWidgetClass,
401 help_form, arg, n);
402 XtAddCallback(help_return, XtNcallback, return_help_menu, NULL);
403
404 /* list of buttons to choose for information on */
405 if (selected_help == Help_info)
406 strcpy(Help_str, Help_info_text);
407 else if (selected_help == Select_area_help)
408 strcpy(Help_str, Select_area_help_text);
409 else {
410 n = 0;
411 XtSetArg(arg[n], XtNfromVert, help_return); n++;
412 if (selected_help == Edit_help) {
413 XtSetArg(arg[n], XtNdefaultColumns, 3); n++;
414 XtSetArg(arg[n], XtNlist, Edit_help_items); n++;
415 }
416 else if (selected_help == Logic_help) {
417 XtSetArg(arg[n], XtNdefaultColumns, 4); n++;
418 XtSetArg(arg[n], XtNlist, Logic_help_items); n++;
419 }
420 else if (selected_help == Formula_control_help) {
421 XtSetArg(arg[n], XtNdefaultColumns, 4); n++;
422 XtSetArg(arg[n], XtNlist, Formula_control_help_items); n++;
423 }
424
425 help_list = XtCreateManagedWidget("help_list", listWidgetClass, help_form,
426 arg, n);
427 XtAddCallback(help_list, XtNcallback, set_help_string, selected_help);
428
429 strcpy(Help_str, " ");
430
431 }
432
433 /* text box */
434
435 n = 0;
436 if ((selected_help == Help_info) || (selected_help == Select_area_help)) {
437 XtSetArg(arg[n], XtNfromVert, help_return); n++;
438 }
439 else {
440 XtSetArg(arg[n], XtNfromVert, help_list); n++;
441 }
442 XtSetArg(arg[n], XtNforeground, Foreground); n++;
443 XtSetArg(arg[n], XtNbackground, Background); n++;
444 XtSetArg(arg[n], XtNstring, Help_str); n++;
445 XtSetArg(arg[n], XtNwrap, XawtextWrapWord); n++;
446 XtSetArg(arg[n], XtNdisplayCaret, False); n++;
447 XtSetArg(arg[n], XtNwidth, 300); n++;
448 XtSetArg(arg[n], XtNheight, 275); n++;
449 Help_text = XtCreateManagedWidget("help_text",asciiTextWidgetClass,
450 help_form, arg, n);
451
452 XtPopup(Help_popup, XtGrabNone);
453
454
455 } /* help_info_callback */
456
457
458 /*************************
459 *
460 * void return_help_menu(entry, client_data, call_data)
461 *
462 *****************************/
463
return_help_menu(entry,client_data,call_data)464 void return_help_menu(entry,client_data, call_data)
465 Widget entry;
466 XtPointer client_data;
467 XtPointer call_data;
468 {
469 Arg arg[1];
470
471 /* reset the sensitivity of the help menu buttons */
472 XtSetArg(arg[0], XtNsensitive, True);
473 XtSetValues(Help_info, arg, 1);
474
475 XtSetArg(arg[0], XtNsensitive, True);
476 XtSetValues(Edit_help, arg, 1);
477
478 XtSetArg(arg[0], XtNsensitive, True);
479 XtSetValues(Logic_help, arg, 1);
480
481 XtSetArg(arg[0], XtNsensitive, True);
482 XtSetValues(Formula_control_help, arg, 1);
483
484 XtSetArg(arg[0], XtNsensitive, True);
485 XtSetValues(Select_area_help, arg, 1);
486
487 XtSetArg(arg[0], XtNsensitive, True);
488 XtSetValues(Cancel, arg, 1);
489
490 /* destroy the help popup */
491 XtDestroyWidget(Help_popup);
492
493
494 /* redisplay formula if have one */
495 if (Crnt_formula)
496 display_formula(Crnt_transform);
497
498
499 } /* return_help_menu */
500
501 /*************************
502 *
503 * void set_help_string(entry, client_data, call_data)
504 *
505 *****************************/
506
set_help_string(entry,client_data,call_data)507 void set_help_string(entry,client_data, call_data)
508 Widget entry;
509 XtPointer client_data;
510 XtPointer call_data;
511 {
512
513 XawListReturnStruct *item = (XawListReturnStruct *)call_data;
514 Widget help_set = (Widget) client_data; /* which set of help selected */
515
516 Arg arg[1];
517
518 /* get appropriate string */
519
520 if (help_set == Edit_help)
521 strcpy(Help_str, Edit_help_text[item->list_index]);
522 else if (help_set == Logic_help)
523 strcpy(Help_str, Logic_help_text[item->list_index]);
524 else
525 strcpy(Help_str, Formula_control_help_text[item->list_index]);
526
527
528 /* reset the string in the widget */
529 XtSetArg(arg[0], XtNstring, Help_str);
530 XtSetValues(Help_text, arg, 1);
531
532 } /* set_help_string */
533
534
535 /*************************
536 *
537 * void destroy_popup(w, client_data, call_data)
538 *
539 *****************************/
540
destroy_popup(w,client_data,call_data)541 void destroy_popup(w, client_data, call_data)
542 Widget w;
543 XtPointer client_data;
544 XtPointer call_data;
545 {
546
547 XtDestroyWidget(client_data);
548
549 /* redisplay formula if have one */
550 if (Crnt_formula)
551 display_formula(Crnt_transform);
552
553
554 } /* destroy_popup */
555
556 /*************************
557 *
558 * void load_callback(entry, client_data, call_data)
559 *
560 *****************************/
561
load_callback(entry,client_data,call_data)562 void load_callback(entry,client_data, call_data)
563 Widget entry;
564 XtPointer client_data;
565 XtPointer call_data;
566 {
567 Widget load_form, load_label, file_text, load_file, cancel;
568 Arg arg[10];
569 int n;
570
571 create_menu_popup("Load", entry); /* create the popup shell */
572
573 n = 0;
574 XtSetArg(arg[n], XtNbackground, Background); n++;
575 load_form = XtCreateManagedWidget("load_form", formWidgetClass,
576 Popup, arg, n);
577
578 n = 0;
579 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
580 XtSetArg(arg[n], XtNbackground, Background); n++;
581 XtSetArg(arg[n], XtNborderWidth, 0); n++;
582 XtSetArg(arg[n], XtNlabel, "Filename:");n++;
583 load_label = XtCreateManagedWidget("load_label", labelWidgetClass,
584 load_form,arg,n);
585
586 /* file name */
587 n = 0;
588 XtSetArg(arg[n], XtNfromVert, load_label); n++;
589 XtSetArg(arg[n], XtNforeground, Foreground); n++;
590 XtSetArg(arg[n], XtNeditType, XawtextEdit); n++;
591 XtSetArg(arg[n], XtNwidth, 176); n++;
592 XtSetArg(arg[n], XtNstring, Crnt_file); n++;
593 file_text = XtCreateManagedWidget("file_text", asciiTextWidgetClass,
594 load_form, arg, n);
595
596 n = 0;
597 XtSetArg(arg[n], XtNfromVert, file_text); n++;
598 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
599 XtSetArg(arg[n], XtNlabel, "Load file");n++;
600 load_file = XtCreateManagedWidget("load_file",commandWidgetClass,
601 load_form,arg,n);
602 XtAddCallback(load_file, XtNcallback, set_load_file, file_text);
603
604 n = 0;
605 XtSetArg(arg[n], XtNfromVert, file_text); n++;
606 XtSetArg(arg[n], XtNfromHoriz, load_file); n++;
607 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
608 XtSetArg(arg[n], XtNlabel, "Cancel");n++;
609 cancel = XtCreateManagedWidget("cancel",commandWidgetClass,
610 load_form,arg,n);
611 XtAddCallback(cancel, XtNcallback, destroy_popup, Popup);
612
613
614 XtPopup(Popup, XtGrabNone);
615
616 } /* end load_callback */
617
618
619 /*************************
620 *
621 * void set_load_file(button, client_data, call_data)
622 *
623 *****************************/
624
set_load_file(button,client_data,call_data)625 void set_load_file(button, client_data, call_data)
626 Widget button;
627 XtPointer client_data;
628 XtPointer call_data;
629 {
630 Widget file_name = (Widget) client_data;
631 int c;
632 Arg arg[1];
633
634 XtSetArg(arg[0], XtNstring, &File_str);
635 XtGetValues(file_name, arg, 1);
636
637 strcpy(Crnt_file, File_str);
638
639 /* attempt to save list, if any errors, return to popup */
640 /* if no errors, set up pointers and display first formula */
641
642 c = load_formula_list(Crnt_file);
643 if (c) {
644 XtDestroyWidget(Popup); /* remove load file popup */
645
646 /* display first formula */
647 Top_formula = Crnt_formula;
648 Crnt_transform = Crnt_formula;
649 display_formula(Crnt_transform);
650 if (Display_setup)
651 user_error("File loaded.\n");
652 }
653
654 } /* set_load_file */
655
656
657 /*************************
658 *
659 * int load_formula_list(filename)
660 *
661 *****************************/
662
load_formula_list(filename)663 int load_formula_list(filename)
664 char filename[];
665 {
666 int errors;
667 struct formula_ptr *p1, *p2;
668 struct formula_ptr_2 *q1, *q2;
669 struct formula *f;
670 FILE *fp;
671
672 fp = fopen(Crnt_file, "r");
673 if (fp == NULL && Display_setup) {
674 strcpy(Error_string, "Error: Cannot open ");
675 strcat(Error_string, Crnt_file);
676 strcat(Error_string, ".\n");
677 user_error(Error_string);
678 return(0);
679 }
680 else {
681 p1 = read_formula_list(fp, &errors);
682
683 if (errors)
684 exit(1);
685
686 q2 = NULL;
687 while (p1) {
688 q1 = get_formula_ptr_2();
689 q1->f = p1->f;
690 install_up_pointers(q1->f);
691 q1->f->parent = NULL;
692 q1->prev = q2;
693 if (q2)
694 q2->next = q1;
695 else
696 Crnt_formula = q1;
697 q2 = q1;
698 p2 = p1;
699 p1 = p1->next;
700 free_formula_ptr(p2);
701 }
702
703 /* print out formulas loaded in to the screen */
704
705 q2 = Crnt_formula;
706 while (q2 != NULL) {
707 print_formula(stdout, q2->f);
708 fprintf(stdout, ".\n");
709 q2 = q2->next;
710 }
711
712 fclose(fp);
713
714 return(1);
715
716 }
717
718 } /* load_formula_list */
719
720 /*************************
721 *
722 * void save_callback(w, client_data, call_data)
723 *
724 *****************************/
725
save_callback(entry,client_data,call_data)726 void save_callback(entry,client_data, call_data)
727 Widget entry;
728 XtPointer client_data;
729 XtPointer call_data;
730 {
731
732 Widget save_form, save_label, file_text, save_file, cancel;
733 Arg arg[10];
734 int n;
735
736
737 if (Crnt_formula) {
738
739 create_menu_popup("Save", entry); /* create the popup shell */
740
741 n = 0;
742 XtSetArg(arg[n], XtNbackground, Background); n++;
743 save_form = XtCreateManagedWidget("save_form", formWidgetClass,
744 Popup, arg, n);
745
746 n = 0;
747 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
748 XtSetArg(arg[n], XtNbackground, Background); n++;
749 XtSetArg(arg[n], XtNborderWidth, 0); n++;
750 XtSetArg(arg[n], XtNlabel, "Filename:");n++;
751 save_label = XtCreateManagedWidget("save_label", labelWidgetClass,
752 save_form,arg,n);
753
754 /* file name */
755 n = 0;
756 XtSetArg(arg[n], XtNfromVert, save_label); n++;
757 XtSetArg(arg[n], XtNforeground, Foreground); n++;
758 XtSetArg(arg[n], XtNeditType, XawtextEdit); n++;
759 XtSetArg(arg[n], XtNwidth, 176); n++;
760 XtSetArg(arg[n], XtNstring, Crnt_file); n++;
761 file_text = XtCreateManagedWidget("file_text", asciiTextWidgetClass,
762 save_form, arg, n);
763
764 n = 0;
765 XtSetArg(arg[n], XtNfromVert, file_text); n++;
766 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
767 XtSetArg(arg[n], XtNlabel, "Save file");n++;
768 save_file = XtCreateManagedWidget("save_file",commandWidgetClass,
769 save_form,arg,n);
770 XtAddCallback(save_file, XtNcallback, set_save_file, file_text);
771
772 n = 0;
773 XtSetArg(arg[n], XtNfromVert, file_text); n++;
774 XtSetArg(arg[n], XtNfromHoriz, save_file); n++;
775 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
776 XtSetArg(arg[n], XtNlabel, "Cancel");n++;
777 cancel = XtCreateManagedWidget("cancel",commandWidgetClass,
778 save_form,arg,n);
779 XtAddCallback(cancel, XtNcallback, destroy_popup, Popup);
780
781 XtPopup(Popup, XtGrabNone);
782 }
783
784 else
785 user_error("No formulas are currently loaded.\n");
786
787 } /* end save_callback */
788
789 /*************************
790 *
791 * void set_save_file(button, client_data, call_data)
792 *
793 *****************************/
794
set_save_file(button,client_data,call_data)795 void set_save_file(button, client_data, call_data)
796 Widget button;
797 XtPointer client_data;
798 XtPointer call_data;
799 {
800
801 Widget file_name = (Widget) client_data;
802 int c;
803 Arg arg[1];
804
805 XtSetArg(arg[0], XtNstring, &File_str);
806 XtGetValues(file_name, arg, 1);
807
808 strcpy(Crnt_file, File_str);
809
810 /* attempt to save list, if any errors, return to popup */
811
812 c = save_formula_list(Crnt_file);
813
814 if (c) {
815
816 XtDestroyWidget(Popup);
817
818 /* redisplay formula if have one */
819 if (Crnt_formula)
820 display_formula(Crnt_transform);
821
822 if (Display_setup)
823 user_error("File saved.\n");
824 }
825
826 } /* set_save_file */
827
828
829 /*************************
830 *
831 * int save_formula_list(filename)
832 *
833 *****************************/
834
save_formula_list(filename)835 int save_formula_list(filename)
836 char filename[];
837 {
838 FILE *fp;
839 struct formula_ptr_2 *p, *q;
840
841 if ((fp = fopen(filename,"w")) == NULL && Display_setup) {
842 strcpy(Error_string, "Error: cannot open ");
843 strcat(Error_string, filename);
844 strcat(Error_string, ".\n");
845 user_error(Error_string);
846 return(0);
847 }
848 else {
849
850 /* save the formula list pointed to by Top_formula */
851
852 p = Top_formula;
853 while(p) {
854 q = find_end(p); /* find end of current transformation list */
855 print_formula(fp, q->f);
856 fprintf(fp,".\n");
857 p = p->next;
858 }
859
860
861 fclose(fp);
862 return(1);
863 }
864
865 } /* save_formula_list */
866
867
868 /*******************
869 * LOGIC CALLBACKS
870 ********************/
871
872 /*************************
873 *
874 * void clausify_callback(w, client_data, call_data)
875 *
876 *****************************/
877
clausify_callback(w,client_data,call_data)878 void clausify_callback(w,client_data, call_data)
879 Widget w;
880 XtPointer client_data;
881 XtPointer call_data;
882 {
883 struct formula *f;
884
885
886 if (Crnt_formula) {
887 if (Sel_area != B)
888 user_error("Clausify is done on the entire formula,\nno selections necessary.\n");
889 else {
890 f = Sel_area->f;
891 transform(f, clausify_formed);
892 user_error("WARNING: further logic transformations may be unsound,\nbecuase universal quantifiers are gone.\n");
893 }
894 }
895 else
896 user_error("No formulas are currently loaded.\n");
897
898 } /* end clausify_callback */
899
900
901 /*************************
902 *
903 * void operate_callback(w, client_data, call_data)
904 *
905 *****************************/
906
operate_callback(w,client_data,call_data)907 void operate_callback(w,client_data, call_data)
908 Widget w;
909 XtPointer client_data;
910 XtPointer call_data;
911 {
912
913 struct formula *f;
914 int n;
915 Arg arg[10];
916 Widget to_conj, to_disj, cancel, iff_form;
917
918
919 if (Crnt_formula) {
920 if (Sel_area->type != OPERATOR)
921 user_error("Operate requires selection of\nan operator (not, imp, iff).\n");
922 else {
923 /* depending on type of operator, perform transformation */
924 switch(Sel_area->subtype) {
925 case NOT_OP:
926 f = Sel_area->parent->f;
927 transform(f, negation_inward);
928 break;
929
930 case IMP_OP:
931 f = Sel_area->parent->f;
932 transform(f, expand_imp);
933 break;
934
935 case IFF_OP:
936 /* create a popup widget, for to conj or disj */
937
938 create_menu_popup("Iff_op", w);
939
940 n = 0;
941 XtSetArg(arg[n], XtNbackground, Background); n++;
942 iff_form = XtCreateManagedWidget("iff_form", formWidgetClass,
943 Popup, arg, n);
944
945 /* command buttons */
946 n = 0;
947 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
948 XtSetArg(arg[n], XtNlabel, "To Conj");n++;
949 to_conj = XtCreateManagedWidget("to_conj",commandWidgetClass,
950 iff_form,arg,n);
951 XtAddCallback(to_conj, XtNcallback, expandConj_callback, NULL);
952
953 n = 0;
954 XtSetArg(arg[n], XtNfromVert, to_conj); n++;
955 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
956 XtSetArg(arg[n], XtNlabel, "To Disj");n++;
957 to_disj = XtCreateManagedWidget("to_disj",commandWidgetClass,
958 iff_form,arg,n);
959 XtAddCallback(to_disj, XtNcallback, expandDisj_callback, NULL);
960
961 n = 0;
962 XtSetArg(arg[n], XtNfromVert, to_disj); n++;
963 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT));n++;
964 XtSetArg(arg[n], XtNlabel, "Cancel");n++;
965 cancel = XtCreateManagedWidget("cancel",commandWidgetClass,
966 iff_form,arg,n);
967 XtAddCallback(cancel, XtNcallback, destroy_popup, Popup);
968
969 XtPopup(Popup, XtGrabNone);
970
971 break;
972
973 default:
974 user_error("Operate requires selection of not, imp, or iff operators.");
975 break;
976 }
977 }
978 }
979 else
980 user_error("No formulas are currently loaded.\n");
981
982 } /* operate_callback */
983
984 /*************************
985 *
986 * void nnf_callback(w, client_data, call_data)
987 *
988 *****************************/
989
nnf_callback(w,client_data,call_data)990 void nnf_callback(w,client_data, call_data)
991 Widget w;
992 XtPointer client_data;
993 XtPointer call_data;
994 {
995 struct formula *f;
996
997
998 if (Crnt_formula) {
999
1000 if (Sel_area->type != FORMULA)
1001 user_error("NNF requires a formula (or subformula) as a selection.\n");
1002 else {
1003 f = Sel_area->f;
1004 transform(f, nnf);
1005 }
1006 }
1007 else
1008 user_error("No formulas are currently loaded.\n");
1009
1010 } /* end nnf_callback */
1011
1012 /*************************
1013 *
1014 * void skolemize_callback(w, client_data, call_data)
1015 *
1016 *****************************/
1017
skolemize_callback(w,client_data,call_data)1018 void skolemize_callback(w,client_data, call_data)
1019 Widget w;
1020 XtPointer client_data;
1021 XtPointer call_data;
1022 {
1023 struct formula *f;
1024
1025
1026 if (Crnt_formula) {
1027
1028 if (Sel_area != B)
1029 user_error("Skolemize is done on the entire formula,\nno selections necessary.\n");
1030 else {
1031 f = Sel_area->f;
1032 transform(f, nnf_skolemize);
1033 }
1034 }
1035 else
1036 user_error("No formulas are currently loaded.\n");
1037
1038 } /* end skolemize_callback */
1039
1040 /*************************
1041 *
1042 * void cnf_callback(w, client_data, call_data)
1043 *
1044 *****************************/
1045
cnf_callback(w,client_data,call_data)1046 void cnf_callback(w,client_data, call_data)
1047 Widget w;
1048 XtPointer client_data;
1049 XtPointer call_data;
1050 {
1051 struct formula *f;
1052
1053
1054 if (Crnt_formula) {
1055
1056 if (Sel_area->type != FORMULA)
1057 user_error("CNF requires a formula (or subformula) as a selection.\n");
1058 else {
1059 f = Sel_area->f;
1060 transform(f, nnf_cnf);
1061 }
1062 }
1063 else
1064 user_error("No formulas are currently loaded.\n");
1065
1066 } /* end cnf_callback */
1067
1068 /*************************
1069 *
1070 * void cnf_simp_callback(w, client_data, call_data)
1071 *
1072 *****************************/
1073
cnf_simp_callback(w,client_data,call_data)1074 void cnf_simp_callback(w,client_data, call_data)
1075 Widget w;
1076 XtPointer client_data;
1077 XtPointer call_data;
1078 {
1079 struct formula *f;
1080
1081
1082 if (Crnt_formula) {
1083
1084 if (Sel_area->type != FORMULA)
1085 user_error("CNF requires a formula (or subformula) as a selection.\n");
1086 else {
1087 f = Sel_area->f;
1088 Flags[SIMPLIFY_FOL].val = 1;
1089 transform(f, rms_cnf); /* nnf_cnf, or rms_cnf for quants */
1090 Flags[SIMPLIFY_FOL].val = 0;
1091 }
1092 }
1093 else
1094 user_error("No formulas are currently loaded.\n");
1095
1096 } /* end cnf_simp_callback */
1097
1098 /*************************
1099 *
1100 * void rms_cnf_callback(w, client_data, call_data)
1101 *
1102 *****************************/
1103
rms_cnf_callback(w,client_data,call_data)1104 void rms_cnf_callback(w,client_data, call_data)
1105 Widget w;
1106 XtPointer client_data;
1107 XtPointer call_data;
1108 {
1109 struct formula *f;
1110
1111
1112 if (Crnt_formula) {
1113
1114 if (Sel_area->type != FORMULA)
1115 user_error("RMS CNF requires a formula (or subformula) as a selection.\n");
1116 else {
1117 f = Sel_area->f;
1118 transform(f, rms_cnf);
1119 }
1120 }
1121 else
1122 user_error("No formulas are currently loaded.\n");
1123
1124 } /* end rms_cnf_callback */
1125
1126 /*************************
1127 *
1128 * void rms_dnf_callback(w, client_data, call_data)
1129 *
1130 *****************************/
1131
rms_dnf_callback(w,client_data,call_data)1132 void rms_dnf_callback(w,client_data, call_data)
1133 Widget w;
1134 XtPointer client_data;
1135 XtPointer call_data;
1136 {
1137 struct formula *f;
1138
1139
1140 if (Crnt_formula) {
1141
1142 if (Sel_area->type != FORMULA)
1143 user_error("RMS DNF requires a formula (or subformula) as a selection.\n");
1144 else {
1145 f = Sel_area->f;
1146 transform(f, rms_dnf);
1147 }
1148 }
1149 else
1150 user_error("No formulas are currently loaded.\n");
1151
1152 } /* end rms_dnf_callback */
1153
1154 /*************************
1155 *
1156 * void dnf_callback(w, client_data, call_data)
1157 *
1158 *****************************/
1159
dnf_callback(w,client_data,call_data)1160 void dnf_callback(w, client_data, call_data)
1161 Widget w;
1162 XtPointer client_data;
1163 XtPointer call_data;
1164 {
1165 struct formula *f;
1166
1167
1168 if (Crnt_formula) {
1169
1170 if (Sel_area->type != FORMULA)
1171 user_error("DNF requires a formula (or subformula) as a selection.\n");
1172 else {
1173 f = Sel_area->f;
1174 transform(f, nnf_dnf);
1175 }
1176 }
1177 else
1178 user_error("No formulas are currently loaded.\n");
1179
1180 } /* end dnf_callback */
1181
1182 /*************************
1183 *
1184 * void dnf_simp_callback(w, client_data, call_data)
1185 *
1186 *****************************/
1187
dnf_simp_callback(w,client_data,call_data)1188 void dnf_simp_callback(w, client_data, call_data)
1189 Widget w;
1190 XtPointer client_data;
1191 XtPointer call_data;
1192 {
1193 struct formula *f;
1194
1195
1196 if (Crnt_formula) {
1197
1198 if (Sel_area->type != FORMULA)
1199 user_error("DNF requires a formula (or subformula) as a selection.\n");
1200 else {
1201 f = Sel_area->f;
1202 Flags[SIMPLIFY_FOL].val = 1;
1203 transform(f, rms_dnf); /* nnf_dnf, or rms_dnf for quants */
1204 Flags[SIMPLIFY_FOL].val = 0;
1205 }
1206 }
1207 else
1208 user_error("No formulas are currently loaded.\n");
1209 } /* end dnf_simp_callback */
1210
1211 /*************************
1212 *
1213 * void redo_callback(w, client_data, call_data)
1214 *
1215 *****************************/
1216
redo_callback(w,client_data,call_data)1217 void redo_callback(w,client_data, call_data)
1218 Widget w;
1219 XtPointer client_data;
1220 XtPointer call_data;
1221 {
1222
1223 if (Crnt_formula) {
1224 if (Crnt_transform->right == NULL)
1225 user_error("Nothing more to be redone.\n");
1226 else {
1227 Crnt_transform = Crnt_transform->right;
1228 display_formula(Crnt_transform);
1229 }
1230 }
1231 else
1232 user_error("No formulas are currently loaded.\n");
1233
1234 } /* end redo_callback */
1235
1236 /*************************
1237 *
1238 * void undo_callback(w, client_data, call_data)
1239 *
1240 *****************************/
1241
undo_callback(w,client_data,call_data)1242 void undo_callback(w,client_data, call_data)
1243 Widget w;
1244 XtPointer client_data;
1245 XtPointer call_data;
1246 {
1247
1248
1249 if (Crnt_formula) {
1250 if (Crnt_transform->left == NULL)
1251 user_error("Nothing more to be undone.\n");
1252 else {
1253 Crnt_transform = Crnt_transform->left;
1254 display_formula(Crnt_transform);
1255 }
1256 }
1257 else
1258 user_error("No formulas are currently loaded.\n");
1259
1260 } /* end undo_callback */
1261
1262 /*************************
1263 *
1264 * void expandConj_callback(w, client_data, call_data)
1265 *
1266 *****************************/
1267
expandConj_callback(w,client_data,call_data)1268 void expandConj_callback(w,client_data, call_data)
1269 Widget w;
1270 XtPointer client_data;
1271 XtPointer call_data;
1272 {
1273 struct formula *f;
1274
1275 XtDestroyWidget(Popup); /* remove the popup with iff options */
1276
1277 f = Sel_area->parent->f;
1278 transform(f, iff_to_conj);
1279
1280 } /* end expandConj_callback */
1281
1282 /*************************
1283 *
1284 * void expandDisj_callback(w, client_data, call_data)
1285 *
1286 *****************************/
1287
expandDisj_callback(w,client_data,call_data)1288 void expandDisj_callback(w,client_data, call_data)
1289 Widget w;
1290 XtPointer client_data;
1291 XtPointer call_data;
1292 {
1293 struct formula *f;
1294
1295 XtDestroyWidget(Popup); /* remove the popup with iff options */
1296
1297 f = Sel_area->parent->f;
1298 transform(f, iff_to_disj);
1299
1300 } /* end expandDisj_callback */
1301
1302 /*************************
1303 *
1304 * void edit_callback(w, client_data, call_data)
1305 *
1306 *****************************/
1307
edit_callback(w,client_data,call_data)1308 void edit_callback(w,client_data, call_data)
1309 Widget w;
1310 XtPointer client_data;
1311 XtPointer call_data;
1312 {
1313 struct formula *f;
1314
1315 strcpy(Edit_str, "\0");
1316
1317
1318 if (Crnt_formula) {
1319
1320 if (Sel_area->type == FORMULA) {
1321
1322 /* get the selected area in a string */
1323 f = Sel_area->f;
1324 sprint_formula(Edit_str, f);
1325
1326 /* create a popup text widget with a replace button */
1327 create_edit_popup(replace_button);
1328 }
1329 else
1330 user_error("Edit requires a formula (or subformula) as a selection.\n");
1331 }
1332 else
1333 user_error("No formulas are currently loaded.\n");
1334
1335 } /* end edit_callback */
1336
1337 /*************************
1338 *
1339 * void abbreviate_callback(w, client_data, call_data)
1340 *
1341 *****************************/
1342
abbreviate_callback(w,client_data,call_data)1343 void abbreviate_callback(w,client_data, call_data)
1344 Widget w;
1345 XtPointer client_data;
1346 XtPointer call_data;
1347 {
1348 struct formula *f;
1349
1350 printf("called abbreviate_callback.\n");
1351
1352 } /* abbreviate_callback */
1353
1354 /*************************
1355 *
1356 * void replace_callback(w, client_data, call_data)
1357 *
1358 *****************************/
1359
replace_callback(w,client_data,call_data)1360 void replace_callback(w,client_data, call_data)
1361 Widget w;
1362 XtPointer client_data;
1363 XtPointer call_data;
1364 {
1365 Arg arg[1];
1366
1367 struct formula *f1 = (struct formula *) client_data;
1368
1369
1370 XtSetArg(arg[0], XtNstring, &Str);
1371 XtGetValues(Edit_text, arg, 1);
1372
1373 edit_transform(f1, replace_text);
1374
1375 if (!Have_message)
1376 XtDestroyWidget(Edit_popup);
1377
1378 } /* end replace_callback */
1379
1380 /*************************
1381 *
1382 * void edit_transform(f, trans_proc, flag)
1383 *
1384 *****************************/
1385
edit_transform(f,trans_proc,flag)1386 void edit_transform(f, trans_proc, flag)
1387 struct formula *f;
1388 struct formula *(*trans_proc)();
1389 int flag;
1390 {
1391 struct formula *copy, *parent, *prev, *f1, *save_next;
1392 struct formula_ptr_2 *p, *q;
1393 struct formula_box *sub_box;
1394
1395 parent = f->parent;
1396 if (parent) {
1397 prev = NULL;
1398 for (f1 = parent->first_child; f1 != f; f1 = f1->next)
1399 prev = f1;
1400 }
1401
1402 copy = copy_formula(Crnt_transform->f);
1403 install_up_pointers(copy);
1404
1405 save_next = f->next;
1406 f = trans_proc(f, flag);
1407
1408 /* f == NULL means failure, so do not update */
1409
1410 if (f != NULL) {
1411 f->next = save_next;
1412 install_up_pointers(f);
1413
1414 if (parent) { /* if not at the top */
1415 if (prev)
1416 prev->next = f;
1417 else
1418 parent->first_child = f;
1419 f->parent = parent;
1420 }
1421 else {
1422 Crnt_transform->f = f;
1423 f->parent = NULL;
1424 }
1425
1426 /* free any undone/unedited formulas */
1427 if (Crnt_transform->right) {
1428 free_formulas(Crnt_transform->right);
1429 Crnt_transform->right = NULL;
1430 }
1431 else if (Crnt_transform->up) {
1432 free_formulas(Crnt_transform->up);
1433 Crnt_transform->up = NULL;
1434 }
1435
1436 p = get_formula_ptr_2();
1437 p->f = Crnt_transform->f;
1438
1439 Crnt_transform->up = p;
1440 p->down = Crnt_transform;
1441 Crnt_transform->f = copy;
1442 Crnt_transform = p;
1443
1444 display_formula(Crnt_transform);
1445
1446 /* now highlight (and select) the transformed subterm */
1447
1448 sub_box = find_sub_box(B, f);
1449 if (sub_box && sub_box != B) {
1450 Sel_area = sub_box;
1451 Highlighted = 1;
1452 draw_formula_box_inverted(Sel_area, Sel_area->abs_x_loc, Sel_area->abs_y_loc);
1453 }
1454 }
1455
1456 } /* edit_transform */
1457
1458 /*************
1459 *
1460 * struct formula *str_2_formula(buf)
1461 *
1462 *************/
1463
str_2_formula(buf)1464 struct formula *str_2_formula(buf)
1465 char *buf;
1466 {
1467 struct term *t;
1468 struct formula *f;
1469 int i = 0;
1470
1471 t = str_to_term(buf, &i, 0);
1472 if (t) {
1473 skip_white(buf, &i);
1474 if (buf[i] != '\0' && buf[i] != '.') {
1475 fprintf(stderr, "end of formula not at end of string (missing parentheses?)\n");
1476 zap_term(t);
1477 f = NULL;
1478 }
1479 else {
1480 t = term_fixup(t);
1481 f = term_to_formula(t);
1482 zap_term(t);
1483 }
1484 }
1485 else
1486 f = NULL;
1487 return(f);
1488
1489 } /* str_2_formula */
1490
1491 /*************************
1492 *
1493 * struct formula *replace_text(f, flag)
1494 *
1495 *****************************/
1496
replace_text(f,flag)1497 struct formula *replace_text(f, flag)
1498 struct formula *f;
1499 int flag;
1500 {
1501 f = str_2_formula(Str); /* convert the string to a formula */
1502 if (f == NULL)
1503 user_error("Error in converting string to formula.\nSee standard output for more details.");
1504 return(f);
1505
1506 } /* replace_text */
1507
1508 /*************************
1509 *
1510 * struct formula *make_deleted(f, flag)
1511 *
1512 *****************************/
1513
make_deleted(f,flag)1514 struct formula *make_deleted(f, flag)
1515 struct formula *f;
1516 int flag;
1517 {
1518 struct formula *f1, *prev;
1519 int i;
1520
1521 /* flag is index of subformula to be deleted */
1522 f1 = f->first_child;
1523 i = 1;
1524 prev = NULL;
1525 while (i != flag) {
1526 prev = f1;
1527 f1 = f1->next;
1528 i++;
1529 }
1530 if (prev)
1531 prev->next = f1->next;
1532 else
1533 f->first_child = f1->next;
1534
1535 zap_formula(f1);
1536
1537 if (f->first_child && f->first_child->next == NULL) {
1538 /* if just one remaining */
1539 f1 = f;
1540 f = f->first_child;
1541 f->next = f1->next;
1542 free_formula(f1);
1543 }
1544 return(f);
1545
1546 } /* make_deleted */
1547
1548 /*************************
1549 *
1550 * struct formula *join_formulas(f, flag)
1551 *
1552 *****************************/
1553
join_formulas(f,flag)1554 struct formula *join_formulas(f, flag)
1555 struct formula *f;
1556 int flag;
1557 {
1558 f = str_2_formula(Edit_str); /* convert new string to formula */
1559
1560 if (f == NULL)
1561 user_error("Error in converting string to formula.\nSee standard output for more details.");
1562 return(f);
1563
1564 } /* join_formulas */
1565
1566 /*************************
1567 *
1568 * struct formula_ptr_2 *find_end(q)
1569 *
1570 *****************************/
1571
find_end(q)1572 struct formula_ptr_2 *find_end(q)
1573 struct formula_ptr_2 *q;
1574 {
1575 while( q->right || q->up) {
1576 if (q->right)
1577 q = find_end(q->right);
1578 else
1579 q = find_end(q->up);
1580 }
1581 return(q);
1582
1583 } /* find_end */
1584
1585 /*************************
1586 *
1587 * void clear_text_callback(w, client_data, call_data)
1588 *
1589 *****************************/
1590
clear_text_callback(w,client_data,call_data)1591 void clear_text_callback(w,client_data, call_data)
1592 Widget w;
1593 XtPointer client_data;
1594 XtPointer call_data;
1595 {
1596 Arg arg[1];
1597
1598 Widget text = (Widget) client_data;
1599
1600
1601 XtSetArg(arg[0], XtNstring, "");
1602 XtSetValues(text, arg, 1);
1603
1604 } /* end clear_text_callback */
1605
1606
1607 /*************************
1608 *
1609 * void conjoin_callback(w, client_data, call_data)
1610 *
1611 *****************************/
1612
conjoin_callback(w,client_data,call_data)1613 void conjoin_callback(w,client_data, call_data)
1614 Widget w;
1615 XtPointer client_data;
1616 XtPointer call_data;
1617 {
1618
1619
1620 if (Crnt_formula) {
1621 if (Sel_area->type == FORMULA) {
1622
1623 strcpy(Edit_str, "\0");
1624
1625 /* create a popup text widget with a conjoin button */
1626 create_edit_popup(conjoin_button);
1627
1628 }
1629 else
1630 user_error("Conjoin requires a formula (or subformula)\nas a selection.\n");
1631
1632 }
1633 else
1634 user_error("No formulas are currently loaded.\n");
1635
1636 } /* end conjoin_callback */
1637
1638
1639 /*************************
1640 *
1641 * void conjoin_with_callback(w, client_data, call_data)
1642 *
1643 *****************************/
1644
conjoin_with_callback(w,client_data,call_data)1645 void conjoin_with_callback(w, client_data, call_data)
1646 Widget w;
1647 XtPointer client_data;
1648 XtPointer call_data;
1649 {
1650 char temp_str[TEXT_LENGTH];
1651 int i;
1652 Arg arg[1];
1653
1654
1655 /* build a string consisting of "( Sel_area & New_text )" */
1656 strcpy(Edit_str, "(");
1657
1658 i = sprint_formula(temp_str, Sel_area->f);
1659 strcat(Edit_str, temp_str);
1660 strcat(Edit_str, " & ");
1661
1662 XtSetArg(arg[0], XtNstring, &Str);
1663 XtGetValues(Edit_text, arg, 1);
1664 strcat(Edit_str, Str);
1665 strcat(Edit_str, ")");
1666
1667 edit_transform(Sel_area->f, join_formulas, 0);
1668
1669 /* if no message, conjoin was successful, destroy popup */
1670 /* o.w. leave it for possible correction */
1671
1672 if (!Have_message)
1673 XtDestroyWidget(Edit_popup);
1674
1675 } /* end conjoin_with_callback */
1676
1677
1678 /*************************
1679 *
1680 * void disjoin_callback(w, client_data, call_data)
1681 *
1682 *****************************/
1683
disjoin_callback(w,client_data,call_data)1684 void disjoin_callback(w,client_data, call_data)
1685 Widget w;
1686 XtPointer client_data;
1687 XtPointer call_data;
1688 {
1689
1690
1691 if (Crnt_formula) {
1692 if (Sel_area->type == FORMULA) {
1693
1694 strcpy(Edit_str, "\0");
1695
1696 /* create a popup text widget with a disjoin button */
1697 create_edit_popup(disjoin_button);
1698
1699 }
1700 else
1701 user_error("Disjoin requires a formula (or subformula)\nas a selection.\n");
1702
1703 }
1704 else
1705 user_error("No formulas are currently loaded.\n");
1706
1707 } /* end disjoin_callback */
1708
1709 /*************************
1710 *
1711 * void disjoin_with_callback(w, client_data, call_data)
1712 *
1713 *****************************/
1714
disjoin_with_callback(w,client_data,call_data)1715 void disjoin_with_callback(w, client_data, call_data)
1716 Widget w;
1717 XtPointer client_data;
1718 XtPointer call_data;
1719 {
1720 char temp_str[TEXT_LENGTH];
1721 int i;
1722 Arg arg[1];
1723
1724
1725 /* build a string consisting of "( Sel_area | New_text )" */
1726 strcpy(Edit_str, "(");
1727
1728 i = sprint_formula(temp_str, Sel_area->f);
1729 strcat(Edit_str, temp_str);
1730 strcat(Edit_str, " | ");
1731
1732 XtSetArg(arg[0], XtNstring, &Str);
1733 XtGetValues(Edit_text, arg, 1);
1734 strcat(Edit_str, Str);
1735 strcat(Edit_str, ")");
1736
1737 edit_transform(Sel_area->f, join_formulas, 0);
1738
1739 /* if no message, disjoin was successful, destroy popup */
1740 /* o.w. leave it for possible correction */
1741
1742 if (!Have_message)
1743 XtDestroyWidget(Edit_popup);
1744
1745 } /* end disjoin_with_callback */
1746
1747 /*************************
1748 *
1749 * void quantify_callback(w, client_data, call_data)
1750 *
1751 *****************************/
1752
quantify_callback(w,client_data,call_data)1753 void quantify_callback(w,client_data, call_data)
1754 Widget w;
1755 XtPointer client_data;
1756 XtPointer call_data;
1757 {
1758
1759
1760 if (Crnt_formula) {
1761 if (Sel_area->type == FORMULA) {
1762
1763 strcpy(Edit_str, "\0");
1764
1765 /* create a popup text widget with an add_quantifiers button */
1766 create_edit_popup(add_quantifiers_button);
1767
1768 }
1769 else
1770 user_error("Quantify requires a formula (or subformula)\nas a selection.\n");
1771
1772 }
1773 else
1774 user_error("No formulas are currently loaded.\n");
1775
1776 } /* end quantify_callback */
1777
1778
1779 /*************************
1780 *
1781 * void add_quantify_callback(w, client_data, call_data)
1782 *
1783 *****************************/
1784
add_quantify_callback(w,client_data,call_data)1785 void add_quantify_callback(w, client_data, call_data)
1786 Widget w;
1787 XtPointer client_data;
1788 XtPointer call_data;
1789 {
1790 char temp_str[TEXT_LENGTH];
1791 int i;
1792 Arg arg[1];
1793
1794
1795 /* build a string consisting of "(New_quantifiers Sel_area)" */
1796 strcpy(Edit_str, "(");
1797
1798 XtSetArg(arg[0], XtNstring, &Str);
1799 XtGetValues(Edit_text, arg, 1);
1800 strcat(Edit_str, Str);
1801 strcat(Edit_str, " ");
1802
1803 i = sprint_formula(temp_str, Sel_area->f);
1804 strcat(Edit_str, temp_str);
1805 strcat(Edit_str, ")");
1806
1807 edit_transform(Sel_area->f, join_formulas, 0);
1808
1809 /* if no message, quantification was successful, destroy popup */
1810 /* o.w. leave it for possible correction */
1811
1812 if (!Have_message)
1813 XtDestroyWidget(Edit_popup);
1814
1815 } /* end add_quantify_callback */
1816
1817
1818 /*************************
1819 *
1820 * void negate_callback(w, client_data, call_data)
1821 *
1822 *****************************/
1823
negate_callback(w,client_data,call_data)1824 void negate_callback(w,client_data, call_data)
1825 Widget w;
1826 XtPointer client_data;
1827 XtPointer call_data;
1828 {
1829
1830 struct formula *f;
1831
1832
1833 if (Crnt_formula) {
1834 if (Sel_area->type == FORMULA) {
1835
1836 f = Sel_area->f;
1837
1838 /* negate the formula (or subformula) and place in list */
1839 edit_transform(f, negate_formula, 0);
1840
1841 }
1842 else
1843 user_error("Negate requires a formula (or subformula)\nas a selection.\n");
1844
1845 }
1846 else
1847 user_error("No formulas are currently loaded.\n");
1848
1849 } /* end negate_callback */
1850
1851 /*************************
1852 *
1853 * void new_formula_callback(w, client_data, call_data)
1854 *
1855 *****************************/
1856
new_formula_callback(w,client_data,call_data)1857 void new_formula_callback(w, client_data, call_data)
1858 Widget w;
1859 XtPointer client_data;
1860 XtPointer call_data;
1861 {
1862
1863
1864 strcpy(Edit_str, "\0");
1865
1866 /* create a popup text widget with an insert button */
1867 create_edit_popup(insert_button);
1868
1869 } /* end new_formula_callback */
1870
1871
1872 /*************************
1873 *
1874 * void insert_formula_callback(w, client_data, call_data)
1875 *
1876 *****************************/
1877
insert_formula_callback(w,client_data,call_data)1878 void insert_formula_callback(w,client_data, call_data)
1879 Widget w;
1880 XtPointer client_data;
1881 XtPointer call_data;
1882 {
1883 struct formula *f;
1884 struct formula_ptr_2 *q;
1885 int i;
1886
1887 Arg arg[1];
1888
1889
1890 XtSetArg(arg[0], XtNstring, &Str);
1891 XtGetValues(Edit_text, arg, 1);
1892
1893 f = str_2_formula(Str); /* convert string to formula form */
1894
1895 if (f) {
1896 /* setup in a formula list node */
1897 install_up_pointers(f);
1898 f->parent = NULL;
1899 q = get_formula_ptr_2();
1900 q->f = f;
1901
1902 /* insert into formula list after current formula */
1903 if (Crnt_formula) {
1904 q->next = Crnt_formula->next;
1905 Crnt_formula->next = q;
1906 }
1907 else
1908 Top_formula = q;
1909
1910 if (q->next)
1911 q->next->prev = q;
1912 q->prev = Crnt_formula;
1913
1914 Crnt_formula = q;
1915 Crnt_transform = q;
1916
1917 XtDestroyWidget(Edit_popup);
1918
1919 display_formula(Crnt_transform);
1920 }
1921 else
1922 user_error("Error in converting string to formula.\nSee standard output for more details.");
1923
1924 } /* end insert_formula_callback */
1925
1926 /*************************
1927 *
1928 * void delete_formula_callback(w, client_data, call_data)
1929 *
1930 *****************************/
1931
delete_formula_callback(w,client_data,call_data)1932 void delete_formula_callback(w,client_data, call_data)
1933 Widget w;
1934 XtPointer client_data;
1935 XtPointer call_data;
1936 {
1937 struct formula_ptr_2 *p;
1938 struct formula *f, *f1;
1939 int i;
1940
1941
1942 if (Crnt_formula) {
1943
1944 if (Sel_area == B) {
1945
1946 if (Crnt_formula == Crnt_transform) {
1947
1948 p = Crnt_formula; /* hold for freeing nodes */
1949
1950 /* remove formula from list */
1951
1952 if (Crnt_formula->prev)
1953 Crnt_formula->prev->next = Crnt_formula->next;
1954 else
1955 Top_formula = Crnt_formula->next;
1956
1957 if (Crnt_formula->next) {
1958 Crnt_formula->next->prev = Crnt_formula->prev;
1959 Crnt_formula = Crnt_formula->next;
1960 }
1961 else
1962 Crnt_formula = Crnt_formula->prev;
1963
1964 Crnt_transform = Crnt_formula;
1965
1966 if (Top_formula == NULL) {
1967 XClearWindow(Dpy,Win);
1968 user_error("Empty formula list.\n");
1969 }
1970 else display_formula(Crnt_transform);
1971
1972 free_formulas(p); /* kill all the transformations of the */
1973 /* deleted formula */
1974
1975 }
1976 else
1977 user_error("Delete formula removes from the original formula list,\nnot from the edit/logic transformed formulas.");
1978 }
1979 else if (Sel_area->type == OPERATOR)
1980 user_error("Delete formula cannot delete an operator.");
1981 else if (Sel_area->parent->subtype != AND_FORM &&
1982 Sel_area->parent->subtype != OR_FORM)
1983 user_error("Deletion of a subformula must be from a\nconjunction or a disjunction.");
1984 else {
1985 f = Sel_area->parent->f; /* t is AND or OR */
1986 /* find index of subformula to be deleted, and send that in */
1987 i = 1;
1988 for (f1 = f->first_child; f1 != Sel_area->f; f1 = f1->next)
1989 i++;
1990 edit_transform(f, make_deleted, i);
1991 }
1992 }
1993 else
1994 user_error("No formulas are currently loaded.");
1995
1996 } /* end delete_formula_callback */
1997
1998 /*************************
1999 *
2000 * void unedit_callback(w, client_data, call_data)
2001 *
2002 *****************************/
2003
unedit_callback(w,client_data,call_data)2004 void unedit_callback(w,client_data, call_data)
2005 Widget w;
2006 XtPointer client_data;
2007 XtPointer call_data;
2008 {
2009
2010
2011 if (Crnt_formula) {
2012 if (Crnt_transform->down == NULL)
2013 user_error("Nothing more to be un-edited.\n");
2014 else {
2015 Crnt_transform = Crnt_transform->down;
2016 display_formula(Crnt_transform);
2017 }
2018 }
2019 else
2020 user_error("No formulas are currently loaded.\n");
2021
2022 } /* end unedit_callback */
2023
2024 /*************************
2025 *
2026 * void reedit_callback(w, client_data, call_data)
2027 *
2028 *****************************/
2029
reedit_callback(w,client_data,call_data)2030 void reedit_callback(w,client_data, call_data)
2031 Widget w;
2032 XtPointer client_data;
2033 XtPointer call_data;
2034 {
2035
2036
2037 if (Crnt_formula) {
2038 if (Crnt_transform->up == NULL)
2039 user_error("Nothing more to be re-edited.\n");
2040 else {
2041 Crnt_transform = Crnt_transform->up;
2042 display_formula(Crnt_transform);
2043 }
2044 }
2045 else
2046 user_error("No formulas are currently loaded.\n");
2047
2048 } /* end reedit_callback */
2049
2050 /*************************
2051 *
2052 * void font_menu_callback(w, client_data, call_data)
2053 *
2054 *****************************/
2055
font_menu_callback(w,client_data,call_data)2056 void font_menu_callback(w, client_data, call_data)
2057 Widget w;
2058 XtPointer client_data;
2059 XtPointer call_data;
2060 {
2061
2062 Widget font_form, smallfont, medfont, largefont, cancel;
2063 int n;
2064 Arg arg[10];
2065
2066
2067 create_menu_popup("fonts", w); /* create the popup shell */
2068
2069 n = 0;
2070 XtSetArg(arg[n], XtNbackground, Background); n++;
2071 font_form = XtCreateManagedWidget("font_form", formWidgetClass, Popup,
2072 arg, n);
2073
2074 /* command buttons */
2075
2076 /* small font */
2077 n = 0;
2078 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, SMALLFONT));n++;
2079 XtSetArg(arg[n], XtNlabel, "Small");n++;
2080 smallfont = XtCreateManagedWidget("smallfont",commandWidgetClass,
2081 font_form,arg,n);
2082 XtAddCallback(smallfont, XtNcallback, font_callback, SMALLFONT);
2083
2084 /* medium font */
2085 n = 0;
2086 XtSetArg(arg[n], XtNfromVert, smallfont); n++;
2087 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, MEDFONT));n++;
2088 XtSetArg(arg[n], XtNlabel, "Medium");n++;
2089 medfont = XtCreateManagedWidget("medfont", commandWidgetClass,
2090 font_form, arg, n);
2091 XtAddCallback(medfont, XtNcallback, font_callback, MEDFONT);
2092
2093 /* large font */
2094 n = 0;
2095 XtSetArg(arg[n], XtNfromVert, medfont); n++;
2096 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LARGEFONT));n++;
2097 XtSetArg(arg[n], XtNlabel, "Large");n++;
2098 largefont = XtCreateManagedWidget("largefont", commandWidgetClass,
2099 font_form, arg, n);
2100 XtAddCallback(largefont, XtNcallback, font_callback, LARGEFONT);
2101
2102 /* cancel */
2103 n = 0;
2104 XtSetArg(arg[n], XtNfromVert,largefont); n++;
2105 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2106 XtSetArg(arg[n], XtNlabel, "Cancel"); n++;
2107 cancel = XtCreateManagedWidget("cancel",commandWidgetClass,
2108 font_form, arg, n);
2109 XtAddCallback(cancel, XtNcallback, destroy_popup, Popup);
2110
2111 XtPopup(Popup, XtGrabNone);
2112
2113
2114 } /* font_menu_callback */
2115
2116 /*************************
2117 *
2118 * void create_menu_popup(name, parent)
2119 *
2120 *****************************/
2121
create_menu_popup(name,parent)2122 void create_menu_popup(name, parent)
2123 char name[];
2124 Widget parent;
2125 {
2126
2127 Dimension width, height;
2128 Position x, y;
2129 int n;
2130 Arg arg[5];
2131
2132 n = 0;
2133 XtSetArg(arg[n], XtNwidth, &width); n++;
2134 XtSetArg(arg[n], XtNheight, &height); n++;
2135 XtGetValues(parent, arg, n);
2136 XtTranslateCoords(parent, (Position) (width/2), (Position) (height/2),
2137 &x, &y);
2138
2139 n = 0;
2140 XtSetArg(arg[n], XtNx, x); n++;
2141 XtSetArg(arg[n], XtNy, y); n++;
2142 XtSetArg(arg[n], XtNborderWidth, 1);n++;
2143 Popup = XtCreatePopupShell(name,transientShellWidgetClass, Outline,
2144 arg,n);
2145
2146 } /* create_menu_popup */
2147
2148
2149 /*************************
2150 *
2151 * void create_edit_popup(create_text_op_button)
2152 *
2153 *****************************/
2154
2155 void create_edit_popup(create_text_op_button)
2156 Widget (*create_text_op_button)();
2157 {
2158
2159 Dimension width, height;
2160 Position x,y;
2161 int n;
2162 Arg arg[15];
2163 Widget edit_form, text_op_button, clear_text, cancel_edit;
2164
2165 /* create the shell */
2166 n = 0;
2167 XtSetArg(arg[n], XtNwidth, &width); n++;
2168 XtSetArg(arg[n], XtNheight, &height); n++;
2169 XtGetValues(Outline, arg, n);
2170 XtTranslateCoords(Outline, (Position)((width/2)-200),
2171 (Position)(height/2), &x, &y);
2172
2173 n = 0;
2174 XtSetArg(arg[n], XtNx, x); n++;
2175 XtSetArg(arg[n], XtNy, y); n++;
2176 Edit_popup = XtCreatePopupShell("Edit_popup", transientShellWidgetClass,
2177 Outline, arg, n);
2178
2179 /* form widget to hold the buttons & text */
2180 n = 0;
2181 XtSetArg(arg[n], XtNbackground, Foreground); n++;
2182 XtSetArg(arg[n], XtNforeground, Foreground); n++;
2183 edit_form = XtCreateManagedWidget("edit_form",formWidgetClass,
2184 Edit_popup, arg, n);
2185
2186 /* text_op_button */
2187 text_op_button = create_text_op_button(edit_form);
2188
2189 /* clear text button */
2190 n = 0;
2191 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2192 XtSetArg(arg[n], XtNfromVert, text_op_button); n++;
2193 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2194 XtSetArg(arg[n], XtNlabel, "Clear"); n++;
2195 clear_text = XtCreateManagedWidget("clear_text", commandWidgetClass,
2196 edit_form, arg, n);
2197
2198 /* cancel button */
2199 n = 0;
2200 XtSetArg(arg[n], XtNfromVert, clear_text); n++;
2201 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2202 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2203 XtSetArg(arg[n], XtNlabel, "Cancel"); n++;
2204 cancel_edit = XtCreateManagedWidget("cancel", commandWidgetClass,
2205 edit_form, arg, n);
2206 XtAddCallback(cancel_edit, XtNcallback, destroy_popup, Edit_popup);
2207
2208 /* text widget */
2209 n = 0;
2210 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2211 XtSetArg(arg[n], XtNfromHoriz, text_op_button); n++;
2212 XtSetArg(arg[n], XtNforeground, Foreground); n++;
2213 XtSetArg(arg[n], XtNeditType, XawtextEdit); n++;
2214 XtSetArg(arg[n], XtNscrollVertical, XawtextScrollWhenNeeded); n++;
2215 XtSetArg(arg[n], XtNautoFill, True); n++;
2216 XtSetArg(arg[n], XtNheight, 150); n++;
2217 XtSetArg(arg[n], XtNwidth, 300); n++;
2218 XtSetArg(arg[n], XtNwrap, XawtextWrapWord); n++;
2219 XtSetArg(arg[n], XtNstring, Edit_str); n++;
2220 Edit_text = XtCreateManagedWidget("edit_text", asciiTextWidgetClass,
2221 edit_form, arg, n);
2222
2223 XtAddCallback(clear_text, XtNcallback, clear_text_callback,
2224 (XtPointer) Edit_text);
2225
2226 XtPopup(Edit_popup, XtGrabNone);
2227
2228 } /* create_edit_popup */
2229
2230
2231 /*************************
2232 *
2233 * Widget replace_button(parent)
2234 *
2235 *****************************/
2236
replace_button(parent)2237 Widget replace_button(parent)
2238 Widget parent;
2239 {
2240
2241 Widget button;
2242 int n;
2243 Arg arg[5];
2244
2245 n = 0;
2246 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2247 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2248 XtSetArg(arg[n], XtNlabel, "Replace"); n++;
2249 button = XtCreateManagedWidget("replace", commandWidgetClass, parent,
2250 arg, n);
2251
2252 XtAddCallback(button, XtNcallback, replace_callback,
2253 (XtPointer)(Sel_area->f));
2254
2255 return(button);
2256
2257 } /* replace_button */
2258
2259 /*************************
2260 *
2261 * Widget conjoin_button(parent)
2262 *
2263 *****************************/
2264
conjoin_button(parent)2265 Widget conjoin_button(parent)
2266 Widget parent;
2267 {
2268
2269 Widget button;
2270 int n;
2271 Arg arg[5];
2272
2273 n = 0;
2274 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2275 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2276 XtSetArg(arg[n], XtNlabel, "Conjoin with"); n++;
2277 button = XtCreateManagedWidget("conjoin_with", commandWidgetClass, parent,
2278 arg, n);
2279
2280 XtAddCallback(button, XtNcallback, conjoin_with_callback, NULL);
2281
2282 return(button);
2283
2284 } /* conjoin_button */
2285
2286
2287 /*************************
2288 *
2289 * Widget disjoin_button(parent)
2290 *
2291 *****************************/
2292
disjoin_button(parent)2293 Widget disjoin_button(parent)
2294 Widget parent;
2295 {
2296
2297 Widget button;
2298 int n;
2299 Arg arg[5];
2300
2301 n = 0;
2302 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2303 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2304 XtSetArg(arg[n], XtNlabel, "Disjoin with"); n++;
2305 button = XtCreateManagedWidget("disjoin_with", commandWidgetClass, parent,
2306 arg, n);
2307
2308 XtAddCallback(button, XtNcallback, disjoin_with_callback, NULL);
2309
2310 return(button);
2311
2312 } /* disjoin_button */
2313
2314
2315 /*************************
2316 *
2317 * Widget add_quantifiers_button(parent)
2318 *
2319 *****************************/
2320
add_quantifiers_button(parent)2321 Widget add_quantifiers_button(parent)
2322 Widget parent;
2323 {
2324
2325 Widget button;
2326 int n;
2327 Arg arg[5];
2328
2329 n = 0;
2330 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2331 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2332 XtSetArg(arg[n], XtNlabel, " Add\nQuantifiers"); n++;
2333 button = XtCreateManagedWidget("add_quantifiers", commandWidgetClass, parent,
2334 arg, n);
2335
2336 XtAddCallback(button, XtNcallback, add_quantify_callback, NULL);
2337
2338 return(button);
2339
2340 } /* add_quantifiers_button */
2341
2342
2343 /*************************
2344 *
2345 * Widget insert_button(parent)
2346 *
2347 *****************************/
2348
insert_button(parent)2349 Widget insert_button(parent)
2350 Widget parent;
2351 {
2352
2353 Widget button;
2354 int n;
2355 Arg arg[5];
2356
2357 n = 0;
2358 XtSetArg(arg[n], XtNhighlightThickness, 0); n++;
2359 XtSetArg(arg[n], XtNfont, XLoadQueryFont(Dpy, LABELFONT)); n++;
2360 XtSetArg(arg[n], XtNlabel, "Insert"); n++;
2361 button = XtCreateManagedWidget("insert", commandWidgetClass, parent,
2362 arg, n);
2363
2364 XtAddCallback(button, XtNcallback, insert_formula_callback, NULL);
2365
2366 return(button);
2367
2368 } /* insert_button */
2369
2370