# HG changeset patch
# User wenzelm
# Date 1569857320 -7200
# Node ID 60abd1e94168bd9c7f6dc7b268d00d00c4dd3e89
# Parent  030a6baa5cb2cc4d4b928fcf1df61ec46baeb667
obsolete (see 030a6baa5cb2 and d14ddb1df52c);

diff -r 030a6baa5cb2 -r 60abd1e94168 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Mon Sep 30 16:40:35 2019 +0200
+++ b/src/Pure/General/graph.ML	Mon Sep 30 17:28:40 2019 +0200
@@ -41,7 +41,6 @@
   val is_minimal: 'a T -> key -> bool
   val is_maximal: 'a T -> key -> bool
   val is_isolated: 'a T -> key -> bool
-  val maximal_descendants: 'a T -> key -> int option
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
@@ -181,16 +180,6 @@
 
 fun is_isolated G x = is_minimal G x andalso is_maximal G x;
 
-(*longest path to some maximal element*)
-fun maximal_descendants G =
-  let
-    val next = imm_preds G;
-    fun reach depth x R =
-      if (case Table.lookup R x of SOME d => d >= depth | NONE => false) then R
-      else Keys.fold_rev (reach (depth + 1)) (next x) (Table.update (x, depth) R);
-    val result = fold (reach 0) (maximals G) Table.empty;
-  in Table.lookup result end;
-
 
 (* node operations *)
 
diff -r 030a6baa5cb2 -r 60abd1e94168 src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Sep 30 16:40:35 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Sep 30 17:28:40 2019 +0200
@@ -500,27 +500,6 @@
         Symtab.update (a, ())) all_visible all_required
   end;
 
-structure Eager_Graph = Graph(type key = int * string val ord = prod_ord int_ord string_ord);
-
-fun schedule_execution f nodes =
-  if Options.default_bool \<^system_option>\<open>execution_eager\<close>
-  then
-    let
-      val decorate = the o String_Graph.maximal_descendants nodes;
-      fun add_node (d, a) = Eager_Graph.default_node ((d, a), String_Graph.get_node nodes a);
-    in
-      (nodes, Eager_Graph.empty) |-> String_Graph.fold (fn (a, (_, (preds, _))) =>
-        let
-          val a' = `decorate a;
-          val bs' = String_Graph.Keys.fold (cons o `decorate) preds [];
-        in
-          fold add_node (a' :: bs')
-          #> fold (fn b' => Eager_Graph.add_edge (b', a')) bs'
-        end)
-      |> Eager_Graph.schedule (fn deps => fn ((_, x), y) => f (map (apfst #2) deps) (x, y))
-    end
-  else String_Graph.schedule f nodes;
-
 fun start_execution state = state |> map_state (fn (versions, blobs, commands, execution) =>
   timeit "Document.start_execution" (fn () =>
     let
@@ -541,7 +520,7 @@
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
       val _ =
-        nodes |> schedule_execution
+        nodes |> String_Graph.schedule
           (fn deps => fn (name, node) =>
             if Symtab.defined required name orelse visible_node node orelse pending_result node then
               let
diff -r 030a6baa5cb2 -r 60abd1e94168 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Sep 30 16:40:35 2019 +0200
+++ b/src/Pure/Tools/dump.scala	Mon Sep 30 17:28:40 2019 +0200
@@ -126,8 +126,7 @@
           "ML_statistics=false" +
           "parallel_proofs=0" +
           "editor_tracing_messages=0" +
-          "editor_presentation" +
-          "execution_eager"
+          "editor_presentation"
       (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
     }