View Javadoc

1   package fr.ove.openmath.mfd2;
2   
3   import java.awt.*;
4   import java.awt.event.*;
5   import java.util.*;
6   import java.io.*;
7   import java.net.*;
8   import fr.ove.openmath.mfd2.*;
9   import fr.ove.openmath.mfd2.events.*;
10  import fr.ove.openmath.mfd2.frames.*;
11  import fr.inria.openmath.omapi.*;
12  import fr.ove.openmath.exceptions.*;
13  import fr.ove.errordialog.*;
14  
15  /***
16  * The main panel of the application Mfd2.
17  *
18  * 
19  */
20  public class PanelMfd2 extends Panel implements PanelJomesListener {
21      // Le panel contenu tous les menus et assimilÈs
22  	Panel panelMenu;
23  	
24  	// Le panel contenant tout ce qui va concerner la commande lazy de la bd
25  	Panel panelLazy;
26  	Button setLazyButton;
27  	Label labelLazy;
28  	Panel panelRadio;
29  	CheckboxGroup lazyGroup;
30  	Checkbox radioOn;
31  	Checkbox radioOff;
32  	
33  	Button clearButton;
34  	
35  	// Le panel contenant tout ce qui va concerner la commande de la dÈduction de la bd
36  	Panel panelDeduction;
37  	Panel panelDepth;
38  	Label labelDepth;
39  	TextField entryDepth;
40  	Panel panelHeight;
41  	Label labelHeight;
42  	TextField entryHeight;
43  	
44  	// Le panel principal concernant les requÍtes ? la bd
45  	Panel panelMain;
46      Mfd2ScrollPane mfd2ScrollPane;
47  	Panel panelRequest;
48  	TextField entryRequest;
49  	Panel panelButton;
50  	Button buttonRequest;
51  	Button buttonContaining;
52  	Button buttonClear;
53  	
54  	// Dernier ÈlÈment de l'interface, une fenÍtre de status
55  	TextArea statusArea;
56  	//StatusArea statusArea;
57      
58      // La liste des RequÍtes
59      Vector listRequests = new Vector();
60      // La requÍte courante
61      PanelJomes currentRequest;
62      
63      // Les fenÍtre OpenMath
64      ShowOM frameRequest;
65      ShowOM frameResult;
66      
67      RequestContaining frameContaining;
68      boolean isContainingRequest = false;
69      
70      boolean updateEntryRequest = true;
71      
72      // La communication
73  	private InputStream inputStream;
74  	private OutputStream outputStream;
75  	
76  	private Selector selector;
77      
78      /***
79      * The constructor
80      */
81  	public PanelMfd2(Socket socket) {
82  	    try {
83          	outputStream = socket.getOutputStream();
84          	inputStream = socket.getInputStream();
85  	    }
86  	    catch (IOException ioe) {
87  	        System.out.println("Can't get streams from socket");
88  	        ioe.printStackTrace();
89  	    }
90  	    
91  		Font commonFont = new Font("Dialog", Font.PLAIN, 14);
92  		Color commonColor = Color.lightGray;
93  		
94  		setLayout(new BorderLayout(0,0));
95  		setBackground(commonColor);
96  		
97  		panelMenu = new Panel();
98  		panelMenu.setLayout(new FlowLayout(FlowLayout.LEFT, 5, 2));
99  		panelMenu.setBackground(commonColor);
100 		add("North", panelMenu);
101 		
102 		// La barre de menu
103         MenuBar menuBar = new MenuBar();
104         
105         // Premier menu : chargement des livres
106         Menu menu = new Menu("Load Book");
107         
108         // Qui va traiter les ÈvÈnements du type ActionEvent
109         MenuLoadHandler menuLoadHandler = new MenuLoadHandler();
110         
111         // On met dans ce premier menu tous les items nÈcessaires (i.e. les livres ? charger)
112         MenuItem menuItem = new MenuItem("base.fdb");
113 		menuItem.setActionCommand(menuItem.getLabel());
114 		menuItem.addActionListener(menuLoadHandler);
115         menu.add(menuItem);
116         
117         menuItem = new MenuItem("basic.fdb");
118 		menuItem.setActionCommand(menuItem.getLabel());
119 		menuItem.addActionListener(menuLoadHandler);
120         menu.add(menuItem);
121 		
122         menuItem = new MenuItem("even.fdb");
123 		menuItem.setActionCommand(menuItem.getLabel());
124 		menuItem.addActionListener(menuLoadHandler);
125         menu.add(menuItem);
126 		
127         menuItem = new MenuItem("trigo.fdb");
128 		menuItem.setActionCommand(menuItem.getLabel());
129 		menuItem.addActionListener(menuLoadHandler);
130         menu.add(menuItem);
131         
132         menuItem = new MenuItem("AS");
133 		menuItem.setActionCommand(menuItem.getLabel());
134 		menuItem.addActionListener(menuLoadHandler);
135         menu.add(menuItem);
136         
137         // On met ce menu dans la barre de menus
138         menuBar.add(menu);
139         
140         // Second menu : vision OpenMath de la chose
141         menu = new Menu("OpenMath");
142         
143         // Qui va traiter les ÈvÈnements du type ActionEvent
144         MenuOpenMathHandler menuOpenMathHandler = new MenuOpenMathHandler();
145 
146         // On met dans ce premier menu tous les items nÈcessaires
147         menuItem = new MenuItem("Request");
148 		menuItem.setActionCommand(menuItem.getLabel());
149 		menuItem.addActionListener(menuOpenMathHandler);
150         menu.add(menuItem);
151         
152         menuItem = new MenuItem("Result");
153 		menuItem.setActionCommand(menuItem.getLabel());
154 		menuItem.addActionListener(menuOpenMathHandler);
155         menu.add(menuItem);
156         
157         // On met ce menu dans la barre de menus
158         menuBar.add(menu);
159         
160         // Le panel spÈcial pour pouvoir mettre des barres de menu dans des applets.
161         MenuPanel menuPanel = new MenuPanel();
162 		menuPanel.setFont(commonFont);
163 		// Comme les menus dÈroulants sont en fait des Popup Menus et qu'on ne peut pas changer
164 		// leur couleur (ni quoi que ce soit d'ailleurs) on met la barre de menu ? la mÍme couleur
165 		// que ces derniers
166         menuPanel.setBackground(commonColor);
167         menuPanel.setMenuBar(menuBar);
168         menuPanel.setBounds(0, 0, 470, 30);
169         
170         // On ajoute la barre de menu
171         panelMenu.add(menuPanel);
172 		
173     	setLazyButton = new Button("Lazy OFF");
174     	setLazyButton.setFont(commonFont);
175     	setLazyButton.setBackground(commonColor);
176     	
177     	setLazyButton.addActionListener(
178     	    new ActionListener () {
179         		public void actionPerformed(ActionEvent event) {
180         		    String currentLabel = setLazyButton.getLabel();
181         		    boolean lazy;
182         		    if (currentLabel.equals("Lazy ON")) {
183                 		setLazyButton.setLabel("Lazy OFF");
184                 		lazy = false;
185                 	}
186                     else {
187                 		setLazyButton.setLabel("Lazy ON");
188                 		lazy = true;
189                 	}
190                 	
191 		            statusArea.append("> set lazy " + lazy + " sent\n");
192                     String omObject = "<OMOBJ>\n  <OMA>\n    <OMS cd=\"mfd2\" name=\"setlazy\"/>\n    <OMS cd=\"logic\" name=\"" + lazy + "\"/>\n  </OMA>\n</OMOBJ>";
193                     setObject(omObject.getBytes());
194             	}
195     	    }
196     	);
197 		
198 		panelMenu.add(setLazyButton);
199 		
200 		clearButton = new Button("Clear");
201     	clearButton.setFont(commonFont);
202     	clearButton.setBackground(commonColor);
203 		
204     	clearButton.addActionListener(
205     	    new ActionListener () {
206         		public void actionPerformed(ActionEvent event) {
207                     statusArea.append("> clear sent\n");
208                     String omObject = "<OMOBJ>\n  <OMS cd=\"mfd2\" name=\"clear\"/>\n</OMOBJ>";
209                     setObject(omObject.getBytes());
210             	}
211     	    }
212     	);
213 		
214 		panelMenu.add(clearButton);
215 				
216 		panelDeduction = new Panel();
217 		panelDeduction.setLayout(new FlowLayout(FlowLayout.CENTER,10,0));
218 		panelMenu.add(panelDeduction);
219 		
220 		panelDepth = new Panel();
221 		panelDepth.setLayout(new FlowLayout(FlowLayout.LEFT,0,0));
222 		panelDeduction.add(panelDepth);
223 		
224 		labelDepth = new Label("Depth");
225 		labelDepth.setFont(commonFont);
226 		panelDepth.add(labelDepth);
227 		
228 		entryDepth = new TextField();
229 		entryDepth.setFont(commonFont);
230 		entryDepth.setText("1");
231 		panelDepth.add(entryDepth);
232 		
233         // On tape sur la touche entrÈe (on envoie le paramËtre de dÈduction)
234 		entryDepth.addActionListener(
235 		    new ActionListener() {
236 		        public void actionPerformed(ActionEvent event) {
237 		            statusArea.append("> deduction depth sent : " + entryDepth.getText() + "\n");
238                     String omObject = "<OMOBJ>\n  <OMA>\n    <OMS cd=\"mfd2\" name=\"setdepth\"/>\n    <OMI> " + entryDepth.getText() + " </OMI>\n  </OMA>\n</OMOBJ>";
239                     setObject(omObject.getBytes());
240                 }
241             }
242         );
243 
244 		panelHeight = new Panel();
245 		panelHeight.setLayout(new FlowLayout(FlowLayout.LEFT,0,0));
246 		panelDeduction.add(panelHeight);
247 		
248 		labelHeight = new Label("Height");
249 		labelHeight.setFont(commonFont);
250 		panelHeight.add(labelHeight);
251 		
252 		entryHeight = new TextField();
253 		entryHeight.setFont(commonFont);
254 		entryHeight.setText("2");
255 		panelHeight.add(entryHeight);
256 		
257         // On tape sur la touche entrÈe (on envoie le paramËtre de dÈduction)
258 		entryHeight.addActionListener(
259 		    new ActionListener() {
260 		        public void actionPerformed(ActionEvent event) {
261 		            statusArea.append("> deduction height sent : " + entryHeight.getText() + "\n");
262                     String omObject = "<OMOBJ>\n  <OMA>\n    <OMS cd=\"mfd2\" name=\"setheight\"/>\n    <OMI> " + entryHeight.getText() + " </OMI>\n  </OMA>\n</OMOBJ>";
263                     //System.out.println("On envoie height :\n " + omObject);
264                     setObject(omObject.getBytes());
265                 }
266             }
267         );
268 
269 		panelMain = new Panel();
270 		panelMain.setLayout(new BorderLayout(0,0));
271 		add("Center", panelMain);
272 		
273 		
274         // Le panneau o? vont se trouver les diffÈrentes requÍtes et leur rÈponse respective
275         mfd2ScrollPane = new Mfd2ScrollPane(460, 300, 5);
276         mfd2ScrollPane.setBackground(Color.white);
277         
278         // La premiËre requÍte (qui est donc la requÍte courante)
279         currentRequest = new PanelJomes();
280         currentRequest.addPanelJomesListener(this);
281         
282         mfd2ScrollPane.add(currentRequest);
283         // On l'ajoute ? la liste des requÍtes
284         listRequests.addElement(currentRequest);
285         
286         // On ajoute les requÍte au panel
287         panelMain.add("Center", mfd2ScrollPane);
288 		
289 		panelRequest = new Panel();
290 		panelRequest.setLayout(new BorderLayout(0,0));
291 		panelMain.add("South", panelRequest);
292 		
293 		entryRequest = new TextField();
294 		entryRequest.setFont(new Font("Dialog", Font.BOLD, 14)/*commonFont*/);
295 		entryRequest.requestFocus();
296 		panelRequest.add("Center", entryRequest);
297 		
298 		// Le traitement des actions sur la zone de saisie
299 		// On saisi du texte
300 		entryRequest.addTextListener(
301         	new TextListener() {
302         	    public void textValueChanged(TextEvent event) {
303         	        if (!entryRequest.getText().equals("")) {
304             	        updateEntryRequest = false;
305             			currentRequest.setLinearRequest(entryRequest.getText());
306             	        updateEntryRequest = true;
307             		}
308         		}
309         	}
310         );
311         
312         // On tape sur la touche entrÈe (on envoie la requÍte)
313 		entryRequest.addActionListener(
314 		    new ActionListener() {
315 		        public void actionPerformed(ActionEvent event) {
316 		            byte[] omRequest = currentRequest.getOpenMathRequest().getBytes();
317 		            if (omRequest.length > 0) {
318     		            statusArea.append("> Request sent\n");
319     		            setObject(omRequest);
320     		            
321     		            /*
322     		            // A revoir parce que Áa Áa veut dire que l'on change de requÍte courante avant
323     		            // d'avoir, a priori, reÁu la rÈponse ? la requÍte.
324     		            // En attendant, on fait.....
325     		            
326     		            // Si la requÍte courante est la derniËre de la liste, alors on crÈÈ une nouvelle
327     		            // requÍte. Sinon, on met le requÍte suivante comme requÍte courante.
328     		            int currentRequestIndex = listRequests.indexOf(currentRequest);
329     		            if (currentRequestIndex == (listRequests.size() -1))
330         		            // CrÈation d'un nouvelle requÍte
331         		            createNewRequest();
332         		        else {
333         		            currentRequest = (PanelJomes) listRequests.elementAt(currentRequestIndex + 1);
334         		            
335                             // On envoie un ÈvÈnement comme quoi il faut les mettre ? jour
336                     	    PanelJomesEvent panelJomesEvent = new PanelJomesEvent(currentRequest);
337                     	    panelJomesEvent.setAction(PanelJomesEvent.UPDATE, null);
338                     	    currentRequest.firePanelJomesEvent(panelJomesEvent);
339                     	    
340                             // On envoie un ÈvÈnement comme quoi il faut mettre ? jour qui est sÈlectionnÈ
341                     	    panelJomesEvent.setAction(PanelJomesEvent.UPDATE_SELECTION, null);
342                     	    currentRequest.firePanelJomesEvent(panelJomesEvent);
343                     	    
344                     	    // Le focus sur la saisie de la requÍte
345                     	    entryRequest.requestFocus();
346         		        }
347         		        */
348                     }
349                 }
350             }
351         );
352 
353 		
354 		panelButton = new Panel();
355 		panelButton.setLayout(new FlowLayout(FlowLayout.LEFT, 0, 0));
356         panelButton.setFont(commonFont);
357 		panelButton.setBackground(commonColor);
358 		panelRequest.add("East", panelButton);
359 		
360 		buttonRequest = new Button();
361 		buttonRequest.setLabel("New");
362 		buttonRequest.setFont(commonFont);
363 		buttonRequest.setBackground(commonColor);
364 		panelButton.add(buttonRequest);
365 		
366 		// Le traitement des actions sur le bouton
367 		buttonRequest.addActionListener(
368 		    new ActionListener() {
369 		        public void actionPerformed(ActionEvent event) {
370 		            // CrÈation d'un nouvelle requÍte
371 		            createNewRequest();
372                 }
373             }
374         );
375 
376 		buttonContaining = new Button();
377 		buttonContaining.setLabel("Find");
378 		buttonContaining.setFont(commonFont);
379 		buttonContaining.setBackground(commonColor);
380 		panelButton.add(buttonContaining);
381 		
382 		frameContaining = new RequestContaining((Frame) getParent(), this);
383 		frameContaining.setVisible(false);
384 		
385 		// Le traitement des actions sur le bouton
386 		buttonContaining.addActionListener(
387 		    new ActionListener() {
388 		        public void actionPerformed(ActionEvent event) {
389 		            if (frameContaining.isVisible())
390 		                frameContaining.setVisible(false);
391 		            else
392 		                frameContaining.setVisible(true);
393                 }
394             }
395         );
396 
397 		buttonClear = new Button();
398 		buttonClear.setLabel("Clear");
399 		buttonClear.setFont(commonFont);
400 		buttonClear.setBackground(commonColor);
401 		panelButton.add(buttonClear);
402 		
403 		// Le traitement des actions sur le bouton
404 		buttonClear.addActionListener(
405 		    new ActionListener() {
406 		        public void actionPerformed(ActionEvent event) {
407                     mfd2ScrollPane.removeAll();
408                     listRequests.setSize(0);
409                     
410                     createNewRequest();
411                 }
412             }
413         );
414 
415 		statusArea = new TextArea(5, 2);
416 		statusArea.setBounds(0,402,734,150);
417 		statusArea.setFont(new Font("Dialog", Font.PLAIN, 10));
418 		add("South", statusArea);
419 		
420 		selector = new Selector(this, currentRequest);
421 		selector.start();
422 	}
423 	
424 	public void createNewRequest() {
425         currentRequest = new PanelJomes();
426         mfd2ScrollPane.add(currentRequest);
427         
428         selector.setOwner(currentRequest);
429         
430         currentRequest.addPanelJomesListener(this);
431 
432         // On l'ajoute ? la liste des requÍtes
433         listRequests.addElement(currentRequest);
434         
435         // On associe les listeners potentiel de currentRequest
436         if (frameRequest != null)
437             currentRequest.addPanelJomesListener(frameRequest);
438             
439         if (frameResult != null)
440             currentRequest.addPanelJomesListener(frameResult);
441         
442 	    // Initialisation de la zone de saisie de la requÍte
443 	    entryRequest.requestFocus();
444 	    
445         // On envoie un ÈvÈnement comme quoi il faut les mettre ? jour
446 	    PanelJomesEvent panelJomesEvent = new PanelJomesEvent(currentRequest);
447 	    panelJomesEvent.setAction(PanelJomesEvent.UPDATE, null);
448 	    currentRequest.firePanelJomesEvent(panelJomesEvent);
449 	    
450 	    //currentRequest.setSelected(true);
451         // On envoie un ÈvÈnement comme quoi il faut mettre ? jour qui est sÈlectionnÈ
452 	    panelJomesEvent.setAction(PanelJomesEvent.UPDATE_SELECTION, null);
453 	    currentRequest.firePanelJomesEvent(panelJomesEvent);
454     }
455     
456 	public void setIsConstainingRequest(boolean isContainingRequest) {
457 	    this.isContainingRequest = isContainingRequest;
458 	}
459 	
460     /*******************************************************
461      *                                                    *
462      *  ImplÈmentation de l'interface PanelJomesListener  *
463      *                                                    *
464      ******************************************************/
465 
466     public void consumePanelJomesEvent(PanelJomesEvent panelJomesEvent) {
467         currentRequest = (PanelJomes) panelJomesEvent.getSource();
468         selector.setOwner(currentRequest);
469         
470         int action = panelJomesEvent.getAction();
471         switch (action) {
472             case PanelJomesEvent.UPDATE_REQUEST :
473             case PanelJomesEvent.UPDATE :
474                 if (updateEntryRequest) {
475                     entryRequest.setText(currentRequest.getLinearRequest());
476                     entryRequest.setCaretPosition(entryRequest.getText().length());
477                 }
478             case PanelJomesEvent.UPDATE_RESULT :
479                 validate();
480                 break;
481             case PanelJomesEvent.UPDATE_SELECTION :
482                 for (Enumeration e = listRequests.elements(); e.hasMoreElements(); )
483                     ((PanelJomes) e.nextElement()).setSelected(false);
484                     
485                 currentRequest.setSelected(true);
486         }
487     }
488     	
489 	public InputStream getInputStream() {
490 	    return inputStream;
491 	}
492 	
493 	public void setStatusMessage(String mesg) {
494 	    statusArea.append(mesg);
495 	}
496     
497     /***
498      * Setter method for the  object property.
499      * Wraps the object into an <CODE>CommEvent</CODE> and fires it off to the
500      * communication module(s)
501      * @param obj the " object" to be communicated
502      */
503     public void setObject(byte[] obj) {
504         try {
505         	outputStream.write(obj);
506         }
507         catch (IOException ioe) {
508             System.out.println("Can't write into the socket");
509             ioe.printStackTrace();
510         }
511     }
512     
513     public void closeStreams() {
514         try {
515             outputStream.close();
516             inputStream.close();
517         }
518         catch (IOException ioe) {
519             System.out.println("Can't close IO-streams");
520             ioe.printStackTrace();
521         }
522     }
523     
524     public Selector getSelector() {
525         return selector;
526     }
527     
528     public PanelJomes getCurrentRequest() {
529         return currentRequest;
530     }    
531 	
532 	// Les ActionListener pour les menus
533 
534     private class MenuLoadHandler implements ActionListener {
535         public void actionPerformed(ActionEvent e) {
536             String action = e.getActionCommand();
537             statusArea.append("> load " + action + "\n");
538             
539             String omObject = "<OMOBJ>\n  <OMA>\n    <OMS cd=\"mfd2\" name=\"load\"/>\n    <OMSTR>" + action + "</OMSTR>\n  </OMA>\n</OMOBJ>";
540             setObject(omObject.getBytes());
541         }
542     }
543     
544     private class MenuOpenMathHandler implements ActionListener {
545         public void actionPerformed(ActionEvent e) {
546             String action = e.getActionCommand();
547             int panelJomesAction;
548             
549             ShowOM frame;
550             
551             if (action.equals("Request")) {
552                 panelJomesAction = PanelJomesEvent.UPDATE_REQUEST;
553                 if (frameRequest != null)
554                     frame = frameRequest;
555                 else {
556                     frame = new ShowOM("Request");
557                     frameRequest = frame;
558             		frameContaining.addRequestContainingListener(frame);
559                 }
560             }
561             else {
562                 panelJomesAction = PanelJomesEvent.UPDATE_RESULT;
563                 if (frameResult != null)
564                     frame = frameResult;
565                 else {
566                     frame = new ShowOM("Result");
567                     frameResult = frame;
568             		frameContaining.addRequestContainingListener(frame);
569                 }
570             }
571             
572             
573             frame.show();
574             Component comps[] = mfd2ScrollPane.getAll();
575             int count = comps.length;
576             PanelJomes pj;
577             for (int i = 0; i < count; i++) {
578                 pj = (PanelJomes) comps[i];
579                 pj.removeAllPanelJomesListener();
580                 
581                 if (frameRequest != null)
582                     pj.addPanelJomesListener(frameRequest);
583                     
584                 if (frameResult != null)
585                     pj.addPanelJomesListener(frameResult);
586                     
587                 pj.addPanelJomesListener(PanelMfd2.this);
588             }
589             
590             // On envoie un ÈvÈnement comme quoi il faut les mettre ? jour
591     	    PanelJomesEvent panelJomesEvent = new PanelJomesEvent(currentRequest);
592     	    panelJomesEvent.setAction(panelJomesAction, null);
593     	    currentRequest.firePanelJomesEvent(panelJomesEvent);
594             
595         }
596     }
597 }