diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/library/lib.ml b/library/lib.ml index df48bc7cbd..d0a015bd95 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -29,14 +29,17 @@ and library_segment = library_entry list let lib_stk = ref ([] : (section_path * node) list) let module_name = ref None -let path_prefix = ref (["Scratch"] : dir_path) +let path_prefix = ref ([Nametab.default_root] : dir_path) + +let module_sp () = + match !module_name with Some m -> m | None -> [Nametab.default_root] let recalc_path_prefix () = let rec recalc = function | (sp, OpenedSection _) :: _ -> let (pl,id,_) = repr_path sp in pl@[string_of_id id] | _::l -> recalc l - | [] -> (match !module_name with Some m -> m | None -> ["Scratch"]) + | [] -> module_sp () in path_prefix := recalc !lib_stk @@ -116,8 +119,10 @@ let check_for_module () = with Not_found -> () let start_module s = - if !module_name <> None then error "a module is already started"; - if !path_prefix <> ["Scratch"] then error "some sections are already opened"; + if !module_name <> None then + error "a module is already started"; + if !path_prefix <> [Nametab.default_root] then + error "some sections are already opened"; module_name := Some s; Univ.set_module s; let _ = add_anonymous_entry (Module s) in @@ -195,7 +200,10 @@ let reset_name id = in reset_to sp -let is_section_p sp = dirpath_prefix_of sp !path_prefix +(* [dir] is a section dir if [module] < [dir] <= [path_prefix] *) +let is_section_p sp = + not (dirpath_prefix_of sp (module_sp ())) + & (dirpath_prefix_of sp !path_prefix) (* State and initialization. *) |