diff options
Diffstat (limited to 'Build/source/texk/tex4htk/java/xtpipes/FileInfo.java')
-rwxr-xr-x | Build/source/texk/tex4htk/java/xtpipes/FileInfo.java | 170 |
1 files changed, 170 insertions, 0 deletions
diff --git a/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java b/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java new file mode 100755 index 00000000000..f951ec3bdb8 --- /dev/null +++ b/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java @@ -0,0 +1,170 @@ +package xtpipes; +/* +FileInfo.java (2008-01-26-00:38) +*/ +import java.io.File; +import java.io.PrintWriter; + +public class FileInfo{ + static String [] classPaths = null; +static String [] scriptPaths = null; +static java.util.HashMap <String,String> registry = + new java.util.HashMap <String,String>(); +static String slash = System.getProperty("file.separator"); +static String ii_scriptDir; +static PrintWriter log; +static boolean trace; + + public FileInfo(PrintWriter log, String iii_scriptDir, boolean trace){ + FileInfo.log = log; + FileInfo.ii_scriptDir = iii_scriptDir; + FileInfo.trace = trace; + classPaths = FileInfo.getPaths( System.getProperty("java.class.path") ); +if( iii_scriptDir != null ){ + scriptPaths = FileInfo.getPaths( iii_scriptDir ); +} + + + } + public static String searchFile( String file ){ + String key = ((ii_scriptDir == null)? "" : ii_scriptDir ) + + "!" + file; + String result = (String) registry.get( key ); + if( result == null ){ + for(int i=0; i<2; i++){ + if( trace ){ + log.println( "Searching: " + file ); + } + if( (new File(file)).exists() ){ + result = ( file.indexOf(slash) == -1 )? + (System.getProperty("user.dir") + slash + file) + : + file; + } + else { + if( ii_scriptDir != null ){ + int k = scriptPaths.length; +while( k>0 ){ + k--; + if( trace ){ + log.println( "Searching: " + file + + ", recursively in directory: " + scriptPaths[k] ); + } + result = searchDirectory( new File(scriptPaths[k]), file); + if( result != null ){ break; } +} +String s = ii_scriptDir + file; +if( (new File( s )).exists() ){ result = s; } + + } + if( result == null ){ + int k = classPaths.length; +String toFile = "xtpipes" + slash + "lib" + slash + file; +while( k>0 ){ + k--; + String s = classPaths[k] + toFile; + if( trace ){ log.println( "Searching: " + s ); } + if( new File(s).exists() ){ result = s; break; } +} + + } } + if( result != null ){ break; } + file = new File(file).getName(); + } + if( result != null ){ + result = FileInfo.cleanPath(result); + registry.put(key, result); + } + } + if( trace ){ + if( result == null ){ + log.println( + "Directory paths from xtpipes command line option -i: " + + ii_scriptDir ); + } else { log.println( "Found: " + result + "\n" ); } + log.flush(); + } + return result; +} + + static String [] getPaths( String dirs ){ + String [] paths = null; + paths = dirs.split( System.getProperty("path.separator") ); + int k = paths.length; + while( k>0 ){ + k--; + paths[k] = cleanPath( paths[k] ); + + int len = paths[k].length(); + if( (len>1) && (paths[k].lastIndexOf(slash + ".") == (len-1)) ){ + paths[k] = paths[k].substring(0,len-1); + } else if( (len>0) && ((len-1) != paths[k].lastIndexOf( slash )) ){ + paths[k] += slash; + } } + return paths; +} + + public static String cleanPath( String path ){ + String slash = System.getProperty("file.separator"); + String userDir = System.getProperty( "user.dir" ); + if( (path.length() > 0) && (path.charAt(0) == '~') ){ + if( (path.length() == 1) || (path.charAt(1) != '~') ){ + path = System.getProperty( "user.home" ) + + path.substring(1); + } } + + if( path.startsWith("..") ){ + path = userDir.substring(0, + Math.max(0,Math.max( + userDir.lastIndexOf("/") + , + userDir.lastIndexOf("\\") + ))) + + path.substring(2); + } + if( path.startsWith(".") ){ + path = userDir + slash + path.substring(1); + } + + int i; + while( + ((i=path.indexOf("/..")) != -1) + || + ((i=path.indexOf("\\..")) != -1) + ){ + String s = path.substring(0,i); + int j = Math.max(s.lastIndexOf("/"), s.lastIndexOf("\\")); + path = path.substring(0,j) + path.substring(i+3); + } + while( + ((i=path.indexOf("/.")) != -1) + || + ((i=path.indexOf("\\.")) != -1) + ){ + String s = path.substring(0,i); + int j = Math.max(s.indexOf("/"), s.indexOf("\\")); + path = path.substring(0,j) + path.substring(i+2); + } + + return path; +} + + static String searchDirectory(File dir, String file) { + String result = null; + if( dir.isDirectory() ){ + String [] children = dir.list(); + for (int i=0; i<children.length; i++) { + result = searchDirectory( new File(dir,children[i]), file); + if( result != null ) { break; } + } + } else { + String s = dir.toString(); + if( s.equals(file) || s.endsWith(slash + file) ){ + result = s; + } + } + return result; +} + +} + |