equal
deleted
inserted
replaced
78 |
78 |
79 def platform_file(path: String) = |
79 def platform_file(path: String) = |
80 new File(platform_path(path)) |
80 new File(platform_path(path)) |
81 |
81 |
82 |
82 |
83 /* processes */ |
83 /* source files */ |
|
84 |
|
85 private def try_file(file: File) = if (file.isFile) Some(file) else None |
|
86 |
|
87 def source_file(path: String): Option[File] = { |
|
88 if (path == "ML") None |
|
89 else if (path.startsWith("/") || path == "") |
|
90 try_file(platform_file(path)) |
|
91 else { |
|
92 val pure_file = platform_file("~~/src/Pure/" + path) |
|
93 if (pure_file.isFile) Some(pure_file) |
|
94 else if (getenv("ML_SOURCES") != "") |
|
95 try_file(platform_file("$ML_SOURCES/" + path)) |
|
96 else None |
|
97 } |
|
98 } |
|
99 |
|
100 |
|
101 /* shell processes */ |
84 |
102 |
85 def execute(redirect: Boolean, args: String*): Process = { |
103 def execute(redirect: Boolean, args: String*): Process = { |
86 val cmdline = new java.util.LinkedList[String] |
104 val cmdline = new java.util.LinkedList[String] |
87 if (is_cygwin) cmdline.add(platform_path("/bin/env")) |
105 if (is_cygwin) cmdline.add(platform_path("/bin/env")) |
88 for (s <- args) cmdline.add(s) |
106 for (s <- args) cmdline.add(s) |
147 |
165 |
148 /* symbols */ |
166 /* symbols */ |
149 |
167 |
150 private def read_symbols(path: String) = { |
168 private def read_symbols(path: String) = { |
151 val file = new File(platform_path(path)) |
169 val file = new File(platform_path(path)) |
152 if (file.canRead) Source.fromFile(file).getLines |
170 if (file.isFile) Source.fromFile(file).getLines |
153 else Iterator.empty |
171 else Iterator.empty |
154 } |
172 } |
155 val symbols = new Symbol.Interpretation( |
173 val symbols = new Symbol.Interpretation( |
156 read_symbols("$ISABELLE_HOME/etc/symbols") ++ |
174 read_symbols("$ISABELLE_HOME/etc/symbols") ++ |
157 read_symbols("$ISABELLE_HOME_USER/etc/symbols")) |
175 read_symbols("$ISABELLE_HOME_USER/etc/symbols")) |