Java API By Example, From Geeks To Geeks.

1 /* 2  * jEdit.java - Main class of the jEdit editor 3  * :tabSize=8:indentSize=8:noTabs=false: 4  * :folding=explicit:collapseFolds=1: 5  * 6  * Copyright (C) 1998, 2005 Slava Pestov 7  * 8  * This program is free software; you can redistribute it and/or 9  * modify it under the terms of the GNU General Public License 10  * as published by the Free Software Foundation; either version 2 11  * of the License, or any later version. 12  * This program is distributed in the hope that it will be useful, 13  * but WITHOUT ANY WARRANTY; without even the implied warranty of 14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 15  * GNU General Public License for more details. 16  * 17  * You should have received a copy of the GNU General Public License 18  * along with this program; if not, write to the Free Software 19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. 20  */ 21 22 package org.gjt.sp.jedit; 23 24 //{{{ Imports 25 import bsh.UtilEvalError; 26 import javax.swing.*; 27 import java.awt.event.KeyEvent ; 28 import java.awt.*; 29 import java.io.*; 30 import java.net.*; 31 import java.text.MessageFormat ; 32 import java.util.*; 33 import java.util.List ; 34 35 import org.xml.sax.XMLReader ; 36 import org.xml.sax.InputSource ; 37 import org.xml.sax.SAXException ; 38 import org.xml.sax.SAXParseException ; 39 import org.xml.sax.helpers.XMLReaderFactory ; 40 41 import org.gjt.sp.jedit.bufferio.BufferIORequest; 42 import org.gjt.sp.jedit.bufferio.JEditKillRing; 43 import org.gjt.sp.jedit.buffer.KillRing; 44 import org.gjt.sp.jedit.buffer.JEditBuffer; 45 import org.gjt.sp.jedit.msg.*; 46 import org.gjt.sp.jedit.gui.*; 47 import org.gjt.sp.jedit.help.HelpViewer; 48 import org.gjt.sp.jedit.io.*; 49 import org.gjt.sp.jedit.pluginmgr.PluginManager; 50 import org.gjt.sp.jedit.search.SearchAndReplace; 51 import org.gjt.sp.jedit.syntax.*; 52 import org.gjt.sp.jedit.textarea.*; 53 import org.gjt.sp.util.Log; 54 import org.gjt.sp.util.StandardUtilities; 55 import org.gjt.sp.util.XMLUtilities; 56 import org.gjt.sp.util.IOUtilities; 57 //}}} 58 59 /** 60  * The main class of the jEdit text editor. 61  * @author Slava Pestov 62  * @version $Id: jEdit.java 8291 2007-01-01 22:19:04Z olearyni $ 63  */ 64 public class jEdit 65 { 66     //{{{ getVersion() method 67 /** 68      * Returns the jEdit version as a human-readable string. 69      */ 70     public static String getVersion() 71     { 72         return MiscUtilities.buildToVersion(getBuild()); 73     } //}}} 74 75     //{{{ getBuild() method 76 /** 77      * Returns the internal version. MiscUtilities.compareStrings() can be used 78      * to compare different internal versions. 79      */ 80     public static String getBuild() 81     { 82         // (major).(minor).(<99 = preX, 99 = final).(bug fix) 83 return "04.03.09.00"; 84     } //}}} 85 86     //{{{ main() method 87 /** 88      * The main method of the jEdit application. 89      * This should never be invoked directly. 90      * @param args The command line arguments 91      */ 92     public static void main(String [] args) 93     { 94         //{{{ Check for Java 1.5 or later 95 String javaVersion = System.getProperty("java.version"); 96         if(javaVersion.compareTo("1.5") < 0) 97         { 98             System.err.println("You are running Java version " 99                 + javaVersion + '.'); 100             System.err.println("jEdit requires Java 1.5 or later."); 101             System.exit(1); 102         } //}}} 103 104         // later on we need to know if certain code is called from 105 // the main thread 106 mainThread = Thread.currentThread(); 107 108         settingsDirectory = ".jedit"; 109 110         // MacOS users expect the app to keep running after all windows 111 // are closed 112 background = OperatingSystem.isMacOS(); 113 114         //{{{ Parse command line 115 boolean endOpts = false; 116         int level = Log.WARNING; 117         String portFile = "server"; 118         boolean restore = true; 119         boolean newView = true; 120         boolean newPlainView = false; 121         boolean gui = true; // open initial view? 122 boolean loadPlugins = true; 123         boolean runStartupScripts = true; 124         boolean quit = false; 125         boolean wait = false; 126         String userDir = System.getProperty("user.dir"); 127 128         // script to run 129 String scriptFile = null; 130 131         for(int i = 0; i < args.length; i++) 132         { 133             String arg = args[i]; 134             if(arg == null) 135                 continue; 136             else if(arg.length() == 0) 137                 args[i] = null; 138             else if(arg.startsWith("-") && !endOpts) 139             { 140                 if(arg.equals("--")) 141                     endOpts = true; 142                 else if(arg.equals("-usage")) 143                 { 144                     version(); 145                     System.err.println(); 146                     usage(); 147                     System.exit(1); 148                 } 149                 else if(arg.equals("-version")) 150                 { 151                     version(); 152                     System.exit(1); 153                 } 154                 else if(arg.startsWith("-log=")) 155                 { 156                     try 157                     { 158                         level = Integer.parseInt(arg.substring("-log=".length())); 159                     } 160                     catch(NumberFormatException nf) 161                     { 162                         System.err.println("Malformed option: " + arg); 163                     } 164                 } 165                 else if(arg.equals("-nosettings")) 166                     settingsDirectory = null; 167                 else if(arg.startsWith("-settings=")) 168                     settingsDirectory = arg.substring(10); 169                 else if(arg.startsWith("-noserver")) 170                     portFile = null; 171                 else if(arg.equals("-server")) 172                     portFile = "server"; 173                 else if(arg.startsWith("-server=")) 174                     portFile = arg.substring(8); 175                 else if(arg.startsWith("-background")) 176                     background = true; 177                 else if(arg.startsWith("-nobackground")) 178                     background = false; 179                 else if(arg.equals("-gui")) 180                     gui = true; 181                 else if(arg.equals("-nogui")) 182                     gui = false; 183                 else if(arg.equals("-newview")) 184                     newView = true; 185                 else if(arg.equals("-newplainview")) 186                     newPlainView = true; 187                 else if(arg.equals("-reuseview")) 188                     newPlainView = newView = false; 189                 else if(arg.equals("-restore")) 190                     restore = true; 191                 else if(arg.equals("-norestore")) 192                     restore = false; 193                 else if(arg.equals("-plugins")) 194                     loadPlugins = true; 195                 else if(arg.equals("-noplugins")) 196                     loadPlugins = false; 197                 else if(arg.equals("-startupscripts")) 198                     runStartupScripts = true; 199                 else if(arg.equals("-nostartupscripts")) 200                     runStartupScripts = false; 201                 else if(arg.startsWith("-run=")) 202                     scriptFile = arg.substring(5); 203                 else if(arg.equals("-wait")) 204                     wait = true; 205                 else if(arg.equals("-quit")) 206                     quit = true; 207                 else 208                 { 209                     System.err.println("Unknown option: " 210                         + arg); 211                     usage(); 212                     System.exit(1); 213                 } 214                 args[i] = null; 215             } 216         } //}}} 217 218         //{{{ We need these initializations very early on 219 if(settingsDirectory != null) 220         { 221             settingsDirectory = MiscUtilities.constructPath( 222                 System.getProperty("user.home"), 223                 settingsDirectory); 224             settingsDirectory = MiscUtilities.resolveSymlinks( 225                 settingsDirectory); 226         } 227 228         if(settingsDirectory != null && portFile != null) 229             portFile = MiscUtilities.constructPath(settingsDirectory,portFile); 230         else 231             portFile = null; 232 233         Log.init(true,level); 234         //}}} 235 236         //{{{ Try connecting to another running jEdit instance 237 if(portFile != null && new File(portFile).exists()) 238         { 239             try 240             { 241                 BufferedReader in = new BufferedReader(new FileReader(portFile)); 242                 String check = in.readLine(); 243                 if(!check.equals("b")) 244                     throw new Exception ("Wrong port file format"); 245 246                 int port = Integer.parseInt(in.readLine()); 247                 int key = Integer.parseInt(in.readLine()); 248 249                 Socket socket = new Socket(InetAddress.getByName("127.0.0.1"),port); 250                 DataOutputStream out = new DataOutputStream( 251                     socket.getOutputStream()); 252                 out.writeInt(key); 253 254                 String script; 255                 if(quit) 256                 { 257                     script = "socket.close();\n" 258                         + "jEdit.exit(null,true);\n"; 259                 } 260                 else 261                 { 262                     script = makeServerScript(wait,restore, 263                         newView,newPlainView,args, 264                         scriptFile); 265                 } 266 267                 out.writeUTF(script); 268 269                 Log.log(Log.DEBUG,jEdit.class,"Waiting for server"); 270                 // block until its closed 271 try 272                 { 273                     socket.getInputStream().read(); 274                 } 275                 catch(Exception e) 276                 { 277                 } 278 279                 in.close(); 280                 out.close(); 281 282                 System.exit(0); 283             } 284             catch(Exception e) 285             { 286                 // ok, this one seems to confuse newbies 287 // endlessly, so log it as NOTICE, not 288 // ERROR 289 Log.log(Log.NOTICE,jEdit.class,"An error occurred" 290                     + " while connecting to the jEdit server instance."); 291                 Log.log(Log.NOTICE,jEdit.class,"This probably means that" 292                     + " jEdit crashed and/or exited abnormally"); 293                 Log.log(Log.NOTICE,jEdit.class,"the last time it was run."); 294                 Log.log(Log.NOTICE,jEdit.class,"If you don't" 295                     + " know what this means, don't worry."); 296                 Log.log(Log.NOTICE,jEdit.class,e); 297             } 298         } 299 300         if(quit) 301         { 302             // if no server running and user runs jedit -quit, 303 // just exit 304 System.exit(0); 305         } //}}} 306 307         // don't show splash screen if there is a file named 308 // 'nosplash' in the settings directory 309 if(!new File(settingsDirectory,"nosplash").exists()) 310             GUIUtilities.showSplashScreen(); 311 312         //{{{ Initialize settings directory 313 Writer stream; 314         if(settingsDirectory != null) 315         { 316             File _settingsDirectory = new File(settingsDirectory); 317             if(!_settingsDirectory.exists()) 318                 _settingsDirectory.mkdirs(); 319             File _macrosDirectory = new File(settingsDirectory,"macros"); 320             if(!_macrosDirectory.exists()) 321                 _macrosDirectory.mkdir(); 322 323             String logPath = MiscUtilities.constructPath( 324                 settingsDirectory,"activity.log"); 325 326             backupSettingsFile(new File(logPath)); 327 328             try 329             { 330                 stream = new BufferedWriter(new FileWriter(logPath)); 331 332                 // Write a warning message: 333 String lineSep = System.getProperty("line.separator"); 334                 stream.write("Log file created on " + new Date()); 335                 stream.write(lineSep); 336                 stream.write("IMPORTANT:"); 337                 stream.write(lineSep); 338                 stream.write("Because updating this file after " 339                     + "every log message would kill"); 340                 stream.write(lineSep); 341                 stream.write("performance, it will be *incomplete* " 342                     + "unless you invoke the"); 343                 stream.write(lineSep); 344                 stream.write("Utilities->Troubleshooting->Update " 345                     + "Activity Log on Disk command!"); 346                 stream.write(lineSep); 347             } 348             catch(Exception e) 349             { 350                 e.printStackTrace(); 351                 stream = null; 352             } 353         } 354         else 355         { 356             stream = null; 357         } //}}} 358 359         Log.setLogWriter(stream); 360 361         Log.log(Log.NOTICE,jEdit.class,"jEdit version " + getVersion()); 362         Log.log(Log.MESSAGE,jEdit.class,"Settings directory is " 363             + settingsDirectory); 364 365         //{{{ Get things rolling 366 GUIUtilities.advanceSplashProgress("init"); 367         initMisc(); 368         GUIUtilities.advanceSplashProgress("init system properties"); 369         initSystemProperties(); 370 371         GUIUtilities.advanceSplashProgress("init GUI"); 372         GUIUtilities.init(); 373         GUIUtilities.advanceSplashProgress("init beanshell"); 374         BeanShell.init(); 375 376         GUIUtilities.advanceSplashProgress("loading site properties"); 377         if(jEditHome != null) 378             initSiteProperties(); 379 380         GUIUtilities.advanceSplashProgress("loading user properties"); 381         initUserProperties(); 382         Options.SIMPLIFIED_KEY_HANDLING = jEdit.getBooleanProperty("newkeyhandling"); 383         //}}} 384 385         //{{{ Initialize server 386 if(portFile != null) 387         { 388             GUIUtilities.advanceSplashProgress("init server"); 389             server = new EditServer(portFile); 390             if(!server.isOK()) 391                 server = null; 392         } 393         else 394         { 395             GUIUtilities.advanceSplashProgress(); 396             if(background) 397             { 398                 background = false; 399                 Log.log(Log.WARNING,jEdit.class,"You cannot specify both the" 400                     + " -background and -noserver switches"); 401             } 402         } //}}} 403 404         //{{{ Do more stuff 405 GUIUtilities.advanceSplashProgress("init look and feel"); 406         initPLAF(); 407         GUIUtilities.advanceSplashProgress("init VFS Manager"); 408         VFSManager.init(); 409         GUIUtilities.advanceSplashProgress("init resources"); 410         initResources(); 411         SearchAndReplace.load(); 412 413 414 415         if(loadPlugins) 416         { 417             GUIUtilities.advanceSplashProgress("init plugins"); 418             initPlugins(); 419         } 420         else 421             GUIUtilities.advanceSplashProgress(); 422 423         Registers.setSaver(new JEditRegisterSaver()); 424         Registers.setListener(new JEditRegistersListener()); 425         GUIUtilities.advanceSplashProgress("init history model"); 426         HistoryModel.setSaver(new JEditHistoryModelSaver()); 427         HistoryModel.loadHistory(); 428         GUIUtilities.advanceSplashProgress("init buffer history"); 429         BufferHistory.load(); 430         GUIUtilities.advanceSplashProgress("init killring"); 431         KillRing.setInstance(new JEditKillRing()); 432         KillRing.getInstance().load(); 433         GUIUtilities.advanceSplashProgress("init various properties"); 434         propertiesChanged(); 435 436         GUIUtilities.advanceSplashProgress("init modes"); 437 438         // Buffer sort 439 sortBuffers = getBooleanProperty("sortBuffers"); 440         sortByName = getBooleanProperty("sortByName"); 441 442         reloadModes(); 443 444         GUIUtilities.advanceSplashProgress("activate plugins"); 445         //}}} 446 447         //{{{ Activate plugins that must be activated at startup 448 for(int i = 0; i < jars.size(); i++) 449         { 450             jars.elementAt(i).activatePluginIfNecessary(); 451         } //}}} 452 453         //{{{ Load macros and run startup scripts, after plugins and settings are loaded 454 GUIUtilities.advanceSplashProgress("init macros"); 455         Macros.loadMacros(); 456         Macros.getMacroActionSet().initKeyBindings(); 457 458         if(runStartupScripts && jEditHome != null) 459         { 460             String path = MiscUtilities.constructPath(jEditHome,"startup"); 461             File file = new File(path); 462             if(file.exists()) 463             { 464                 runStartupScripts(file); 465             } 466             else 467                 GUIUtilities.advanceSplashProgress(); 468         } 469         else 470             GUIUtilities.advanceSplashProgress("run startup scripts"); 471 472         if(runStartupScripts && settingsDirectory != null) 473         { 474             String path = MiscUtilities.constructPath(settingsDirectory,"startup"); 475             File file = new File(path); 476             if (file.exists()) 477             { 478                 GUIUtilities.advanceSplashProgress("run startup scripts"); 479                 runStartupScripts(file); 480             } 481             else 482             { 483                 GUIUtilities.advanceSplashProgress(); 484                 file.mkdirs(); 485             } 486         } 487         else 488         { 489             GUIUtilities.advanceSplashProgress(); 490         } //}}} 491 492         //{{{ Run script specified with -run= parameter 493 if(scriptFile != null) 494         { 495             GUIUtilities.advanceSplashProgress("run script file"); 496             scriptFile = MiscUtilities.constructPath(userDir,scriptFile); 497             try 498             { 499                 BeanShell.getNameSpace().setVariable("args",args); 500             } 501             catch(UtilEvalError e) 502             { 503                 Log.log(Log.ERROR,jEdit.class,e); 504             } 505             BeanShell.runScript(null,scriptFile,null,false); 506         } 507         else 508         { 509             GUIUtilities.advanceSplashProgress(); 510         } 511         //}}} 512 513         GUIUtilities.advanceSplashProgress(); 514 515         // Open files, create the view and hide the splash screen. 516 finishStartup(gui,restore,userDir,args); 517     } //}}} 518 519     //{{{ Property methods 520 521     //{{{ getProperties() method 522 /** 523      * Returns the properties object which contains all known 524      * jEdit properties. Note that as of jEdit 4.2pre10, this returns a 525      * new collection, not the existing properties instance. 526      * @since jEdit 3.1pre4 527      */ 528     public static final Properties getProperties() 529     { 530         return propMgr.getProperties(); 531     } //}}} 532 533     //{{{ getProperty() method 534 /** 535      * Fetches a property, returning null if it's not defined. 536      * @param name The property 537      */ 538     public static final String getProperty(String name) 539     { 540         return propMgr.getProperty(name); 541     } //}}} 542 543     //{{{ getProperty() method 544 /** 545      * Fetches a property, returning the default value if it's not 546      * defined. 547      * @param name The property 548      * @param def The default value 549      */ 550     public static final String getProperty(String name, String def) 551     { 552         String value = propMgr.getProperty(name); 553         if(value == null) 554             return def; 555         else 556             return value; 557     } //}}} 558 559     //{{{ getProperty() method 560 /** 561      * Returns the property with the specified name.<p> 562      * 563      * The elements of the <code>args</code> array are substituted 564      * into the value of the property in place of strings of the 565      * form <code>{<i>n</i>}</code>, where <code><i>n</i></code> is an index 566      * in the array.<p> 567      * 568      * You can find out more about this feature by reading the 569      * documentation for the <code>format</code> method of the 570      * <code>java.text.MessageFormat</code> class. 571      * 572      * @param name The property 573      * @param args The positional parameters 574      */ 575     public static final String getProperty(String name, Object [] args) 576     { 577         if(name == null) 578             return null; 579         if(args == null) 580             return getProperty(name); 581         else 582         { 583             String value = getProperty(name); 584             if(value == null) 585                 return null; 586             else 587                 return MessageFormat.format(value,args); 588         } 589     } //}}} 590 591     //{{{ getBooleanProperty() method 592 /** 593      * Returns the value of a boolean property. 594      * @param name The property 595      */ 596     public static final boolean getBooleanProperty(String name) 597     { 598         return getBooleanProperty(name,false); 599     } //}}} 600 601     //{{{ getBooleanProperty() method 602 /** 603      * Returns the value of a boolean property. 604      * @param name The property 605      * @param def The default value 606      */ 607     public static final boolean getBooleanProperty(String name, boolean def) 608     { 609         String value = getProperty(name); 610         if(value == null) 611             return def; 612         else if(value.equals("true") || value.equals("yes") 613             || value.equals("on")) 614             return true; 615         else if(value.equals("false") || value.equals("no") 616             || value.equals("off")) 617             return false; 618         else 619             return def; 620     } //}}} 621 622     //{{{ getIntegerProperty() method 623 /** 624      * Returns the value of an integer property. 625      * @param name The property 626      * @param def The default value 627      * @since jEdit 4.0pre1 628      */ 629     public static final int getIntegerProperty(String name, int def) 630     { 631         String value = getProperty(name); 632         if(value == null) 633             return def; 634         else 635         { 636             try 637             { 638                 return Integer.parseInt(value.trim()); 639             } 640             catch(NumberFormatException nf) 641             { 642                 return def; 643             } 644         } 645     } //}}} 646 647     //{{{ getDoubleProperty() method 648 public static double getDoubleProperty(String name, double def) 649     { 650         String value = getProperty(name); 651         if(value == null) 652             return def; 653         else 654         { 655             try 656             { 657                 return Double.parseDouble(value.trim()); 658             } 659             catch(NumberFormatException nf) 660             { 661                 return def; 662             } 663         } 664     } 665     //}}} 666 667     //{{{ getFontProperty() method 668 /** 669      * Returns the value of a font property. The family is stored 670      * in the <code><i>name</i></code> property, the font size is stored 671      * in the <code><i>name</i>size</code> property, and the font style is 672      * stored in <code><i>name</i>style</code>. For example, if 673      * <code><i>name</i></code> is <code>view.gutter.font</code>, the 674      * properties will be named <code>view.gutter.font</code>, 675      * <code>view.gutter.fontsize</code>, and 676      * <code>view.gutter.fontstyle</code>. 677      * 678      * @param name The property 679      * @since jEdit 4.0pre1 680      */ 681     public static final Font getFontProperty(String name) 682     { 683         return getFontProperty(name,null); 684     } //}}} 685 686     //{{{ getFontProperty() method 687 /** 688      * Returns the value of a font property. The family is stored 689      * in the <code><i>name</i></code> property, the font size is stored 690      * in the <code><i>name</i>size</code> property, and the font style is 691      * stored in <code><i>name</i>style</code>. For example, if 692      * <code><i>name</i></code> is <code>view.gutter.font</code>, the 693      * properties will be named <code>view.gutter.font</code>, 694      * <code>view.gutter.fontsize</code>, and 695      * <code>view.gutter.fontstyle</code>. 696      * 697      * @param name The property 698      * @param def The default value 699      * @since jEdit 4.0pre1 700      */ 701     public static final Font getFontProperty(String name, Font def) 702     { 703         String family = getProperty(name); 704         String sizeString = getProperty(name + "size"); 705         String styleString = getProperty(name + "style"); 706 707         if(family == null || sizeString == null || styleString == null) 708             return def; 709         else 710         { 711             int size, style; 712 713             try 714             { 715                 size = Integer.parseInt(sizeString); 716             } 717             catch(NumberFormatException nf) 718             { 719                 return def; 720             } 721 722             try 723             { 724                 style = Integer.parseInt(styleString); 725             } 726             catch(NumberFormatException nf) 727             { 728                 return def; 729             } 730 731             return new Font(family,style,size); 732         } 733     } //}}} 734 735     //{{{ getColorProperty() method 736 /** 737      * Returns the value of a color property. 738      * @param name The property name 739      * @since jEdit 4.0pre1 740      */ 741     public static Color getColorProperty(String name) 742     { 743         return getColorProperty(name,Color.black); 744     } //}}} 745 746     //{{{ getColorProperty() method 747 /** 748      * Returns the value of a color property. 749      * @param name The property name 750      * @param def The default value 751      * @since jEdit 4.0pre1 752      */ 753     public static Color getColorProperty(String name, Color def) 754     { 755         String value = getProperty(name); 756         if(value == null) 757             return def; 758         else 759             return GUIUtilities.parseColor(value,def); 760     } //}}} 761 762     //{{{ setColorProperty() method 763 /** 764      * Sets the value of a color property. 765      * @param name The property name 766      * @param value The value 767      * @since jEdit 4.0pre1 768      */ 769     public static void setColorProperty(String name, Color value) 770     { 771         setProperty(name,GUIUtilities.getColorHexString(value)); 772     } //}}} 773 774     //{{{ setProperty() method 775 /** 776      * Sets a property to a new value. 777      * @param name The property 778      * @param value The new value 779      */ 780     public static final void setProperty(String name, String value) 781     { 782         propMgr.setProperty(name,value); 783     } //}}} 784 785     //{{{ setTemporaryProperty() method 786 /** 787      * Sets a property to a new value. Properties set using this 788      * method are not saved to the user properties list. 789      * @param name The property 790      * @param value The new value 791      * @since jEdit 2.3final 792      */ 793     public static final void setTemporaryProperty(String name, String value) 794     { 795         propMgr.setTemporaryProperty(name,value); 796     } //}}} 797 798     //{{{ setBooleanProperty() method 799 /** 800      * Sets a boolean property. 801      * @param name The property 802      * @param value The value 803      */ 804     public static final void setBooleanProperty(String name, boolean value) 805     { 806         setProperty(name,value ? "true" : "false"); 807     } //}}} 808 809     //{{{ setIntegerProperty() method 810 /** 811      * Sets the value of an integer property. 812      * @param name The property 813      * @param value The value 814      * @since jEdit 4.0pre1 815      */ 816     public static final void setIntegerProperty(String name, int value) 817     { 818         setProperty(name,String.valueOf(value)); 819     } //}}} 820 821     //{{{ setDoubleProperty() method 822 public static final void setDoubleProperty(String name, double value) 823     { 824         setProperty(name,String.valueOf(value)); 825     } 826     //}}} 827 828     //{{{ setFontProperty() method 829 /** 830      * Sets the value of a font property. The family is stored 831      * in the <code><i>name</i></code> property, the font size is stored 832      * in the <code><i>name</i>size</code> property, and the font style is 833      * stored in <code><i>name</i>style</code>. For example, if 834      * <code><i>name</i></code> is <code>view.gutter.font</code>, the 835      * properties will be named <code>view.gutter.font</code>, 836      * <code>view.gutter.fontsize</code>, and 837      * <code>view.gutter.fontstyle</code>. 838      * 839      * @param name The property 840      * @param value The value 841      * @since jEdit 4.0pre1 842      */ 843     public static final void setFontProperty(String name, Font value) 844     { 845         setProperty(name,value.getFamily()); 846         setIntegerProperty(name + "size",value.getSize()); 847         setIntegerProperty(name + "style",value.getStyle()); 848     } //}}} 849 850     //{{{ unsetProperty() method 851 /** 852      * Unsets (clears) a property. 853      * @param name The property 854      */ 855     public static final void unsetProperty(String name) 856     { 857         propMgr.unsetProperty(name); 858     } //}}} 859 860     //{{{ resetProperty() method 861 /** 862      * Resets a property to its default value. 863      * @param name The property 864      * 865      * @since jEdit 2.5pre3 866      */ 867     public static final void resetProperty(String name) 868     { 869         propMgr.resetProperty(name); 870     } //}}} 871 872     //{{{ propertiesChanged() method 873 /** 874      * Reloads various settings from the properties. 875      */ 876     public static void propertiesChanged() 877     { 878         initKeyBindings(); 879 880         Autosave.setInterval(getIntegerProperty("autosave",30)); 881 882         saveCaret = getBooleanProperty("saveCaret"); 883 884         UIDefaults defaults = UIManager.getDefaults(); 885 886         // give all text areas the same font 887 Font font = getFontProperty("view.font"); 888 889         //defaults.put("TextField.font",font); 890 defaults.put("TextArea.font",font); 891         defaults.put("TextPane.font",font); 892 893         // Enable/Disable tooltips 894 ToolTipManager.sharedInstance().setEnabled( 895             jEdit.getBooleanProperty("showTooltips")); 896 897         initProxy(); 898 899         // we do this here instead of adding buffers to the bus. 900 Buffer buffer = buffersFirst; 901         while(buffer != null) 902         { 903             buffer.resetCachedProperties(); 904             buffer.propertiesChanged(); 905             buffer = buffer.next; 906         } 907 908         HistoryModel.setMax(getIntegerProperty("history",25)); 909         KillRing.getInstance().propertiesChanged(getIntegerProperty("history",25)); 910 911         EditBus.send(new PropertiesChanged(null)); 912     } //}}} 913 914     //}}} 915 916     //{{{ Plugin management methods 917 918     //{{{ getNotLoadedPluginJARs() method 919 /** 920      * Returns a list of plugin JARs pathnames that are not currently loaded 921      * by examining the user and system plugin directories. 922      * @since jEdit 3.2pre1 923      */ 924     public static String [] getNotLoadedPluginJARs() 925     { 926         List <String > returnValue = new ArrayList<String >(); 927 928         if(jEditHome != null) 929         { 930             String systemPluginDir = MiscUtilities 931                 .constructPath(jEditHome,"jars"); 932 933             String [] list = new File(systemPluginDir).list(); 934             if(list != null) 935                 getNotLoadedPluginJARs(returnValue,systemPluginDir,list); 936         } 937 938         if(settingsDirectory != null) 939         { 940             String userPluginDir = MiscUtilities 941                 .constructPath(settingsDirectory,"jars"); 942             String [] list = new File(userPluginDir).list(); 943             if(list != null) 944             { 945                 getNotLoadedPluginJARs(returnValue, 946                     userPluginDir,list); 947             } 948         } 949 950         String [] _returnValue = new String [returnValue.size()]; 951         returnValue.toArray(_returnValue); 952         return _returnValue; 953     } //}}} 954 955     //{{{ getPlugin() method 956 /** 957      * Returns the plugin with the specified class name. 958      * Only works for plugins that were loaded. 959      */ 960     public static EditPlugin getPlugin(String name) 961     { 962         return getPlugin(name, false); 963     } //}}} 964 965     //{{{ getPlugin(String, boolean) method 966 /** 967      * Returns the plugin with the specified class name. 968      * If * <code>loadIfNecessary</code> is true, the plugin will be searched for, 969      * loaded, and activated in case it has not yet been loaded. 970      * 971      * @param name the classname of the main Plugin class. 972      * @param loadIfNecessary - loads plugin + dependencies if it is not loaded yet. 973      * @since jEdit 4.2pre4 974      */ 975     public static EditPlugin getPlugin(String name, boolean loadIfNecessary) 976     { 977         EditPlugin[] plugins = getPlugins(); 978         EditPlugin plugin = null; 979         for(int i = 0; i < plugins.length; i++) 980         { 981             if(plugins[i].getClassName().equals(name)) 982                 plugin = plugins[i]; 983             if(loadIfNecessary) 984             { 985                 if(plugin instanceof EditPlugin.Deferred) 986                 { 987                     plugin.getPluginJAR().activatePlugin(); 988                     plugin = plugin.getPluginJAR().getPlugin(); 989                     break; 990                 } 991             } 992         } 993         if (!loadIfNecessary) return plugin; 994         String jarPath = PluginJAR.findPlugin(name); 995         PluginJAR pjar = PluginJAR.load(jarPath, true); 996         return pjar.getPlugin(); 997     } //}}} 998 999     //{{{ getPlugins() method 1000 /** 1001     * Returns an array of installed plugins. 1002     */ 1003    public static EditPlugin[] getPlugins() 1004    { 1005        List <EditPlugin> vector = new ArrayList<EditPlugin>(); 1006        for(int i = 0; i < jars.size(); i++) 1007        { 1008            EditPlugin plugin = jars.elementAt(i).getPlugin(); 1009            if(plugin != null) 1010                vector.add(plugin); 1011        } 1012 1013        EditPlugin[] array = new EditPlugin[vector.size()]; 1014        vector.toArray(array); 1015        return array; 1016    } //}}} 1017 1018    //{{{ getPluginJARs() method 1019 /** 1020     * Returns an array of installed plugins. 1021     * @since jEdit 4.2pre1 1022     */ 1023    public static PluginJAR[] getPluginJARs() 1024    { 1025        PluginJAR[] array = new PluginJAR[jars.size()]; 1026        jars.copyInto(array); 1027        return array; 1028    } //}}} 1029 1030    //{{{ getPluginJAR() method 1031 /** 1032     * Returns the JAR with the specified path name. 1033     * @param path The path name 1034     * @since jEdit 4.2pre1 1035     */ 1036    public static PluginJAR getPluginJAR(String path) 1037    { 1038        for(int i = 0; i < jars.size(); i++) 1039        { 1040            PluginJAR jar = jars.elementAt(i); 1041            if(jar.getPath().equals(path)) 1042                return jar; 1043        } 1044 1045        return null; 1046    } //}}} 1047 1048    //{{{ addPluginJAR() method 1049 /** 1050     * Loads the plugin JAR with the specified path. Some notes about this 1051     * method: 1052     * 1053     * <ul> 1054     * <li>Calling this at a time other than jEdit startup can have 1055     * unpredictable results if the plugin has not been updated for the 1056     * jEdit 4.2 plugin API. 1057     * <li>You must make sure yourself the plugin is not already loaded. 1058     * <li>After loading, you just make sure all the plugin's dependencies 1059     * are satisified before activating the plugin, using the 1060     * {@link PluginJAR#checkDependencies()} method. 1061     * </ul> 1062     * 1063     * @param path The JAR file path 1064     * @since jEdit 4.2pre1 1065     */ 1066    public static void addPluginJAR(String path) 1067    { 1068        PluginJAR jar = new PluginJAR(new File(path)); 1069        jars.addElement(jar); 1070        jar.init(); 1071        jEdit.unsetProperty("plugin-blacklist."+MiscUtilities.getFileName(path)); 1072        EditBus.send(new PluginUpdate(jar,PluginUpdate.LOADED,false)); 1073        if(!isMainThread()) 1074        { 1075            EditBus.send(new DynamicMenuChanged("plugins")); 1076            initKeyBindings(); 1077        } 1078    } //}}} 1079 1080    //{{{ addPluginJARsFromDirectory() method 1081 /** 1082     * Loads all plugins in a directory. 1083     * @param directory The directory 1084     * @since jEdit 4.2pre1 1085     */ 1086    private static void addPluginJARsFromDirectory(String directory) 1087    { 1088        Log.log(Log.NOTICE,jEdit.class,"Loading plugins from " 1089            + directory); 1090 1091        File file = new File(directory); 1092        if(!(file.exists() && file.isDirectory())) 1093            return; 1094        String [] plugins = file.list(); 1095        if(plugins == null) 1096            return; 1097 1098        for(int i = 0; i < plugins.length; i++) 1099        { 1100            String plugin = plugins[i]; 1101            if(!plugin.toLowerCase().endsWith(".jar")) 1102                continue; 1103 1104            String path = MiscUtilities.constructPath(directory,plugin); 1105            if (jEdit.getBooleanProperty("plugin-blacklist."+plugin)) 1106                continue; 1107            // remove this when 4.1 plugin API is deprecated 1108 if(plugin.equals("EditBuddy.jar") 1109                || plugin.equals("PluginManager.jar") 1110                || plugin.equals("Firewall.jar") 1111                || plugin.equals("Tidy.jar") 1112                || plugin.equals("DragAndDrop.jar")) 1113            { 1114                pluginError(path,"plugin-error.obsolete",null); 1115                continue; 1116            } 1117 1118            addPluginJAR(path); 1119        } 1120    } //}}} 1121 1122    //{{{ removePluginJAR() method 1123 /** 1124     * Unloads the given plugin JAR with the specified path. Note that 1125     * calling this at a time other than jEdit shutdown can have 1126     * unpredictable results if the plugin has not been updated for the 1127     * jEdit 4.2 plugin API. 1128     * 1129     * @param jar The <code>PluginJAR</code> instance 1130     * @param exit Set to true if jEdit is exiting; enables some 1131     * shortcuts so the editor can close faster. 1132     * @since jEdit 4.2pre1 1133     */ 1134    public static void removePluginJAR(PluginJAR jar, boolean exit) 1135    { 1136        if(exit) 1137        { 1138            jar.uninit(true); 1139        } 1140        else 1141        { 1142            jar.uninit(false); 1143            jars.removeElement(jar); 1144            initKeyBindings(); 1145        } 1146 1147        EditBus.send(new PluginUpdate(jar,PluginUpdate.UNLOADED,exit)); 1148        if(!isMainThread() && !exit) 1149            EditBus.send(new DynamicMenuChanged("plugins")); 1150    } //}}} 1151 1152    //}}} 1153 1154    //{{{ Action methods 1155 1156    //{{{ getActionContext() method 1157 /** 1158     * Returns the action context used to store editor actions. 1159     * @since jEdit 4.2pre1 1160     */ 1161    public static ActionContext getActionContext() 1162    { 1163        return actionContext; 1164    } //}}} 1165 1166    //{{{ addActionSet() method 1167 /** 1168     * Adds a new action set to jEdit's list of ActionSets (viewable from the shortcuts 1169     * option pane). By default, each plugin has one ActionSet, 1170     * but some plugins may create dynamic action sets, such as ProjectViewer and Console. 1171     * These plugins must call removeActionSet() when the plugin is unloaded. 1172     * 1173     * @since jEdit 4.0pre1 1174     * @see removeActionSet() 1175     */ 1176    public static void addActionSet(ActionSet actionSet) 1177    { 1178        actionContext.addActionSet(actionSet); 1179    } //}}} 1180 1181    //{{{ removeActionSet() method 1182 /** 1183     * Removes an action set from jEdit's list. 1184     * Plugins that add a dynamic action set must call this method at plugin 1185     * unload time. 1186     * @since jEdit 4.2pre1 1187     */ 1188    public static void removeActionSet(ActionSet actionSet) 1189    { 1190        actionContext.removeActionSet(actionSet); 1191    } //}}} 1192 1193    //{{{ getBuiltInActionSet() method 1194 /** 1195     * Returns the set of commands built into jEdit. 1196     * @since jEdit 4.2pre1 1197     */ 1198    public static ActionSet getBuiltInActionSet() 1199    { 1200        return builtInActionSet; 1201    } //}}} 1202 1203    //{{{ getActionSets() method 1204 /** 1205     * Returns all registered action sets. 1206     * @since jEdit 4.0pre1 1207     */ 1208    public static ActionSet[] getActionSets() 1209    { 1210        return actionContext.getActionSets(); 1211    } //}}} 1212 1213    //{{{ getAction() method 1214 /** 1215     * Returns the specified action. 1216     * @param name The action name 1217     */ 1218    public static EditAction getAction(String name) 1219    { 1220        return actionContext.getAction(name); 1221    } //}}} 1222 1223    //{{{ getActionSetForAction() method 1224 /** 1225     * Returns the action set that contains the specified action. 1226     * 1227     * @param action The action 1228     * @since jEdit 4.2pre1 1229     */ 1230    public static ActionSet getActionSetForAction(String action) 1231    { 1232        return actionContext.getActionSetForAction(action); 1233    } //}}} 1234 1235    //{{{ getActionSetForAction() method 1236 /** 1237     * @deprecated Use the form that takes a String instead 1238     */ 1239    public static ActionSet getActionSetForAction(EditAction action) 1240    { 1241        return actionContext.getActionSetForAction(action.getName()); 1242    } //}}} 1243 1244    //{{{ getActions() method 1245 /** 1246     * @deprecated Call getActionNames() instead 1247     */ 1248    public static EditAction[] getActions() 1249    { 1250        String [] names = actionContext.getActionNames(); 1251        EditAction[] actions = new EditAction[names.length]; 1252        for(int i = 0; i < actions.length; i++) 1253        { 1254            actions[i] = actionContext.getAction(names[i]); 1255            if(actions[i] == null) 1256                Log.log(Log.ERROR,jEdit.class,"wtf: " + names[i]); 1257        } 1258        return actions; 1259    } //}}} 1260 1261    //{{{ getActionNames() method 1262 /** 1263     * Returns all registered action names. 1264     */ 1265    public static String [] getActionNames() 1266    { 1267        return actionContext.getActionNames(); 1268    } //}}} 1269 1270    //}}} 1271 1272    //{{{ Edit mode methods 1273 1274    //{{{ reloadModes() method 1275 /** 1276     * Reloads all edit modes. 1277     * @since jEdit 3.2pre2 1278     */ 1279    public static void reloadModes() 1280    { 1281        /* Try to guess the eventual size to avoid unnecessary 1282         * copying */ 1283        modes = new Vector<Mode>(160); 1284 1285        //{{{ Load the global catalog 1286 if(jEditHome == null) 1287            loadModeCatalog("/modes/catalog",true); 1288        else 1289        { 1290            loadModeCatalog(MiscUtilities.constructPath(jEditHome, 1291                "modes","catalog"),false); 1292        } //}}} 1293 1294        //{{{ Load user catalog 1295 if(settingsDirectory != null) 1296        { 1297            File userModeDir = new File(MiscUtilities.constructPath( 1298                settingsDirectory,"modes")); 1299            if(!userModeDir.exists()) 1300                userModeDir.mkdirs(); 1301 1302            File userCatalog = new File(MiscUtilities.constructPath( 1303                settingsDirectory,"modes","catalog")); 1304            if(!userCatalog.exists()) 1305            { 1306                // create dummy catalog 1307 FileWriter out = null; 1308                try 1309                { 1310                    out = new FileWriter(userCatalog); 1311                    out.write(jEdit.getProperty("defaultCatalog")); 1312                } 1313                catch(IOException io) 1314                { 1315                    Log.log(Log.ERROR,jEdit.class,io); 1316                } 1317                finally 1318                { 1319                    IOUtilities.closeQuietly(out); 1320                } 1321            } 1322 1323            loadModeCatalog(userCatalog.getPath(),false); 1324        } //}}} 1325 1326        Buffer buffer = buffersFirst; 1327        while(buffer != null) 1328        { 1329            // This reloads the token marker and sends a message 1330 // which causes edit panes to repaint their text areas 1331 buffer.setMode(); 1332 1333            buffer = buffer.next; 1334        } 1335    } //}}} 1336 1337    //{{{ getMode() method 1338 /** 1339     * Returns the edit mode with the specified name. 1340     * @param name The edit mode 1341     */ 1342    public static Mode getMode(String name) 1343    { 1344        for(int i = 0; i < modes.size(); i++) 1345        { 1346            Mode mode = modes.elementAt(i); 1347            if(mode.getName().equals(name)) 1348                return mode; 1349        } 1350        return null; 1351    } //}}} 1352 1353    //{{{ getModes() method 1354 /** 1355     * Returns an array of installed edit modes. 1356     */ 1357    public static Mode[] getModes() 1358    { 1359        Mode[] array = new Mode[modes.size()]; 1360        modes.copyInto(array); 1361        return array; 1362    } //}}} 1363 1364    //}}} 1365 1366    //{{{ Buffer creation methods 1367 1368    //{{{ openFiles() method 1369 /** 1370     * Opens the file names specified in the argument array. This 1371     * handles +line and +marker arguments just like the command 1372     * line parser. 1373     * @param parent The parent directory 1374     * @param args The file names to open 1375     * @since jEdit 3.2pre4 1376     */ 1377    public static Buffer openFiles(View view, String parent, String [] args) 1378    { 1379        Buffer retVal = null; 1380        Buffer lastBuffer = null; 1381 1382        for(int i = 0; i < args.length; i++) 1383        { 1384            String arg = args[i]; 1385            if(arg == null) 1386                continue; 1387            else if(arg.startsWith("+line:") || arg.startsWith("+marker:")) 1388            { 1389                if(lastBuffer != null) 1390                    gotoMarker(view,lastBuffer,arg); 1391                continue; 1392            } 1393 1394            lastBuffer = openFile(null,parent,arg,false,null); 1395 1396            if(retVal == null && lastBuffer != null) 1397                retVal = lastBuffer; 1398        } 1399 1400        if(view != null && retVal != null) 1401            view.setBuffer(retVal); 1402 1403        return retVal; 1404    } //}}} 1405 1406    //{{{ openFile() method 1407 /** 1408     * Opens a file. Note that as of jEdit 2.5pre1, this may return 1409     * null if the buffer could not be opened. 1410     * @param view The view to open the file in 1411     * @param path The file path 1412     * 1413     * @since jEdit 2.4pre1 1414     */ 1415    public static Buffer openFile(View view, String path) 1416    { 1417        return openFile(view,null,path,false,new Hashtable()); 1418    } //}}} 1419 1420    //{{{ openFile() method 1421 /** 1422     * @deprecated The openFile() forms with the readOnly parameter 1423     * should not be used. The readOnly prameter is no longer supported. 1424     */ 1425    public static Buffer openFile(View view, String parent, 1426        String path, boolean readOnly, boolean newFile) 1427    { 1428        return openFile(view,parent,path,newFile,new Hashtable()); 1429    } //}}} 1430 1431    //{{{ openFile() method 1432 /** 1433     * @deprecated The openFile() forms with the readOnly parameter 1434     * should not be used. The readOnly prameter is no longer supported. 1435     */ 1436    public static Buffer openFile(View view, String parent, 1437        String path, boolean readOnly, boolean newFile, 1438        Hashtable props) 1439    { 1440        return openFile(view,parent,path,newFile,props); 1441    } //}}} 1442 1443    //{{{ openFile() method 1444 /** 1445     * Opens a file. This may return null if the buffer could not be 1446     * opened for some reason. 1447     * @param view The view to open the file in 1448     * @param parent The parent directory of the file 1449     * @param path The path name of the file 1450     * @param newFile True if the file should not be loaded from disk 1451     * be prompted if it should be reloaded 1452     * @param props Buffer-local properties to set in the buffer 1453     * 1454     * @since jEdit 3.2pre10 1455     */ 1456    public static Buffer openFile(View view, String parent, 1457        String path, boolean newFile, Hashtable props) 1458    { 1459        PerspectiveManager.setPerspectiveDirty(true); 1460 1461        if(view != null && parent == null) 1462            parent = view.getBuffer().getDirectory(); 1463 1464        if(MiscUtilities.isURL(path)) 1465        { 1466            if(MiscUtilities.getProtocolOfURL(path).equals("file")) 1467                path = path.substring(5); 1468        } 1469 1470        path = MiscUtilities.constructPath(parent,path); 1471 1472        Buffer newBuffer; 1473 1474        synchronized (editBusOrderingLock) 1475        { 1476            synchronized(bufferListLock) 1477            { 1478                Buffer buffer = getBuffer(path); 1479                if(buffer != null) 1480                { 1481                    if(view != null) 1482                        view.setBuffer(buffer); 1483 1484                    return buffer; 1485                } 1486 1487                if(props == null) 1488                    props = new Hashtable(); 1489 1490                BufferHistory.Entry entry = BufferHistory.getEntry(path); 1491 1492                if(entry != null && saveCaret && props.get(Buffer.CARET) == null) 1493                { 1494                    props.put(Buffer.CARET, entry.caret); 1495                    /* if(entry.selection != null) 1496                    { 1497                        // getSelection() converts from string to 1498                        // Selection[] 1499                        props.put(Buffer.SELECTION,entry.getSelection()); 1500                    } */ 1501                } 1502 1503                if(entry != null && props.get(JEditBuffer.ENCODING) == null) 1504                { 1505                    if(entry.encoding != null) 1506                        props.put(JEditBuffer.ENCODING,entry.encoding); 1507                } 1508 1509                newBuffer = new Buffer(path,newFile,false,props); 1510 1511                if(!newBuffer.load(view,false)) 1512                    return null; 1513 1514                addBufferToList(newBuffer); 1515            } 1516 1517            EditBus.send(new BufferUpdate(newBuffer,view,BufferUpdate.CREATED)); 1518        } 1519 1520        if(view != null) 1521            view.setBuffer(newBuffer); 1522 1523        return newBuffer; 1524    } //}}} 1525 1526    //{{{ openTemporary() method 1527 /** 1528     * Opens a temporary buffer. A temporary buffer is like a normal 1529     * buffer, except that an event is not fired, the the buffer is 1530     * not added to the buffers list. 1531     * 1532     * @param view The view to open the file in 1533     * @param parent The parent directory of the file 1534     * @param path The path name of the file 1535     * @param newFile True if the file should not be loaded from disk 1536     * 1537     * @since jEdit 3.2pre10 1538     */ 1539    public static Buffer openTemporary(View view, String parent, 1540        String path, boolean newFile) 1541    { 1542        if(view != null && parent == null) 1543            parent = view.getBuffer().getDirectory(); 1544 1545        if(MiscUtilities.isURL(path)) 1546        { 1547            if(MiscUtilities.getProtocolOfURL(path).equals("file")) 1548                path = path.substring(5); 1549        } 1550 1551        path = MiscUtilities.constructPath(parent,path); 1552 1553        synchronized(bufferListLock) 1554        { 1555            Buffer buffer = getBuffer(path); 1556            if(buffer != null) 1557                return buffer; 1558 1559            buffer = new Buffer(path,newFile,true,new Hashtable()); 1560            if(!buffer.load(view,false)) 1561                return null; 1562            else 1563                return buffer; 1564        } 1565    } //}}} 1566 1567    //{{{ commitTemporary() method 1568 /** 1569     * Adds a temporary buffer to the buffer list. This must be done 1570     * before allowing the user to interact with the buffer in any 1571     * way. 1572     * @param buffer The buffer 1573     */ 1574    public static void commitTemporary(Buffer buffer) 1575    { 1576        if(!buffer.isTemporary()) 1577            return; 1578 1579        PerspectiveManager.setPerspectiveDirty(true); 1580 1581        addBufferToList(buffer); 1582        buffer.commitTemporary(); 1583 1584        // send full range of events to avoid breaking plugins 1585 EditBus.send(new BufferUpdate(buffer,null,BufferUpdate.CREATED)); 1586        EditBus.send(new BufferUpdate(buffer,null,BufferUpdate.LOAD_STARTED)); 1587        EditBus.send(new BufferUpdate(buffer,null,BufferUpdate.LOADED)); 1588    } //}}} 1589 1590    //{{{ newFile() method 1591 /** 1592     * Creates a new `untitled' file. 1593     * @param view The view to create the file in 1594     */ 1595    public static Buffer newFile(View view) 1596    { 1597        String path; 1598 1599        if(view != null && view.getBuffer() != null) 1600        { 1601            path = view.getBuffer().getDirectory(); 1602            VFS vfs = VFSManager.getVFSForPath(path); 1603            // don't want 'New File' to create a read only buffer 1604 // if current file is on SQL VFS or something 1605 if((vfs.getCapabilities() & VFS.WRITE_CAP) == 0) 1606                path = System.getProperty("user.home"); 1607        } 1608        else 1609            path = null; 1610 1611        return newFile(view,path); 1612    } //}}} 1613 1614    //{{{ newFile() method 1615 /** 1616     * Creates a new `untitled' file. 1617     * @param view The view to create the file in 1618     * @param dir The directory to create the file in 1619     * @since jEdit 3.1pre2 1620     */ 1621    public static Buffer newFile(View view, String dir) 1622    { 1623        // If only one new file is open which is clean, just close 1624 // it, which will create an 'Untitled-1' 1625 if(dir != null 1626            && buffersFirst != null 1627            && buffersFirst == buffersLast 1628            && buffersFirst.isUntitled() 1629            && !buffersFirst.isDirty()) 1630        { 1631            closeBuffer(view,buffersFirst); 1632            // return the newly created 'untitled-1' 1633 return buffersFirst; 1634        } 1635 1636        // Find the highest Untitled-n file 1637 int untitledCount = 0; 1638        Buffer buffer = buffersFirst; 1639        while(buffer != null) 1640        { 1641            if(buffer.getName().startsWith("Untitled-")) 1642            { 1643                try 1644                { 1645                    untitledCount = Math.max(untitledCount, 1646                        Integer.parseInt(buffer.getName() 1647                        .substring(9))); 1648                } 1649                catch(NumberFormatException nf) 1650                { 1651                } 1652            } 1653            buffer = buffer.next; 1654        } 1655 1656        return openFile(view,dir,"Untitled-" + (untitledCount+1),true,null); 1657    } //}}} 1658 1659    //}}} 1660 1661    //{{{ Buffer management methods 1662 1663    //{{{ closeBuffer() method 1664 /** 1665     * Closes a buffer. If there are unsaved changes, the user is 1666     * prompted if they should be saved first. 1667     * @param view The view 1668     * @param buffer The buffer 1669     * @return True if the buffer was really closed, false otherwise 1670     */ 1671    public static boolean closeBuffer(View view, Buffer buffer) 1672    { 1673        // Wait for pending I/O requests 1674 if(buffer.isPerformingIO()) 1675        { 1676            VFSManager.waitForRequests(); 1677            if(VFSManager.errorOccurred()) 1678                return false; 1679        } 1680 1681        if(buffer.isDirty()) 1682        { 1683            Object [] args = { buffer.getName() }; 1684            int result = GUIUtilities.confirm(view,"notsaved",args, 1685                JOptionPane.YES_NO_CANCEL_OPTION, 1686                JOptionPane.WARNING_MESSAGE); 1687            if(result == JOptionPane.YES_OPTION) 1688            { 1689                if(!buffer.save(view,null,true)) 1690                    return false; 1691 1692                VFSManager.waitForRequests(); 1693                if(buffer.getBooleanProperty(BufferIORequest 1694                    .ERROR_OCCURRED)) 1695                { 1696                    return false; 1697                } 1698            } 1699            else if(result != JOptionPane.NO_OPTION) 1700                return false; 1701        } 1702        else 1703        { 1704            // if the buffer is untitled, not dirty and alone, no need to close it 1705 if (buffer.isUntitled() && bufferCount == 1) 1706                return false; 1707        } 1708 1709        _closeBuffer(view,buffer); 1710 1711        return true; 1712    } //}}} 1713 1714    //{{{ _closeBuffer() method 1715 /** 1716     * Closes the buffer, even if it has unsaved changes. 1717     * @param view The view, may be null 1718     * @param buffer The buffer 1719     * 1720     * @exception NullPointerException if the buffer is null 1721     * 1722     * @since jEdit 2.2pre1 1723     */ 1724    public static void _closeBuffer(View view, Buffer buffer) 1725    { 1726        if(buffer.isClosed()) 1727        { 1728            // can happen if the user presses C+w twice real 1729 // quick and the buffer has unsaved changes 1730 return; 1731        } 1732 1733        PerspectiveManager.setPerspectiveDirty(true); 1734 1735        if(!buffer.isNewFile()) 1736        { 1737            if(view != null) 1738                view.getEditPane().saveCaretInfo(); 1739            Integer _caret = (Integer )buffer.getProperty(Buffer.CARET); 1740            int caret = _caret == null ? 0 : _caret.intValue(); 1741 1742            BufferHistory.setEntry(buffer.getPath(),caret, 1743                (Selection[])buffer.getProperty(Buffer.SELECTION), 1744                buffer.getStringProperty(JEditBuffer.ENCODING)); 1745        } 1746 1747        String path = buffer.getSymlinkPath(); 1748        if((VFSManager.getVFSForPath(path).getCapabilities() 1749            & VFS.CASE_INSENSITIVE_CAP) != 0) 1750        { 1751            path = path.toLowerCase(); 1752        } 1753        EditBus.send(new BufferUpdate(buffer,view,BufferUpdate.CLOSING)); 1754        bufferHash.remove(path); 1755        removeBufferFromList(buffer); 1756        buffer.close(); 1757        DisplayManager.bufferClosed(buffer); 1758 1759        EditBus.send(new BufferUpdate(buffer,view,BufferUpdate.CLOSED)); 1760        if(jEdit.getBooleanProperty("persistentMarkers")) 1761            buffer.updateMarkersFile(view); 1762 1763        // Create a new file when the last is closed 1764 if(buffersFirst == null && buffersLast == null) 1765            newFile(view); 1766    } //}}} 1767 1768    //{{{ closeAllBuffers() method 1769 /** 1770     * Closes all open buffers. 1771     * @param view The view 1772     */ 1773    public static boolean closeAllBuffers(View view) 1774    { 1775        return closeAllBuffers(view,false); 1776    } //}}} 1777 1778    //{{{ closeAllBuffers() method 1779 /** 1780     * Closes all open buffers. 1781     * @param view The view 1782     * @param isExiting This must be false unless this method is 1783     * being called by the exit() method 1784     */ 1785    public static boolean closeAllBuffers(View view, boolean isExiting) 1786    { 1787        if(view != null) 1788            view.getEditPane().saveCaretInfo(); 1789 1790        boolean dirty = false; 1791 1792        boolean saveRecent = !(isExiting && jEdit.getBooleanProperty("restore")); 1793 1794        Buffer buffer = buffersFirst; 1795        while(buffer != null) 1796        { 1797            if(buffer.isDirty()) 1798            { 1799                dirty = true; 1800                break; 1801            } 1802            buffer = buffer.next; 1803        } 1804 1805        if(dirty) 1806        { 1807            boolean ok = new CloseDialog(view).isOK(); 1808            if(!ok) 1809                return false; 1810        } 1811 1812        // Wait for pending I/O requests 1813 VFSManager.waitForRequests(); 1814        if(VFSManager.errorOccurred()) 1815            return false; 1816 1817        // close remaining buffers (the close dialog only deals with 1818 // dirty ones) 1819 1820        buffer = buffersFirst; 1821 1822        // zero it here so that BufferTabs doesn't have any problems 1823 buffersFirst = buffersLast = null; 1824        bufferHash.clear(); 1825        bufferCount = 0; 1826 1827        while(buffer != null) 1828        { 1829            if(!buffer.isNewFile() && saveRecent) 1830            { 1831                Integer _caret = (Integer )buffer.getProperty(Buffer.CARET); 1832                int caret = _caret == null ? 0 : _caret.intValue(); 1833                BufferHistory.setEntry(buffer.getPath(),caret, 1834                    (Selection[])buffer.getProperty(Buffer.SELECTION), 1835                    buffer.getStringProperty(JEditBuffer.ENCODING)); 1836            } 1837 1838            buffer.close(); 1839            DisplayManager.bufferClosed(buffer); 1840            if(!isExiting) 1841            { 1842                EditBus.send(new BufferUpdate(buffer,view, 1843                    BufferUpdate.CLOSED)); 1844            } 1845            if(jEdit.getBooleanProperty("persistentMarkers")) 1846                buffer.updateMarkersFile(view); 1847            buffer = buffer.next; 1848        } 1849 1850        if(!isExiting) 1851            newFile(view); 1852 1853        PerspectiveManager.setPerspectiveDirty(true); 1854 1855        return true; 1856    } //}}} 1857 1858    //{{{ saveAllBuffers() method 1859 /** 1860     * Saves all open buffers. 1861     * @param view The view 1862     * @since jEdit 4.2pre1 1863     */ 1864    public static void saveAllBuffers(View view) 1865    { 1866        saveAllBuffers(view,jEdit.getBooleanProperty("confirmSaveAll")); 1867    } //}}} 1868 1869    //{{{ saveAllBuffers() method 1870 /** 1871     * Saves all open buffers. 1872     * @param view The view 1873     * @param confirm If true, a confirmation dialog will be shown first 1874     * @since jEdit 2.7pre2 1875     */ 1876    public static void saveAllBuffers(View view, boolean confirm) 1877    { 1878        if(confirm) 1879        { 1880            int result = GUIUtilities.confirm(view,"saveall",null, 1881                JOptionPane.YES_NO_OPTION, 1882                JOptionPane.QUESTION_MESSAGE); 1883            if(result != JOptionPane.YES_OPTION) 1884                return; 1885        } 1886 1887        Buffer current = view.getBuffer(); 1888 1889        Buffer buffer = buffersFirst; 1890        while(buffer != null) 1891        { 1892            if(buffer.isDirty()) 1893            { 1894                if(buffer.isNewFile()) 1895                    view.setBuffer(buffer); 1896                buffer.save(view,null,true); 1897            } 1898 1899            buffer = buffer.next; 1900        } 1901 1902        view.setBuffer(current); 1903    } //}}} 1904 1905    //{{{ reloadAllBuffers() method 1906 /** 1907     * Reloads all open buffers. 1908     * @param view The view 1909     * @param confirm If true, a confirmation dialog will be shown first 1910     * if any buffers are dirty 1911     * @since jEdit 2.7pre2 1912     */ 1913    public static void reloadAllBuffers(View view, boolean confirm) 1914    { 1915        boolean hasDirty = false; 1916        Buffer[] buffers = jEdit.getBuffers(); 1917 1918        for(int i = 0; i < buffers.length && !hasDirty; i++) 1919            hasDirty = !buffers[i].isNewFile() && buffers[i].isDirty(); 1920 1921        if(confirm && hasDirty) 1922        { 1923            int result = GUIUtilities.confirm(view,"reload-all",null, 1924                JOptionPane.YES_NO_OPTION, 1925                JOptionPane.QUESTION_MESSAGE); 1926            if(result != JOptionPane.YES_OPTION) 1927                return; 1928        } 1929 1930        // save caret info. Buffer.load() will load it. 1931 View _view = viewsFirst; 1932        while(_view != null) 1933        { 1934            EditPane[] panes = _view.getEditPanes(); 1935            for(int i = 0; i < panes.length; i++) 1936            { 1937                panes[i].saveCaretInfo(); 1938            } 1939 1940            _view = _view.next; 1941        } 1942 1943        for(int i = 0; i < buffers.length; i++) 1944        { 1945            Buffer buffer = buffers[i]; 1946            if (buffer.isNewFile()) 1947                continue; 1948            buffer.load(view,true); 1949        } 1950    } //}}} 1951 1952    //{{{ _getBuffer() method 1953 /** 1954     * Returns the buffer with the specified path name. The path name 1955     * must be an absolute, canonical, path. 1956     * 1957     * @param path The path name 1958     * @see MiscUtilities#constructPath(String,String) 1959     * @see MiscUtilities#resolveSymlinks(String) 1960     * @see #getBuffer(String) 1961     * 1962     * @since jEdit 4.2pre7 1963     */ 1964    public static Buffer _getBuffer(String path) 1965    { 1966        // paths on case-insensitive filesystems are stored as lower 1967 // case in the hash. 1968 if((VFSManager.getVFSForPath(path).getCapabilities() 1969            & VFS.CASE_INSENSITIVE_CAP) != 0) 1970        { 1971            path = path.toLowerCase(); 1972        } 1973 1974        synchronized(bufferListLock) 1975        { 1976            return bufferHash.get(path); 1977        } 1978    } //}}} 1979 1980    //{{{ getBuffer() method 1981 /** 1982     * Returns the buffer with the specified path name. The path name 1983     * must be an absolute path. This method automatically resolves 1984     * symbolic links. If performance is critical, cache the canonical 1985     * path and call {@link #_getBuffer(String)} instead. 1986     * 1987     * @param path The path name 1988     * @see MiscUtilities#constructPath(String,String) 1989     * @see MiscUtilities#resolveSymlinks(String) 1990     */ 1991    public static Buffer getBuffer(String path) 1992    { 1993        return _getBuffer(MiscUtilities.resolveSymlinks(path)); 1994    } //}}} 1995 1996    //{{{ getBuffers() method 1997 /** 1998     * Returns an array of open buffers. 1999     */ 2000    public static Buffer[] getBuffers() 2001    { 2002        synchronized(bufferListLock) 2003        { 2004            Buffer[] buffers = new Buffer[bufferCount]; 2005            Buffer buffer = buffersFirst; 2006            for(int i = 0; i < bufferCount; i++) 2007            { 2008                buffers[i] = buffer; 2009                buffer = buffer.next; 2010            } 2011            return buffers; 2012        } 2013    } //}}} 2014 2015    //{{{ getBufferCount() method 2016 /** 2017     * Returns the number of open buffers. 2018     */ 2019    public static int getBufferCount() 2020    { 2021        return bufferCount; 2022    } //}}} 2023 2024    //{{{ getFirstBuffer() method 2025 /** 2026     * Returns the first buffer. 2027     */ 2028    public static Buffer getFirstBuffer() 2029    { 2030        return buffersFirst; 2031    } //}}} 2032 2033    //{{{ getLastBuffer() method 2034 /** 2035     * Returns the last buffer. 2036     */ 2037    public static Buffer getLastBuffer() 2038    { 2039        return buffersLast; 2040    } //}}} 2041 2042    //{{{ checkBufferStatus() method 2043 /** 2044     * Checks each buffer's status on disk and shows the dialog box 2045     * informing the user that buffers changed on disk, if necessary. 2046     * @param view The view 2047     * @since jEdit 4.2pre1 2048     */ 2049    public static void checkBufferStatus(View view) 2050    { 2051        // still need to call the status check even if the option is 2052 // off, so that the write protection is updated if it changes 2053 // on disk 2054 2055        // auto reload changed buffers? 2056 boolean autoReload = getBooleanProperty("autoReload"); 2057 2058        // the problem with this is that if we have two edit panes 2059 // looking at the same buffer and the file is reloaded both 2060 // will jump to the same location 2061 View _view = viewsFirst; 2062        while(_view != null) 2063        { 2064            EditPane[] editPanes = _view.getEditPanes(); 2065            for(int i = 0; i < editPanes.length; i++) 2066            { 2067                editPanes[i].saveCaretInfo(); 2068            } 2069            _view = _view.next; 2070        } 2071 2072        Buffer buffer = buffersFirst; 2073        int[] states = new int[bufferCount]; 2074        int i = 0; 2075        boolean notifyFileChanged = false; 2076        while(buffer != null) 2077        { 2078            states[i] = buffer.checkFileStatus(view); 2079 2080            switch(states[i]) 2081            { 2082            case Buffer.FILE_CHANGED: 2083                if(buffer.getAutoReload()) 2084                { 2085                    if(buffer.isDirty()) 2086                        notifyFileChanged = true; 2087                    else 2088                        buffer.load(view,true); 2089                } 2090                else // no automatic reload even if general setting is true 2091 autoReload = false; 2092                // don't notify user if "do nothing" was chosen 2093 if(buffer.getAutoReloadDialog()) 2094                    notifyFileChanged = true; 2095                break; 2096            case Buffer.FILE_DELETED: 2097                notifyFileChanged = true; 2098                break; 2099            } 2100 2101            buffer = buffer.next; 2102            i++; 2103        } 2104 2105        if(notifyFileChanged) 2106            new FilesChangedDialog(view,states,autoReload); 2107    } //}}} 2108 2109    //}}} 2110 2111    //{{{ View methods 2112 2113    //{{{ getInputHandler() method 2114 /** 2115     * Returns the current input handler (key binding to action mapping) 2116     * @see org.gjt.sp.jedit.gui.InputHandler 2117     */ 2118    public static InputHandler getInputHandler() 2119    { 2120        return inputHandler; 2121    } //}}} 2122 2123    /* public static void newViewTest() 2124    { 2125        long time = System.currentTimeMillis(); 2126        for(int i = 0; i < 30; i++) 2127        { 2128            Buffer b = newFile(null); 2129            b.insert(0,"x"); 2130            new View(b,null,false); 2131        } 2132        System.err.println(System.currentTimeMillis() - time); 2133    } */ 2134 2135    //{{{ newView() method 2136 /** 2137     * Creates a new view. 2138     * @param view An existing view 2139     * @since jEdit 3.2pre2 2140     */ 2141    public static View newView(View view) 2142    { 2143        return newView(view,null,false); 2144    } //}}} 2145 2146    //{{{ newView() method 2147 /** 2148     * Creates a new view of a buffer. 2149     * @param view An existing view 2150     * @param buffer The buffer 2151     */ 2152    public static View newView(View view, Buffer buffer) 2153    { 2154        return newView(view,buffer,false); 2155    } //}}} 2156 2157    //{{{ newView() method 2158 /** 2159     * Creates a new view of a buffer. 2160     * @param view An existing view 2161     * @param buffer The buffer 2162     * @param plainView If true, the view will not have dockable windows or 2163     * tool bars. 2164     * 2165     * @since 4.1pre2 2166     */ 2167    public static View newView(View view, Buffer buffer, boolean plainView) 2168    { 2169        View.ViewConfig config; 2170        if(view != null && (plainView == view.isPlainView())) 2171            config = view.getViewConfig(); 2172        else 2173            config = new View.ViewConfig(plainView); 2174        return newView(view,buffer,config); 2175    } //}}} 2176 2177    //{{{ newView() method 2178 /** 2179     * Creates a new view. 2180     * @param view An existing view 2181     * @param buffer A buffer to display, or null 2182     * @param config Encapsulates the view geometry, split configuration 2183     * and if the view is a plain view 2184     * @since jEdit 4.2pre1 2185     */ 2186    public static View newView(View view, Buffer buffer, View.ViewConfig config) 2187    { 2188        PerspectiveManager.setPerspectiveDirty(true); 2189 2190        try 2191        { 2192            if(view != null) 2193            { 2194                view.showWaitCursor(); 2195                view.getEditPane().saveCaretInfo(); 2196            } 2197 2198            View newView = new View(buffer,config); 2199            addViewToList(newView); 2200 2201            if(!config.plainView) 2202            { 2203                DockableWindowManager wm = newView.getDockableWindowManager(); 2204                if(config.top != null 2205                    && config.top.length() != 0) 2206                    wm.showDockableWindow(config.top); 2207 2208                if(config.left != null 2209                    && config.left.length() != 0) 2210                    wm.showDockableWindow(config.left); 2211 2212                if(config.bottom != null 2213                    && config.bottom.length() != 0) 2214                    wm.showDockableWindow(config.bottom); 2215 2216                if(config.right != null 2217                    && config.right.length() != 0) 2218                    wm.showDockableWindow(config.right); 2219            } 2220 2221            newView.pack(); 2222 2223            if(config.width != 0 && config.height != 0) 2224            { 2225                Rectangle desired = new Rectangle( 2226                    config.x,config.y,config.width, 2227                    config.height); 2228                if(OperatingSystem.isX11() && Debug.GEOMETRY_WORKAROUND) 2229                { 2230                    new GUIUtilities.UnixWorkaround(newView, 2231                        "view",desired,config.extState); 2232                } 2233                else 2234                { 2235                    newView.setBounds(desired); 2236                    newView.setExtendedState(config.extState); 2237                } 2238            } 2239            else 2240                GUIUtilities.centerOnScreen(newView); 2241 2242            EditBus.send(new ViewUpdate(newView,ViewUpdate.CREATED)); 2243 2244            newView.setVisible(true); 2245 2246            // show tip of the day 2247 if(newView == viewsFirst) 2248            { 2249                newView.getTextArea().requestFocus(); 2250 2251                // Don't show the welcome message if jEdit was started 2252 // with the -nosettings switch 2253 if(settingsDirectory != null && getBooleanProperty("firstTime")) 2254                    new HelpViewer("welcome.html"); 2255                else if(jEdit.getBooleanProperty("tip.show")) 2256                    new TipOfTheDay(newView); 2257 2258                setBooleanProperty("firstTime",false); 2259            } 2260            else 2261                GUIUtilities.requestFocus(newView,newView.getTextArea()); 2262 2263            return newView; 2264        } 2265        finally 2266        { 2267            if(view != null) 2268                view.hideWaitCursor(); 2269        } 2270    } //}}} 2271 2272    //{{{ closeView() method 2273 /** 2274     * Closes a view. 2275     * 2276     * jEdit will exit if this was the last open view. 2277     */ 2278    public static void closeView(View view) 2279    { 2280        closeView(view,true); 2281    } //}}} 2282 2283    //{{{ getViews() method 2284 /** 2285     * Returns an array of all open views. 2286     */ 2287    public static View[] getViews() 2288    { 2289        View[] views = new View[viewCount]; 2290        View view = viewsFirst; 2291        for(int i = 0; i < viewCount; i++) 2292        { 2293            views[i] = view; 2294            view = view.next; 2295        } 2296        return views; 2297    } //}}} 2298 2299    //{{{ getViewCount() method 2300 /** 2301     * Returns the number of open views. 2302     */ 2303    public static int getViewCount() 2304    { 2305        return viewCount; 2306    } //}}} 2307 2308    //{{{ getFirstView() method 2309 /** 2310     * Returns the first view. 2311     */ 2312    public static View getFirstView() 2313    { 2314        return viewsFirst; 2315    } //}}} 2316 2317    //{{{ getLastView() method 2318 /** 2319     * Returns the last view. 2320     */ 2321    public static View getLastView() 2322    { 2323        return viewsLast; 2324    } //}}} 2325 2326    //{{{ getActiveView() method 2327 /** 2328     * Returns the currently focused view. 2329     * @since jEdit 4.1pre1 2330     */ 2331    public static View getActiveView() 2332    { 2333        if(activeView == null) 2334        { 2335            // eg user just closed a view and didn't focus another 2336 return viewsFirst; 2337        } 2338        else 2339            return activeView; 2340    } //}}} 2341 2342    //}}} 2343 2344    //{{{ Miscellaneous methods 2345 2346    //{{{ isMainThread() method 2347 /** 2348     * Returns true if the currently running thread is the main thread. 2349     * @since jEdit 4.2pre1 2350     */ 2351    public static boolean isMainThread() 2352    { 2353        return Thread.currentThread() == mainThread; 2354    } //}}} 2355 2356    //{{{ isBackgroundMode() method 2357 /** 2358     * Returns true if jEdit was started with the <code>-background</code> 2359     * command-line switch. 2360     * @since jEdit 4.0pre4 2361     */ 2362    public static boolean isBackgroundModeEnabled() 2363    { 2364        return background; 2365    } //}}} 2366 2367    //{{{ showMemoryStatusDialog() method 2368 /** 2369     * Performs garbage collection and displays a dialog box showing 2370     * memory status. 2371     * @param view The view 2372     * @since jEdit 4.0pre1 2373     */ 2374    public static void showMemoryDialog(View view) 2375    { 2376        Runtime rt = Runtime.getRuntime(); 2377        int before = (int) (rt.freeMemory() / 1024); 2378        System.gc(); 2379        int after = (int) (rt.freeMemory() / 1024); 2380        int total = (int) (rt.totalMemory() / 1024); 2381 2382        JProgressBar progress = new JProgressBar(0,total); 2383        progress.setValue(total - after); 2384        progress.setStringPainted(true); 2385        progress.setString(jEdit.getProperty("memory-status.use", 2386            new Object [] { total - after, total })); 2387 2388        Object [] message = new Object [4]; 2389        message[0] = getProperty("memory-status.gc", 2390            new Object [] { after - before }); 2391        message[1] = Box.createVerticalStrut(12); 2392        message[2] = progress; 2393        message[3] = Box.createVerticalStrut(6); 2394 2395        JOptionPane.showMessageDialog(view,message, 2396            jEdit.getProperty("memory-status.title"), 2397            JOptionPane.INFORMATION_MESSAGE); 2398    } //}}} 2399 2400    //{{{ getJEditHome() method 2401 /** 2402     * Returns the jEdit install directory. 2403     */ 2404    public static String getJEditHome() 2405    { 2406        return jEditHome; 2407    } //}}} 2408 2409    //{{{ getSettingsDirectory() method 2410 /** 2411     * Returns the path of the directory where user-specific settings 2412     * are stored. This will be <code>null</code> if jEdit was 2413     * started with the <code>-nosettings</code> command-line switch; do not 2414     * blindly use this method without checking for a <code>null</code> 2415     * return value first. 2416     */ 2417    public static String getSettingsDirectory() 2418    { 2419        return settingsDirectory; 2420    } //}}} 2421 2422    //{{{ getJARCacheDirectory() method 2423 /** 2424     * Returns the directory where plugin cache files are stored. 2425     * @since jEdit 4.2pre1 2426     */ 2427    public static String getJARCacheDirectory() 2428    { 2429        return jarCacheDirectory; 2430    } //}}} 2431 2432    //{{{ backupSettingsFile() method 2433 /** 2434     * Backs up the specified file in the settings directory. 2435     * You should call this on any settings files your plugin 2436     * writes. 2437     * @param file The file 2438     * @since jEdit 4.0pre1 2439     */ 2440    public static void backupSettingsFile(File file) 2441    { 2442        if(settingsDirectory == null) 2443            return; 2444 2445        String backupDir = MiscUtilities.constructPath( 2446            settingsDirectory,"settings-backup"); 2447        File dir = new File(backupDir); 2448        if(!dir.exists()) 2449            dir.mkdirs(); 2450 2451        // ... sweet. saveBackup() will create backupDir if it 2452 // doesn't exist. 2453 2454        MiscUtilities.saveBackup(file,5,null,"~",backupDir); 2455    } //}}} 2456 2457    //{{{ saveSettings() method 2458 /** 2459     * Saves all user preferences to disk. 2460     */ 2461    public static void saveSettings() 2462    { 2463        if(settingsDirectory == null) 2464            return; 2465 2466        Abbrevs.save(); 2467        FavoritesVFS.saveFavorites(); 2468        HistoryModel.saveHistory(); 2469        Registers.saveRegisters(); 2470        SearchAndReplace.save(); 2471        BufferHistory.save(); 2472        KillRing.getInstance().save(); 2473 2474        File file1 = new File(MiscUtilities.constructPath( 2475            settingsDirectory,"#properties#save#")); 2476        File file2 = new File(MiscUtilities.constructPath( 2477            settingsDirectory,"properties")); 2478        if(file2.exists() && file2.lastModified() != propsModTime) 2479        { 2480            Log.log(Log.WARNING,jEdit.class,file2 + " changed" 2481                + " on disk; will not save user properties"); 2482        } 2483        else 2484        { 2485            backupSettingsFile(file2); 2486 2487            try 2488            { 2489                OutputStream out = new FileOutputStream(file1); 2490                propMgr.saveUserProps(out); 2491                file2.delete(); 2492                file1.renameTo(file2); 2493            } 2494            catch(IOException io) 2495            { 2496                Log.log(Log.ERROR,jEdit.class,io); 2497            } 2498 2499            propsModTime = file2.lastModified(); 2500        } 2501    } //}}} 2502 2503    //{{{ exit() method 2504 /** 2505     * Exits cleanly from jEdit, prompting the user if any unsaved files 2506     * should be saved first. 2507     * @param view The view from which this exit was called 2508     * @param reallyExit If background mode is enabled and this parameter 2509     * is true, then jEdit will close all open views instead of exiting 2510     * entirely. 2511     */ 2512    public static void exit(View view, boolean reallyExit) 2513    { 2514        // Close dialog, view.close() call need a view... 2515 if(view == null) 2516            view = activeView; 2517 2518        // Wait for pending I/O requests 2519 VFSManager.waitForRequests(); 2520 2521        // Send EditorExitRequested 2522 EditBus.send(new EditorExitRequested(view)); 2523 2524        // Even if reallyExit is false, we still exit properly 2525 // if background mode is off 2526 reallyExit |= !background; 2527 2528        PerspectiveManager.savePerspective(false); 2529 2530        try 2531        { 2532            PerspectiveManager.setPerspectiveEnabled(false); 2533 2534            // Close all buffers 2535 if(!closeAllBuffers(view,reallyExit)) 2536                return; 2537        } 2538        finally 2539        { 2540            PerspectiveManager.setPerspectiveEnabled(true); 2541        } 2542 2543        // If we are running in background mode and 2544 // reallyExit was not specified, then return here. 2545 if(!reallyExit) 2546        { 2547            // in this case, we can't directly call 2548 // view.close(); we have to call closeView() 2549 // for all open views 2550 view = viewsFirst; 2551            while(view != null) 2552            { 2553                closeView(view,false); 2554                view = view.next; 2555            } 2556 2557            // Save settings in case user kills the backgrounded 2558 // jEdit process 2559 saveSettings(); 2560        } 2561        else 2562        { 2563            // Save view properties here 2564 if(view != null) 2565                view.close(); 2566 2567            // Stop autosave timer 2568 Autosave.stop(); 2569 2570            // Stop server 2571 if(server != null) 2572                server.stopServer(); 2573 2574            // Stop all plugins 2575 PluginJAR[] plugins = getPluginJARs(); 2576            for(int i = 0; i < plugins.length; i++) 2577            { 2578                removePluginJAR(plugins[i],true); 2579            } 2580 2581            // Send EditorExiting 2582 EditBus.send(new EditorExiting(null)); 2583 2584            // Save settings 2585 saveSettings(); 2586 2587            // Close activity log stream 2588 Log.closeStream(); 2589 2590            // Byebye... 2591 System.exit(0); 2592        } 2593    } //}}} 2594 2595    //{{{ getEditServer() method 2596 /** 2597     * Returns the edit server instance. You can use this to find out the 2598     * port number jEdit is listening on. 2599     * @since jEdit 4.2pre10 2600     */ 2601    public static EditServer getEditServer() 2602    { 2603        return server; 2604    } //}}} 2605 2606    //}}} 2607 2608    //{{{ Package-private members 2609 2610    //{{{ updatePosition() method 2611 /** 2612     * If buffer sorting is enabled, this repositions the buffer. 2613     */ 2614    static void updatePosition(String oldPath, Buffer buffer) 2615    { 2616        if((VFSManager.getVFSForPath(oldPath).getCapabilities() 2617            & VFS.CASE_INSENSITIVE_CAP) != 0) 2618        { 2619            oldPath = oldPath.toLowerCase(); 2620        } 2621 2622        bufferHash.remove(oldPath); 2623 2624        String path = buffer.getSymlinkPath(); 2625        if((VFSManager.getVFSForPath(path).getCapabilities() 2626            & VFS.CASE_INSENSITIVE_CAP) != 0) 2627        { 2628            path = path.toLowerCase(); 2629        } 2630 2631        bufferHash.put(path,buffer); 2632 2633        if(sortBuffers) 2634        { 2635            removeBufferFromList(buffer); 2636            addBufferToList(buffer); 2637        } 2638    } //}}} 2639 2640    //{{{ addMode() method 2641 /** 2642     * Do not call this method. It is only public so that classes 2643     * in the org.gjt.sp.jedit.syntax package can access it. 2644     * @param mode The edit mode 2645     */ 2646    public static void addMode(Mode mode) 2647    { 2648        //Log.log(Log.DEBUG,jEdit.class,"Adding edit mode " 2649 // + mode.getName()); 2650 2651        modes.addElement(mode); 2652    } //}}} 2653 2654    //{{{ loadMode() method 2655 /** 2656     * Loads an XML-defined edit mode from the specified reader. 2657     * @param mode The edit mode 2658     */ 2659    /* package-private */ static void loadMode(Mode mode) 2660    { 2661        final String fileName = (String )mode.getProperty("file"); 2662 2663        Log.log(Log.NOTICE,jEdit.class,"Loading edit mode " + fileName); 2664 2665        XMLReader parser = null; 2666        try { 2667            parser = XMLReaderFactory.createXMLReader(); 2668        } catch (SAXException saxe) { 2669            Log.log(Log.ERROR, jEdit.class, saxe); 2670            return; 2671        } 2672        XModeHandler xmh = new XModeHandler(mode.getName()) 2673        { 2674            public void error(String what, Object subst) 2675            { 2676                String msg; 2677 2678                Object line = "<unknown>"; 2679                if(subst == null) 2680                    msg = jEdit.getProperty("xmode-error." + what); 2681                else 2682                { 2683                    msg = jEdit.getProperty("xmode-error." + what, 2684                        new String [] { subst.toString() }); 2685                    if(subst instanceof Throwable ) 2686                        Log.log(Log.ERROR,this,subst); 2687                    if (subst instanceof SAXParseException ) { 2688                        line = ((SAXParseException )subst).getLineNumber(); 2689                    } 2690                } 2691 2692                Object [] args = { fileName, line, null, msg }; 2693                GUIUtilities.error(null,"xmode-error",args); 2694            } 2695 2696            public TokenMarker getTokenMarker(String modeName) 2697            { 2698                Mode mode = getMode(modeName); 2699                if(mode == null) 2700                    return null; 2701                else 2702                    return mode.getTokenMarker(); 2703            } 2704        }; 2705 2706        mode.setTokenMarker(xmh.getTokenMarker()); 2707 2708        Reader grammar = null; 2709 2710        try 2711        { 2712            grammar = new BufferedReader(new FileReader(fileName)); 2713 2714            InputSource isrc = new InputSource (grammar); 2715            isrc.setSystemId("jedit.jar"); 2716            parser.setContentHandler(xmh); 2717            parser.setDTDHandler(xmh); 2718            parser.setEntityResolver(xmh); 2719            parser.setErrorHandler(xmh); 2720            parser.parse(isrc); 2721 2722            mode.setProperties(xmh.getModeProperties()); 2723        } 2724        catch (Throwable e) 2725        { 2726            Log.log(Log.ERROR, jEdit.class, e); 2727 2728            if (e instanceof SAXParseException ) 2729            { 2730                String message = e.getMessage(); 2731                int line = ((SAXParseException )e).getLineNumber(); 2732                int col = ((SAXParseException )e).getColumnNumber(); 2733 2734                Object [] args = { fileName, line, col, message }; 2735                GUIUtilities.error(null,"xmode-error",args); 2736            } 2737        } 2738        finally 2739        { 2740            IOUtilities.closeQuietly(grammar); 2741        } 2742    } //}}} 2743 2744    //{{{ addPluginProps() method 2745 static void addPluginProps(Properties map) 2746    { 2747        propMgr.addPluginProps(map); 2748    } //}}} 2749 2750    //{{{ removePluginProps() method 2751 static void removePluginProps(Properties map) 2752    { 2753        propMgr.removePluginProps(map); 2754    } //}}} 2755 2756    //{{{ pluginError() method 2757 /** 2758     * 2759     * @param messageProp - a property of a message to print 2760     * @param args a list of arguments whch correspond to {0} and {1} in the string to print. 2761     */ 2762    static void pluginError(String path, String messageProp, 2763        Object [] args) 2764    { 2765        synchronized(pluginErrorLock) 2766        { 2767            if(pluginErrors == null) 2768                pluginErrors = new Vector<ErrorListDialog.ErrorEntry>(); 2769 2770            ErrorListDialog.ErrorEntry newEntry = 2771                new ErrorListDialog.ErrorEntry( 2772                path,messageProp,args); 2773 2774            for(int i = 0; i < pluginErrors.size(); i++) 2775            { 2776                if(pluginErrors.get(i).equals(newEntry)) 2777                    return; 2778            } 2779            pluginErrors.addElement(newEntry); 2780 2781            if(startupDone) 2782            { 2783                SwingUtilities.invokeLater(new Runnable () 2784                { 2785                    public void run() 2786                    { 2787                        showPluginErrorDialog(); 2788                    } 2789                }); 2790            } 2791        } 2792    } //}}} 2793 2794    //{{{ setActiveView() method 2795 static void setActiveView(View view) 2796    { 2797        jEdit.activeView = view; 2798    } //}}} 2799 2800    //}}} 2801 2802    //{{{ Private members 2803 2804    //{{{ Static variables 2805 private static String jEditHome; 2806    private static String settingsDirectory; 2807    private static String jarCacheDirectory; 2808    private static long propsModTime; 2809    private static PropertyManager propMgr; 2810    private static EditServer server; 2811    private static boolean background; 2812    private static ActionContext actionContext; 2813    private static ActionSet builtInActionSet; 2814    private static Vector<ErrorListDialog.ErrorEntry> pluginErrors; 2815    private static final Object pluginErrorLock = new Object (); 2816    private static Vector<PluginJAR> jars; 2817    private static Vector<Mode> modes; 2818    private static boolean saveCaret; 2819    private static InputHandler inputHandler; 2820 2821    // buffer link list 2822 private static boolean sortBuffers; 2823    private static boolean sortByName; 2824    private static int bufferCount; 2825    private static Buffer buffersFirst; 2826    private static Buffer buffersLast; 2827    private static Map<String , Buffer> bufferHash; 2828 2829    // makes openTemporary() thread-safe 2830 private static final Object bufferListLock = new Object (); 2831 2832    private static final Object editBusOrderingLock = new Object (); 2833 2834    // view link list 2835 private static int viewCount; 2836    private static View viewsFirst; 2837    private static View viewsLast; 2838    private static View activeView; 2839 2840    private static boolean startupDone; 2841 2842    private static Thread mainThread; 2843    //}}} 2844 2845    private jEdit() {} 2846 2847    //{{{ usage() method 2848 private static void usage() 2849    { 2850        System.out.println("Usage: jedit [<options>] [<files>]"); 2851 2852        System.out.println(" <file> +marker:<marker>: Positions caret" 2853            + " at marker <marker>"); 2854        System.out.println(" <file> +line:<line>: Positions caret" 2855            + " at line number <line>"); 2856        System.out.println(" <file> +line:<line>,<column>: Positions caret" 2857            + " at line number <line> and column number <column>"); 2858        System.out.println(" --: End of options"); 2859        System.out.println(" -background: Run in background mode"); 2860        System.out.println(" -nobackground: Disable background mode (default)"); 2861        System.out.println(" -gui: Only if running in background mode; open initial view (default)"); 2862        System.out.println(" -nogui: Only if running in background mode; don't open initial view"); 2863        System.out.println(" -log=<level>: Log messages with level equal to or higher than this to"); 2864        System.out.println(" standard error. <level> must be between 1 and 9. Default is 7."); 2865        System.out.println(" -newplainview: Client instance opens a new plain view"); 2866        System.out.println(" -newview: Client instance opens a new view (default)"); 2867        System.out.println(" -plugins: Load plugins (default)"); 2868        System.out.println(" -noplugins: Don't load any plugins"); 2869        System.out.println(" -restore: Restore previously open files (default)"); 2870        System.out.println(" -norestore: Don't restore previously open files"); 2871        System.out.println(" -reuseview: Client instance reuses existing view"); 2872        System.out.println(" -quit: Quit a running instance"); 2873        System.out.println(" -run=<script>: Run the specified BeanShell script"); 2874        System.out.println(" -server: Read/write server info from/to $HOME/.jedit/server (default)"); 2875        System.out.println(" -server=<name>: Read/write server info from/to $HOME/.jedit/<name>"); 2876        System.out.println(" -noserver: Don't start edit server"); 2877        System.out.println(" -settings=<path>: Load user-specific settings from <path>"); 2878        System.out.println(" -nosettings: Don't load user-specific settings"); 2879        System.out.println(" -startupscripts: Run startup scripts (default)"); 2880        System.out.println(" -nostartupscripts: Don't run startup scripts"); 2881        System.out.println(" -usage: Print this message and exit"); 2882        System.out.println(" -version: Print jEdit version and exit"); 2883        System.out.println(" -wait: Wait until the user closes the specified buffer in the server"); 2884        System.out.println(" instance. Does nothing if passed to the initial jEdit instance."); 2885        System.out.println(); 2886        System.out.println("Report bugs to http://sourceforge.net/tracker/?group_id=588&atid=100588"); 2887    } //}}} 2888 2889    //{{{ version() method 2890 private static void version() 2891    { 2892        System.out.println("jEdit " + getVersion()); 2893    } //}}} 2894 2895    //{{{ makeServerScript() method 2896 /** 2897     * Creates a BeanShell script that can be sent to a running edit server. 2898     */ 2899    private static String makeServerScript(boolean wait, 2900        boolean restore, boolean newView, 2901        boolean newPlainView, String [] args, 2902        String scriptFile) 2903    { 2904        StringBuilder script = new StringBuilder (); 2905 2906        String userDir = System.getProperty("user.dir"); 2907 2908        script.append("parent = \""); 2909        script.append(MiscUtilities.charsToEscapes(userDir)); 2910        script.append("\";\n"); 2911 2912        script.append("args = new String["); 2913        script.append(args.length); 2914        script.append("];\n"); 2915 2916        for(int i = 0; i < args.length; i++) 2917        { 2918            script.append("args["); 2919            script.append(i); 2920            script.append("] = "); 2921 2922            if(args[i] == null) 2923                script.append("null"); 2924            else 2925            { 2926                script.append('"'); 2927                script.append(MiscUtilities.charsToEscapes(args[i])); 2928                script.append('"'); 2929            } 2930 2931            script.append(";\n"); 2932        } 2933 2934        script.append("view = jEdit.getLastView();\n"); 2935        script.append("buffer = EditServer.handleClient("); 2936        script.append(restore).append(',').append(newView).append(',').append(newPlainView); 2937        script.append(",parent,args);\n"); 2938        script.append("if(buffer != null && ").append(wait).append(") {\n"); 2939        script.append("\tbuffer.setWaitSocket(socket);\n"); 2940        script.append("\tdoNotCloseSocket = true;\n"); 2941        script.append("}\n"); 2942        script.append("if(view != jEdit.getLastView() && ").append(wait).append(") {\n"); 2943        script.append("\tjEdit.getLastView().setWaitSocket(socket);\n"); 2944        script.append("\tdoNotCloseSocket = true;\n"); 2945        script.append("}\n"); 2946        script.append("if(doNotCloseSocket == void)\n"); 2947        script.append("\tsocket.close();\n"); 2948 2949        if(scriptFile != null) 2950        { 2951            scriptFile = MiscUtilities.constructPath(userDir,scriptFile); 2952            script.append("BeanShell.runScript(view,\"") 2953                .append(MiscUtilities.charsToEscapes(scriptFile)) 2954                .append("\",null,this.namespace);\n"); 2955        } 2956 2957        return script.toString(); 2958    } //}}} 2959 2960    //{{{ initMisc() method 2961 /** 2962     * Initialise various objects, register protocol handlers. 2963     */ 2964    private static void initMisc() 2965    { 2966        jars = new Vector<PluginJAR>(); 2967        actionContext = new ActionContext() 2968        { 2969            public void invokeAction(EventObject evt, 2970                EditAction action) 2971            { 2972                View view = GUIUtilities.getView( 2973                    (Component)evt.getSource()); 2974 2975                boolean actionBarVisible; 2976                if(view.getActionBar() == null 2977                    || !view.getActionBar().isShowing()) 2978                    actionBarVisible = false; 2979                else 2980                { 2981                    actionBarVisible = view.getActionBar() 2982                        .isVisible(); 2983                } 2984 2985                view.getInputHandler().invokeAction(action); 2986 2987                if(actionBarVisible) 2988                { 2989                    // XXX: action bar might not be 'temp' 2990 ActionBar actionBar = view 2991                        .getActionBar(); 2992                    if(actionBar != null) 2993                        view.removeToolBar(actionBar); 2994                } 2995            } 2996        }; 2997 2998        bufferHash = new HashMap<String , Buffer>(); 2999 3000        inputHandler = new DefaultInputHandler(null); 3001 3002        // Add our protocols to java.net.URL's list 3003 System.getProperties().put("java.protocol.handler.pkgs", 3004            "org.gjt.sp.jedit.proto|" + 3005            System.getProperty("java.protocol.handler.pkgs","")); 3006 3007        // Set the User-Agent string used by the java.net HTTP handler 3008 String userAgent = "jEdit/" + getVersion() 3009            + " (Java " + System.getProperty("java.version") 3010            + ". " + System.getProperty("java.vendor") 3011            + "; " + System.getProperty("os.arch") + ')'; 3012        System.getProperties().put("http.agent",userAgent); 3013 3014        /* Determine installation directory. 3015         * If the jedit.home property is set, use that. 3016         * Then, look for jedit.jar in the classpath. 3017         * If that fails, assume this is the web start version. */ 3018        jEditHome = System.getProperty("jedit.home"); 3019        if(jEditHome == null) 3020        { 3021            String classpath = System 3022                .getProperty("java.class.path"); 3023            int index = classpath.toLowerCase() 3024                .indexOf("jedit.jar"); 3025            int start = classpath.lastIndexOf(File 3026                .pathSeparator,index) + 1; 3027            // if started with java -jar jedit.jar 3028 if(start == index) 3029            { 3030                jEditHome = System.getProperty("user.dir"); 3031            } 3032            else if(index > start) 3033            { 3034                jEditHome = classpath.substring(start, 3035                    index - 1); 3036            } 3037            else 3038            { 3039                // check if web start 3040 /* if(jEdit.class.getResource("/modes/catalog") != null) 3041                { 3042                    // modes bundled in; hence web start 3043                    jEditHome = null; 3044                } 3045                else */ 3046                { 3047                    // use user.dir as last resort 3048 jEditHome = System.getProperty("user.dir"); 3049 3050                    Log.log(Log.WARNING,jEdit.class,"jedit.jar not in class path!"); 3051                    Log.log(Log.WARNING,jEdit.class,"Assuming jEdit is installed in " 3052                        + jEditHome + '.'); 3053                    Log.log(Log.WARNING,jEdit.class,"Override with jedit.home " 3054                        + "system property."); 3055                } 3056            } 3057        } 3058 3059        jEditHome = MiscUtilities.resolveSymlinks(jEditHome); 3060 3061        Log.log(Log.MESSAGE,jEdit.class,"jEdit home directory is " + jEditHome); 3062 3063        if(settingsDirectory != null) 3064        { 3065            jarCacheDirectory = MiscUtilities.constructPath( 3066                settingsDirectory,"jars-cache"); 3067            new File(jarCacheDirectory).mkdirs(); 3068        } 3069 3070        //if(jEditHome == null) 3071 // Log.log(Log.DEBUG,jEdit.class,"Web start mode"); 3072 3073        // Add an EditBus component that will reload edit modes and 3074 // macros if they are changed from within the editor 3075 EditBus.addToBus(new SettingsReloader()); 3076 3077        // Perhaps if Xerces wasn't slightly brain-damaged, we would 3078 // not need this 3079 SwingUtilities.invokeLater(new Runnable () 3080        { 3081            public void run() 3082            { 3083                Thread.currentThread().setContextClassLoader( 3084                    new JARClassLoader()); 3085            } 3086        }); 3087    } //}}} 3088 3089    //{{{ initSystemProperties() method 3090 /** 3091     * Load system properties. 3092     */ 3093    private static void initSystemProperties() 3094    { 3095        propMgr = new PropertyManager(); 3096 3097        try 3098        { 3099            propMgr.loadSystemProps(jEdit.class.getResourceAsStream( 3100                "/org/gjt/sp/jedit/jedit.props")); 3101            propMgr.loadSystemProps(jEdit.class.getResourceAsStream( 3102                "/org/gjt/sp/jedit/jedit_gui.props")); 3103            propMgr.loadSystemProps(jEdit.class.getResourceAsStream( 3104                "/org/gjt/sp/jedit/jedit_keys.props")); 3105        } 3106        catch(Exception e) 3107        { 3108            Log.log(Log.ERROR,jEdit.class, 3109                "Error while loading system properties!"); 3110            Log.log(Log.ERROR,jEdit.class, 3111                "One of the following property files could not be loaded:\n" 3112                + "- jedit.props\n" 3113                + "- jedit_gui.props\n" 3114                + "- jedit_keys.props\n" 3115                + "jedit.jar is probably corrupt."); 3116            Log.log(Log.ERROR,jEdit.class,e); 3117            System.exit(1); 3118        } 3119    } //}}} 3120 3121    //{{{ initSiteProperties() method 3122 /** 3123     * Load site properties. 3124     */ 3125    private static void initSiteProperties() 3126    { 3127        // site properties are loaded as default properties, overwriting 3128 // jEdit's system properties 3129 3130        String siteSettingsDirectory = MiscUtilities.constructPath( 3131            jEditHome, "properties"); 3132        File siteSettings = new File(siteSettingsDirectory); 3133 3134        if (!(siteSettings.exists() && siteSettings.isDirectory())) 3135            return; 3136 3137        String [] snippets = siteSettings.list(); 3138        if (snippets == null) 3139            return; 3140 3141        Arrays.sort(snippets, 3142            new MiscUtilities.StringICaseCompare()); 3143 3144        for (int i = 0; i < snippets.length; ++i) 3145        { 3146            String snippet = snippets[i]; 3147            if(!snippet.toLowerCase().endsWith(".props")) 3148                continue; 3149 3150            try 3151            { 3152                String path = MiscUtilities.constructPath( 3153                    siteSettingsDirectory,snippet); 3154                Log.log(Log.DEBUG,jEdit.class, 3155                    "Loading site snippet: " + path); 3156 3157                propMgr.loadSiteProps(new FileInputStream(new File(path))); 3158            } 3159            catch(FileNotFoundException fnf) 3160            { 3161                Log.log(Log.DEBUG,jEdit.class,fnf); 3162            } 3163            catch(IOException e) 3164            { 3165                Log.log(Log.ERROR,jEdit.class,"Cannot load site snippet " 3166                    + snippet); 3167                Log.log(Log.ERROR,jEdit.class,e); 3168            } 3169        } 3170    } //}}} 3171 3172    //{{{ initResources() method 3173 private static void initResources() 3174    { 3175        builtInActionSet = new ActionSet(null,null,null, 3176            jEdit.class.getResource("actions.xml")); 3177        builtInActionSet.setLabel(getProperty("action-set.jEdit")); 3178        builtInActionSet.load(); 3179 3180        actionContext.addActionSet(builtInActionSet); 3181 3182        DockableWindowFactory.getInstance() 3183            .loadDockableWindows(null, 3184            jEdit.class.getResource("dockables.xml"), 3185            null); 3186 3187        ServiceManager.loadServices(null, 3188            jEdit.class.getResource("services.xml"), 3189            null); 3190    } //}}} 3191 3192    //{{{ initPlugins() method 3193 /** 3194     * Loads plugins. 3195     */ 3196    private static void initPlugins() 3197    { 3198        if(jEditHome != null) 3199        { 3200            addPluginJARsFromDirectory(MiscUtilities.constructPath( 3201                jEditHome,"jars")); 3202        } 3203 3204        if(settingsDirectory != null) 3205        { 3206            File jarsDirectory = new File(settingsDirectory,"jars"); 3207            if(!jarsDirectory.exists()) 3208                jarsDirectory.mkdir(); 3209            addPluginJARsFromDirectory(jarsDirectory.getPath()); 3210        } 3211 3212        PluginJAR[] jars = getPluginJARs(); 3213        for(int i = 0; i < jars.length; i++) 3214        { 3215            jars[i].checkDependencies(); 3216        } 3217    } //}}} 3218 3219    //{{{ initUserProperties() method 3220 /** 3221     * Loads user properties. 3222     */ 3223    private static void initUserProperties() 3224    { 3225        if(settingsDirectory != null) 3226        { 3227            File file = new File(MiscUtilities.constructPath( 3228                settingsDirectory,"properties")); 3229            propsModTime = file.lastModified(); 3230 3231            try 3232            { 3233                propMgr.loadUserProps( 3234                    new FileInputStream(file)); 3235            } 3236            catch(FileNotFoundException fnf) 3237            { 3238                //Log.log(Log.DEBUG,jEdit.class,fnf); 3239 } 3240            catch(Exception e) 3241            { 3242                Log.log(Log.ERROR,jEdit.class,e); 3243            } 3244        } 3245    } //}}} 3246 3247    //{{{ fontStyleToString() method 3248 private static String fontStyleToString(int style) 3249    { 3250        if(style == 0) 3251            return "PLAIN"; 3252        else if(style == Font.BOLD) 3253            return "BOLD"; 3254        else if(style == Font.ITALIC) 3255            return "ITALIC"; 3256        else if(style == (Font.BOLD | Font.ITALIC)) 3257            return "BOLDITALIC"; 3258        else 3259            throw new RuntimeException ("Invalid style: " + style); 3260    } //}}} 3261 3262    //{{{ fontToString() method 3263 private static String fontToString(Font font) 3264    { 3265        return font.getFamily() 3266            + '-' 3267            + fontStyleToString(font.getStyle()) 3268            + '-' 3269            + font.getSize(); 3270    } //}}} 3271 3272    //{{{ initPLAF() method 3273 /** 3274     * Sets the Swing look and feel. 3275     */ 3276    private static void initPLAF() 3277    { 3278        Font primaryFont = jEdit.getFontProperty( 3279            "metal.primary.font"); 3280        if(primaryFont != null) 3281        { 3282            String primaryFontString = 3283                fontToString(primaryFont); 3284 3285            System.getProperties().put( 3286                "swing.plaf.metal.controlFont", 3287                primaryFontString); 3288            System.getProperties().put( 3289                "swing.plaf.metal.menuFont", 3290                primaryFontString); 3291        } 3292 3293        Font secondaryFont = jEdit.getFontProperty( 3294            "metal.secondary.font"); 3295        if(secondaryFont != null) 3296        { 3297            String secondaryFontString = 3298                fontToString(secondaryFont); 3299 3300            System.getProperties().put( 3301                "swing.plaf.metal.systemFont", 3302                secondaryFontString); 3303            System.getProperties().put( 3304                "swing.plaf.metal.userFont", 3305                secondaryFontString); 3306        } 3307 3308        try 3309        { 3310            String lf = getProperty("lookAndFeel"); 3311            if(lf != null && lf.length() != 0) 3312                UIManager.setLookAndFeel(lf); 3313            else if(OperatingSystem.isMacOS()) 3314            { 3315                UIManager.setLookAndFeel(UIManager 3316                    .getSystemLookAndFeelClassName()); 3317            } 3318            else 3319            { 3320                UIManager.setLookAndFeel(UIManager 3321                    .getCrossPlatformLookAndFeelClassName()); 3322            } 3323        } 3324        catch(Exception e) 3325        { 3326            Log.log(Log.ERROR,jEdit.class,e); 3327        } 3328 3329        UIDefaults defaults = UIManager.getDefaults(); 3330 3331        // give all Swing components our colors 3332 if(jEdit.getBooleanProperty("textColors")) 3333        { 3334            Color background = new javax.swing.plaf.ColorUIResource ( 3335                jEdit.getColorProperty("view.bgColor")); 3336            Color foreground = new javax.swing.plaf.ColorUIResource ( 3337                jEdit.getColorProperty("view.fgColor")); 3338            Color caretColor = new javax.swing.plaf.ColorUIResource ( 3339                jEdit.getColorProperty("view.caretColor")); 3340            Color selectionColor = new javax.swing.plaf.ColorUIResource ( 3341                jEdit.getColorProperty("view.selectionColor")); 3342 3343            String [] prefixes = { "TextField", "TextArea", "List", "Table" }; 3344            for(int i = 0; i < prefixes.length; i++) 3345            { 3346                String prefix = prefixes[i]; 3347                defaults.put(prefix + ".disabledBackground",background); 3348                defaults.put(prefix + ".background",background); 3349                defaults.put(prefix + ".disabledForeground",foreground); 3350                defaults.put(prefix + ".foreground",foreground); 3351                defaults.put(prefix + ".caretForeground",caretColor); 3352                defaults.put(prefix + ".selectionForeground",foreground); 3353                defaults.put(prefix + ".selectionBackground",selectionColor); 3354                //defaults.put(prefix + ".inactiveForeground",foreground); 3355 } 3356 3357            defaults.put("Tree.background",background); 3358            defaults.put("Tree.foreground",foreground); 3359            defaults.put("Tree.textBackground",background); 3360            defaults.put("Tree.textForeground",foreground); 3361            defaults.put("Tree.selectionForeground",foreground); 3362            defaults.put("Tree.selectionBackground",selectionColor); 3363        } 3364 3365        defaults.remove("SplitPane.border"); 3366        defaults.remove("SplitPaneDivider.border"); 3367 3368        JFrame.setDefaultLookAndFeelDecorated( 3369            getBooleanProperty("decorate.frames")); 3370        JDialog.setDefaultLookAndFeelDecorated( 3371            getBooleanProperty("decorate.dialogs")); 3372 3373        KeyboardFocusManager.setCurrentKeyboardFocusManager( 3374            new MyFocusManager()); 3375    } //}}} 3376 3377    //{{{ runStartupScripts() method 3378 /** 3379     * Runs scripts in a directory. 3380     */ 3381    private static void runStartupScripts(File directory) 3382    { 3383        if (!directory.isDirectory()) 3384            return; 3385 3386        File[] snippets = directory.listFiles(); 3387        if (snippets == null) 3388            return; 3389 3390        Arrays.sort(snippets, 3391            new MiscUtilities.StringICaseCompare()); 3392 3393        for(int i = 0; i < snippets.length; ++i) 3394        { 3395            File snippet = snippets[i]; 3396 3397            Macros.Handler handler = Macros.getHandlerForPathName( 3398                snippet.getPath()); 3399            if(handler == null) 3400                continue; 3401 3402            try 3403            { 3404                Macros.Macro newMacro = handler.createMacro( 3405                    snippet.getName(), 3406                    snippet.getPath()); 3407                handler.runMacro(null,newMacro,false); 3408            } 3409            catch(Exception e) 3410            { 3411                Log.log(Log.ERROR,jEdit.class,e); 3412            } 3413        } 3414    } //}}} 3415 3416    //{{{ initProxy() method 3417 private static void initProxy() 3418    { 3419        boolean socksEnabled = jEdit.getBooleanProperty("socks.enabled"); 3420        if(!socksEnabled) 3421        { 3422            Log.log(Log.DEBUG,jEdit.class,"SOCKS proxy disabled"); 3423            System.getProperties().remove("socksProxyHost"); 3424            System.getProperties().remove("socksProxyPort"); 3425        } 3426        else 3427        { 3428            String socksHost = jEdit.getProperty("firewall.socks.host"); 3429            if( socksHost != null ) 3430            { 3431                System.setProperty("socksProxyHost", socksHost); 3432                Log.log(Log.DEBUG, jEdit.class, 3433                    "SOCKS proxy enabled: " + socksHost); 3434            } 3435 3436            String socksPort = jEdit.getProperty("firewall.socks.port"); 3437            if(socksPort != null) 3438                System.setProperty("socksProxyPort", socksPort); 3439        } 3440 3441        boolean httpEnabled = jEdit.getBooleanProperty("firewall.enabled"); 3442        if (!httpEnabled) 3443        { 3444            Log.log(Log.DEBUG, jEdit.class, "HTTP proxy disabled"); 3445            System.getProperties().remove("proxySet"); 3446            System.getProperties().remove("proxyHost"); 3447            System.getProperties().remove("proxyPort"); 3448            System.getProperties().remove("http.proxyHost"); 3449            System.getProperties().remove("http.proxyPort"); 3450            System.getProperties().remove("http.nonProxyHosts"); 3451            Authenticator.setDefault(null); 3452        } 3453        else 3454        { 3455            // set proxy host 3456 String host = jEdit.getProperty("firewall.host"); 3457            if (host == null) 3458                return; 3459 3460            System.setProperty("http.proxyHost", host); 3461            Log.log(Log.DEBUG, jEdit.class, "HTTP proxy enabled: " + host); 3462            // set proxy port 3463 String port = jEdit.getProperty("firewall.port"); 3464            if (port != null) 3465                System.setProperty("http.proxyPort", port); 3466 3467            // set non proxy hosts list 3468 String nonProxyHosts = jEdit.getProperty("firewall.nonProxyHosts"); 3469            if (nonProxyHosts != null) 3470                System.setProperty("http.nonProxyHosts", nonProxyHosts); 3471 3472            // set proxy authentication 3473 String username = jEdit.getProperty("firewall.user"); 3474            String password = jEdit.getProperty("firewall.password"); 3475 3476            // null not supported? 3477 if(password == null) 3478                password = ""; 3479 3480            if(username == null || username.length()==0) 3481            { 3482                Log.log(Log.DEBUG, jEdit.class, "HTTP proxy without user"); 3483                Authenticator.setDefault(new FirewallAuthenticator(null)); 3484            } 3485            else 3486            { 3487                Log.log(Log.DEBUG, jEdit.class, "HTTP proxy user: " + username); 3488                PasswordAuthentication pw = new PasswordAuthentication( 3489                    username,password.toCharArray() 3490                ); 3491                Authenticator.setDefault(new FirewallAuthenticator(pw)); 3492            } 3493        } 3494    } //}}} 3495 3496    //{{{ FirewallAuthenticator class 3497 static class FirewallAuthenticator extends Authenticator 3498    { 3499        PasswordAuthentication pw; 3500 3501        FirewallAuthenticator(PasswordAuthentication pw) 3502        { 3503            this.pw = pw; 3504        } 3505 3506        protected PasswordAuthentication getPasswordAuthentication() 3507        { 3508            return pw; 3509        } 3510    } //}}} 3511 3512    //{{{ finishStartup() method 3513 private static void finishStartup(final boolean gui, final boolean restore, 3514        final String userDir, final String [] args) 3515    { 3516        SwingUtilities.invokeLater(new Runnable () { 3517            public void run() 3518            { 3519                Buffer buffer = openFiles(null,userDir,args); 3520 3521                int count = getBufferCount(); 3522                if(count == 0) 3523                    newFile(null); 3524 3525                View view; 3526 3527                boolean restoreFiles = restore 3528                    && jEdit.getBooleanProperty("restore") 3529                    && (count == 0 || 3530                    jEdit.getBooleanProperty("restore.cli")); 3531 3532                if(gui || count != 0) 3533                { 3534                    view = PerspectiveManager 3535                        .loadPerspective( 3536                        restoreFiles); 3537 3538                    if(view == null) 3539                        view = newView(null,buffer); 3540                    else if(buffer != null) 3541                        view.setBuffer(buffer); 3542                } 3543 3544                // Start I/O threads 3545 EditBus.send(new EditorStarted(null)); 3546 3547                VFSManager.start(); 3548 3549                // Start edit server 3550 if(server != null) 3551                    server.start(); 3552 3553                GUIUtilities.hideSplashScreen(); 3554 3555                Log.log(Log.MESSAGE,jEdit.class,"Startup " 3556                    + "complete"); 3557 3558                //{{{ Report any plugin errors 3559 if(pluginErrors != null) 3560                { 3561                    showPluginErrorDialog(); 3562                } //}}} 3563 3564                startupDone = true; 3565 3566                // in one case not a single AWT class will 3567 // have been touched (splash screen off + 3568 // -nogui -nobackground switches on command 3569 // line) 3570 Toolkit.getDefaultToolkit(); 3571            } 3572        }); 3573    } //}}} 3574 3575    //{{{ showPluginErrorDialog() method 3576 private static void showPluginErrorDialog() 3577    { 3578        if(pluginErrors == null) 3579            return; 3580 3581        String caption = getProperty( 3582            "plugin-error.caption" + (pluginErrors.size() == 1 3583            ? "-1" : "")); 3584 3585        Frame frame = (PluginManager.getInstance() == null 3586            ? viewsFirst 3587            : PluginManager.getInstance()); 3588 3589        new ErrorListDialog(frame, 3590            getProperty("plugin-error.title"), 3591            caption,pluginErrors,true); 3592        pluginErrors = null; 3593    } //}}} 3594 3595    //{{{ getNotLoadedPluginJARs() method 3596 private static void getNotLoadedPluginJARs(List <String > returnValue, 3597        String dir, String [] list) 3598    { 3599loop: for(int i = 0; i < list.length; i++) 3600        { 3601            String name = list[i]; 3602            if(!name.toLowerCase().endsWith(".jar")) 3603                continue loop; 3604 3605            String path = MiscUtilities.constructPath(dir,name); 3606 3607            for(int j = 0; j < jars.size(); j++) 3608            { 3609                PluginJAR jar = jars.elementAt(j); 3610                String jarPath = jar.getPath(); 3611                String jarName = MiscUtilities.getFileName(jarPath); 3612 3613                if(path.equals(jarPath)) 3614                    continue loop; 3615                else if(!new File(jarPath).exists() 3616                    && name.equals(jarName)) 3617                    continue loop; 3618            } 3619 3620            returnValue.add(path); 3621        } 3622    } //}}} 3623 3624    //{{{ gotoMarker() method 3625 private static void gotoMarker(final View view, final Buffer buffer, 3626        final String marker) 3627    { 3628        VFSManager.runInAWTThread(new Runnable () 3629        { 3630            public void run() 3631            { 3632                int pos; 3633 3634                // Handle line number 3635 if(marker.startsWith("+line:")) 3636                { 3637                    try 3638                    { 3639                        String arg = marker.substring(6); 3640                        String [] lineCol = arg.split(","); 3641                        int line, col; 3642                        if(lineCol.length > 1) 3643                        { 3644                            line = Integer.parseInt(lineCol[0]); 3645                            col = Integer.parseInt(lineCol[1]); 3646                        } 3647                        else 3648                        { 3649                            line = Integer.parseInt(marker.substring(6)); 3650                            col = 1; 3651                        } 3652                        pos = buffer.getLineStartOffset(line - 1) + (col - 1); 3653                    } 3654                    catch(Exception e) 3655                    { 3656                        return; 3657                    } 3658                } 3659                // Handle marker 3660 else if(marker.startsWith("+marker:")) 3661                { 3662                    if(marker.length() != 9) 3663                        return; 3664 3665                    Marker m = buffer.getMarker(marker.charAt(8)); 3666                    if(m == null) 3667                        return; 3668                    pos = m.getPosition(); 3669                } 3670                // Can't happen 3671 else 3672                    throw new InternalError (); 3673 3674                if(view != null && view.getBuffer() == buffer) { 3675                    view.getTextArea().setCaretPosition(pos); 3676                    buffer.setIntegerProperty(Buffer.CARET,pos); 3677                    buffer.setBooleanProperty(Buffer.CARET_POSITIONED,true); 3678                } 3679                else 3680                { 3681                    buffer.setIntegerProperty(Buffer.CARET,pos); 3682                    buffer.setBooleanProperty(Buffer.CARET_POSITIONED,true); 3683                    buffer.unsetProperty(Buffer.SCROLL_VERT); 3684                } 3685            } 3686        }); 3687    } //}}} 3688 3689    //{{{ addBufferToList() method 3690 private static void addBufferToList(Buffer buffer) 3691    { 3692        synchronized(bufferListLock) 3693        { 3694            String symlinkPath = buffer.getSymlinkPath(); 3695            if((VFSManager.getVFSForPath(symlinkPath).getCapabilities() 3696                & VFS.CASE_INSENSITIVE_CAP) != 0) 3697            { 3698                symlinkPath = symlinkPath.toLowerCase(); 3699            } 3700 3701            // if only one, clean, 'untitled' buffer is open, we 3702 // replace it 3703 if(viewCount <= 1 && buffersFirst != null 3704                && buffersFirst == buffersLast 3705                && buffersFirst.isUntitled() 3706                && !buffersFirst.isDirty()) 3707            { 3708                Buffer oldBuffersFirst = buffersFirst; 3709                buffersFirst = buffersLast = buffer; 3710                DisplayManager.bufferClosed(oldBuffersFirst); 3711                EditBus.send(new BufferUpdate(oldBuffersFirst, 3712                    null,BufferUpdate.CLOSED)); 3713 3714                bufferHash.clear(); 3715 3716                bufferHash.put(symlinkPath,buffer); 3717                return; 3718            } 3719 3720            bufferCount++; 3721 3722            bufferHash.put(symlinkPath,buffer); 3723 3724            if(buffersFirst == null) 3725            { 3726                buffersFirst = buffersLast = buffer; 3727                return; 3728            } 3729            //{{{ Sort buffer list 3730 else if(sortBuffers) 3731            { 3732                String str11, str12; 3733                if(sortByName) 3734                { 3735                    str11 = buffer.getName(); 3736                    str12 = buffer.getDirectory(); 3737                } 3738                else 3739                { 3740                    str11 = buffer.getDirectory(); 3741                    str12 = buffer.getName(); 3742                } 3743 3744                Buffer _buffer = buffersFirst; 3745                while(_buffer != null) 3746                { 3747                    String str21, str22; 3748                    if(sortByName) 3749                    { 3750                        str21 = _buffer.getName(); 3751                        str22 = _buffer.getDirectory(); 3752                    } 3753                    else 3754                    { 3755                        str21 = _buffer.getDirectory(); 3756                        str22 = _buffer.getName(); 3757                    } 3758 3759                    int comp = StandardUtilities.compareStrings(str11,str21,true); 3760                    if(comp < 0 || (comp == 0 && StandardUtilities.compareStrings(str12,str22,true) < 0)) 3761                    { 3762                        buffer.next = _buffer; 3763                        buffer.prev = _buffer.prev; 3764                        _buffer.prev = buffer; 3765                        if(_buffer != buffersFirst) 3766                            buffer.prev.next = buffer; 3767                        else 3768                            buffersFirst = buffer; 3769                        return; 3770                    } 3771 3772                    _buffer = _buffer.next; 3773                } 3774            } //}}} 3775 3776            buffer.prev = buffersLast; 3777            // fixes the hang that can occur if we 'save as' to a 3778 // new filename which requires re-sorting 3779 buffer.next = null; 3780            buffersLast.next = buffer; 3781            buffersLast = buffer; 3782        } 3783    } //}}} 3784 3785    //{{{ removeBufferFromList() method 3786 private static void removeBufferFromList(Buffer buffer) 3787    { 3788        synchronized(bufferListLock) 3789        { 3790            bufferCount--; 3791 3792            String path = buffer.getPath(); 3793            if(OperatingSystem.isCaseInsensitiveFS()) 3794                path = path.toLowerCase(); 3795 3796            bufferHash.remove(path); 3797 3798            if(buffer == buffersFirst && buffer == buffersLast) 3799            { 3800                buffersFirst = buffersLast = null; 3801                return; 3802            } 3803 3804            if(buffer == buffersFirst) 3805            { 3806                buffersFirst = buffer.next; 3807                buffer.next.prev = null; 3808            } 3809            else 3810            { 3811                buffer.prev.next = buffer.next; 3812            } 3813 3814            if(buffer == buffersLast) 3815            { 3816                buffersLast = buffersLast.prev; 3817                buffer.prev.next = null; 3818            } 3819            else 3820            { 3821                buffer.next.prev = buffer.prev; 3822            } 3823 3824            // fixes the hang that can occur if we 'save as' to a new 3825 // filename which requires re-sorting 3826 buffer.next = buffer.prev = null; 3827        } 3828    } //}}} 3829 3830    //{{{ addViewToList() method 3831 private static void addViewToList(View view) 3832    { 3833        viewCount++; 3834 3835        if(viewsFirst == null) 3836            viewsFirst = viewsLast = view; 3837        else 3838        { 3839            view.prev = viewsLast; 3840            viewsLast.next = view; 3841            viewsLast = view; 3842        } 3843    } //}}} 3844 3845    //{{{ removeViewFromList() method 3846 private static void removeViewFromList(View view) 3847    { 3848        viewCount--; 3849 3850        if(viewsFirst == viewsLast) 3851        { 3852            viewsFirst = viewsLast = null; 3853            return; 3854        } 3855 3856        if(view == viewsFirst) 3857        { 3858            viewsFirst = view.next; 3859            view.next.prev = null; 3860        } 3861        else 3862        { 3863            view.prev.next = view.next; 3864        } 3865 3866        if(view == viewsLast) 3867        { 3868            viewsLast = viewsLast.prev; 3869            view.prev.next = null; 3870        } 3871        else 3872        { 3873            view.next.prev = view.prev; 3874        } 3875    } //}}} 3876 3877    //{{{ closeView() method 3878 /** 3879     * closeView() used by exit(). 3880     */ 3881    private static void closeView(View view, boolean callExit) 3882    { 3883        PerspectiveManager.setPerspectiveDirty(true); 3884 3885        if(viewsFirst == viewsLast && callExit) 3886            exit(view,false); /* exit does editor event & save */ 3887        else 3888        { 3889            EditBus.send(new ViewUpdate(view,ViewUpdate.CLOSED)); 3890 3891            view.close(); 3892            removeViewFromList(view); 3893 3894            if(view == activeView) 3895                activeView = null; 3896        } 3897    } //}}} 3898 3899    //{{{ loadModeCatalog() method 3900 /** 3901     * Loads a mode catalog file. 3902     * @since jEdit 3.2pre2 3903     */ 3904    private static void loadModeCatalog(String path, boolean resource) 3905    { 3906        Log.log(Log.MESSAGE,jEdit.class,"Loading mode catalog file " + path); 3907 3908        ModeCatalogHandler handler = new ModeCatalogHandler( 3909            MiscUtilities.getParentOfPath(path),resource); 3910        try 3911        { 3912            InputStream _in; 3913            if(resource) 3914                _in = jEdit.class.getResourceAsStream(path); 3915            else 3916                _in = new FileInputStream(path); 3917            XMLUtilities.parseXML(_in, handler); 3918        } 3919        catch(IOException e) 3920        { 3921            Log.log(Log.ERROR,jEdit.class,e); 3922        } 3923    } //}}} 3924 3925    //{{{ initKeyBindings() method 3926 /** 3927     * Loads all key bindings from the properties. 3928     * @since 3.1pre1 3929     */ 3930    private static void initKeyBindings() 3931    { 3932        inputHandler.removeAllKeyBindings(); 3933 3934        ActionSet[] actionSets = getActionSets(); 3935        for(int i = 0; i < actionSets.length; i++) 3936        { 3937            actionSets[i].initKeyBindings(); 3938        } 3939    } //}}} 3940 3941    //}}} 3942 3943    //{{{ MyFocusManager class 3944 static class MyFocusManager extends DefaultKeyboardFocusManager 3945    { 3946        MyFocusManager() 3947        { 3948            setDefaultFocusTraversalPolicy(new LayoutFocusTraversalPolicy()); 3949        } 3950 3951        public boolean postProcessKeyEvent(KeyEvent evt) 3952        { 3953            if (Options.SIMPLIFIED_KEY_HANDLING) { 3954                boolean result; 3955 3956                /* 3957                    Commenting this out is experimental. 3958 3959                    This code (if not commented out) seems to be the cause for 3960                    https://sourceforge.net/tracker/index.php?func=detail&aid=1542026&group_id=588&atid=100588 3961 3962                    Because the simplified key handling is still experimental, breaking things here is still allowed. ;-) 3963 3964                    My intuition says that we should separate 3965                    (1) key sequences which invoke some special actions against 3966                    (2) key sequences which are ordinary input. 3967 3968                    While the former should be available in most or all jEdit windows, 3969                    the latter should be available only within jEdit buffers. 3970 3971                    Currently, it seems, both former and latter are handled globally, leading to the errorneous behaviour 3972                    of emitting keys to the buffer which are intendet to popup menus. 3973 3974                    Commenting this out leads to an inavailability of keyboard shortcuts if other windows than a View have the focus. (This is a regression.) 3975                    In the long term, we should really separate global key-sequence triggered actions from local input. 3976                */ 3977                if(!evt.isConsumed()) 3978                { 3979                    Component comp = (Component)evt.getSource(); 3980                    if(!comp.isShowing()) 3981                        return true; 3982 3983                    for(;;) 3984                    { 3985                        if(comp instanceof View) 3986                        { 3987                            ((View)comp).processKeyEvent(evt,View.VIEW,true); 3988                            return true; 3989                        } 3990                        else if(comp == null || comp instanceof Window 3991                            || comp instanceof JEditTextArea) 3992                        { 3993                            if (comp instanceof PluginManager) 3994                            { 3995                                evt.setSource(comp); 3996                                ((PluginManager)comp).processKeyEvents(evt); 3997                            } 3998                            break; 3999                        } 4000                        else 4001                            comp = comp.getParent(); 4002                    } 4003                } 4004 4005                result = super.postProcessKeyEvent(evt); 4006                 4007                return result; 4008            } else { 4009                if(!evt.isConsumed()) 4010                { 4011                    Component comp = (Component)evt.getSource(); 4012                    if(!comp.isShowing()) 4013                        return true; 4014     4015                    for(;;) 4016                    { 4017                        if(comp instanceof View) 4018                        { 4019                            ((View)comp).getInputHandler().processKeyEvent(evt, 4020                                View.VIEW, false); 4021                            return true; 4022                        } 4023                        else if(comp == null || comp instanceof Window 4024                            || comp instanceof JEditTextArea) 4025                        { 4026                            if (comp instanceof PluginManager) 4027                            { 4028                                evt.setSource(comp); 4029                                ((PluginManager)comp).processKeyEvents(evt); 4030                            } 4031                            break; 4032                        } 4033                        else 4034                            comp = comp.getParent(); 4035                    } 4036                } 4037     4038                return super.postProcessKeyEvent(evt); 4039            } 4040        } 4041    } //}}} 4042} 4043

A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame Popular Tags