# HG changeset patch # User wenzelm # Date 1358102732 -3600 # Node ID 5fc8b83322f5c9103746c30cdd11356ea5e24e7c # Parent e32a283b8ce0528d3547e717175e74dd1656abb7 more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress; diff -r e32a283b8ce0 -r 5fc8b83322f5 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sun Jan 13 15:04:55 2013 +0100 +++ b/src/Pure/PIDE/document.ML Sun Jan 13 19:45:32 2013 +0100 @@ -71,7 +71,7 @@ perspective: perspective, (*visible commands, last*) entries: (exec_id * exec) option Entries.T * bool, (*command entries with excecutions, stable*) result: exec option} (*result of last execution*) -and version = Version of node Graph.T (*development graph wrt. static imports*) +and version = Version of node String_Graph.T (*development graph wrt. static imports*) with fun make_node (header, perspective, entries, result) = @@ -134,9 +134,10 @@ fun set_result result = map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); -fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; -fun default_node name = Graph.default_node (name, empty_node); -fun update_node name f = default_node name #> Graph.map_node name f; +fun get_node nodes name = String_Graph.get_node nodes name + handle String_Graph.UNDEF _ => empty_node; +fun default_node name = String_Graph.default_node (name, empty_node); +fun update_node name f = default_node name #> String_Graph.map_node name f; (* node edits and associated executions *) @@ -182,7 +183,7 @@ (* version operations *) -val empty_version = Version Graph.empty; +val empty_version = Version String_Graph.empty; fun nodes_of (Version nodes) = nodes; val node_of = get_node o nodes_of; @@ -204,12 +205,12 @@ |> default_node name |> fold default_node imports; val nodes2 = nodes1 - |> Graph.Keys.fold - (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); + |> String_Graph.Keys.fold + (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name); val (nodes3, errors2) = - (Graph.add_deps_acyclic (name, imports) nodes2, errors1) - handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); - in Graph.map_node name (set_header (master, header, errors2)) nodes3 end + (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1) + handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); + in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end | Perspective perspective => update_node name (set_perspective perspective) nodes); fun put_node (name, node) (Version nodes) = @@ -294,7 +295,7 @@ val commands' = (versions', Inttab.empty) |-> Inttab.fold (fn (_, version) => nodes_of version |> - Graph.fold (fn (_, (node, _)) => node |> + String_Graph.fold (fn (_, (node, _)) => node |> iterate_entries (fn ((_, id), _) => SOME o Inttab.insert (K true) (id, the_command state id)))); in (versions', commands', execution) end); @@ -339,7 +340,7 @@ {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true} (fn () => (OS.Process.sleep (seconds 0.02); - nodes_of (the_version state version_id) |> Graph.schedule + nodes_of (the_version state version_id) |> String_Graph.schedule (fn deps => fn (name, node) => if not (visible_node node) andalso finished_theory node then Future.value () @@ -366,13 +367,13 @@ fun make_required nodes = let val all_visible = - Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] - |> Graph.all_preds nodes + String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] + |> String_Graph.all_preds nodes |> map (rpair ()) |> Symtab.make; val required = Symtab.fold (fn (a, ()) => - exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? + exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ? Symtab.update (a, ())) all_visible Symtab.empty; in Symtab.defined required end; @@ -476,7 +477,7 @@ val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state); val updated = timeit "Document.update" (fn () => - nodes |> Graph.schedule + nodes |> String_Graph.schedule (fn deps => fn (name, node) => (singleton o Future.forks) {name = "Document.update", group = NONE, diff -r e32a283b8ce0 -r 5fc8b83322f5 src/Pure/Thy/thy_info.ML --- a/src/Pure/Thy/thy_info.ML Sun Jan 13 15:04:55 2013 +0100 +++ b/src/Pure/Thy/thy_info.ML Sun Jan 13 19:45:32 2013 +0100 @@ -55,11 +55,11 @@ (* derived graph operations *) -fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G - handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); +fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G + handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); fun new_entry name parents entry = - Graph.new_node (name, entry) #> add_deps name parents; + String_Graph.new_node (name, entry) #> add_deps name parents; (* thy database *) @@ -74,7 +74,8 @@ fun base_name s = Path.implode (Path.base (Path.explode s)); local - val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T); + val database = + Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T); in fun get_thys () = ! database; fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f); @@ -85,13 +86,13 @@ fun thy_graph f x = f (get_thys ()) x; -fun get_names () = Graph.topological_order (get_thys ()); +fun get_names () = String_Graph.topological_order (get_thys ()); (* access thy *) fun lookup_thy name = - SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE; + SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE; val known_thy = is_some o lookup_thy; @@ -139,10 +140,10 @@ if is_finished name then error (loader_msg "attempt to change finished theory" [name]) else let - val succs = thy_graph Graph.all_succs [name]; + val succs = thy_graph String_Graph.all_succs [name]; val _ = Output.urgent_message (loader_msg "removing" succs); val _ = List.app (perform Remove) succs; - val _ = change_thys (fold Graph.del_node succs); + val _ = change_thys (fold String_Graph.del_node succs); in () end); fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () => @@ -179,13 +180,13 @@ (Thm.join_theory_proofs thy; Future.join present; commit (); thy); val schedule_seq = - Graph.schedule (fn deps => fn (_, task) => + String_Graph.schedule (fn deps => fn (_, task) => (case task of Task (parents, body) => finish_thy (body (task_parents deps parents)) | Finished thy => thy)) #> ignore; val schedule_futures = uninterruptible (fn _ => - Graph.schedule (fn deps => fn (name, task) => + String_Graph.schedule (fn deps => fn (name, task) => (case task of Task (parents, body) => (singleton o Future.forks) @@ -265,7 +266,7 @@ val path = Path.expand (Path.explode str); val name = Path.implode (Path.base path); in - (case try (Graph.get_node tasks) name of + (case try (String_Graph.get_node tasks) name of SOME task => (task_finished task, tasks) | NONE => let @@ -305,7 +306,7 @@ (* use_thy *) fun use_thys_wrt dir arg = - schedule_tasks (snd (require_thys [] dir arg Graph.empty)); + schedule_tasks (snd (require_thys [] dir arg String_Graph.empty)); val use_thys = use_thys_wrt Path.current; val use_thy = use_thys o single; @@ -340,6 +341,6 @@ (* finish all theories *) -fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry))); +fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); end;