1
2
3
4
5
6 package net.kwfgrid.gwui.gui;
7
8 import net.kwfgrid.gworkflowdl.protocol.structure.ProtocolWorkflow;
9 import net.kwfgrid.gworkflowdl.protocol.structure.ProtocolPlace;
10
11 import org.glassbox.executor.Executor;
12
13 import java.awt.BorderLayout;
14 import javax.swing.*;
15
16 public class PlaceInspectorFrame extends JFrame {
17 PlaceTokenEditor _tokeneditor;
18 PlacePropertiesEditor _propertieseditor;
19 PlaceDescriptionEditor _descriptioneditor;
20 PlaceIDView _idview;
21 PlaceTokenClassEditor _tokenclasseditor;
22 WorkflowElementEditorContainer _view;
23 boolean _editable;
24 ProtocolWorkflow _workflow;
25 Executor _executor;
26
27 public PlaceInspectorFrame(ProtocolWorkflow workflow, Executor executor) {
28 super("Place Inspector");
29 _workflow = workflow;
30 _executor = executor;
31 getContentPane().setLayout(new BorderLayout());
32 _view = null;
33 _idview = null;
34 _tokeneditor = null;
35 _tokenclasseditor = null;
36 _propertieseditor = null;
37 _descriptioneditor = null;
38 _editable = true;
39 }
40
41 public void setEnabled(boolean enabled) {
42 super.setEnabled(enabled);
43 if (_view!=null) _view.setEnabled(enabled);
44 }
45
46 public void setEditable(boolean editable) {
47 _editable = editable;
48 if (_view!=null) _view.setEditable(editable);
49 }
50
51 public void setPlace(ProtocolPlace place) {
52 if (_view!=null) {
53 _view.dispose();
54 getContentPane().removeAll();
55 getContentPane().invalidate();
56 }
57 if (place!=null) {
58 _idview = new PlaceIDView(_workflow, place);
59 _tokenclasseditor = new PlaceTokenClassEditor(_executor,
60 _workflow,
61 place);
62 _tokeneditor = new PlaceTokenEditor(_executor,
63 _workflow,
64 place);
65 _propertieseditor = new PlacePropertiesEditor(_executor,
66 _workflow,
67 place);
68 _descriptioneditor = new PlaceDescriptionEditor(_executor,
69 _workflow,
70 place);
71 _view = new WorkflowElementEditorContainer(_workflow,
72 place,
73 new AbstractWorkflowElementView[] { _idview,
74 _descriptioneditor,
75 _propertieseditor,
76 _tokenclasseditor,
77 _tokeneditor },
78 new double[] { 0.0, 0.5, 0.0, 0.0, 0.5 });
79 JScrollPane pane = new JScrollPane(_view.getView());
80 pane.setBorder(null);
81 getContentPane().add(pane, BorderLayout.CENTER);
82 getContentPane().setSize(getContentPane().getLayout().preferredLayoutSize(getContentPane()));
83 getContentPane().validate();
84 _view.setEnabled(isEnabled());
85 _view.setEditable(_editable);
86 pack();
87 show();
88 } else {
89 _view = null;
90 _tokeneditor = null;
91 _tokenclasseditor = null;
92 _propertieseditor = null;
93 _descriptioneditor = null;
94 _idview = null;
95 hide();
96 }
97 }
98 }