/* ** xmagic - version 1.1. ** xmagic.c ** */ #include #include #include #include #include "defs.h" #include #include #include #include #include #include #include #include #include #include #include #include #include #include #define NO_OF_AXIOMS 23 #define NO_OF_FRAGMENTS 9 #define OUTPUT_SIZE 65536 #define ILLEGAL 3 Widget global_file_dialog, the_global_shell, the_global_pop_up, global_axiom_dialog, global_mat_no_dialog, global_max_mat_dialog, global_time_dialog, the_global_help_pop_up, global_help_button, global_super_axiom_button, verbose_list, global_magic_output, logic_list, order_list, tty_list, file_list, global_pro_label, global_scrollbar; Boolean parallel_magic = False; char *super_string; int no_of_procs = 0; int max_procs = 8; void getit(), getfile(), getsymbol(), getdefine(), inform(), ring(), update_scrollbar(); XtActionsRec action_table[] = { {"getit", getit}, {"getfile", getfile}, {"getsymbol", getsymbol}, {"getdefine", getdefine}, {"inform", inform}, }; XtCallbackProc whereami(); static String fallback_resources [] = { "XMagic*switch_dialog.value.translations: #override \\n Return: getit()", "XMagic*file_dialog.value.translations: #override \\n Return: getfile()", "XMagic*symbol_dialog.value.translations: #override \\n Return: getsymbol()", "XMagic*define_dialog.value.translations: #override \\n Return: getdefine()", "XMagic*axiom_dialog.value.translations: #override \\n Return: no-op(RingBell)", NULL, }; String global_file_string, extra_string; main(argc, argv) unsigned int argc; char *argv []; { XtAppContext app_con; void quit_action (), go_action (), logic_action (), order_action (), tty_action (), file_action (), make_list (), make_button (), make_dialog (), accept_action (), add_action (), make_add_axioms (), help_action (), make_help (), make_bad_guy_dialog (); extern void main_axiom_button_action (), reset_action (), stop_action (), con_action (), make_connectives (), verbose_action (); Widget shell_widget, the_box, quit_button, go_button, logic_label, order_label, tty_label, file_label, file_dialog, the_pop_up, reset_button, stop_button, bad_guy_dialog, time_list, axiom_button, fragment_label, fragment_form, con_button, help_button, help_pop_up, main_pane, magic_output, verbose_label, pro_label, num_label, scrollbar, verbose_toggle; /* ** external globals defined in jump.c */ extern Widget global_bad_guy_list, global_number_list, global_size_list, global_time_list, global_connectives_shell, verbose_list, fragment_widget [NO_OF_FRAGMENTS]; extern Display *display_ptr; int i; static String file_name = "xmagic.save", mat_no = "100 ", max_mat = "10 ", time = "30 min ", logic_items [] = {"FD", "B", "DW", "TW", "EW", "C", "T", "E", "R", "CK", "S4", NULL,}, order_items [] = {"distributive lattice", "lattice", "total order", NULL,}, tty_items [] = {"none", "pretty", "ugly", "summary", NULL,}, verbose_items []= {"silent", "verbose", NULL,}, file_items [] = {"none", "pretty", "ugly", "summary", NULL,}; static XtCallbackRec quit_calls [] = {{quit_action, NULL}, {NULL, NULL},}, go_calls [] = {{go_action, NULL}, {NULL, NULL},}, help_calls [] = {{help_action, NULL}, {NULL, NULL},}, verbose_calls []= {{verbose_action, NULL}, {NULL, NULL},}, logic_calls [] = {{logic_action, NULL}, {NULL, NULL},}, order_calls [] = {{order_action, NULL}, {NULL, NULL},}, tty_calls [] = {{tty_action, NULL}, {NULL, NULL},}, file_calls [] = {{file_action, NULL}, {NULL, NULL},}, accept_calls [] = {{accept_action, NULL}, {NULL, NULL},}, axiom_calls [] = {{main_axiom_button_action, NULL}, {NULL, NULL},}, con_calls [] = {{con_action, NULL}, {NULL, NULL},}, reset_calls [] = {{reset_action, NULL}, {NULL, NULL},}, stop_calls [] = {{stop_action, NULL}, {NULL, NULL},}; Arg text_args [30], args [30]; String scroll_trans_string = "#override \n\ : NotifyScroll(Proportional) \ inform() EndScroll()\n\ : StartScroll(Continuous)\ MoveThumb() NotifyThumb() \n\ : MoveThumb() NotifyThumb()"; XtTranslations scroll_translations; /* ** Fish out the -# option from the command line - this option defines ** number of processes */ for (i = 1; i < argc; i++) if (strncmp (argv [i], "-#", 2) == 0) { i++; if (i < argc) { if (! isdigit (*argv [i])) fatal ("usage: xmagic [-# number] [options]"); sscanf (argv [i], "%d", &no_of_procs); if (no_of_procs < 2) fatal ("must be more than 1 process"); } else fatal ("usage: xmagic [-# number] [options]"); } /* ** Allocate plenty of space for the super_string (the display) ** */ super_string = (char *) malloc (OUTPUT_SIZE * sizeof (char)); *super_string = '\0'; global_file_string = (char *) malloc (BUFSIZ * sizeof (char)); extra_string = (char *) malloc (BUFSIZ * sizeof (char)); /* ** Establish the connection with magic; invoke_magic will make use ** of no_of_procs defined in the command line. */ invoke_magic (); /* ** Initiate X Windows */ /* shell_widget = XtInitialize ("xmagic", "XMagic", NULL, NULL, ** &argc, argv ); */ shell_widget = XtAppInitialize(&app_con, "XMagic", NULL, ZERO, &argc, argv, fallback_resources, NULL, ZERO); XtAppAddActions(app_con, action_table, XtNumber(action_table)); main_pane = XtCreateManagedWidget ("main_pane", panedWidgetClass, shell_widget, NULL, 0); /* ** Create the forms */ the_box = XtCreateManagedWidget ("the_box", formWidgetClass, main_pane, NULL, 0); /* ** Create the lists */ make_list (the_box, &logic_label, "logic_label", "logic:", &logic_list, "logic_list", logic_items, logic_calls, 2, NULL, 4, NULL, 4); make_list (the_box, &order_label, "order_label", "order:", &order_list, "order_list", order_items, order_calls, 1, logic_list, 10, NULL, 4); /* make_list (the_box, &verbose_label, "verbose_label", "", ** &verbose_list, "verbose_list", verbose_items, verbose_calls, 1, ** order_list, 6, NULL, 4); */ i = 0; XtSetArg (args [i], XtNfromVert, (XtArgVal) order_list); i++; XtSetArg (args [i], XtNvertDistance, (XtArgVal) -19); i++; XtSetArg (args [i], XtNfromHoriz, (XtArgVal) order_list); i++; XtSetArg (args [i], XtNhorizDistance, (XtArgVal) 12); i++; XtSetArg (args [i], XtNcallback, (XtArgVal) verbose_calls); i++; verbose_toggle = XtCreateManagedWidget ("verbose", toggleWidgetClass, the_box, args, i); make_fragment (the_box, &fragment_label, &fragment_form, logic_list, 10, order_list, 4); make_list (the_box, &tty_label, "tty_label", "tty output:", &tty_list, "tty_list", tty_items, tty_calls, 1, NULL, 4, logic_list, 10); make_list (the_box, &file_label, "file_label", "file output:", &file_list, "file_list", file_items, file_calls, 1, tty_label, 10, logic_list, 10); /* ** Create the dialog box for the file name, pass the value of the ** pointer to the appropriate global variable for communication with ** the "accept" button callback. */ make_dialog (the_box, &file_dialog, "file_dialog", "file name:", file_name, False, 0, "change", accept_calls, NULL, NULL, NULL, NULL, file_list, 4, file_label, 1); global_file_dialog = file_dialog; /* ** Create the scrollbal and accompanying labels */ i = 0; XtSetArg (args [i], XtNfromVert, (XtArgVal) NULL); i++; XtSetArg (args [i], XtNvertDistance, (XtArgVal) 5); i++; XtSetArg (args [i], XtNfromHoriz, (XtArgVal) order_list); i++; XtSetArg (args [i], XtNhorizDistance, (XtArgVal) 6); i++; XtSetArg (args [i], XtNborderWidth, (XtArgVal) 0); i++; XtSetArg (args [i], XtNlabel, (XtArgVal) "processors:"); i++; pro_label = XtCreateManagedWidget ("processors", labelWidgetClass, the_box, args, i); i = 0; XtSetArg (args [i], XtNlength, (XtArgVal) 248); i++; XtSetArg (args [i], XtNfromVert, (XtArgVal) pro_label); i++; XtSetArg (args [i], XtNvertDistance, (XtArgVal) 3); i++; XtSetArg (args [i], XtNfromHoriz, (XtArgVal) verbose_toggle); i++; XtSetArg (args [i], XtNhorizDistance, (XtArgVal) 14); i++; XtSetArg (args [i], XtNthickness, (XtArgVal) 10); i++; XtSetArg (args [i], XtNminimumThumb, (XtArgVal) 30); i++; XtSetArg (args [i], XtNthumb, (XtArgVal) None); i++; scroll_translations = XtParseTranslationTable (scroll_trans_string); XtSetArg (args [i], XtNtranslations, (XtArgVal) scroll_translations); i++; scrollbar = XtCreateManagedWidget ("scrollbar", scrollbarWidgetClass, the_box, args, i); global_scrollbar = scrollbar; XtSetSensitive (scrollbar, False); i = 0; XtSetArg (args [i], XtNlabel, (XtArgVal) " "); i++; XtSetArg (args [i], XtNfromHoriz, (XtArgVal) order_list); i++; XtSetArg (args [i], XtNhorizDistance, (XtArgVal) 47); i++; XtSetArg (args [i], XtNfromVert, (XtArgVal) pro_label); i++; XtSetArg (args [i], XtNvertDistance, (XtArgVal) 3); i++; num_label = XtCreateManagedWidget ("num_label", labelWidgetClass, the_box, args, i); global_pro_label = num_label; XtAddCallback (scrollbar, XtNjumpProc, whereami, (XtPointer) num_label); make_jump (the_box, &bad_guy_dialog, &time_list, scrollbar, 6, NULL, 0); /* ** Create a pop-up shell for axioms. ** The shell class can be topLevelShellWidgetClass or ** overrideShellWidgetClass. */ the_pop_up = XtCreatePopupShell ("xmagic: add axioms", topLevelShellWidgetClass, shell_widget, NULL, 0); the_global_pop_up = the_pop_up; make_add_axioms (the_pop_up); /* ** Create a pop-up shell for help_button. ** */ help_pop_up = XtCreatePopupShell ("xmagic: help", topLevelShellWidgetClass, shell_widget, NULL, 0); the_global_help_pop_up = help_pop_up; make_help (help_pop_up); /* ** Create a pop-up shell for connectives. ** */ global_connectives_shell = XtCreatePopupShell ("xmagic: connectives", topLevelShellWidgetClass, shell_widget, NULL, 0); make_connectives (global_connectives_shell); /* ** Create the buttons; upper row */ make_button (the_box, &help_button, "help_button", "help", help_calls, NULL, 4, file_dialog, 12); global_help_button = help_button; make_button (the_box, &axiom_button, "add_axioms", "add axioms", axiom_calls, tty_label, 10, file_dialog, 12); global_super_axiom_button = axiom_button; make_button (the_box, &con_button, "add_cons", "connectives", con_calls, axiom_button, 25, file_dialog, 12); /* ** Create the buttons; lower row */ make_button (the_box, &go_button, "go_button", "run", go_calls, NULL, 4, help_button, 5); /* ** Don't make the stop button; it's not implemented yet ** ** ** make_button (the_box, ** &stop_button, "stop_button", "stop", stop_calls, ** tty_label, 10, help_button, 5); */ make_button (the_box, &reset_button, "reset_button", "reset all", reset_calls, tty_label, 10, help_button, 5); make_button (the_box, &quit_button, "quit_button", "quit", quit_calls, axiom_button, 25, help_button, 5); /* ** Now create the text widget in the bottom part of the main_pane ** */ i = 0; XtSetArg (text_args [i], XtNtype, (XtArgVal) XawAsciiString); i++; XtSetArg (text_args [i], XtNstring, (XtArgVal) super_string); i++; XtSetArg (text_args [i], XtNuseStringInPlace, (XtArgVal) True); i++; XtSetArg (text_args [i], XtNscrollVertical, (XtArgVal) XawtextScrollAlways); i++; XtSetArg (text_args [i], XtNwrap, (XtArgVal) XawtextWrapWord); i++; XtSetArg (text_args [i], XtNheight, (XtArgVal) 13*30+4); i++; XtSetArg (text_args [i], XtNeditType, (XtArgVal) XawtextEdit); i++; XtSetArg (text_args [i], XtNlength, (XtArgVal) OUTPUT_SIZE); i++; magic_output = XtCreateManagedWidget ("magic_output", asciiTextWidgetClass, main_pane, text_args, i); global_magic_output = magic_output; /* ** Put all the widgets visibly on the screen and start the ** main loop */ XtRealizeWidget (shell_widget); XtRealizeWidget (the_pop_up); XtRealizeWidget (help_pop_up); XtRealizeWidget (global_connectives_shell); XawTextEnableRedisplay (magic_output); display_ptr = XtDisplay (shell_widget); /* ** Highlight the defaults */ XtListHighlight (logic_list, 0); XtListHighlight (order_list, 0); /* XtListHighlight (verbose_list, 0); */ XtListHighlight (tty_list, 0); XtListHighlight (file_list, 0); XtListHighlight (global_bad_guy_list, 1); XtListHighlight (global_number_list, 1); XtListHighlight (global_size_list, 1); XtListHighlight (global_time_list, 1); for (i = 0; i < NO_OF_FRAGMENTS; i++) XtListHighlight (fragment_widget [i], 0); /* XtSetSensitive (reset_button, False); */ /* XtSetSensitive (stop_button, False); */ /* ** Send defaults to magic */ if (receive_all () == ILLEGAL) { ring (); send_to_magic ("\n"); } send_to_magic ("FD\n"); receive_all (); send_to_magic ("I\nnone\nnone\n"); receive_all (); if (parallel_magic){ XtSetSensitive (scrollbar, True); update_scrollbar(); } /* ** loop ad infinitum */ /* XtMainLoop (); */ XtAppMainLoop(app_con); }