/* Research Project: Graphical Database for Category Theory J. Bradbury, Dr. R. Rosebrugh, I. Rutherford Matt Graves, Jesse Tweedle Mount Allison University 2003 File: CategoryInternalFrame.java Description: Displays a category using VGJ Graph, GraphCanvas, AngleControlPanel, ViewportScroller, ScrolledPanel and LPanel. The constructor takes a Category as a parameter, so the New/Open/Load category displays are indistinguishable. */ // import statements import javax.swing.JInternalFrame; import javax.swing.*; import java.io.*; import java.awt.event.*; import java.awt.*; import javax.swing.event.*; import java.beans.*; public class CategoryInternalFrame extends JInternalFrame implements InternalFrameListener { private JInternalFrame[] toolFrames; // collection of internal tool frames // --------- VGJ/Category Objects for graph/canvas and category ---------------- private Graph graph_; // Graph object private GraphCanvas graphCanvas_; // GraphCanvas object private Category category_; // category to be displayed // ----------------------------------------------------------------------------- // --------- VGJ objects for displaying and controlling display ---------------- private AngleControlPanel angleControlPanel_; private ViewportScroller viewportScroller_; private ScrolledPanel scrolledPanel_; // ----------------------------------------------------------------------------- // ---------- GUI JPanel for displaying and controlling 3D display ------------- private JPanel VGJPanel; // ----------------------------------------------------------------------------- // ---------- GUI J/LPanels for displaying angle/viewport controls ---------------- private JPanel controlPanel; private LPanel viewportScrollPanel; private LPanel anglePanel; // ----------------------------------------------------------------------------- // --------- GUI JPanel for displaying category information -------------------- private JPanel informationPanel; // ----------------------------------------------------------------------------- // --------- GUI JSplitPane for dividing information and VGJ panels ------------- private JSplitPane outerSplitPane; // ----------------------------------------------------------------------------- // --------- GUI JLabels for displaying information titles ---------------------- private JLabel objectLabel; private JLabel arrowLabel; private JLabel relationLabel; private JLabel commentLabel; // ----------------------------------------------------------------------------- // ---------- GUI JTextAreas for displaying category information --------------- private JTextArea objectArea; private JTextArea arrowArea; private JTextArea relationArea; private JTextArea commentArea; // ----------------------------------------------------------------------------- // ---------- GUI JScrollPanes for displaying category text areas -------------- private JScrollPane objectPane; private JScrollPane arrowPane; private JScrollPane relationPane; private JScrollPane commentPane; // ----------------------------------------------------------------------------- public CategoryInternalFrame(Category newCategory_) { super(newCategory_.name, true, //resizable true, //closable true, //maximizable true);//iconifiable setFrameIcon(new ImageIcon("cat.gif")); // ------------- Set size, location and menu bar of JIFrame ----------------- setPreferredSize(new Dimension(640,480)); setLocation(new java.util.Random().nextInt(250) , new java.util.Random().nextInt(100) ); setJMenuBar(createJMenuBar()); toolFrames = new JInternalFrame[12]; setDefaultCloseOperation(DO_NOTHING_ON_CLOSE); this.addInternalFrameListener(this); // -------------------------------------------------------------------------- // ------------- Initialize graph_, graphCanvas_, and category_ objects ----- graph_ = new Graph(); category_ = newCategory_; graphCanvas_ = new GraphCanvas(graph_, this, category_); graphCanvas_.setMouseMode(GraphCanvas.SELECT_BOTH); Node.defaults.setBoundingBox(20, 20, 20); // -------------------------------------------------------------------------- if(category_.gml == "graph [\ndirected 1\n]\n") category_.setGML(); // ------------- Initialize VGJ controls ------------------------------------ viewportScroller_ = new ViewportScroller(90, 90, 500.0, 500.0, 400.0, 400.0, 0.0, 0.0); scrolledPanel_ = new ScrolledPanel(graphCanvas_); angleControlPanel_ = new AngleControlPanel(180, 76); // -------------------------------------------------------------------------- // ------------- Initialize viewportScrollPanel; contains viewportScroller -- viewportScrollPanel = new LPanel(); viewportScrollPanel.constraints.insets.bottom = 0; viewportScrollPanel.addLabel("Viewing Offset", 0, 0, 1.0, 1.0, 0, 0); viewportScrollPanel.constraints.insets.top = viewportScrollPanel.constraints.insets.bottom = 0; viewportScrollPanel.addComponent(viewportScroller_, 0, 0, 1.0, 1.0, 0, 0); viewportScrollPanel.constraints.insets.top = viewportScrollPanel.constraints.insets.bottom = 0; viewportScrollPanel.finish(); // -------------------------------------------------------------------------- // ------------- Initialize anglePanel; contains angleControlPanel ---------- anglePanel = new LPanel(); anglePanel.constraints.insets.top = 0; anglePanel.addComponent(angleControlPanel_, 0, 0, 1.0, 1.0, 1, 0); anglePanel.finish(); // -------------------------------------------------------------------------- // ------------- Initialize control panel; contains angle and viewport ------ controlPanel = new JPanel(); controlPanel.setLayout(new FlowLayout()); controlPanel.add(anglePanel); controlPanel.add(viewportScrollPanel); // -------------------------------------------------------------------------- //-------------- Initialize VGJ Panel --------------------------------------- VGJPanel = new JPanel(); VGJPanel.setLayout(new BorderLayout()); VGJPanel.add("South", controlPanel); VGJPanel.add("Center", scrolledPanel_); // -------------------------------------------------------------------------- // --------- Initialize "Objects" label, textarea and scrollpane ----------- objectLabel = new JLabel("Object(s):"); objectArea = new JTextArea(5, 5); objectArea.setLineWrap(true); objectArea.setWrapStyleWord(true); objectArea.setEditable(false); objectPane = new JScrollPane(objectArea); objectPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS); objectPane.setBorder(BorderFactory.createEtchedBorder()); // -------------------------------------------------------------------------- // ---------- Initialize "Arrows" label, textarea and scrollpane ------------ arrowLabel = new JLabel("Arrow(s):"); arrowArea = new JTextArea(5, 5); arrowArea.setLineWrap(true); arrowArea.setEditable(false); arrowArea.setWrapStyleWord(true); arrowPane = new JScrollPane(arrowArea); arrowPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS); arrowPane.setBorder(BorderFactory.createEtchedBorder()); // -------------------------------------------------------------------------- // ---------- Initialize "Relations" label, textarea and scrollpane --------- relationLabel = new JLabel("Relation(s):"); relationArea = new JTextArea(5, 5); relationPane = new JScrollPane(relationArea); relationPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS); relationArea.setLineWrap(true); relationArea.setEditable(false); relationArea.setWrapStyleWord(true); relationPane.setBorder(BorderFactory.createEtchedBorder()); // -------------------------------------------------------------------------- // ---------- Initialize "Comments" label, textarea and scrollpane ---------- commentLabel = new JLabel("Comment(s):"); commentArea = new JTextArea(5, 5); commentPane = new JScrollPane(commentArea); commentPane.setVerticalScrollBarPolicy(JScrollPane.VERTICAL_SCROLLBAR_ALWAYS); commentArea.setLineWrap(true); commentArea.setWrapStyleWord(true); commentPane.setBorder(BorderFactory.createEtchedBorder()); // -------------------------------------------------------------------------- // ---------- Initialize "Category Information" panel ----------------------- informationPanel = new JPanel(); informationPanel.setLayout(new GridBagLayout()); // -------------------------------------------------------------------------- // ---------- Initialize splitpane between Information and VGJ panels ------- outerSplitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, false, informationPanel, VGJPanel); outerSplitPane.setDividerLocation(200); outerSplitPane.setOneTouchExpandable(true); outerSplitPane.setResizeWeight(0.1); // -------------------------------------------------------------------------- /* add all text components to displayPanel; object label and scrollpane, * arrow label and scrollpane, relation label and scrollpane, comment * label and scrollpane */ informationPanel.add(objectLabel, new GridBagConstraints(0, 0, 1, 1, 0.0, 0.0 ,GridBagConstraints.WEST, GridBagConstraints.NONE, new Insets(0, 5, 0, 0), 0, 0)); informationPanel.add(arrowLabel, new GridBagConstraints(0, 2, 1, 1, 0.0, 0.0 ,GridBagConstraints.WEST, GridBagConstraints.NONE, new Insets(0, 5, 0, 0), 0, 0)); informationPanel.add(relationLabel, new GridBagConstraints(0, 4, 1, 1, 0.0, 0.0 ,GridBagConstraints.WEST, GridBagConstraints.NONE, new Insets(0, 5, 0, 0), 0, 0)); informationPanel.add(commentLabel, new GridBagConstraints(0, 6, 1, 1, 0.0, 0.0 ,GridBagConstraints.WEST, GridBagConstraints.NONE, new Insets(0, 5, 0, 0), 0, 0)); informationPanel.add(objectPane, new GridBagConstraints(0, 1, 5, 1, 1.0, 1.0 ,GridBagConstraints.CENTER, GridBagConstraints.BOTH, new Insets(0, 5, 0, 1), 0, 0)); informationPanel.add(arrowPane, new GridBagConstraints(0, 3, 5, 1, 1.0, 2.0 ,GridBagConstraints.CENTER, GridBagConstraints.BOTH, new Insets(0, 5, 0, 1), 0, 0)); informationPanel.add(relationPane, new GridBagConstraints(0, 5, 5, 1, 1.0, 2.0 ,GridBagConstraints.CENTER, GridBagConstraints.BOTH, new Insets(0, 5, 0, 1), 0, 0)); informationPanel.add(commentPane, new GridBagConstraints(0, 7, 5, 1, 1.0, 1.0 ,GridBagConstraints.CENTER, GridBagConstraints.BOTH, new Insets(0, 5, 0, 1), 0, 0)); /* End layout of information panel */ getContentPane().add(outerSplitPane); // ----------- Displays Category graph (in VGJ panel) and text (in info) ---- displayCategoryText(category_); displayCategoryGraph(category_.gml); graphCanvas_.update(false); // -------------------------------------------------------------------------- } public JMenuBar createJMenuBar() { // ----------- Initialize category menu bar to be returned ------------------ JMenuBar categoryMenuBar = new JMenuBar(); // -------------------------------------------------------------------------- // ----------- Initialize menus; contains tools and file options ------------ JMenu tools_menu = new JMenu("Tools"); // tools_menu.setMnemonic(KeyEvent.VK_T); JMenu file_menu = new JMenu("File"); // file_menu.setMnemonic(KeyEvent.VK_F); JMenu settings_menu = new JMenu("Settings"); // settings_menu.setMnemonic(KeyEvent.VK_E); // -------------------------------------------------------------------------- // -----------------------------------Settings----------------------------------------- ButtonGroup zoom_group = new ButtonGroup(); ActionListener acl = new ActionListener() { public void actionPerformed(ActionEvent e) { zoom_action(e); } }; JMenu zoom_menu = new JMenu("Zoom"); // zoom_menu.setMnemonic(KeyEvent.VK_Z); JRadioButtonMenuItem zoom_25 = new JRadioButtonMenuItem("25%"); zoom_25.addActionListener(acl); JRadioButtonMenuItem zoom_50 = new JRadioButtonMenuItem("50%"); zoom_50.addActionListener(acl); JRadioButtonMenuItem zoom_75 = new JRadioButtonMenuItem("75%"); zoom_75.addActionListener(acl); JRadioButtonMenuItem zoom_100 = new JRadioButtonMenuItem("100%", true); zoom_100.addActionListener(acl); JRadioButtonMenuItem zoom_125 = new JRadioButtonMenuItem("125%"); zoom_125.addActionListener(acl); JRadioButtonMenuItem zoom_150 = new JRadioButtonMenuItem("150%"); zoom_150.addActionListener(acl); JRadioButtonMenuItem zoom_200 = new JRadioButtonMenuItem("200%"); zoom_200.addActionListener(acl); zoom_menu.add(zoom_25); zoom_menu.add(zoom_50); zoom_menu.add(zoom_75); zoom_menu.add(zoom_100); zoom_menu.add(zoom_125); zoom_menu.add(zoom_150); zoom_menu.add(zoom_200); zoom_group.add(zoom_25); zoom_group.add(zoom_50); zoom_group.add(zoom_75); zoom_group.add(zoom_100); zoom_group.add(zoom_125); zoom_group.add(zoom_150); zoom_group.add(zoom_200); JCheckBoxMenuItem show_controls = new JCheckBoxMenuItem("Show VGJ Controls", true); // show_controls.setMnemonic(KeyEvent.VK_V); show_controls.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { show_controls_action(e); } }); JMenuItem view_gml = new JMenuItem("View GML"); // view_gml.setMnemonic(KeyEvent.VK_G); view_gml.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { view_gml_action(); } }); // ---------------------------------------------------------------------------------------- // ----------- Initialize all category tools -------------------------------- JMenuItem make_confluent = new JMenuItem("Make Confluent"); make_confluent.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { make_confluent_action(); } }); JMenuItem equality_of_composites = new JMenuItem("Equality of Composites"); equality_of_composites.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { equality_of_composites_action(); } }); JMenuItem make_dual = new JMenuItem("Make Dual"); make_dual.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { make_dual_action(); } }); JMenuItem isomorphism = new JMenuItem("Isomorphism?"); isomorphism.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { isomorphism_action(); } }); JMenuItem initial = new JMenuItem("Initial Object?"); initial.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { initial_action(); } }); JMenuItem epimorphism = new JMenuItem("Epimorphism?"); epimorphism.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { epimorphism_action(); } }); JMenuItem coequalizer = new JMenuItem("Coequalizer?"); coequalizer.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { coequalizer_action(); } }); JMenuItem sum = new JMenuItem("Sum?"); sum.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { sum_action(); } }); JMenuItem terminal = new JMenuItem("Terminal Object?"); terminal.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { terminal_action(); } }); JMenuItem monomorphism = new JMenuItem("Monomorphism?"); monomorphism.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { monomorphism_action(); } }); JMenuItem equalizer = new JMenuItem("Equalizer?"); equalizer.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { equalizer_action(); } }); JMenuItem product = new JMenuItem("Product?"); product.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { product_action(); } }); JMenuItem partial_order = new JMenuItem("Partial Order?"); partial_order.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { partial_order_action(); } }); JMenuItem product_categories = new JMenuItem("Create Product"); product_categories.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { product_category_action(); } }); JMenuItem sum_categories = new JMenuItem("Create Sum"); sum_categories.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { sum_category_action(); } }); // JMenuItem slice = new JMenuItem("Create Slice"); // slice.addActionListener(new ActionListener() { // public void actionPerformed(ActionEvent e) { // slice_action(); // } // }); JMenuItem pullback = new JMenuItem("Pullback?"); pullback.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { pullback_action(); } }); JMenuItem pushout = new JMenuItem("Pushout?"); pushout.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { pushout_action(); } }); // -------------------------------------------------------------------------- // ----------- Initialize all file menu options ----------------------------- JMenuItem add_data_category = new JMenuItem("Add Data"); // add_data_category.setMnemonic(KeyEvent.VK_A); add_data_category.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { add_data_category(); } }); JMenuItem remove_data_category = new JMenuItem("Remove Data"); // remove_data_category.setMnemonic(KeyEvent.VK_R); remove_data_category.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { remove_data_category(); } }); JMenuItem save_category = new JMenuItem("Save"); // save_category.setMnemonic(KeyEvent.VK_S); save_category.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { save_category_action(); } }); JMenuItem save_as_category = new JMenuItem("Save As"); save_as_category.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { save_as_category_action(); } }); JMenuItem close_category = new JMenuItem("Close"); // close_category.setMnemonic(KeyEvent.VK_C); close_category.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent e) { close_category_action(); } }); // -------------------------------------------------------------------------- settings_menu.add(zoom_menu); settings_menu.addSeparator(); settings_menu.add(show_controls); settings_menu.add(view_gml); // ----------- Add all category tools to the tool menu ---------------------- tools_menu.add(make_confluent); tools_menu.add(equality_of_composites); tools_menu.add(make_dual); tools_menu.add(isomorphism); tools_menu.addSeparator(); tools_menu.add(coequalizer); tools_menu.add(epimorphism); tools_menu.add(initial); tools_menu.add(pushout); tools_menu.add(sum); tools_menu.addSeparator(); tools_menu.add(equalizer); tools_menu.add(monomorphism); tools_menu.add(pullback); tools_menu.add(product); tools_menu.add(terminal); tools_menu.addSeparator(); tools_menu.add(partial_order); tools_menu.add(product_categories); tools_menu.add(sum_categories); // tools_menu.add(slice); // -------------------------------------------------------------------------- // ----------- Add all file options to the file menu ------------------------ file_menu.add(add_data_category); file_menu.add(remove_data_category); file_menu.addSeparator(); file_menu.add(save_category); file_menu.add(save_as_category); file_menu.add(close_category); // -------------------------------------------------------------------------- // ----------- add the file/tool menus to the menu bar ---------------------- categoryMenuBar.add(file_menu); categoryMenuBar.add(tools_menu); categoryMenuBar.add(settings_menu); // -------------------------------------------------------------------------- // return the category menu bar return categoryMenuBar; } // end of createMenuBar() private boolean displayCategoryGraph(String gmltext) // perform a graph update here...need to pass text to graph object { String text = gmltext; StringBufferInputStream stream = new StringBufferInputStream(text); GMLlexer lexer = new GMLlexer(stream); Graph newgraph; try { GMLobject GMLgraph = new GMLobject(lexer, null); GMLobject GMLtmp; // If the GML doesn't contain a graph, assume it is a graph. GMLtmp = GMLgraph.getGMLSubObject("graph", GMLobject.GMLlist, false); if(GMLtmp != null) GMLgraph = GMLtmp; newgraph = new Graph(GMLgraph); graph_.copy(newgraph); } catch(ParseError error) { JOptionPane.showMessageDialog(this, error.getMessage() + " at line " + lexer.getLineNumber() + " at or near \"" + lexer.getStringval() + "\".", "Error", JOptionPane.ERROR_MESSAGE); return false; } catch(IOException error) { JOptionPane.showMessageDialog(this, error.getMessage(), "Error", JOptionPane.ERROR_MESSAGE); return false; } return true; } private void displayCategoryText(Category c) //Displays category in the viewbox text area { int counter = 0; objectArea.setText(""); arrowArea.setText(""); relationArea.setText(""); commentArea.setText(""); for (int i = 0; i < c.num_objects; i++) { if (i < (c.num_objects - 1)) objectArea.append(c.obj[i] + ", "); if (i == (c.num_objects - 1)) objectArea.append(c.obj[i] + ".\n"); } for (int i = 0; i < c.num_arrows; i++) { if (i < (c.num_arrows - 1)) { arrowArea.append(c.arrow[i] + ":"); arrowArea.append(c.obj[c.arr[i][0]] + "->"); arrowArea.append(c.obj[c.arr[i][1]] + ", "); } if (i == (c.num_arrows - 1)) { arrowArea.append(c.arrow[i] + ":"); arrowArea.append(c.obj[c.arr[i][0]] + "->"); arrowArea.append(c.obj[c.arr[i][1]] +". " ); } } relationArea.setText(c.relationsToString()); commentArea.setText(c.comment); objectArea.setCaretPosition(0); arrowArea.setCaretPosition(0); relationArea.setCaretPosition(0); commentArea.setCaretPosition(0); } public GraphCanvas getCanvas() { return graphCanvas_; } public Graph getGraph() { return graph_; } public boolean handleEvent(Event event) { // -------------- A scrolledPanel event; either RESIZE or OFFSET ------------- if(event.target instanceof ScrolledPanel) { if(event.id == ScrolledPanel.RESIZE) // RESIZE event from panel; update viewportScroller_ (small box) dimensions { DDimension tmp_dim; tmp_dim = scrolledPanel_.getPortSize(); viewportScroller_.setPortSize(tmp_dim.width, tmp_dim.height); tmp_dim = scrolledPanel_.getContentSize(); viewportScroller_.setContentSize(tmp_dim.width, tmp_dim.height); tmp_dim = scrolledPanel_.getOffset(); viewportScroller_.setOffset(tmp_dim.width, tmp_dim.height); return true; } // end RESIZE if else if(event.id == ScrolledPanel.OFFSET) // OFFSET event; update viewportScroller_ (small box) offsets { DDimension tmp_dim = scrolledPanel_.getOffset(); viewportScroller_.setOffset(tmp_dim.width, tmp_dim.height); return true; } // end OFFSET else if graphCanvas_.paintOver(graphCanvas_.getGraphicsInternal_()); } // end ScrolledPanel else if // -------------------------------------------------------------------------- // ----------- A viewportScroller event; either SCROLL or DONE -------------- else if(event.target instanceof ViewportScroller) { if(event.id == ViewportScroller.SCROLL) { // display only edges (no objects); then scroll to specified location //graphCanvas_.setWireframe(true); scrolledPanel_.scrollTo((int)viewportScroller_.getOffsetX(), (int)viewportScroller_.getOffsetY()); } // end SCROLL if else if(event.id == ViewportScroller.DONE) { // display both edges and objects; scroll to specified location //graphCanvas_.setWireframe(false); scrolledPanel_.scrollTo((int)viewportScroller_.getOffsetX(), (int)viewportScroller_.getOffsetY()); } // end DONE else if //System.out.println("scrolling"); graphCanvas_.paintOver(graphCanvas_.getGraphicsInternal_()); } // end ViewportScroller else if // -------------------------------------------------------------------------- // ----------- An AngleControlPanel event; either ANGLE or DONE ------------- else if(event.target instanceof AngleControlPanel) { if(event.id == AngleControlPanel.ANGLE) { // display only edges (no objects); then set desired angles DPoint angles = (DPoint)event.arg; // graphCanvas_.setWireframe(true); graphCanvas_.setViewAngles(angles.x, angles.y); } // end ANGLE if else if(event.id == AngleControlPanel.DONE) { // display both edges and objects; set desired angles DPoint angles = (DPoint)event.arg; // graphCanvas_.setWireframe(false); graphCanvas_.setViewAngles(angles.x, angles.y); } // end DONE else if //System.out.println("angles"); graphCanvas_.paintOver(graphCanvas_.getGraphicsInternal_()); } // end AngleControlPanel else if // -------------------------------------------------------------------------- // call inherited handler return super.handleEvent(event); } private void save_category_action() { graphCanvas_.unselectItems(); GraphEdit ge = new GraphEdit(graph_, graphCanvas_); category_.gml = ge.getGMLText(); ge.dispose(); //Save Category information including current display //of category in file if (category_.file_ == null) //&& something else) { save_as_category_action(); } else { SaveFileWriter save_ = new SaveFileWriter(category_.file_, this); save_.saveCategory(); category_.originalGml = category_.gml; } } private void save_as_category_action() { graphCanvas_.unselectItems(); GraphEdit ge = new GraphEdit(graph_, graphCanvas_); category_.gml = ge.getGMLText(); ge.dispose(); //Save Category information including current display //of category in file JFileChooser save_file = new JFileChooser(); save_file.addChoosableFileFilter(new CatFilter()); save_file.addChoosableFileFilter(new CglFilter()); save_file.setAcceptAllFileFilterUsed(false); int fileOption = save_file.showSaveDialog(this); if (fileOption == JFileChooser.CANCEL_OPTION) {} else if (fileOption == JFileChooser.APPROVE_OPTION) { int replaceFile = JOptionPane.YES_OPTION; File file_ = save_file.getSelectedFile(); if (file_.exists()) { replaceFile = JOptionPane.showInternalConfirmDialog(this, "File " + file_.getPath() + " already exists.\n Do you want to replace it?", "Save As", JOptionPane.YES_NO_OPTION, JOptionPane.PLAIN_MESSAGE); } /* if (!file_.getName().toLowerCase().endsWith(".cgl") && !file_.getName().toLowerCase().endsWith(".cat")) file_ = new File(file_.getPath() + ".cgl");*/ if (save_file.getFileFilter() instanceof CatFilter) { file_ = new File(file_.getPath() + ".cat"); } else if (save_file.getFileFilter() instanceof CglFilter) { file_ = new File(file_.getPath() + ".cgl"); } if (replaceFile == JOptionPane.YES_OPTION) { SaveFileWriter save_ = new SaveFileWriter(file_, this); save_.saveCategory(); //Save current graphical display as original category_.originalGml = category_.gml; } } } private void close_category_action() { int saveOption = JOptionPane.NO_OPTION; // System.out.println(category_.isModified()); if (category_.isModified()) { if (this.isIcon()) { try {this.setIcon(false);} catch (PropertyVetoException e) {} } saveOption = JOptionPane.showInternalConfirmDialog(this, "Save changes to " + category_.name + "?", "GDCT", JOptionPane.YES_NO_CANCEL_OPTION, JOptionPane.QUESTION_MESSAGE); } if (saveOption == JOptionPane.CANCEL_OPTION) {return;} // don't exit, don't save else if (saveOption == JOptionPane.YES_OPTION) {save_category_action();} else if (saveOption == JOptionPane.NO_OPTION) {} // exit without saving; which means let the method finish, therefore this option really doesn't do anything this.dispose(); } private void add_data_category() { AddDataFrame adf = new AddDataFrame(this); displayTool(adf); adf.setLocation((int)this.getLocation().getX() + (int)adf.getWidth()/2, (int)this.getLocation().getY() + 50); adf.setSize(450, 450); } private void remove_data_category() { RemoveDataFrame rdf = new RemoveDataFrame(this); displayTool(rdf); rdf.setLocation((int)this.getLocation().getX() + (int)rdf.getWidth()/2, (int)this.getLocation().getY() + 50); rdf.setSize(450, 450); } private void zoom_action(ActionEvent e) { graphCanvas_.setScale(Double.parseDouble(((JRadioButtonMenuItem)e.getSource()).getText().replaceAll("%", ""))/100.0); this.validate(); } private void view_gml_action() { GraphEdit ge = new GraphEdit(graph_, graphCanvas_); displayTool(ge); } private void show_controls_action(ActionEvent e) { angleControlPanel_.setVisible(((JCheckBoxMenuItem)e.getSource()).isSelected()); viewportScrollPanel.setVisible(((JCheckBoxMenuItem)e.getSource()).isSelected()); } private void make_confluent_action() { MakeConfluentPane mcp = new MakeConfluentPane(this); } private void equality_of_composites_action() { EqualityCompositesFrame ecf = new EqualityCompositesFrame(this); if (checkTool(ecf)) displayTool(ecf); } private void make_dual_action() { MakeDualPane mdp = new MakeDualPane(this); } private void isomorphism_action() { IsoFrame isof = new IsoFrame(this); if (checkTool(isof)) displayTool(isof); } private void menu_action(ActionEvent e) { try { Class temp_class = Class.forName(((JMenuItem)e.getSource()).getText() + "Frame"); System.out.println("class name: " + temp_class.getName()); displayTool((JInternalFrame)(temp_class.newInstance())); } catch (ClassNotFoundException cnfe) {cnfe.printStackTrace();} catch (InstantiationException ie) {ie.printStackTrace();} catch (IllegalAccessException iae) {iae.printStackTrace();} } private void initial_action() { InitialObjectFrame iof = new InitialObjectFrame(this); if (checkTool(iof)) displayTool(iof); } private void epimorphism_action() { EpiFrame ef = new EpiFrame(this); if (checkTool(ef)) displayTool(ef); } private void coequalizer_action() { CoequalizerFrame cef = new CoequalizerFrame(this); if (checkTool(cef)) displayTool(cef); } private void sum_action() { SumFrame sf = new SumFrame(this); if (checkTool(sf)) displayTool(sf); } private void terminal_action() { TerminalObjectFrame tof = new TerminalObjectFrame(this); if (checkTool(tof)) displayTool(tof); } private void monomorphism_action() { MonoFrame mf = new MonoFrame(this); if (checkTool(mf)) displayTool(mf); } private void equalizer_action() { EqualizerFrame ef = new EqualizerFrame(this); if (checkTool(ef)) displayTool(ef); } private void product_action() { ProductFrame pf = new ProductFrame(this); if (checkTool(pf)) displayTool(pf); } private void partial_order_action() { PartialOrderPane pop = new PartialOrderPane(this); } private void product_category_action() { ProductCategory pc = new ProductCategory(this); pc.createProductCategory(); } private void sum_category_action() { SumCategory sc = new SumCategory(this); sc.createSumCategory(); } // private void slice_action() // { // SliceCategory sc = new SliceCategory(this); // sc.createSliceCategory(); // } private void pullback_action() { PullbackFrame pb = new PullbackFrame(this); if (checkTool(pb)) displayTool(pb); } private void pushout_action() { PushoutFrame po = new PushoutFrame(this); if (checkTool(po)) displayTool(po); } public Category getCategory() { return category_; } public void setCategory(Category new_category) { category_ = new_category; displayCategoryGraph(category_.gml); displayCategoryText(category_); } private void closeTools() { for (int i=0; i