equal
deleted
inserted
replaced
28 |
28 |
29 |
29 |
30 /* file name */ |
30 /* file name */ |
31 |
31 |
32 val Thy_Path1 = new Regex("([^/]*)\\.thy") |
32 val Thy_Path1 = new Regex("([^/]*)\\.thy") |
33 val Thy_Path2 = new Regex("(.*/)([^/]*)\\.thy") |
33 val Thy_Path2 = new Regex("(.*)/([^/]*)\\.thy") |
34 |
34 |
35 def split_thy_path(path: String): Option[(String, String)] = |
35 def split_thy_path(path: String): Option[(String, String)] = |
36 path match { |
36 path match { |
37 case Thy_Path1(name) => Some(("", name)) |
37 case Thy_Path1(name) => Some(("", name)) |
38 case Thy_Path2(dir, name) => Some((dir, name)) |
38 case Thy_Path2(dir, name) => Some((dir, name)) |