jedit.java

Java写的文本编辑器

		newView.show();

		return newView;
	}

	/**
	 * Closes a view. jEdit will exit if this was the last open view.
	 */
	public static void closeView(View view)
	{
		closeView(view,true);
	}

	/**
	 * Returns an array of all open views.
	 */
	public static View[] getViews()
	{
		View[] views = new View[viewCount];
		View view = viewsFirst;
		for(int i = 0; i < viewCount; i++)
		{
			views[i] = view;
			view = view.next;
		}
		return views;
	}

	/**
	 * Returns the number of open views.
	 */
	public static int getViewCount()
	{
		return viewCount;
	}

	/**
	 * Returns the first view.
	 */
	public static View getFirstView()
	{
		return viewsFirst;
	}

	/**
	 * Returns the last view.
	 */
	public static View getLastView()
	{
		return viewsLast;
	}

	/**
	 * Returns the jEdit install directory.
	 */
	public static String getJEditHome()
	{
		return jEditHome;
	}

	/**
	 * Returns the user settings directory.
	 */
	public static String getSettingsDirectory()
	{
		return settingsDirectory;
	}

	/**
	 * Saves all user preferences to disk.
	 */
	public static void saveSettings()
	{
		if(settingsDirectory != null)
		{
			// Save the recent file list
			File file = new File(MiscUtilities.constructPath(
				settingsDirectory, "recent.xml"));
			if(file.exists() && file.lastModified() != recentModTime)
			{
				Log.log(Log.WARNING,jEdit.class,file + " changed"
					+ " on disk; will not save recent files");
			}
			else
			{
				BufferHistory.save(file);
			}
			recentModTime = file.lastModified();

			file = new File(MiscUtilities.constructPath(
				settingsDirectory, "history"));
			if(file.exists() && file.lastModified() != historyModTime)
			{
				Log.log(Log.WARNING,jEdit.class,file + " changed"
					+ " on disk; will not save history");
			}
			else
			{
				HistoryModel.saveHistory(file);
			}
			historyModTime = file.lastModified();

			SearchAndReplace.save();
			Abbrevs.save();
			FavoritesVFS.saveFavorites();

			file = new File(MiscUtilities.constructPath(
				settingsDirectory,"properties"));
			if(file.exists() && file.lastModified() != propsModTime)
			{
				Log.log(Log.WARNING,jEdit.class,file + " changed"
					+ " on disk; will not save user properties");
			}
			else
			{
				try
				{
					OutputStream out = new FileOutputStream(file);
					props.save(out,"jEdit properties");
					out.close();
				}
				catch(IOException io)
				{
					Log.log(Log.ERROR,jEdit.class,io);
				}

				propsModTime = file.lastModified();
			}
		}
	}

	/**
	 * Exits cleanly from jEdit, prompting the user if any unsaved files
	 * should be saved first.
	 * @param view The view from which this exit was called
	 * @param reallyExit If background mode is enabled and this parameter
	 * is true, then jEdit will close all open views instead of exiting
	 * entirely.
	 */
	public static void exit(View view, boolean reallyExit)
	{
		// Wait for pending I/O requests
		VFSManager.waitForRequests();

		// Send EditorExitRequested
		EditBus.send(new EditorExitRequested(view));

		// Even if reallyExit is false, we still exit properly
		// if background mode is off
		reallyExit |= !background;

		saveOpenFiles(view);

		// Close all buffers
		if(!closeAllBuffers(view,reallyExit))
			return;

		// If we are running in background mode and
		// reallyExit was not specified, then return here.
		if(!reallyExit)
		{
			// in this case, we can't directly call
			// view.close(); we have to call closeView()
			// for all open views
			view = viewsFirst;
			while(view != null)
			{
				closeView(view,false);
				view = view.next;
			}

			// Save settings in case user kills the backgrounded
			// jEdit process
			saveSettings();

			return;
		}

		// Save view properties here - it unregisters
		// listeners, and we would have problems if the user
		// closed a view but cancelled an unsaved buffer close
		view.close();

		// Stop autosave timer
		Autosave.stop();

		// Stop server
		if(server != null)
			server.stopServer();

		// Stop all plugins
		EditPlugin[] plugins = getPlugins();
		for(int i = 0; i < plugins.length; i++)
		{
			plugins[i].stop();
		}

		// Send EditorExiting
		EditBus.send(new EditorExiting(null));

		// Save settings
		saveSettings();

		// Close activity log stream
		Log.closeStream();

		// Byebye...
		System.exit(0);
	}

	// package-private members

	/**
	 * If buffer sorting is enabled, this repositions the buffer.
	 */
	static void updatePosition(Buffer buffer)
	{
		if(sortBuffers)
		{
			removeBufferFromList(buffer);
			addBufferToList(buffer);
		}
	}

	/**
	 * Do not call this method. It is only public so that classes
	 * in the org.gjt.sp.jedit.syntax package can access it.
	 * @param mode The edit mode
	 */
	public static void addMode(Mode mode)
	{
		Log.log(Log.DEBUG,jEdit.class,"Adding edit mode "
			+ mode.getName());

		modes.addElement(mode);
	}

	/**
	 * Loads an XML-defined edit mode from the specified reader.
	 * @param mode The edit mode
	 */
	/* package-private */ static void loadMode(Mode mode)
	{
		Object fileName = mode.getProperty("file");

		Log.log(Log.NOTICE,jEdit.class,"Loading edit mode " + fileName);

		XmlParser parser = new XmlParser();
		XModeHandler xmh = new XModeHandler(parser,mode.getName(),fileName.toString());
		parser.setHandler(xmh);
		try
		{
			Reader grammar;
			if(fileName instanceof URL)
			{
				grammar = new BufferedReader(
					new InputStreamReader(
					((URL)fileName).openStream()));
			}
			else
			{
				grammar = new BufferedReader(new FileReader(
					(String)fileName));
			}

			parser.parse(null, null, grammar);
		}
		catch (Exception e)
		{
			Log.log(Log.ERROR, jEdit.class, e);

			if (e instanceof XmlException)
			{
				XmlException xe = (XmlException) e;
				int line = xe.getLine();
				String message = xe.getMessage();

				Object[] args = { fileName, new Integer(line), message };
				GUIUtilities.error(null,"xmode-parse",args);
			}

			// give it an empty token marker to avoid problems
			TokenMarker marker = new TokenMarker();
			marker.addRuleSet("MAIN",new ParserRuleSet());
			mode.setTokenMarker(marker);
		}
	}

	/**
	 * Loads the properties from the specified input stream. This
	 * calls the <code>load()</code> method of the properties object
	 * and closes the stream.
	 * @param in The input stream
	 * @param def If true, the properties will be loaded into the
	 * default table
	 * @exception IOException if an I/O error occured
	 */
	/* package-private */ static void loadProps(InputStream in, boolean def)
		throws IOException
	{
		in = new BufferedInputStream(in);
		if(def)
			defaultProps.load(in);
		else
			props.load(in);
		in.close();
	}

	/**
	 * Adds a plugin to the editor.
	 * @param plugin The plugin
	 */
	/* package-private */ static void addPlugin(EditPlugin plugin)
	{
		plugins.addPlugin(plugin);
	}

	/**
	 * Loads the specified action list.
	 * @since jEdit 3.1pre1
	 */
	/* package-private */ static boolean loadActions(String path, Reader in,
		boolean plugin)
	{
		Log.log(Log.DEBUG,jEdit.class,"Loading actions from " + path);

		ActionListHandler ah = new ActionListHandler(path,plugin);
		XmlParser parser = new XmlParser();
		parser.setHandler(ah);
		try
		{
			parser.parse(null, null, in);
			return true;
		}
		catch(XmlException xe)
		{
			int line = xe.getLine();
			String message = xe.getMessage();
			Log.log(Log.ERROR,jEdit.class,path + ":" + line
				+ ": " + message);
		}
		catch(Exception e)
		{
			Log.log(Log.ERROR,jEdit.class,e);
		}

		return false;
	}

	// private members
	private static String jEditHome;
	private static String settingsDirectory;
	private static long propsModTime, historyModTime, recentModTime;
	private static Properties defaultProps;
	private static Properties props;
	private static EditServer server;
	private static boolean background;
	private static Hashtable actionHash;
	private static Vector jars;
	private static EditPlugin.JAR plugins; /* plugins without a JAR */
	private static Vector modes;
	private static Vector recent;
	private static boolean saveCaret;
	private static InputHandler inputHandler;

	// buffer link list
	private static boolean sortBuffers;
	private static boolean sortByName;
	private static int bufferCount;
	private static Buffer buffersFirst;
	private static Buffer buffersLast;

	// view link list
	private static int viewCount;
	private static View viewsFirst;
	private static View viewsLast;

	private jEdit() {}

	private static void usage()
	{
		System.out.println("Usage: jedit [<options>] [<files>]");

		System.out.println("	<file> +marker:<marker>: Positions caret"
			+ " at marker <marker>");
		System.out.println("	<file> +line:<line>: Positions caret"
			+ " at line number <line>");
		System.out.println("	--: End of options");
		System.out.println("	-background: Run in background mode");
		System.out.println("	-norestore: Don't restore previously open files");
		System.out.println("	-run=<script>: Run the specified BeanShell script");
		System.out.println("	-server: Read/write server"
			+ " info from/to $HOME/.jedit/server");
		System.out.println("	-server=<name>: Read/write server"
			+ " info from/to $HOME/.jedit/<name>");
		System.out.println("	-noserver: Don't start edit server");
		System.out.println("	-settings=<path>: Load user-specific"
			+ " settings from <path>");
		System.out.println("	-nosettings: Don't load user-specific"
			+ " settings");
		System.out.println("	-nostartupscripts: Don't run startup scripts");
		System.out.println("	-version: Print jEdit version and exit");
		System.out.println("	-usage: Print this message and exit");
		System.out.println();
		System.out.println("To set minimum activity log level,"
			+ " specify a number as the first");
		System.out.println("command line parameter"
			+ " (1-9, 1 = print everything, 9 = fatal errors only)");
		System.out.println();
		System.out.println("Report bugs to Slava Pestov <[e-mail]>.");
	}

	private static void version()
	{
		System.out.println("jEdit " + getVersion());
	}

	/**
	 * Creates a BeanShell script that can be sent to a running edit server.
	 */
	private static String makeServerScript(boolean restore,
		String[] args, String scriptFile)
	{
		StringBuffer script = new StringBuffer();

		String userDir = System.getProperty("user.dir");

		script.append("parent = \"");
		script.append(MiscUtilities.charsToEscapes(userDir));
		script.append("\";\n");

		script.append("args = new String[");
		script.append(args.length);
		script.append("];\n");

		for(int i = 0; i < args.length; i++)
		{
			script.append("args[");
			script.append(i);
			script.append("] = ");

			if(args[i] == null)
				script.append("null");
			else
			{
				script.append('"');
				script.append(MiscUtilities.charsToEscapes(args[i]));
				script.append('"');
			}

			script.append(";\n");
		}

		script.append("EditServer.handleClient(" + restore + ",parent,args);\n");

		if(scriptFile != null)
		{
			scriptFile = MiscUtilities.constructPath(userDir,scriptFile);
			script.append("BeanShell.runScript(null,\""
				+ MiscUtilities.charsToEscapes(scriptFile)
				+ "\",false,false);\n");
		}

		return script.toString();
	}

	/**
	 * Initialise various objects, register protocol handlers.
	 */
	private static void initMisc()
	{
		// Add our protocols to java.net.URL's list
		System.getProperties().put("java.protocol.handler.pkgs",
			"org.gjt.sp.jedit.proto|" +
			System.getProperty("java.protocol.handler.pkgs",""));

		inputHandler = new DefaultInputHandler(null);

		/* Determine installation directory.
		 * If the jedit.home property is set, use that.
		 * Then, look for jedit.jar in the classpath.
		 * If that fails, assume this is the web start version. */
		jEditHome = System.getProperty("jedit.home");
		if(jEditHome == null)
		{
			String classpath = System
				.getProperty("java.class.path");
			int index = classpath.toLowerCase()
				.indexOf("jedit.jar");
			int start = classpath.lastIndexOf(File
				.pathSeparator,index) + 1;
			// if started with java -jar jedit.jar
			/* if(classpath.equalsIgnoreCase("jedit.jar"))
			{
				jEditHome = System.getProperty("user.dir");
			}
			else */ if(index > start)
			{
				jEditHome = classpath.substring(start,
					index - 1);
			}
			else
			{
				// check if web start
				/* if(jEdit.class.getResource("/modes/catalog") != null)
				{
					// modes bundled in; hence web start
					jEditHome = null;
				}
				else */
				{
					// use user.dir as last resort
					jEditHome = System.getProperty("user.dir");
				}
			}
		}

		Log.log(Log.MESSAGE,jEdit.class,"jEdit home directory is " + jEditHome);

		//if(jEditHome == null)
		//	Log.log(Log.DEBUG,jEdit.class,"Web start mode");

		actionHash = new Hashtable();

		plugins = new EditPlugin.JAR(null,null);
		jars = new Vector();
	}

	/**
	 * Load system properties.
	 */
	private static void initSystemProperties()
	{
		defaultProps = props = new Properties();

		try
		{
			loadProps(jEdit.class.getResourceAsStream(
				"/org/gjt/sp/jedit/jedit.props"),true);
			loadProps(jEdit.class.getResourceAsStream(
				"/org/gjt/sp/jedit/jedit_gui.props"),true);
			loadProps(jEdit.class.getResourceAsStream(
				"/org/gjt/sp/jedit/jedit_keys.props"),true);
		}
		catch(Exception e)
		{
			Log.log(Log.ERROR,jEdit.class,
				"Error while loading system properties!");
			Log.log(Log.ERROR,jEdit.class,
				"One of the following property files could not be loaded:\n"
				+ "- jedit.props\n"
				+ "- jedit_gui.props\n"
				+ "- jedit_keys.props\n"
				+ "jedit.jar is probably corrupt.");
			Log.log(Log.ERROR,jEdit.class,e);
			System.exit(1);
		}
	}

	/**
	 * Load site properties.
	 */