# HG changeset patch
# User wenzelm
# Date 1566842488 -7200
# Node ID d14ddb1df52cd2cd549b71b812415c3c3dca5200
# Parent  5549e686d6acb1475d9e8f52186a3f348dcb35ce
added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);

diff -r 5549e686d6ac -r d14ddb1df52c etc/options
--- a/etc/options	Sun Aug 25 22:17:24 2019 +0200
+++ b/etc/options	Mon Aug 26 20:01:28 2019 +0200
@@ -216,6 +216,9 @@
 option headless_commit_cleanup_delay : real = 60
   -- "delay for cleanup of already imported theories (seconds, 0 = disabled)"
 
+option execution_eager : bool = false
+  -- "prefer theories with shorter stack of decendants"
+
 
 section "Miscellaneous Tools"
 
diff -r 5549e686d6ac -r d14ddb1df52c src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sun Aug 25 22:17:24 2019 +0200
+++ b/src/Pure/General/graph.ML	Mon Aug 26 20:01:28 2019 +0200
@@ -41,6 +41,7 @@
   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*)
@@ -180,6 +181,16 @@
 
 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 5549e686d6ac -r d14ddb1df52c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Aug 25 22:17:24 2019 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Aug 26 20:01:28 2019 +0200
@@ -493,6 +493,27 @@
         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
@@ -513,7 +534,7 @@
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
       val _ =
-        nodes |> String_Graph.schedule
+        nodes |> schedule_execution
           (fn deps => fn (name, node) =>
             if Symtab.defined required name orelse visible_node node orelse pending_result node then
               let