42 |
42 |
43 def ok: Boolean = |
43 def ok: Boolean = |
44 (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
44 (nodes.iterator ++ nodes_committed.iterator).forall({ case (_, st) => st.ok }) |
45 } |
45 } |
46 |
46 |
47 private object Load_State |
|
48 { |
|
49 def finished: Load_State = Load_State(Nil, Nil, 0) |
|
50 |
|
51 def count_file(name: Document.Node.Name): Long = |
|
52 name.path.file.length |
|
53 } |
|
54 |
|
55 private case class Load_State( |
|
56 pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long) |
|
57 { |
|
58 def next( |
|
59 dep_graph: Document.Node.Name.Graph[Unit], |
|
60 finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) = |
|
61 { |
|
62 def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) |
|
63 : (List[Document.Node.Name], Load_State) = |
|
64 { |
|
65 val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished) |
|
66 (load_theories, Load_State(pending1, rest1, load_limit)) |
|
67 } |
|
68 |
|
69 if (!pending.forall(finished)) (Nil, this) |
|
70 else if (rest.isEmpty) (Nil, Load_State.finished) |
|
71 else if (load_limit == 0) load_requirements(rest, Nil) |
|
72 else { |
|
73 val reachable = |
|
74 dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest) |
|
75 val (pending1, rest1) = rest.partition(reachable) |
|
76 load_requirements(pending1, rest1) |
|
77 } |
|
78 } |
|
79 } |
|
80 |
|
81 class Session private[Headless]( |
47 class Session private[Headless]( |
82 session_name: String, |
48 session_name: String, |
83 _session_options: => Options, |
49 _session_options: => Options, |
84 override val resources: Resources) extends isabelle.Session(_session_options, resources) |
50 override val resources: Resources) extends isabelle.Session(_session_options, resources) |
85 { |
51 { |
118 finally { Isabelle_System.rm_tree(tmp_dir) } |
84 finally { Isabelle_System.rm_tree(tmp_dir) } |
119 } |
85 } |
120 |
86 |
121 |
87 |
122 /* theories */ |
88 /* theories */ |
|
89 |
|
90 private object Load_State |
|
91 { |
|
92 def finished: Load_State = Load_State(Nil, Nil, 0) |
|
93 |
|
94 def count_file(name: Document.Node.Name): Long = |
|
95 name.path.file.length |
|
96 } |
|
97 |
|
98 private case class Load_State( |
|
99 pending: List[Document.Node.Name], rest: List[Document.Node.Name], load_limit: Long) |
|
100 { |
|
101 def next( |
|
102 dep_graph: Document.Node.Name.Graph[Unit], |
|
103 finished: Document.Node.Name => Boolean): (List[Document.Node.Name], Load_State) = |
|
104 { |
|
105 def load_requirements(pending1: List[Document.Node.Name], rest1: List[Document.Node.Name]) |
|
106 : (List[Document.Node.Name], Load_State) = |
|
107 { |
|
108 val load_theories = dep_graph.all_preds(pending1).reverse.filterNot(finished) |
|
109 (load_theories, Load_State(pending1, rest1, load_limit)) |
|
110 } |
|
111 |
|
112 if (!pending.forall(finished)) (Nil, this) |
|
113 else if (rest.isEmpty) (Nil, Load_State.finished) |
|
114 else if (load_limit == 0) load_requirements(rest, Nil) |
|
115 else { |
|
116 val reachable = |
|
117 dep_graph.reachable_limit(load_limit, Load_State.count_file, dep_graph.imm_preds, rest) |
|
118 val (pending1, rest1) = rest.partition(reachable) |
|
119 load_requirements(pending1, rest1) |
|
120 } |
|
121 } |
|
122 } |
123 |
123 |
124 private sealed case class Use_Theories_State( |
124 private sealed case class Use_Theories_State( |
125 dep_graph: Document.Node.Name.Graph[Unit], |
125 dep_graph: Document.Node.Name.Graph[Unit], |
126 load_state: Load_State, |
126 load_state: Load_State, |
127 watchdog_timeout: Time, |
127 watchdog_timeout: Time, |