equal
deleted
inserted
replaced
88 s match { |
88 s match { |
89 case Split_File_Name(s1, s2) => Some((s1, s2)) |
89 case Split_File_Name(s1, s2) => Some((s1, s2)) |
90 case _ => None |
90 case _ => None |
91 } |
91 } |
92 |
92 |
|
93 def dir_name(s: String): String = |
|
94 split_file_name(s) match { |
|
95 case Some((dir, _)) => dir |
|
96 case None => "" |
|
97 } |
|
98 |
93 def import_name(s: String): String = |
99 def import_name(s: String): String = |
94 s match { |
100 s match { |
95 case File_Name(name) if !name.endsWith(".thy") => name |
101 case File_Name(name) if !name.endsWith(".thy") => name |
96 case _ => error("Malformed theory import: " + quote(s)) |
102 case _ => error("Malformed theory import: " + quote(s)) |
97 } |
103 } |