changeset 48735 | 35c47932584c |
parent 48707 | ba531af91148 |
child 48755 | 393a37003851 |
--- a/src/Pure/PIDE/document.ML Wed Aug 08 14:30:27 2012 +0200 +++ b/src/Pure/PIDE/document.ML Fri Jul 27 20:54:01 2012 +0200 @@ -378,8 +378,8 @@ (* FIXME provide files via Scala layer, not master_dir *) val (dir, header) = get_header node; val master_dir = - (case Url.explode dir of - Url.File path => path + (case try Url.explode dir of + SOME (Url.File path) => path | _ => Path.current); val parents = #imports header |> map (fn import =>