Docjar: A Java Source and Docuemnt Enginecom.*    java.*    javax.*    org.*    all    new    plug-in

Quick Search    Search Deep

Source code: jpicedt/ui/util/RunExternalCommand.java


1   /*  jPicEdt version 1.3.2, a picture editor for LaTeX.
2       Copyright (C) 1999-2002  Sylvain Reynal
3   
4       This program is free software; you can redistribute it and/or modify
5       it under the terms of the GNU General Public License as published by
6       the Free Software Foundation; either version 2 of the License, or
7       (at your option) any later version.
8   
9       This program is distributed in the hope that it will be useful,
10      but WITHOUT ANY WARRANTY; without even the implied warranty of
11      MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12      GNU General Public License for more details.
13  
14      You should have received a copy of the GNU General Public License
15      along with this program; if not, write to the Free Software
16      Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
17  
18      Sylvain Reynal
19      Département de Physique
20      Ecole Nationale Supérieure de l'Electronique et de ses Applications (ENSEA)
21      6, avenue du Ponceau
22      95014 CERGY CEDEX
23      FRANCE
24  
25      Tel : 00 +33 130 736 245
26      Fax : 00 +33 130 736 667
27      e-mail : reynal@ensea.fr
28      jPicEdt web page : http://www.jpicedt.org
29  */
30  
31  package jpicedt.ui.util;
32  
33  import jpicedt.*;
34  import jpicedt.graphic.io.formatter.*;
35  import jpicedt.graphic.toolkit.*;
36  import jpicedt.graphic.model.*;
37  import jpicedt.graphic.*;
38  
39  import java.io.*;
40  import java.util.*;
41  import java.awt.*;
42  import java.awt.event.*;
43  import javax.swing.*;
44  import javax.swing.border.*;
45  import java.awt.*;
46  
47  /**
48   * A class implementing methods for calling external processes like latex, (x)dvi, ghostscript...
49   * on the current picture file (e.g. the active internal frame)<p>
50   * <p>
51   * A "tmp" file is generated on-the-fly in the "tmp" directory of the underlying platform, 
52   * This tmp file contains an adequate preamble (e.g. usepackage{epic}) depending on current options, and
53   * LaTeX commands (or PsTricks or eepic commands) corresponding to each object found in the given picture.
54   *<p>
55   * These command lines may include the following special symbols :<br> 
56   * - {f} : tmp file name w/o extension (the user need to specify explicitely any extension required by the external program)<br>
57   * - {p} : tmp file path including trailing separator<br>
58   * - {i} : jPicEdt add-ons dir, that is : "jpicedt.home/add-ons" (trailing separtor excluded)
59   * <p>
60   * Ex : kghostview {p}{f}.ps or {i}run_latex.bat {p}{f}
61   * <p>
62   * Since we don't want to resort on platform dependent tricks (working dirs, PATH variables,
63   * root directory names differing on UNIX and Win32 systems, latex command line which might also differ, aso...),
64   * the better thing the user could do is to write one batch/shell script
65   * per process he wants to launch, then provide the names of these scripts to PicEdt.
66   * <p>
67   * Scripts are easy to write on UNIX/Window platforms,
68   * and very likely on MacOS platforms by using AppleScript.
69   *
70   * @author Sylvain Reynal
71   * @since PicEdt 1.2
72   */
73  public class RunExternalCommand extends Thread {
74  
75    /** static field defining an external commands, and also used by ActionDispatcher */
76    public final static String LATEX = "LaTeX";
77    /** static field defining an external commands, and also used by ActionDispatcher */
78    public final static String DVIVIEWER = "DVI";
79    /** static field defining an external commands, and also used by ActionDispatcher */
80    public final static String DVIPS = "Dvips";
81    /** static field defining an external commands, and also used by ActionDispatcher */
82    public final static String GHOSTVIEW = "Ghostview";
83    /** static field defining an external commands, and also used by ActionDispatcher */
84    public final static String USER1 = "UserProgram1";
85    /** static field defining an external commands, and also used by ActionDispatcher */
86    public final static String USER2 = "UserProgram2";
87  
88    /** key used to fetch command parameters from a Properties object */
89    public final static String KEY_LATEX = "command.latex";
90    /** key used to fetch command parameters from a Properties object */
91    public final static String KEY_DVIVIEWER = "command.dvi";
92    /** key used to fetch command parameters from a Properties object */
93    public final static String KEY_DVIPS = "command.dvips";
94    /** key used to fetch command parameters from a Properties object */
95    public final static String KEY_GHOSTVIEW = "command.ghostview";
96    /** key used to fetch command parameters from a Properties object */
97    public final static String KEY_USER1 = "command.user1";
98    /** key used to fetch command parameters from a Properties object */
99    public final static String KEY_USER2 = "command.user2";
100 
101   /** default commands parameters */
102   public static final String DEFAULT_LATEX_COMMAND = "";
103   /** default commands parameters */
104   public static final String DEFAULT_DVI_COMMAND = "";
105   /** default commands parameters */
106   public static final String DEFAULT_DVIPS_COMMAND = "";
107   /** default commands parameters */
108   public static final String DEFAULT_GS_COMMAND = "";
109   /** default commands parameters */
110   public static final String DEFAULT_USER1_COMMAND = "";
111   /** default commands parameters */
112   public static final String DEFAULT_USER2_COMMAND = "";
113 
114   ////////////////////////////////// PRIVATE FIELDS /////////////////////////////////
115 
116   private Drawing drawing;
117   private ContentType contentType;
118   private Process proc; // the process being executed (null if none)
119   private PrintStream printStream; // command's input stream (shared by inner classes)
120   private String commandToRun;   // command (should be one of the following static fields values)
121   private String commandLine; // command line created on-the-fly from the Properties and commandToRun
122   private static File tmpFile; // temp file created by the JVM the first time a command is run
123   private static String tmpPath; // path for tmp file (e.g. "/tmp/"), this is {%p}
124   private static String tmpFilePrefix; // file prefix, e.g. "jpicedt4875" (w/o extension)
125   private static String addonDir; // jPicEdt's add-ons directory, trailing "/" included
126 
127 
128   /////////////////////////////////// METHODS /////////////////////////////////////
129 
130   /**
131    * @param drawing The target document upon which the command will acts
132    * @param contentType the content-type used to format the document
133    * @param commandToRun one of the four predefined constant fields (LATEX, DVIVIEWER, DVIPS or GHOSTVIEW)
134    * @since jPicEdt 1.2
135    */
136   public RunExternalCommand(Drawing drawing, ContentType contentType,String commandToRun) {
137 
138     super("RunExtCom");
139     this.contentType = contentType;
140     this.drawing = drawing;
141     this.commandToRun = commandToRun;
142 
143     try {
144 
145       createTmpFile();
146 
147       // create command line :
148       if (commandToRun == LATEX){
149         // create "/tmp/jpicedt.tex" :
150         BufferedWriter bw = new BufferedWriter(new FileWriter(tmpFile));
151         bw.write(contentType.createFormatter().createFormatter(drawing,FormatterFactory.MAKE_STANDALONE_FILE).format());
152         bw.newLine();
153         bw.close();
154         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_LATEX,DEFAULT_LATEX_COMMAND));
155       }
156       else if (commandToRun == DVIVIEWER){
157         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_DVIVIEWER,DEFAULT_DVI_COMMAND));
158       }
159       else if (commandToRun == DVIPS){
160         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_DVIPS,DEFAULT_DVIPS_COMMAND));
161       }
162       else if (commandToRun == GHOSTVIEW){
163         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_GHOSTVIEW,DEFAULT_GS_COMMAND));
164       }
165       else if (commandToRun == USER1){
166         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_USER1,DEFAULT_USER1_COMMAND));
167       }
168       else if (commandToRun == USER2){
169         commandLine=buildCommandLine(JPicEdt.getProperty(KEY_USER2,DEFAULT_USER2_COMMAND));
170       }
171     }
172     catch(IOException ioEx){
173       JOptionPane.showMessageDialog(null,
174                                     Localizer.currentLocalizer().get("IOError") + " : " + ioEx.getMessage(),
175                                     Localizer.currentLocalizer().get("RunExternalCommand"),
176                                     JOptionPane.ERROR_MESSAGE);
177       commandLine = null;
178       // now command line is null, and run() takes care of that.
179     }
180 
181   }
182 
183   /**
184    * Build the real command line by replacing occurences of special symbols ({f}, {p},...)  in the
185    * given string by their actual value
186    *
187    * @param command command line with {f} and{p}, as specified by the user in the Preferences tabpane
188    * @return The real command line
189    * @since PicEdt 1.2
190    */
191   private String buildCommandLine(String command){
192 
193     StringTokenizer tokenizer = new StringTokenizer(command,"{}",true); // we don't remove spaces ; tokens are returned
194     String realCommand = new String();
195     String token;
196 
197     while (tokenizer.hasMoreTokens()){
198       token = tokenizer.nextToken();
199       if (token.equals("{")) {
200         token = tokenizer.nextToken(); // should be 'p' or 'f' or 'i'
201         if (token.equals("p")) {realCommand += tmpPath; continue;}
202         if (token.equals("f")) {realCommand += tmpFilePrefix; continue;}
203         if (token.equals("i")) {realCommand += getAddonDir(); continue;}
204         continue; // everything else get rejected
205       }
206       if (token.equals("}")) continue;
207       realCommand += token;
208     }
209     realCommand = realCommand.replace('/',File.separatorChar);
210     return realCommand;
211   }
212 
213   /**
214    * run an external process as a thread (overloading Thread.run() method)
215    * we then pipe the process std output to a JTextArea
216    *
217    * @since PicEdt 1.2
218    */
219   public void run() {
220 
221     if (commandLine == null) return;
222 
223     DlgBoxDisplayProcessIOStream dlgBox = new DlgBoxDisplayProcessIOStream();
224 
225     // run process
226     try{
227       proc = Runtime.getRuntime().exec(commandLine);
228     }
229     catch(IOException e){
230       dlgBox.append(e.toString());
231       //e.printStackTrace();
232       return;
233     }
234 
235     // fetch process's output stream (an input stream from the JVM's point of view) and plug a buffered reader input stream on it
236     BufferedReader  bufferedReader= new BufferedReader(new InputStreamReader(proc.getInputStream()));
237 
238     // fetch process's input stream (used by DlgBox)
239     printStream = new PrintStream(proc.getOutputStream(),true);
240 
241     // read output chars from command (we can't use readLine() since it blocks until it encounters a CR, which
242     // can be annoying in case the running process waits for an input, e.g. with a  "?" or "*" prompt as for LaTeX)
243     try{
244       int c;
245       while((c=bufferedReader.read()) != -1){
246         //System.out.print((char)c);
247         dlgBox.append(new Character((char)c).toString());
248       }
249       //System.out.println();
250     }
251     catch(IOException e){
252       dlgBox.append(e.toString());
253     }
254 
255     // wait for command to terminate
256     try {
257       proc.waitFor();
258     }
259     catch (InterruptedException e) {
260       dlgBox.append("\n"+Localizer.currentLocalizer().get("RunExtCmdProcessInterrupted"));
261     }
262 
263     // check its exit value
264 
265     if (proc.exitValue() != 0)
266       dlgBox.append("\n"+Localizer.currentLocalizer().get("RunExtCmdExitValueNonNil"));
267 
268     // close stream
269     try{
270       bufferedReader.close();
271     }
272     catch(IOException e){
273       dlgBox.append(e.toString());
274     }
275 
276     dlgBox.append("\njPicEdt : OK.");
277     dlgBox.dispose();
278 
279     return;
280   }
281 
282   /**
283    * Delete files created by JPicEdt or programms called by JPicEdt (LaTeX, dvips,...).
284    */
285   public static void cleanTmpDir(){
286     if (tmpPath==null) return; // ok, nothing dirty yet !
287     String[] list = new File(tmpPath).list(new FilenameFilter(){
288       public boolean accept(File dir, String name){
289         return name.startsWith(tmpFilePrefix);
290     }});
291     // delete them :
292     for (int i=0; i<list.length; i++){
293       //System.out.println("deleting " + new File(tmpPath,list[i]));
294       new File(tmpPath,list[i]).delete();
295     }
296     tmpFile = null; // force re-creation of tmp file on next call to constructor
297   }
298     
299   /**
300    * Return the add-ons directory w/o trailing "/"
301    */
302   public static String getAddonDir(){
303     if (addonDir==null) {
304       addonDir = MiscUtilities.getJPicEdtHome() + File.separator + "add-ons";
305       //System.out.println("addOnDir = " + addonDir);
306     }
307     return addonDir;
308   }
309 
310   /**
311     * Create a new tmp file if it doesn't exit yet
312    */
313   public static void createTmpFile() throws IOException {
314     if (tmpFile != null) return;
315     tmpFile = File.createTempFile("jpicedt",".tex", JPicEdt.getTmpDir());
316     tmpFile.deleteOnExit();
317     tmpPath = tmpFile.getParent() + File.separator; // "/tmp/"
318     String name =  tmpFile.getName(); // "jpicedt1432.tex"
319     tmpFilePrefix = name.substring(0,name.indexOf(".")); // "jpicedt1432"
320   }
321     
322   /**
323    * @return an AbstractCustomizer suited for editing Properties related to external commands
324    */
325   public static AbstractCustomizer createCustomizer(Properties preferences){
326     return new Customizer(preferences);
327   }
328 
329   /////////////////////////////////////////////////////////////////////////
330   /**
331    * An inner class implementing a JDialog to display external process
332    * inputStream and send keyboard events to process outputStream
333    */
334   public class DlgBoxDisplayProcessIOStream extends JDialog implements ActionListener,KeyListener, Runnable{
335 
336     /** panelStream contains an editable JTextArea and a JScrollPane */
337     JPanel panelStream = new JPanel();
338     JTextArea streamTA = new JTextArea(25,50);
339     JScrollPane scrollStream = new JScrollPane(streamTA);
340     StringBuffer areaBuffer = new StringBuffer(); // buffer for async. filling of streamTA
341 
342     /** panel containing the buttons */
343     JPanel panelButtons = new JPanel();;
344     JButton buttonKill = new JButton(Localizer.currentLocalizer().get("Kill"));
345 
346     /** buffer for typed chars (see KeyTyped) */
347     StringBuffer strBuf = new StringBuffer();
348     
349     boolean visible = false; // force show on first call to append
350 
351     /**
352      * @since PicEdt 1.2
353      */
354     DlgBoxDisplayProcessIOStream() {
355 
356       super();
357       this.setTitle(Localizer.currentLocalizer().get("Commands_boxtitle"));
358       this.setResizable(true);
359       this.setModal(false);
360       this.getContentPane().setLayout(new BorderLayout());
361       //this.setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
362       streamTA.setEditable(false);
363       panelStream.add(scrollStream);
364       panelStream.setBorder(BorderFactory.createEtchedBorder());
365       buttonKill.addActionListener(this);
366       panelButtons.add(buttonKill);
367       panelButtons.setBorder(BorderFactory.createEtchedBorder());
368       this.getContentPane().add(panelStream,BorderLayout.NORTH);
369       this.getContentPane().add(panelButtons,BorderLayout.SOUTH);
370       //Dimension dlgSize = this.getPreferredSize();
371       //this.setSize(getPreferredSize());
372       streamTA.requestFocus(); // so that entering command after a prompt doesn't need a mouse click on the JTextArea
373       streamTA.addKeyListener(this);
374     }
375 
376     /** append text ; thread safe */
377     public void append(String text){
378       areaBuffer.append(text);
379       SwingUtilities.invokeLater(new Thread(this)); 
380       
381     }
382     
383     /** handle asynchronous widgets updating */
384     public void run(){
385       if (!visible) {
386         this.pack();
387         this.setVisible(true);
388         visible=true;
389       }
390       streamTA.append(areaBuffer.toString());
391       //System.out.println(areaBuffer.toString());
392       areaBuffer = new StringBuffer();
393     }
394 
395     public void keyPressed(KeyEvent e){
396 
397       if (e.getKeyCode() == KeyEvent.VK_ENTER && printStream != null) {
398 
399         printStream.println(strBuf.toString()); // flush buffer, sending all typed keys + CR to external process
400         strBuf = new StringBuffer();
401         streamTA.append("\n");
402       }
403     }
404 
405     public void keyReleased(KeyEvent e){}
406 
407     public void keyTyped(KeyEvent e){
408 
409       strBuf.append(e.getKeyChar()); // accumulate types keys in buffer
410       streamTA.append(new Character(e.getKeyChar()).toString());
411 
412     }
413 
414     // called by KILL :
415     public void actionPerformed(ActionEvent e) {
416       proc.destroy();
417       dispose();
418     }
419 
420   } // inner class DlgBoxDisplayProcessIOStream
421 
422   ///////////////////////////////////////////////////////////////////////////
423 
424   /**
425    * A Customizer for the configuration of external commands preferences.
426    * @author Sylvain Reynal
427    * @since PicEdt 1.3
428    */
429   private static class Customizer extends AbstractCustomizer implements ActionListener {
430 
431     private JTextField latexCommandTF, dviviewerCommandTF, dvipsCommandTF, ghostviewCommandTF, user1CommandTF, user2CommandTF;
432     private Properties preferences;
433     private JButton loadConfigBT;
434 
435     /**
436      * Creates a new panel for the configuration of external commands
437      */
438     public Customizer(Properties preferences){
439 
440       this.preferences  = preferences;
441 
442       JPanel p;
443 
444       p = new JPanel(new GridLayout(7,2,5,5));
445       p.setBorder(BorderFactory.createTitledBorder(BorderFactory.createEtchedBorder(),Localizer.currentLocalizer().get("Commands")));
446 
447       p.add(new JLabel(" "+"LaTeX"+" :"));
448       latexCommandTF = new JTextField(20);
449       p.add(latexCommandTF);
450 
451       p.add(new JLabel(" "+Localizer.currentLocalizer().get("DviViewer")+" :"));
452       dviviewerCommandTF = new JTextField(20);
453       p.add(dviviewerCommandTF);
454 
455       p.add(new JLabel(" "+"Dvips"+" :"));
456       dvipsCommandTF = new JTextField(20);
457       p.add(dvipsCommandTF);
458 
459       p.add(new JLabel(" "+"Ghostview"+" :"));
460       ghostviewCommandTF = new JTextField(20);
461       p.add(ghostviewCommandTF);
462 
463       p.add(new JLabel(" "+Localizer.currentLocalizer().get("UserProgram") + " 1 :"));
464       user1CommandTF = new JTextField(20);
465       p.add(user1CommandTF);
466 
467       p.add(new JLabel(" "+Localizer.currentLocalizer().get("UserProgram") + " 2 :"));
468       user2CommandTF = new JTextField(20);
469       p.add(user2CommandTF);
470 
471       p.add(new JLabel(" "+Localizer.currentLocalizer().get("LoadPredefinedConfig")));
472       loadConfigBT = new JButton(Localizer.currentLocalizer().get("Load"));
473       loadConfigBT.addActionListener(this);
474       p.add(loadConfigBT);
475       
476       add(p,BorderLayout.NORTH);
477       
478       // reminder for {f}, {p}, ... shortcuts :
479       Box helpPanel = new Box(BoxLayout.Y_AXIS);
480       //helpPanel.add(new JLabel(" "+Localizer.currentLocalizer().get("Commands_helpstring")));
481       try {createTmpFile();} // security to avoid "null" !
482       catch (IOException ex){}
483       helpPanel.add(new JLabel("Tmp. dir : "));
484       helpPanel.add(new JLabel(" {p} -> \"" + tmpPath + "\""));
485       helpPanel.add(new JLabel("Tmp. TeX file : "));
486       helpPanel.add(new JLabel(" {f} -> \"" + tmpFilePrefix + "\""));
487       helpPanel.add(new JLabel("Add-ons dir. : "));
488       helpPanel.add(new JLabel(" {i} -> \"" + getAddonDir() + "\""));
489       JPanel borderingPanel = new JPanel();
490       borderingPanel.setBorder(BorderFactory.createTitledBorder(BorderFactory.createEtchedBorder(),Localizer.currentLocalizer().get("Help")));
491       borderingPanel.add(helpPanel);
492       add(borderingPanel, BorderLayout.CENTER);
493     }
494 
495     /**
496     * @return the panel title, used e.g. for Border or Tabpane title. 
497     * @since jPicEdt 1.3.2
498     * @author Sylvain Reynal
499     */
500     public String getTitle(){
501       return Localizer.currentLocalizer().get("Commands");
502     }
503 
504 
505     /**
506      * @return the Icon associated with this panel, used e.g. for TabbedPane decoration 
507      * @since jPicEdt 1.3.2
508      * @author Sylvain Reynal
509      */
510     public Icon getIcon(){
511       return null;
512     }
513 
514 
515     /**
516      * @return the tooltip string associated with this panel 
517      * @since jPicEdt 1.3.2
518      * @author Sylvain Reynal
519      */
520     public String getTooltip(){
521       return Localizer.currentLocalizer().get("Commands.tooltip");
522     }
523 
524     /**
525      * Load widgets display content with a default value retrieved from the Properties object
526      * @since jPicEdt 1.3.2
527      * @author Sylvain Reynal
528      */
529     public void loadDefault() {
530       latexCommandTF.setText(DEFAULT_LATEX_COMMAND);
531       dviviewerCommandTF.setText(DEFAULT_DVI_COMMAND);
532       dvipsCommandTF.setText(DEFAULT_DVIPS_COMMAND);
533       ghostviewCommandTF.setText(DEFAULT_GS_COMMAND);
534       user1CommandTF.setText(DEFAULT_USER1_COMMAND);
535       user2CommandTF.setText(DEFAULT_USER2_COMMAND);
536     }
537 
538     /**
539      * Load widgets value from the Properties object given in the constructor
540      * @since jPicEdt 1.3.2
541      * @author Sylvain Reynal
542      */
543     private void load(Properties pref) {
544       latexCommandTF.setText(pref.getProperty(KEY_LATEX,DEFAULT_LATEX_COMMAND));
545       dviviewerCommandTF.setText(pref.getProperty(KEY_DVIVIEWER,DEFAULT_DVI_COMMAND));
546       dvipsCommandTF.setText(pref.getProperty(KEY_DVIPS,DEFAULT_DVIPS_COMMAND));
547       ghostviewCommandTF.setText(pref.getProperty(KEY_GHOSTVIEW,DEFAULT_GS_COMMAND));
548       user1CommandTF.setText(pref.getProperty(KEY_USER1,DEFAULT_USER1_COMMAND));
549       user2CommandTF.setText(pref.getProperty(KEY_USER2,DEFAULT_USER2_COMMAND));
550     }
551 
552     public void load(){
553       load(JPicEdt.getPreferences());
554     }
555     
556     /**
557      * ActionHandler for "loadConfigBT"
558      */
559     public void actionPerformed(ActionEvent e){
560       JFileChooser fileChooser = new JFileChooser(getAddonDir());
561       fileChooser.setDialogTitle(Localizer.currentLocalizer().get("LoadPredefinedConfig"));
562       fileChooser.setFileFilter(new javax.swing.filechooser.FileFilter(){
563         public boolean accept(File f){return f.isDirectory() || f.getPath().endsWith(".properties");}
564         public String getDescription(){return "External scripts configuration files";}
565       });
566       if (fileChooser.showOpenDialog(null) == JFileChooser.CANCEL_OPTION) return;
567       File file =  fileChooser.getSelectedFile();
568       if (file!= null) {
569         Properties prop = new Properties();
570         try {
571           InputStream is = new BufferedInputStream(new FileInputStream(file));
572           prop.load(is);
573           //prop.list(System.out);
574           load(prop);
575           is.close();
576         }
577         catch (IOException ioEx){
578           JOptionPane.showMessageDialog(
579             JOptionPane.getRootFrame(),
580             Localizer.currentLocalizer().get("IOError") + "\n" + ioEx.getMessage(),
581             Localizer.currentLocalizer().get("LoadPredefinedConfig"),
582             JOptionPane.ERROR_MESSAGE);
583         }
584       }
585     }
586 
587     /**
588      * Store current widgets value to the Properties object given in the constructor
589      * @since jPicEdt 1.3.2
590      * @author Sylvain Reynal
591      */
592     public void store(){
593       preferences.setProperty(KEY_LATEX,latexCommandTF.getText());
594       preferences.setProperty(KEY_DVIVIEWER,dviviewerCommandTF.getText());
595       preferences.setProperty(KEY_DVIPS,dvipsCommandTF.getText());
596       preferences.setProperty(KEY_GHOSTVIEW,ghostviewCommandTF.getText());
597       preferences.setProperty(KEY_USER1,user1CommandTF.getText());
598       preferences.setProperty(KEY_USER2,user2CommandTF.getText());
599     }
600 
601 
602   } // PanelExternalCommand
603 
604 
605 } // RunExternalCommand