Skip to content
Snippets Groups Projects
Select Git revision
  • c04de39ed852815eb1b7ab7217bd08dc621ddd68
  • master default protected
  • towards_1.8.0
  • updateTLC
  • 1.1.0-stups
  • 1.0.2-stups
  • 1.0.1-stups
  • 1.0.0-stups
8 results

FilenameToStream.java

Blame
  • Code owners
    Assign users and groups as approvers for specific file changes. Learn more.
    FilenameToStream.java 3.53 KiB
    // Copyright (c) 2003 Compaq Corporation.  All rights reserved.
    // Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
    package util;
    
    import java.io.File;
    import java.util.regex.Pattern;
    
    
    /**
     * Resolver for the name to file handle.
     *
     * LL comment: 24 July 2013: I believe that the only classes that implements this
     * are SimpleFileNameToStream, RCPNameToFileIStream, and RMIFilenameToStreamResolver.
     * I added the isStandardModule method.
     *
     * @author Leslie Lamport
     * @author Simon Zambrovski
     */
    public interface FilenameToStream
    {
    
    	/*
    	 * Higher layers of TLC (and the Toolbox) have to determine if a module was
    	 * loaded from a library location s.a. those defined by TLA_LIBRARY (see
    	 * SimpleFilenameToStream). Thus, capture this information at module load
    	 * time when it is known where a module was loaded from.
    	 */
    	@SuppressWarnings("serial")
    	public static class TLAFile extends File {
    		// The following regex is concerned with determining whether the provided 'parent' string to our
    		//	parent/child constructor looks like the start of a legal absolute file path potentially including
    		//	a drive letter.
    		private static final String ROOT_PATH_REGEX
    								= "^([a-zA-Z]+:)?" + ((File.separatorChar == '\\') ? "\\\\" : File.separator);
    		private static final Pattern ROOT_PATH_PATTERN = Pattern.compile(ROOT_PATH_REGEX);
    		
    		
    		private final boolean isLibraryModule;
    		private transient final FilenameToStream resolver;
    
    		public TLAFile(String pathname, FilenameToStream fts) {
    			this(pathname, false, fts);
    		}
    
    		public TLAFile(String pathname, boolean isLibraryModule, FilenameToStream fts) {
    			super(pathname);
    			this.isLibraryModule = isLibraryModule;
    			this.resolver = fts;
    		}
    
    		public TLAFile(String parent, String child, FilenameToStream fts) {
    			super(parent,
    				  ((ROOT_PATH_PATTERN.matcher(parent).find() && child.startsWith(parent))
    						  ? child.substring(parent.length())
    					      : child));
    			this.isLibraryModule = false;
    			this.resolver = fts;
    		}
    
    		public boolean isLibraryModule() {
    			return isLibraryModule;
    		}
    
    		/**
    		 * @return null if no TLC module override for this module exists.
    		 */
    		public File getModuleOverride() {
    			final File moduleOverride = resolver.resolve(getName().replaceAll(".tla$", ".class"), false);
    			if (moduleOverride.exists()) {
    				// resolve(...) return a File instance even if the file doesn't exist.