equal
deleted
inserted
replaced
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 name mem parents' then (gra', parents union parents') |
58 else (Symtab.update ((name, |
58 else (Symtab.curried_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) |
63 end |
63 end |
64 else (gra, name ins parents) |
64 else (gra, name ins parents) |
65 else |
65 else |
66 make_deps_graph prf' (gra, parents) |
66 make_deps_graph prf' (gra, parents) |