diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6044767c2..cbb0ba664 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -340,13 +340,12 @@ let rec print_library_entry with_values ent = match ent with | (sp,Lib.Leaf lobj) -> [< print_leaf_entry with_values sep (sp,lobj) >] - | (_,Lib.OpenedSection (str,_)) -> - [< 'sTR(" >>>>>>> Section " ^ str); 'fNL >] + | (_,Lib.OpenedSection (id,_)) -> + [< 'sTR " >>>>>>> Section "; pr_id id; 'fNL >] | (sp,Lib.ClosedSection _) -> - [< 'sTR(" >>>>>>> Closed Section " ^ (string_of_id (basename sp))); - 'fNL >] + [< 'sTR " >>>>>>> Closed Section "; pr_id (basename sp); 'fNL >] | (_,Lib.Module dir) -> - [< 'sTR(" >>>>>>> Module " ^ (string_of_dirpath dir)); 'fNL >] + [< 'sTR " >>>>>>> Module "; pr_dirpath dir; 'fNL >] | (_,Lib.FrozenState _) -> [< >] @@ -377,10 +376,13 @@ let list_filter_vec f vec = frec (Array.length vec -1) [] let read_sec_context qid = - let sp, _ = Nametab.locate_module qid in + let dir = + try Nametab.locate_section qid + with Not_found -> error "Unknown section" in let rec get_cxt in_cxt = function - | ((sp',Lib.OpenedSection (str,_)) as hd)::rest -> - if sp' = sp then (hd::in_cxt) else get_cxt (hd::in_cxt) rest + | ((sp,Lib.OpenedSection (_,_)) as hd)::rest -> + let dir' = make_dirpath (wd_of_sp sp) in + if dir = dir' then (hd::in_cxt) else get_cxt (hd::in_cxt) rest | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in @@ -405,7 +407,7 @@ let print_eval red_fun env {uj_val=trm;uj_type=typ} = let print_name qid = try - let sp,_ = Nametab.locate_obj qid in + let sp = Nametab.locate_obj qid in let (sp,lobj) = let (sp,entry) = List.find (fun en -> (fst en) = sp) (Lib.contents_after None) |