author  wenzelm 
Tue, 23 Aug 2011 12:20:12 +0200  
changeset 44385  e7fdb008aa7d 
parent 44384  8f6054a63f96 
child 44386  4048ca2658b7 
permissions  rwrr 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/PIDE/document.ML 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

3 

67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

4 
Document as collection of named nodes, each consisting of an editable 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

5 
list of commands, associated with asynchronous execution process. 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

6 
*) 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

7 

67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

8 
signature DOCUMENT = 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

9 
sig 
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

10 
type id = int 
38373  11 
type version_id = id 
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

12 
type command_id = id 
38373  13 
type exec_id = id 
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

14 
val no_id: id 
38419  15 
val new_id: unit > id 
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

16 
val parse_id: string > id 
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

17 
val print_id: id > string 
44185  18 
type node_header = (string * string list * (string * bool) list) Exn.result 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

19 
datatype node_edit = 
44185  20 
Clear  
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

21 
Edits of (command_id option * command_id option) list  
44384  22 
Header of node_header  
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

23 
Perspective of command_id list 
44156  24 
type edit = string * node_edit 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

25 
type state 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

26 
val init_state: state 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

27 
val join_commands: state > unit 
44301  28 
val cancel_execution: state > Future.task list 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

29 
val define_command: command_id > string > state > state 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

30 
val edit: version_id > version_id > edit list > state > (command_id * exec_id) list * state 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

31 
val execute: version_id > state > state 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

32 
val state: unit > state 
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

33 
val change_state: (state > state) > unit 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

34 
end; 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

35 

67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

36 
structure Document: DOCUMENT = 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

37 
struct 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

38 

67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

39 
(* unique identifiers *) 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

40 

38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

41 
type id = int; 
38373  42 
type version_id = id; 
38363
af7f41a8a0a8
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
wenzelm
parents:
38355
diff
changeset

43 
type command_id = id; 
38373  44 
type exec_id = id; 
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38150
diff
changeset

45 

8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38150
diff
changeset

46 
val no_id = 0; 
40449  47 
val new_id = Synchronized.counter (); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

48 

38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38373
diff
changeset

49 
val parse_id = Markup.parse_int; 
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38373
diff
changeset

50 
val print_id = Markup.print_int; 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

51 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

52 
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

53 
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id); 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

54 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

55 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

56 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

57 
(** document structure **) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

58 

44185  59 
type node_header = (string * string list * (string * bool) list) Exn.result; 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

60 
structure Entries = Linear_Set(type key = command_id val ord = int_ord); 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

61 

43668  62 
abstype node = Node of 
44182  63 
{header: node_header, 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

64 
perspective: command_id list, 
44180  65 
entries: exec_id option Entries.T, (*command entries with excecutions*) 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

66 
result: Toplevel.state lazy} 
43668  67 
and version = Version of node Graph.T (*development graph wrt. static imports*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

68 
with 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

69 

44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

70 
fun make_node (header, perspective, entries, result) = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

71 
Node {header = header, perspective = perspective, entries = entries, result = result}; 
43668  72 

44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

73 
fun map_node f (Node {header, perspective, entries, result}) = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

74 
make_node (f (header, perspective, entries, result)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

75 

44180  76 
fun get_header (Node {header, ...}) = header; 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

77 
fun set_header header = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

78 
map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); 
44180  79 

44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

80 
fun get_perspective (Node {perspective, ...}) = perspective; 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

81 
fun set_perspective perspective = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

82 
map_node (fn (header, _, entries, result) => (header, perspective, entries, result)); 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

83 

e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

84 
fun map_entries f (Node {header, perspective, entries, result}) = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

85 
make_node (header, perspective, f entries, result); 
43668  86 
fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; 
87 
fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; 

88 

44200  89 
fun get_theory pos (Node {result, ...}) = Toplevel.end_theory pos (Lazy.get_finished result); 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

90 
fun set_result result = 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

91 
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); 
44180  92 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

93 
val empty_exec = Lazy.value Toplevel.toplevel; 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

94 
val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), [], Entries.empty, empty_exec); 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

95 
val clear_node = map_node (fn (header, _, _, _) => (header, [], Entries.empty, empty_exec)); 
44185  96 

97 
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; 

44202  98 
fun default_node name = Graph.default_node (name, empty_node); 
99 
fun update_node name f = default_node name #> Graph.map_node name f; 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

100 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

101 

38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

102 
(* node edits and associated executions *) 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

103 

44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

104 
datatype node_edit = 
44185  105 
Clear  
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

106 
Edits of (command_id option * command_id option) list  
44384  107 
Header of node_header  
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

108 
Perspective of command_id list; 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

109 

44156  110 
type edit = string * node_edit; 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

111 

43668  112 
fun the_entry (Node {entries, ...}) id = 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

113 
(case Entries.lookup entries id of 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

114 
NONE => err_undef "command entry" id 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

115 
 SOME entry => entry); 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

116 

43668  117 
fun update_entry (id, exec_id) = 
118 
map_entries (Entries.update (id, SOME exec_id)); 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

119 

38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

120 
fun reset_after id entries = 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

121 
(case Entries.get_after entries id of 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

122 
NONE => entries 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

123 
 SOME next => Entries.update (next, NONE) entries); 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

124 

43668  125 
val edit_node = map_entries o fold 
126 
(fn (id, SOME id2) => Entries.insert_after id (id2, NONE) 

127 
 (id, NONE) => Entries.delete_after id #> reset_after id); 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

128 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

129 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

130 
(* version operations *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

131 

44185  132 
val empty_version = Version Graph.empty; 
133 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

134 
fun nodes_of (Version nodes) = nodes; 
44185  135 
val node_of = get_node o nodes_of; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

136 

44185  137 
fun cycle_msg names = "Cyclic dependency of " ^ space_implode " via " (map quote names); 
44180  138 

44202  139 
fun touch_descendants name nodes = 
140 
fold (fn desc => desc <> name ? update_node desc (map_entries (reset_after NONE))) 

141 
(Graph.all_succs nodes [name]) nodes; 

142 

44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

143 
fun edit_nodes (name, node_edit) (Version nodes) = 
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

144 
Version 
44202  145 
(touch_descendants name 
146 
(case node_edit of 

147 
Clear => update_node name clear_node nodes 

148 
 Edits edits => 

149 
nodes 

150 
> update_node name (edit_node edits) 

151 
 Header header => 

152 
let 

44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

153 
val parents = (case header of Exn.Res (_, parents, _) => parents  _ => []); 
44223
cac52579f2c2
more robust treatment of node dependencies in incremental edits;
wenzelm
parents:
44222
diff
changeset

154 
val nodes1 = nodes 
cac52579f2c2
more robust treatment of node dependencies in incremental edits;
wenzelm
parents:
44222
diff
changeset

155 
> default_node name 
cac52579f2c2
more robust treatment of node dependencies in incremental edits;
wenzelm
parents:
44222
diff
changeset

156 
> fold default_node parents; 
cac52579f2c2
more robust treatment of node dependencies in incremental edits;
wenzelm
parents:
44222
diff
changeset

157 
val nodes2 = nodes1 
44338
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44330
diff
changeset

158 
> Graph.Keys.fold 
700008399ee5
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists  order of adjacency is now standardized wrt. Key.ord;
wenzelm
parents:
44330
diff
changeset

159 
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); 
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

160 
val (header', nodes3) = 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

161 
(header, Graph.add_deps_acyclic (name, parents) nodes2) 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

162 
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); 
44384  163 
in Graph.map_node name (set_header header') nodes3 end 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

164 
 Perspective perspective => 
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

165 
update_node name (set_perspective perspective) nodes)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

166 

44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

167 
fun put_node (name, node) (Version nodes) = 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

168 
Version (update_node name (K node) nodes); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

169 

38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

170 
end; 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

171 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

172 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

173 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

174 
(** global state  document structure and execution process **) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

175 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

176 
abstype state = State of 
40398  177 
{versions: version Inttab.table, (*version_id > document content*) 
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

178 
commands: Toplevel.transition future Inttab.table, (*command_id > transition (future parsing)*) 
44196  179 
execs: Toplevel.state lazy Inttab.table, (*exec_id > execution process*) 
44300
349cc426d929
tuned signature  treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset

180 
execution: Future.group} (*global execution process*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

181 
with 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

182 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

183 
fun make_state (versions, commands, execs, execution) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

184 
State {versions = versions, commands = commands, execs = execs, execution = execution}; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

185 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

186 
fun map_state f (State {versions, commands, execs, execution}) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

187 
make_state (f (versions, commands, execs, execution)); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

188 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

189 
val init_state = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

190 
make_state (Inttab.make [(no_id, empty_version)], 
38449  191 
Inttab.make [(no_id, Future.value Toplevel.empty)], 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

192 
Inttab.make [(no_id, empty_exec)], 
44300
349cc426d929
tuned signature  treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset

193 
Future.new_group NONE); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

194 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

195 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

196 
(* document versions *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

197 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

198 
fun define_version (id: version_id) version = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

199 
map_state (fn (versions, commands, execs, execution) => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

200 
let val versions' = Inttab.update_new (id, version) versions 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

201 
handle Inttab.DUP dup => err_dup "document version" dup 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

202 
in (versions', commands, execs, execution) end); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

203 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

204 
fun the_version (State {versions, ...}) (id: version_id) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

205 
(case Inttab.lookup versions id of 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

206 
NONE => err_undef "document version" id 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

207 
 SOME version => version); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

208 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

209 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

210 
(* commands *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

211 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

212 
fun define_command (id: command_id) text = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

213 
map_state (fn (versions, commands, execs, execution) => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

214 
let 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

215 
val id_string = print_id id; 
44302  216 
val tr = 
217 
Future.fork_pri 2 (fn () => 

218 
Position.setmp_thread_data (Position.id_only id_string) 

219 
(fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ()); 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

220 
val commands' = 
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

221 
Inttab.update_new (id, tr) commands 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

222 
handle Inttab.DUP dup => err_dup "command" dup; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

223 
in (versions, commands', execs, execution) end); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

224 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

225 
fun the_command (State {commands, ...}) (id: command_id) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

226 
(case Inttab.lookup commands id of 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

227 
NONE => err_undef "command" id 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

228 
 SOME tr => tr); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

229 

38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

230 
fun join_commands (State {commands, ...}) = 
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

231 
Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands (); 
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

232 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

233 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

234 
(* command executions *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

235 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

236 
fun define_exec (exec_id, exec) = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

237 
map_state (fn (versions, commands, execs, execution) => 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

238 
let val execs' = Inttab.update_new (exec_id, exec) execs 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

239 
handle Inttab.DUP dup => err_dup "command execution" dup 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

240 
in (versions, commands, execs', execution) end); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

241 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

242 
fun the_exec (State {execs, ...}) exec_id = 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

243 
(case Inttab.lookup execs exec_id of 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

244 
NONE => err_undef "command execution" exec_id 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

245 
 SOME exec => exec); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

246 

41634
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset

247 

28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset

248 
(* document execution *) 
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset

249 

44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44271
diff
changeset

250 
fun cancel_execution (State {execution, ...}) = Future.cancel_group execution; 
41634
28d94383249c
cancel document execution before editing, to improve reactivity on systems with few cores;
wenzelm
parents:
41630
diff
changeset

251 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

252 
end; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

253 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

254 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

255 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

256 
(* toplevel transactions *) 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

257 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

258 
local 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

259 

40391
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40390
diff
changeset

260 
fun timing tr t = Toplevel.status tr (Markup.timing t); 
b0dafbfc05b7
explicit "timing" status for toplevel transactions;
wenzelm
parents:
40390
diff
changeset

261 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

262 
fun proof_status tr st = 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

263 
(case try Toplevel.proof_of st of 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

264 
SOME prf => Toplevel.status tr (Proof.status_markup prf) 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

265 
 NONE => ()); 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

266 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

267 
fun async_state tr st = 
44302  268 
(singleton o Future.forks) 
269 
{name = "Document.async_state", group = SOME (Future.new_group NONE), 

270 
deps = [], pri = 0, interrupts = true} 

271 
(fn () => 

272 
Toplevel.setmp_thread_position tr 

273 
(fn () => Toplevel.print_state false st) ()) 

274 
> ignore; 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

275 

40390  276 
fun run int tr st = 
277 
(case Toplevel.transition int tr st of 

278 
SOME (st', NONE) => ([], SOME st') 

44271
89f40a5939b2
more precise treatment of exception nesting and serial numbers;
wenzelm
parents:
44270
diff
changeset

279 
 SOME (_, SOME (exn, _)) => 
89f40a5939b2
more precise treatment of exception nesting and serial numbers;
wenzelm
parents:
44270
diff
changeset

280 
(case ML_Compiler.exn_messages exn of 
40390  281 
[] => Exn.interrupt () 
282 
 errs => (errs, NONE)) 

44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44247
diff
changeset

283 
 NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); 
40390  284 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

285 
in 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

286 

44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

287 
fun run_command tr st = 
44185  288 
let 
44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

289 
val is_init = Toplevel.is_init tr; 
44185  290 
val is_proof = Keyword.is_proof (Toplevel.name_of tr); 
291 
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); 

292 

293 
val start = Timing.start (); 

294 
val (errs, result) = 

295 
if Toplevel.is_toplevel st andalso not is_init then ([], SOME st) 

296 
else run (is_init orelse is_proof) (Toplevel.set_print false tr) st; 

297 
val _ = timing tr (Timing.result start); 

298 
val _ = List.app (Toplevel.error_msg tr) errs; 

299 
in 

300 
(case result of 

44196  301 
NONE => (Toplevel.status tr Markup.failed; st) 
44185  302 
 SOME st' => 
303 
(Toplevel.status tr Markup.finished; 

304 
proof_status tr st'; 

305 
if do_print then async_state tr st' else (); 

44196  306 
st')) 
44185  307 
end; 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

308 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

309 
end; 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

310 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

311 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

312 

8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

313 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

314 
(** editing **) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

315 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

316 
(* edit *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

317 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

318 
local 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

319 

38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

320 
fun is_changed node' ((_, id), exec) = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

321 
(case try (the_entry node') id of 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

322 
NONE => true 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

323 
 SOME exec' => exec' <> exec); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

324 

44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

325 
fun new_exec (command_id, command) (assigns, execs, exec) = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

326 
let 
38419  327 
val exec_id' = new_id (); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

328 
val exec' = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

329 
Lazy.lazy (fn () => 
40398  330 
let 
44198  331 
val tr = Toplevel.put_id (print_id exec_id') (Future.get_finished command); 
332 
val st = Lazy.get_finished exec; 

44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

333 
in run_command tr st end); 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

334 
in ((command_id, exec_id') :: assigns, (exec_id', exec') :: execs, exec') end; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

335 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

336 
in 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

337 

44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

338 
fun edit (old_id: version_id) (new_id: version_id) edits state = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

339 
let 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

340 
val old_version = the_version state old_id; 
44180  341 
val _ = Time.now (); (* FIXME odd workaround for polyml5.4.0/x86_64 *) 
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

342 
val new_version = fold edit_nodes edits old_version; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

343 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

344 
val updates = 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

345 
nodes_of new_version > Graph.schedule 
44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

346 
(fn deps => fn (name, node) => 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

347 
(case first_entry NONE (is_changed (node_of old_version name)) node of 
44201  348 
NONE => Future.value (([], [], []), node) 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

349 
 SOME ((prev, id), _) => 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

350 
let 
44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

351 
fun init () = 
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

352 
let 
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

353 
val (thy_name, imports, uses) = Exn.release (get_header node); 
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

354 
(* FIXME provide files via Scala layer *) 
44226
1ea760da0f2d
workaround for Cygwin, to make it work in the important special case without extra files;
wenzelm
parents:
44223
diff
changeset

355 
val (dir, files) = 
1ea760da0f2d
workaround for Cygwin, to make it work in the important special case without extra files;
wenzelm
parents:
44223
diff
changeset

356 
if ML_System.platform_is_cygwin then (Path.current, []) 
1ea760da0f2d
workaround for Cygwin, to make it work in the important special case without extra files;
wenzelm
parents:
44223
diff
changeset

357 
else (Path.dir (Path.explode name), map (apfst Path.explode) uses); 
44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

358 

e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

359 
val parents = 
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

360 
imports > map (fn import => 
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

361 
(case Thy_Info.lookup_theory import of 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

362 
SOME thy => thy 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

363 
 NONE => 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

364 
get_theory (Position.file_only import) 
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44202
diff
changeset

365 
(#2 (Future.join (the (AList.lookup (op =) deps import)))))); 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

366 
in Thy_Load.begin_theory dir thy_name imports files parents end; 
44199
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

367 
fun get_command id = 
e38885e3ea60
retrieve imports from document state, with fallback on theory loader for preloaded theories;
wenzelm
parents:
44198
diff
changeset

368 
(id, the_command state id > Future.map (Toplevel.modify_init init)); 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

369 
val perspective = get_perspective node; (* FIXME *) 
44201  370 
in 
44302  371 
(singleton o Future.forks) 
372 
{name = "Document.edit", group = NONE, 

373 
deps = map (Future.task_of o #2) deps, pri = 2, interrupts = false} 

44201  374 
(fn () => 
375 
let 

376 
val prev_exec = 

377 
(case prev of 

378 
NONE => no_id 

379 
 SOME prev_id => the_default no_id (the_entry node prev_id)); 

380 
val (assigns, execs, result) = 

381 
fold_entries (SOME id) (new_exec o get_command o #2 o #1) 

382 
node ([], [], the_exec state prev_exec); 

383 
val node' = node 

384 
> fold update_entry assigns 

385 
> set_result result; 

386 
in ((assigns, execs, [(name, node')]), node') end) 

387 
end)) 

44330  388 
> Future.joins > map #1; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

389 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

390 
val state' = state 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

391 
> fold (fold define_exec o #2) updates 
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

392 
> define_version new_id (fold (fold put_node o #3) updates new_version); 
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

393 

44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

394 
in (maps #1 (rev updates), state') end; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

395 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

396 
end; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

397 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

398 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

399 
(* execute *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

400 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

401 
fun execute version_id state = 
41673  402 
state > map_state (fn (versions, commands, execs, _) => 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

403 
let 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

404 
val version = the_version state version_id; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

405 

9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

406 
fun force_exec NONE = () 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

407 
 force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id)); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

408 

44300
349cc426d929
tuned signature  treat structure Task_Queue as private to implementation;
wenzelm
parents:
44299
diff
changeset

409 
val execution = Future.new_group NONE; 
44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44271
diff
changeset

410 
val _ = 
44201  411 
nodes_of version > Graph.schedule 
412 
(fn deps => fn (name, node) => 

44302  413 
(singleton o Future.forks) 
414 
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME execution)), 

415 
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = true} 

44201  416 
(fold_entries NONE (fn (_, exec) => fn () => force_exec exec) node)); 
40520
77a7b0a7d4b1
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm
parents:
40481
diff
changeset

417 

44299
061599cb6eb0
refined Future.cancel: explicit future allows to join actual cancellation;
wenzelm
parents:
44271
diff
changeset

418 
in (versions, commands, execs, execution) end); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

419 

43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

420 

1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

421 

1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

422 
(** global state **) 
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

423 

1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

424 
val global_state = Synchronized.var "Document" init_state; 
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

425 

1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

426 
fun state () = Synchronized.value global_state; 
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

427 
val change_state = Synchronized.change global_state; 
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

428 

38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

429 
end; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

430 