equal
deleted
inserted
replaced
52 let val name = #name (Present.get_info thy) |
52 let val name = #name (Present.get_info thy) |
53 in if name = "" then [] else [name] end |
53 in if name = "" then [] else [name] end |
54 | NONE => []) |
54 | NONE => []) |
55 | _ => ["global"]); |
55 | _ => ["global"]); |
56 in |
56 in |
57 if name mem parents' then (gra', parents union parents') |
57 if member (op =) parents' name then (gra', parents union parents') |
58 else (Symtab.update (name, |
58 else (Symtab.update (name, |
59 {name = Sign.base_name name, ID = name, |
59 {name = Sign.base_name name, ID = name, |
60 dir = space_implode "/" (session @ prefx), |
60 dir = space_implode "/" (session @ prefx), |
61 unfold = false, path = "", parents = parents'}) gra', |
61 unfold = false, path = "", parents = parents'}) gra', |
62 name ins parents) |
62 name ins parents) |