equal
deleted
inserted
replaced
119 s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) |
119 s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s) |
120 |
120 |
121 fun import_name s = |
121 fun import_name s = |
122 if String.isSuffix ".thy" s then |
122 if String.isSuffix ".thy" s then |
123 error ("Malformed theory import: " ^ quote s) |
123 error ("Malformed theory import: " ^ quote s) |
124 else Path.base_name (Path.explode s); |
124 else Path.file_name (Path.explode s); |
125 |
125 |
126 |
126 |
127 (* header args *) |
127 (* header args *) |
128 |
128 |
129 local |
129 local |