# HG changeset patch # User wenzelm # Date 963523214 -7200 # Node ID 07598d493d331236e0a1452ca3e2199fb6b29dab # Parent 1625c1f172b34d6ab646a1c78fcb62445e539076 tuned; diff -r 1625c1f172b3 -r 07598d493d33 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Thu Jul 13 23:19:40 2000 +0200 +++ b/src/Pure/Thy/thy_info.ML Thu Jul 13 23:20:14 2000 +0200 @@ -81,9 +81,8 @@ (* derived graph operations *) -fun add_deps name parents G = - foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents) - handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess)); +fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G + handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess)); fun upd_deps name entry G = foldl (fn (H, parent) => Graph.del_edge (parent, name) H) (G, Graph.imm_preds G name) @@ -126,7 +125,7 @@ (* access thy *) fun lookup_thy name = - Some (thy_graph Graph.get_node name) handle Graph.UNDEFINED _ => None; + Some (thy_graph Graph.get_node name) handle Graph.UNDEF _ => None; val known_thy = is_some o lookup_thy; fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false); @@ -157,7 +156,7 @@ (mapfilter (apsome #1 o #2) files)); fun get_preds name = - (thy_graph Graph.imm_preds name) handle Graph.UNDEFINED _ => + (thy_graph Graph.imm_preds name) handle Graph.UNDEF _ => error (loader_msg "nothing known about theory" [name]); @@ -417,7 +416,7 @@ fun register G = (Graph.new_node (name, (None, Some theory)) G - handle Graph.DUPLICATE _ => err "duplicate theory entry" []) + handle Graph.DUP _ => err "duplicate theory entry" []) |> add_deps name parent_names; in if not (null nonfinished) then err "non-finished parent theories" nonfinished