summaryrefslogtreecommitdiff
path: root/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java
diff options
context:
space:
mode:
Diffstat (limited to 'Build/source/texk/tex4htk/java/xtpipes/FileInfo.java')
-rw-r--r--Build/source/texk/tex4htk/java/xtpipes/FileInfo.java170
1 files changed, 0 insertions, 170 deletions
diff --git a/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java b/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java
deleted file mode 100644
index 001b273dce1..00000000000
--- a/Build/source/texk/tex4htk/java/xtpipes/FileInfo.java
+++ /dev/null
@@ -1,170 +0,0 @@
-package xtpipes;
-/*
-FileInfo.java (2009-01-27-22:19)
-*/
-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;
-}
-
-}
-