equal
deleted
inserted
replaced
71 val root_file = ThyLoad.ml_path "ROOT"; |
71 val root_file = ThyLoad.ml_path "ROOT"; |
72 *) |
72 *) |
73 |
73 |
74 fun get_rpath rpath_str = |
74 fun get_rpath rpath_str = |
75 (if rpath_str = "" then () else |
75 (if rpath_str = "" then () else |
76 if isSome (!rpath) then |
76 if is_some (! rpath) then |
77 error "Path for remote theory browsing information may only be set once" |
77 error "Path for remote theory browsing information may only be set once" |
78 else |
78 else |
79 rpath := SOME (Url.unpack rpath_str); |
79 rpath := SOME (Url.unpack rpath_str); |
80 (!rpath, rpath_str <> "")); |
80 (!rpath, rpath_str <> "")); |
81 |
81 |