guiframe.java

Petri网分析工具PIPE is open-source

      if(modelFile!=null) path=modelFile.toString();
      else path=appTab.getTitleAt(appTab.getSelectedIndex());
      String filename=new FileBrowser(path).saveFile();
      if (filename!=null) saveNet(new File(filename));
    }
  }
  
	private void saveNet(File outFile){
		try{
			appModel.savePNML(outFile);
      CreateGui.setFile(outFile,appTab.getSelectedIndex());
			appView.netChanged = false;
			appTab.setTitleAt(appTab.getSelectedIndex(),outFile.getName());
      setTitle(outFile.getName());  // Change the window title
    } catch (Exception e) {
      System.err.println(e);
      JOptionPane.showMessageDialog(GuiFrame.this,
          e.toString(),
          "File Output Error",
          JOptionPane.ERROR_MESSAGE);
      return;
    }
	}
  /**
   * Creates a new tab with the selected file, or a new file if filename==null
   * @param filename Filename of net to load, or <b>null</b> to create a new, empty tab
   */ 
  public void createNewTab(String filename) {
    int freeSpace = CreateGui.getFreeSpace();
    String name="";
    setObjects(freeSpace);
    appModel.addObserver((Observer)appView); // Add the view as Observer
    appModel.addObserver((Observer)appGui);  // Add the app window as observer
    
    if(filename==null) {
      name = "New Petri net "+newNameCounter++ +".xml";
    } else 
      try {
        File inFile=new File(filename);
        appModel.loadPNML(inFile.getPath());
        CreateGui.setFile(inFile,freeSpace);
        name=inFile.getName();
      } catch(Exception e) {
        JOptionPane.showMessageDialog(GuiFrame.this,"Error loading file:\n"+filename+"\nGuru meditation:\n"+e.toString(),"File load error",
          JOptionPane.ERROR_MESSAGE);
        e.printStackTrace();
        return;
      }
    appView.repaint();
    appView.netChanged = false;   // Status is unchanged
    
    JScrollPane scroller=new JScrollPane(appView);
    appView.updatePreferredSize();
    scroller.setBorder(new BevelBorder(BevelBorder.LOWERED)); // make it less bad on XP
    appTab.addTab(name,null,scroller,null);
    appTab.setSelectedIndex(freeSpace);
    
    setTitle(name);// Change the program caption
  }
 
	/**
   * If current net has modifications, asks if you want to save and does it if you want.
	 * @return true if handled, false if cancelled 
	 */
	public boolean checkForSave() {
		if(appView.netChanged) {
			int result=JOptionPane.showConfirmDialog(GuiFrame.this,"Current file has changed. Save current file?",
					"Confirm Save Current File",
					JOptionPane.YES_NO_CANCEL_OPTION,
					JOptionPane.WARNING_MESSAGE);
		switch(result) {
			case JOptionPane.YES_OPTION: saveOperation(false); break;
			case JOptionPane.CLOSED_OPTION:
			case JOptionPane.CANCEL_OPTION:
				return false;
		}
	}
	return true;
}

  //On application close,loop through all tabs and check if they have been saved
	public boolean checkForSaveAll(){
		for(int counter = 0;counter < appTab.getTabCount();counter++){
			appTab.setSelectedIndex(counter);
      if (checkForSave()==false) return false;
		}
		return true;
	}
	
  class GridAction extends GuiAction {
		GridAction (String name, String tooltip, String keystroke) {
			super(name, tooltip, keystroke);
		}
		
		public void actionPerformed(ActionEvent e) {
			Grid.increment();
			repaint();
		}
	}
 	
	class FileAction extends GuiAction {
		//constructor
		FileAction(String name, String tooltip, String keystroke) {
			super(name, tooltip, keystroke);
		}
		
		public void actionPerformed(ActionEvent e) {
			if(this==saveAction) saveOperation(false);            		 // code for Save operation
			else if(this==saveAsAction) saveOperation(true);           // code for Save As operations
			else if(this==openAction){                                 // code for Open operation
				File filePath=new FileBrowser(CreateGui.userPath).openFile();
				if ((filePath != null) && filePath.exists() && filePath.isFile() && filePath.canRead()) {
          CreateGui.userPath=filePath.getParent();
					createNewTab(filePath.toString());
				}
			}
			else if(this==createAction)createNewTab(null);              // Create a new tab
			else if((this==exitAction)&&checkForSaveAll()) {
				dispose();
				System.exit(0);
			}
			else if((this==closeAction)&&(appTab.getTabCount()>0)&&checkForSave()) {
				setObjectsNull(appTab.getSelectedIndex());
				appTab.remove(appTab.getSelectedIndex());
			}
      else if(this==exportPNGAction) Export.exportGuiView(appView,Export.PNG);
      else if(this==exportPSAction)  Export.exportGuiView(appView,Export.POSTSCRIPT);
      else if(this==printAction)     Export.exportGuiView(appView,Export.PRINTER);
		}
	}

  class ExampleFileAction extends GuiAction {
    private File file;
    ExampleFileAction(File file) {
      super(file.getName(), "Open example file \""+file.getName()+"\"", null);
      this.file=file;
      putValue(SMALL_ICON, new ImageIcon(CreateGui.imgPath+"Net.png"));
    }
    
    public void actionPerformed(ActionEvent e){
      createNewTab(file.getAbsolutePath());
    }
  }

  class DeleteAction extends GuiAction {
    DeleteAction(String name, String tooltip, String keystroke) {
      super(name, tooltip, keystroke);
    }
    
    public void actionPerformed(ActionEvent e){
      appView.getSelectionObject().deleteSelection();
    }
  }
 
	class TypeAction extends GuiAction {
    TypeAction(String name, int typeID, String tooltip,String keystroke){
      super(name, tooltip, keystroke);
      this.typeID = typeID;
    }
    TypeAction(String name, int typeID, String tooltip,String keystroke, boolean toggleable){
      super(name, tooltip, keystroke, toggleable);
      this.typeID = typeID;
    }
		public void actionPerformed(ActionEvent e){
      this.setSelected(true);
      // deselect other actions
      if(this!=placeAction) placeAction.setSelected(false);
      if(this!=transAction) transAction.setSelected(false);
      if(this!=timedtransAction) timedtransAction.setSelected(false);
      if(this!=  arcAction)   arcAction.setSelected(false);
      if(this!=tokenAction) tokenAction.setSelected(false);
      if(this!=deleteTokenAction) deleteTokenAction.setSelected(false);
      if(this!=selectAction) selectAction.setSelected(false);
      if(this!=annotationAction) annotationAction.setSelected(false);
      
		  if(appView==null) return;

			setMode(typeID);
			appView.getSelectionObject().disableSelection();
			
      statusBar.changeText(typeID);

      if((typeID!=ARC)&&(CreateGui.getView().createArc!=null)) {
        appView.createArc.delete();          
        appView.createArc=null;
        appView.repaint();
      }
     
      if(typeID==SELECT) {
				//disable drawing to eliminate possiblity of connecting arc to old coord of moved component
				statusBar.changeText(typeID);
				appView.getSelectionObject().enableSelection();
      }
		}
		
		private int typeID;
		private String imageFileName;
		private String selectedFileName;
	}
  
  
 
  class AnimateAction extends GuiAction {
    private int typeID;
    private AnimationHistory animBox ;

    AnimateAction(String name,int typeID,String tooltip){
      super(name,tooltip,null);
      this.typeID = typeID;
    }
    AnimateAction(String name,int typeID,String tooltip,boolean toggleable){
      super(name,tooltip,null,toggleable);
      this.typeID = typeID;
    }

    public void actionPerformed(ActionEvent e){
      if(appView==null) return;

      animBox = CreateGui.getAnimationHistory();

      switch(typeID){
      case START:
        if(CreateGui.getView().animationmode) restoreMode();
        else setMode(typeID);
        setAnimationMode(!CreateGui.getView().animationmode);
        break;

      case RANDOM:
        CreateGui.getAnimator().doRandomFiring();
        break;

      case STEPFORWARD:
        animBox.stepForward();
        CreateGui.getAnimator().stepForward();
        break;

      case STEPBACKWARD:
        animBox.stepBackwards();
        CreateGui.getAnimator().stepBack();
        break;
        
      case ANIMATE:
        Animator a=CreateGui.getAnimator();
        if(a.getNumberSequences()>0) {
          a.setNumberSequences(0); // stop animation
          setSelected(false);
        } else {
          stepbackwardAction.setEnabled(false);
          stepforwardAction.setEnabled(false);
          randomAction.setEnabled(false);
          setSelected(true);
          CreateGui.getAnimator().startRandomFiring();
        }
        break;

      default:
        return;
      }

    }
  }
  
  public void setRandomAnimationMode(boolean on) {
    stepbackwardAction.setEnabled(!on);
    stepforwardAction.setEnabled(!on);
    randomAction.setEnabled(!on);
    randomAnimateAction.setSelected(on);
  }

  private void setAnimationMode(boolean on) {
    randomAnimateAction.setSelected(false);
    CreateGui.getAnimator().setNumberSequences(0);
    startAction.setSelected(on);
    if (on) {
      statusBar.changeText(getStatusBar().textforAnimation);
      CreateGui.getView().changeAnimationMode(true);
      CreateGui.getAnimator().storeModel();
      CreateGui.currentPNMLData().setEnabledTransitions();
      CreateGui.getAnimator().highlightEnabledTransitions();
      CreateGui.addAnimationHistory();
      enableActions(false);//disables all non-animation buttons
    } else {
      statusBar.changeText(statusBar.textforDrawing);
      CreateGui.getView().changeAnimationMode(false);
      CreateGui.getAnimator().restoreModel();
      CreateGui.removeAnimationHistory();
      enableActions(true); //renables all non-animation buttons
    }
  }
  
		
	public void setMode(int _mode) {
		if (mode != _mode){				// Don't bother unless new mode is different.
			prev_mode = mode;
			mode = _mode;
		}
	}
		
	public int getMode() {
		return mode;
	}
	
	public void restoreMode() {
		mode = prev_mode;
	      placeAction.setSelected(mode == PLACE);
	      transAction.setSelected(mode == IMMTRANS);
	      timedtransAction.setSelected(mode == TIMEDTRANS);
	      arcAction.setSelected(mode == ARC);
	      tokenAction.setSelected(mode == ADDTOKEN);
	      deleteTokenAction.setSelected(mode == DELTOKEN);
	      selectAction.setSelected(mode == SELECT);
	      annotationAction.setSelected(mode == ANNOTATION);
	}
	
	public void disableGuiMenu() {
		menuBar.setEnabled(false);
		
	}
	
	public void enableGuiMenu() {
		menuBar.setEnabled(true);
	}
	
  public void setTitle(String title) {
    if(title==null) super.setTitle(frameTitle);
    else super.setTitle(frameTitle+": "+title);
  }
  
  public void initExit() {
    exitAction.actionPerformed(null);
  }
	
	class WindowHandler extends WindowAdapter{
		//Handler for window closing event
		public void windowClosing(WindowEvent e){
	    initExit();
		}
	}
	
}