more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
authorwenzelm
Sun Jan 13 19:45:32 2013 +0100 (2013-01-13)
changeset 508625fc8b83322f5
parent 50860 e32a283b8ce0
child 50863 8f6046b7f850
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Jan 13 15:04:55 2013 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Jan 13 19:45:32 2013 +0100
     1.3 @@ -71,7 +71,7 @@
     1.4    perspective: perspective,  (*visible commands, last*)
     1.5    entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
     1.6    result: exec option}  (*result of last execution*)
     1.7 -and version = Version of node Graph.T  (*development graph wrt. static imports*)
     1.8 +and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
     1.9  with
    1.10  
    1.11  fun make_node (header, perspective, entries, result) =
    1.12 @@ -134,9 +134,10 @@
    1.13  fun set_result result =
    1.14    map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result));
    1.15  
    1.16 -fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node;
    1.17 -fun default_node name = Graph.default_node (name, empty_node);
    1.18 -fun update_node name f = default_node name #> Graph.map_node name f;
    1.19 +fun get_node nodes name = String_Graph.get_node nodes name
    1.20 +  handle String_Graph.UNDEF _ => empty_node;
    1.21 +fun default_node name = String_Graph.default_node (name, empty_node);
    1.22 +fun update_node name f = default_node name #> String_Graph.map_node name f;
    1.23  
    1.24  
    1.25  (* node edits and associated executions *)
    1.26 @@ -182,7 +183,7 @@
    1.27  
    1.28  (* version operations *)
    1.29  
    1.30 -val empty_version = Version Graph.empty;
    1.31 +val empty_version = Version String_Graph.empty;
    1.32  
    1.33  fun nodes_of (Version nodes) = nodes;
    1.34  val node_of = get_node o nodes_of;
    1.35 @@ -204,12 +205,12 @@
    1.36              |> default_node name
    1.37              |> fold default_node imports;
    1.38            val nodes2 = nodes1
    1.39 -            |> Graph.Keys.fold
    1.40 -                (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
    1.41 +            |> String_Graph.Keys.fold
    1.42 +                (fn dep => String_Graph.del_edge (dep, name)) (String_Graph.imm_preds nodes1 name);
    1.43            val (nodes3, errors2) =
    1.44 -            (Graph.add_deps_acyclic (name, imports) nodes2, errors1)
    1.45 -              handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    1.46 -        in Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    1.47 +            (String_Graph.add_deps_acyclic (name, imports) nodes2, errors1)
    1.48 +              handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs);
    1.49 +        in String_Graph.map_node name (set_header (master, header, errors2)) nodes3 end
    1.50      | Perspective perspective => update_node name (set_perspective perspective) nodes);
    1.51  
    1.52  fun put_node (name, node) (Version nodes) =
    1.53 @@ -294,7 +295,7 @@
    1.54      val commands' =
    1.55        (versions', Inttab.empty) |->
    1.56          Inttab.fold (fn (_, version) => nodes_of version |>
    1.57 -          Graph.fold (fn (_, (node, _)) => node |>
    1.58 +          String_Graph.fold (fn (_, (node, _)) => node |>
    1.59              iterate_entries (fn ((_, id), _) =>
    1.60                SOME o Inttab.insert (K true) (id, the_command state id))));
    1.61    in (versions', commands', execution) end);
    1.62 @@ -339,7 +340,7 @@
    1.63          {name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
    1.64          (fn () =>
    1.65           (OS.Process.sleep (seconds 0.02);
    1.66 -          nodes_of (the_version state version_id) |> Graph.schedule
    1.67 +          nodes_of (the_version state version_id) |> String_Graph.schedule
    1.68              (fn deps => fn (name, node) =>
    1.69                if not (visible_node node) andalso finished_theory node then
    1.70                  Future.value ()
    1.71 @@ -366,13 +367,13 @@
    1.72  fun make_required nodes =
    1.73    let
    1.74      val all_visible =
    1.75 -      Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.76 -      |> Graph.all_preds nodes
    1.77 +      String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes []
    1.78 +      |> String_Graph.all_preds nodes
    1.79        |> map (rpair ()) |> Symtab.make;
    1.80  
    1.81      val required =
    1.82        Symtab.fold (fn (a, ()) =>
    1.83 -        exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ?
    1.84 +        exists (Symtab.defined all_visible) (String_Graph.immediate_succs nodes a) ?
    1.85            Symtab.update (a, ())) all_visible Symtab.empty;
    1.86    in Symtab.defined required end;
    1.87  
    1.88 @@ -476,7 +477,7 @@
    1.89  
    1.90      val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state);
    1.91      val updated = timeit "Document.update" (fn () =>
    1.92 -      nodes |> Graph.schedule
    1.93 +      nodes |> String_Graph.schedule
    1.94          (fn deps => fn (name, node) =>
    1.95            (singleton o Future.forks)
    1.96              {name = "Document.update", group = NONE,
     2.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jan 13 15:04:55 2013 +0100
     2.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jan 13 19:45:32 2013 +0100
     2.3 @@ -55,11 +55,11 @@
     2.4  
     2.5  (* derived graph operations *)
     2.6  
     2.7 -fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
     2.8 -  handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
     2.9 +fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G
    2.10 +  handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
    2.11  
    2.12  fun new_entry name parents entry =
    2.13 -  Graph.new_node (name, entry) #> add_deps name parents;
    2.14 +  String_Graph.new_node (name, entry) #> add_deps name parents;
    2.15  
    2.16  
    2.17  (* thy database *)
    2.18 @@ -74,7 +74,8 @@
    2.19  fun base_name s = Path.implode (Path.base (Path.explode s));
    2.20  
    2.21  local
    2.22 -  val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
    2.23 +  val database =
    2.24 +    Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T);
    2.25  in
    2.26    fun get_thys () = ! database;
    2.27    fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f);
    2.28 @@ -85,13 +86,13 @@
    2.29  
    2.30  fun thy_graph f x = f (get_thys ()) x;
    2.31  
    2.32 -fun get_names () = Graph.topological_order (get_thys ());
    2.33 +fun get_names () = String_Graph.topological_order (get_thys ());
    2.34  
    2.35  
    2.36  (* access thy *)
    2.37  
    2.38  fun lookup_thy name =
    2.39 -  SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
    2.40 +  SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE;
    2.41  
    2.42  val known_thy = is_some o lookup_thy;
    2.43  
    2.44 @@ -139,10 +140,10 @@
    2.45    if is_finished name then error (loader_msg "attempt to change finished theory" [name])
    2.46    else
    2.47      let
    2.48 -      val succs = thy_graph Graph.all_succs [name];
    2.49 +      val succs = thy_graph String_Graph.all_succs [name];
    2.50        val _ = Output.urgent_message (loader_msg "removing" succs);
    2.51        val _ = List.app (perform Remove) succs;
    2.52 -      val _ = change_thys (fold Graph.del_node succs);
    2.53 +      val _ = change_thys (fold String_Graph.del_node succs);
    2.54      in () end);
    2.55  
    2.56  fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () =>
    2.57 @@ -179,13 +180,13 @@
    2.58    (Thm.join_theory_proofs thy; Future.join present; commit (); thy);
    2.59  
    2.60  val schedule_seq =
    2.61 -  Graph.schedule (fn deps => fn (_, task) =>
    2.62 +  String_Graph.schedule (fn deps => fn (_, task) =>
    2.63      (case task of
    2.64        Task (parents, body) => finish_thy (body (task_parents deps parents))
    2.65      | Finished thy => thy)) #> ignore;
    2.66  
    2.67  val schedule_futures = uninterruptible (fn _ =>
    2.68 -  Graph.schedule (fn deps => fn (name, task) =>
    2.69 +  String_Graph.schedule (fn deps => fn (name, task) =>
    2.70      (case task of
    2.71        Task (parents, body) =>
    2.72          (singleton o Future.forks)
    2.73 @@ -265,7 +266,7 @@
    2.74      val path = Path.expand (Path.explode str);
    2.75      val name = Path.implode (Path.base path);
    2.76    in
    2.77 -    (case try (Graph.get_node tasks) name of
    2.78 +    (case try (String_Graph.get_node tasks) name of
    2.79        SOME task => (task_finished task, tasks)
    2.80      | NONE =>
    2.81          let
    2.82 @@ -305,7 +306,7 @@
    2.83  (* use_thy *)
    2.84  
    2.85  fun use_thys_wrt dir arg =
    2.86 -  schedule_tasks (snd (require_thys [] dir arg Graph.empty));
    2.87 +  schedule_tasks (snd (require_thys [] dir arg String_Graph.empty));
    2.88  
    2.89  val use_thys = use_thys_wrt Path.current;
    2.90  val use_thy = use_thys o single;
    2.91 @@ -340,6 +341,6 @@
    2.92  
    2.93  (* finish all theories *)
    2.94  
    2.95 -fun finish () = change_thys (Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
    2.96 +fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry)));
    2.97  
    2.98  end;