author  wenzelm 
Sat, 11 Aug 2012 19:34:36 +0200  
changeset 48772  e46cd0d26481 
parent 48755  393a37003851 
child 48918  6e5fd4585512 
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 
44478
4fdb1009a370
tuned signature  emphasize traditional read/eval/print terminology, which is still relevant here;
wenzelm
parents:
44476
diff
changeset

5 
list of commands, with asynchronous read/eval/print processes. 
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 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

18 
type node_header = string * Thy_Header.header * string list 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

19 
datatype node_edit = 
48755
393a37003851
apply all text edits to each node, before determining the resulting doc_edits  allow several iterations to consolidate spans etc.;
wenzelm
parents:
48735
diff
changeset

20 
Clear  (* FIXME unused !? *) 
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  
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

22 
Deps 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 
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44643
diff
changeset

27 
val define_command: command_id > string > string > state > state 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

28 
val remove_versions: version_id list > state > state 
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be reassigned;
wenzelm
parents:
47342
diff
changeset

29 
val discontinue_execution: state > unit 
47404
e6e5750f1311
simplified Future.cancel/cancel_group (again)  running threads only;
wenzelm
parents:
47395
diff
changeset

30 
val cancel_execution: state > unit 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

31 
val start_execution: state > unit 
47628  32 
val timing: bool Unsynchronized.ref 
44481  33 
val update: version_id > version_id > edit list > state > 
47388
fe4b245af74c
discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents:
47347
diff
changeset

34 
(command_id * exec_id option) list * state 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

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

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

37 
end; 
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 
structure Document: DOCUMENT = 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

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

41 

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

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

43 

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

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

46 
type command_id = id; 
38373  47 
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

48 

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

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

51 

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

52 
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

53 
val print_id = Markup.print_int; 
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 
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

56 
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

57 

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

58 

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

59 

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

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

61 

48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

62 
type node_header = string * Thy_Header.header * string list; 
47407  63 
type perspective = (command_id > bool) * command_id option; 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

64 
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

65 

48772  66 
type exec = ((Toplevel.state * bool) * unit lazy) Command.memo; (*eval/print process*) 
67 
val no_exec = Command.memo_value ((Toplevel.toplevel, false), Lazy.value ()); 

44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

68 

43668  69 
abstype node = Node of 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

70 
{header: node_header, (*master directory, theory header, errors*) 
47407  71 
perspective: perspective, (*visible commands, last*) 
47340  72 
entries: (exec_id * exec) option Entries.T, (*command entries with excecutions*) 
47407  73 
result: exec option} (*result of last execution*) 
43668  74 
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

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

76 

47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

77 
fun make_node (header, perspective, entries, result) = 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

78 
Node {header = header, perspective = perspective, entries = entries, result = result}; 
43668  79 

47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

80 
fun map_node f (Node {header, perspective, entries, result}) = 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

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

82 

44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

83 
fun make_perspective command_ids : perspective = 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

84 
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids); 
44441  85 

48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

86 
val no_header = ("", Thy_Header.make "" [] [] [], ["Bad theory header"]); 
44441  87 
val no_perspective = make_perspective []; 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

88 

47407  89 
val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE); 
90 
val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE)); 

44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

91 

4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

92 

4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

93 
(* basic components *) 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

94 

48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

95 
fun get_header (Node {header = (master, header, errors), ...}) = 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

96 
if null errors then (master, header) 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

97 
else error (cat_lines errors); 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

98 

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

99 
fun set_header header = 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

100 
map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); 
44180  101 

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

102 
fun get_perspective (Node {perspective, ...}) = perspective; 
44441  103 
fun set_perspective ids = 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

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

105 

47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

106 
val visible_command = #1 o get_perspective; 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

107 
val visible_last = #2 o get_perspective; 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

108 
val visible_node = is_some o visible_last 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

109 

44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

110 
fun map_entries f = 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

111 
map_node (fn (header, perspective, entries, result) => (header, perspective, f entries, result)); 
44643
9987ae55e17b
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
wenzelm
parents:
44614
diff
changeset

112 
fun get_entries (Node {entries, ...}) = entries; 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

113 

5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

114 
fun iterate_entries f = Entries.iterate NONE f o get_entries; 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

115 
fun iterate_entries_after start f (Node {entries, ...}) = 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

116 
(case Entries.get_after entries start of 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

117 
NONE => I 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

118 
 SOME id => Entries.iterate (SOME id) f entries); 
43668  119 

47339
79bd24497ffd
tuned  NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
wenzelm
parents:
47336
diff
changeset

120 
fun get_result (Node {result, ...}) = result; 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

121 
fun set_result result = 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

122 
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); 
44180  123 

44185  124 
fun get_node nodes name = Graph.get_node nodes name handle Graph.UNDEF _ => empty_node; 
44202  125 
fun default_node name = Graph.default_node (name, empty_node); 
126 
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

127 

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

128 

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

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

130 

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

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

133 
Edits of (command_id option * command_id option) list  
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

134 
Deps of node_header  
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

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

136 

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

138 

44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

139 
fun after_entry (Node {entries, ...}) = Entries.get_after entries; 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

140 

44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

141 
fun lookup_entry (Node {entries, ...}) id = 
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

142 
(case Entries.lookup entries id of 
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

143 
NONE => NONE 
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

144 
 SOME (exec, _) => exec); 
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

145 

43668  146 
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

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

148 
NONE => err_undef "command entry" id 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

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

150 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

151 
fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id)) 
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47340
diff
changeset

152 
 the_default_entry _ NONE = (no_id, (no_id, no_exec)); 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

153 

44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

154 
fun update_entry id exec = 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

155 
map_entries (Entries.update (id, exec)); 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

156 

c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

157 
fun reset_entry id node = 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

158 
if is_some (lookup_entry node id) then update_entry id NONE node else node; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

159 

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

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

161 
(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

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

163 
 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

164 

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

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

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

168 

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

169 

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

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

171 

44185  172 
val empty_version = Version Graph.empty; 
173 

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

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

176 

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

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

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

180 
Version 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

181 
(case node_edit of 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

182 
Clear => update_node name clear_node nodes 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

183 
 Edits edits => update_node name (edit_node edits) nodes 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

184 
 Deps (master, header, errors) => 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

185 
let 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

186 
val errors1 = 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

187 
(Thy_Header.define_keywords header; errors) 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

188 
handle ERROR msg => errors @ [msg]; 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

189 
val nodes1 = nodes 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

190 
> default_node name 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

191 
> fold default_node (#imports header); 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

192 
val nodes2 = nodes1 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

193 
> Graph.Keys.fold 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

194 
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

195 
val (nodes3, errors2) = 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

196 
(Graph.add_deps_acyclic (name, #imports header) nodes2, errors1) 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

197 
handle Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); 
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

198 
in Graph.map_node name (set_header (master, header, errors2)) nodes3 end 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

199 
 Perspective perspective => update_node name (set_perspective perspective) nodes); 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

200 

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

201 
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

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

203 

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

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

205 

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

206 

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

207 

47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

208 
(** main state  document structure and execution process **) 
38418
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 
abstype state = State of 
40398  211 
{versions: version Inttab.table, (*version_id > document content*) 
47335  212 
commands: (string * Token.T list lazy) Inttab.table, (*command_id > named span*) 
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be reassigned;
wenzelm
parents:
47342
diff
changeset

213 
execution: version_id * Future.group * bool Unsynchronized.ref} (*current execution process*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

215 

44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

216 
fun make_state (versions, commands, execution) = 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

218 

44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

219 
fun map_state f (State {versions, commands, execution}) = 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

221 

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

222 
val init_state = 
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be reassigned;
wenzelm
parents:
47342
diff
changeset

223 
make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, 
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be reassigned;
wenzelm
parents:
47342
diff
changeset

224 
(no_id, Future.new_group NONE, Unsynchronized.ref false)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

225 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

226 
fun execution_of (State {execution, ...}) = execution; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

227 

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

228 

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

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

230 

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

231 
fun define_version (id: version_id) version = 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

232 
map_state (fn (versions, commands, _) => 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

233 
let 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

234 
val versions' = Inttab.update_new (id, version) versions 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

235 
handle Inttab.DUP dup => err_dup "document version" dup; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

236 
val execution' = (id, Future.new_group NONE, Unsynchronized.ref true); 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

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

238 

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

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

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

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

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

243 

44673  244 
fun delete_version (id: version_id) versions = Inttab.delete id versions 
245 
handle Inttab.UNDEF _ => err_undef "document version" id; 

246 

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

247 

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

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

249 

44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44643
diff
changeset

250 
fun define_command (id: command_id) name text = 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

252 
let 
47395
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

253 
val id_string = print_id id; 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

254 
val span = Lazy.lazy (fn () => 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

255 
Position.setmp_thread_data (Position.id_only id_string) 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

256 
(fn () => 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

257 
Thy_Syntax.parse_tokens 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

258 
(#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ()); 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

259 
val _ = 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

260 
Position.setmp_thread_data (Position.id_only id_string) 
e6261a493f04
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
wenzelm
parents:
47389
diff
changeset

261 
(fn () => Output.status (Markup.markup_only Isabelle_Markup.accepted)) (); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

262 
val commands' = 
46945  263 
Inttab.update_new (id, (name, span)) commands 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

264 
handle Inttab.DUP dup => err_dup "command" dup; 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

266 

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

267 
fun the_command (State {commands, ...}) (id: command_id) = 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

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

269 
NONE => err_undef "command" id 
44644
317e4962dd0f
clarified define_command: store name as structural information;
wenzelm
parents:
44643
diff
changeset

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

271 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

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

273 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

274 
fun remove_versions ids state = state > map_state (fn (versions, _, execution) => 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

275 
let 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

276 
val _ = member (op =) ids (#1 execution) andalso 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

277 
error ("Attempt to remove execution version " ^ print_id (#1 execution)); 
47343
b8aeab386414
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be reassigned;
wenzelm
parents:
47342
diff
changeset

278 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

279 
val versions' = fold delete_version ids versions; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

280 
val commands' = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

281 
(versions', Inttab.empty) > 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

282 
Inttab.fold (fn (_, version) => nodes_of version > 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

283 
Graph.fold (fn (_, (node, _)) => node > 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

284 
iterate_entries (fn ((_, id), _) => 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

285 
SOME o Inttab.insert (K true) (id, the_command state id)))); 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

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

287 

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

288 

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

289 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

290 
(** document execution **) 
47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

291 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

292 
val discontinue_execution = execution_of #> (fn (_, _, running) => running := false); 
47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

293 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

294 
val cancel_execution = execution_of #> (fn (_, group, _) => Future.cancel_group group); 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

295 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

296 
fun terminate_execution state = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

297 
let 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

298 
val (_, group, _) = execution_of state; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

299 
val _ = Future.cancel_group group; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

300 
in Future.join_tasks (Future.group_tasks group) end; 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

301 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

302 
fun start_execution state = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

303 
let 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

304 
fun finished_theory node = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

305 
(case Exn.capture (Command.memo_result o the) (get_result node) of 
48772  306 
Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

307 
 _ => false); 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

308 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

309 
fun run node command_id exec = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

310 
let 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

311 
val (_, print) = Command.memo_eval exec; 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

312 
val _ = 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

313 
if visible_command node command_id 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

314 
then ignore (Lazy.future Future.default_params print) 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

315 
else (); 
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

316 
in () end; 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

317 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

318 
val (version_id, group, running) = execution_of state; 
47633
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

319 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

320 
val _ = 
47633
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

321 
(singleton o Future.forks) 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

322 
{name = "execution", group = SOME group, deps = [], pri = ~2, interrupts = true} 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

323 
(fn () => 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

324 
(OS.Process.sleep (seconds 0.02); 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

325 
nodes_of (the_version state version_id) > Graph.schedule 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

326 
(fn deps => fn (name, node) => 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

327 
if not (visible_node node) andalso finished_theory node then 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

328 
Future.value () 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

329 
else 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

330 
(singleton o Future.forks) 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

331 
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

332 
deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

333 
(fn () => 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

334 
iterate_entries (fn ((_, id), opt_exec) => fn () => 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

335 
(case opt_exec of 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

336 
SOME (_, exec) => if ! running then SOME (run node id exec) else NONE 
e5c5e73f3e30
improved interleaving of start_execution vs. cancel_execution of the next update;
wenzelm
parents:
47631
diff
changeset

337 
 NONE => NONE)) node ())))); 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

338 
in () end; 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

339 

193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

340 

47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

341 

0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

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

343 

47628  344 
val timing = Unsynchronized.ref false; 
345 
fun timeit msg e = cond_timeit (! timing) msg e; 

346 

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

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

348 

47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

349 
fun stable_finished_theory node = 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

350 
is_some (Exn.get_res (Exn.capture (fn () => 
48772  351 
fst (fst (Command.memo_result (the (get_result node)))) 
47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

352 
> Toplevel.end_theory Position.none 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

353 
> Global_Theory.join_proofs) ())); 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

354 

e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

355 
fun stable_command exec = 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

356 
(case Exn.capture Command.memo_result exec of 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

357 
Exn.Exn exn => not (Exn.is_interrupt exn) 
48772  358 
 Exn.Res ((st, _), _) => 
47389
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

359 
(case try Toplevel.theory_of st of 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

360 
NONE => true 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

361 
 SOME thy => is_some (Exn.get_res (Exn.capture Global_Theory.join_recent_proofs thy)))); 
e8552cba702d
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
wenzelm
parents:
47388
diff
changeset

362 

47335  363 
fun make_required nodes = 
364 
let 

365 
val all_visible = 

47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

366 
Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

367 
> Graph.all_preds nodes 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

368 
> map (rpair ()) > Symtab.make; 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

369 

47335  370 
val required = 
47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

371 
Symtab.fold (fn (a, ()) => 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

372 
exists (Symtab.defined all_visible) (Graph.immediate_succs nodes a) ? 
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

373 
Symtab.update (a, ())) all_visible Symtab.empty; 
47335  374 
in Symtab.defined required end; 
375 

47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

376 
fun init_theory imports node = 
47335  377 
let 
378 
(* FIXME provide files via Scala layer, not master_dir *) 

48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

379 
val (dir, header) = get_header node; 
47335  380 
val master_dir = 
48735
35c47932584c
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
wenzelm
parents:
48707
diff
changeset

381 
(case try Url.explode dir of 
35c47932584c
even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
wenzelm
parents:
48707
diff
changeset

382 
SOME (Url.File path) => path 
47335  383 
 _ => Path.current); 
384 
val parents = 

385 
#imports header > map (fn import => 

47407  386 
(case Thy_Info.lookup_theory import of 
47335  387 
SOME thy => thy 
388 
 NONE => 

47339
79bd24497ffd
tuned  NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
wenzelm
parents:
47336
diff
changeset

389 
Toplevel.end_theory (Position.file_only import) 
48772  390 
(fst (fst 
47407  391 
(Command.memo_result 
392 
(the_default no_exec 

48772  393 
(get_result (snd (the (AList.lookup (op =) imports import)))))))))); 
47335  394 
in Thy_Load.begin_theory master_dir header parents end; 
395 

47407  396 
fun check_theory full name node = 
397 
is_some (Thy_Info.lookup_theory name) orelse 

48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

398 
can get_header node andalso (not full orelse is_some (get_result node)); 
47335  399 

44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

400 
fun last_common state last_visible node0 node = 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

401 
let 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

402 
fun update_flags prev (visible, initial) = 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

403 
let 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

404 
val visible' = visible andalso prev <> last_visible; 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

405 
val initial' = initial andalso 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

406 
(case prev of 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

407 
NONE => true 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

408 
 SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

409 
in (visible', initial') end; 
47630  410 
fun get_common ((prev, id), opt_exec) (same, (_, flags)) = 
411 
if same then 

412 
let 

413 
val flags' = update_flags prev flags; 

414 
val same' = 

415 
(case opt_exec of 

416 
NONE => false 

417 
 SOME (exec_id, exec) => 

418 
(case lookup_entry node0 id of 

419 
NONE => false 

420 
 SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec)); 

421 
in SOME (same', (prev, flags')) end 

422 
else NONE; 

423 
val (same, (common, flags)) = 

424 
iterate_entries get_common node (true, (NONE, (true, true))); 

44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

425 
in 
47630  426 
if same then 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

427 
let val last = Entries.get_after (get_entries node) common 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

428 
in (last, update_flags last flags) end 
47630  429 
else (common, flags) 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

430 
end; 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

431 

5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

432 
fun illegal_init () = error "Illegal theory header after end of theory"; 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

433 

47407  434 
fun new_exec state proper_init command_id' (execs, command_exec, init) = 
435 
if not proper_init andalso is_none init then NONE 

44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

436 
else 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

437 
let 
46945  438 
val (name, span) = the_command state command_id' > Lazy.force; 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

439 
val (modify_init, init') = 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

440 
if Keyword.is_theory_begin name then 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

441 
(Toplevel.modify_init (the_default illegal_init init), NONE) 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

442 
else (I, init); 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

443 
val exec_id' = new_id (); 
46876
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

444 
val exec_id'_string = print_id exec_id'; 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

445 
val tr = 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

446 
Position.setmp_thread_data (Position.id_only exec_id'_string) 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

447 
(fn () => 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

448 
#1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

449 
> modify_init 
8f3bb485f628
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
wenzelm
parents:
46739
diff
changeset

450 
> Toplevel.put_id exec_id'_string); 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

451 
val exec' = 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

452 
Command.memo (fn () => 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

453 
Command.run_command (tr ()) (fst (Command.memo_result (snd (snd command_exec))))); 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

454 
val command_exec' = (command_id', (exec_id', exec')); 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

455 
in SOME (command_exec' :: execs, command_exec', init') end; 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

456 

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

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

458 

44481  459 
fun update (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

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

461 
val old_version = the_version state old_id; 
44180  462 
val _ = Time.now (); (* FIXME odd workaround for polyml5.4.0/x86_64 *) 
47628  463 
val new_version = timeit "Document.edit_nodes" (fn () => fold edit_nodes edits old_version); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

464 

44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

465 
val nodes = nodes_of new_version; 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

466 
val is_required = make_required nodes; 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

467 

47628  468 
val _ = timeit "Document.terminate_execution" (fn () => terminate_execution state); 
469 
val updated = timeit "Document.update" (fn () => 

44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

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

471 
(fn deps => fn (name, node) => 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

472 
(singleton o Future.forks) 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

473 
{name = "Document.update", group = NONE, 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

474 
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

475 
(fn () => 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

476 
let 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

477 
val imports = map (apsnd Future.join) deps; 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

478 
val updated_imports = exists (is_some o #3 o #1 o #2) imports; 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

479 
val required = is_required name; 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

480 
in 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

481 
if updated_imports orelse AList.defined (op =) edits name orelse 
47631
97d28302445c
always revisit nodes independently of "required" flag, which may change during editing  avoid "bloodbath effect" when changing perspective while loading;
wenzelm
parents:
47630
diff
changeset

482 
not (stable_finished_theory node) 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

483 
then 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

484 
let 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

485 
val node0 = node_of old_version name; 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

486 
fun init () = init_theory imports node; 
47407  487 
val proper_init = 
488 
check_theory false name node andalso 

489 
forall (fn (name, (_, node)) => check_theory true name node) imports; 

47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

490 

47345
193251980a73
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
wenzelm
parents:
47344
diff
changeset

491 
val last_visible = visible_last node; 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

492 
val (common, (visible, initial)) = 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

493 
if updated_imports then (NONE, (true, true)) 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

494 
else last_common state last_visible node0 node; 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

495 
val common_command_exec = the_default_entry node common; 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

496 

47405  497 
val (new_execs, (command_id', (_, exec')), _) = 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

498 
([], common_command_exec, if initial then SOME init else NONE) > 
44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

499 
(visible orelse required) ? 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

500 
iterate_entries_after common 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

501 
(fn ((prev, id), _) => fn res => 
44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

502 
if not required andalso prev = last_visible then NONE 
47407  503 
else new_exec state proper_init id res) node; 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

504 

44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

505 
val no_execs = 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

506 
iterate_entries_after common 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

507 
(fn ((_, id0), exec0) => fn res => 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

508 
if is_none exec0 then NONE 
47405  509 
else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

510 
else SOME (id0 :: res)) node0 []; 
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

511 

47405  512 
val last_exec = if command_id' = no_id then NONE else SOME command_id'; 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

513 
val result = 
47407  514 
if is_some (after_entry node last_exec) then NONE 
515 
else SOME exec'; 

44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

516 

44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

517 
val node' = node 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

518 
> fold reset_entry no_execs 
47405  519 
> fold (fn (id, exec) => update_entry id (SOME exec)) new_execs 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

520 
> set_result result; 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

521 
val updated_node = 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

522 
if null no_execs andalso null new_execs then NONE 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

523 
else SOME (name, node'); 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

524 
in ((no_execs, new_execs, updated_node), node') end 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

525 
else (([], [], NONE), node) 
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

526 
end)) 
47628  527 
> Future.joins > map #1); 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

528 

44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

529 
val command_execs = 
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

530 
map (rpair NONE) (maps #1 updated) @ 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

531 
map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); 
47406
8818f54773cc
dynamic propagation of node "updated" status, which is required to propagate edits and reassigments and allow direct memo_result;
wenzelm
parents:
47405
diff
changeset

532 
val updated_nodes = map_filter #3 updated; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

533 

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

534 
val state' = state 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

535 
> define_version new_id (fold put_node updated_nodes new_version); 
47388
fe4b245af74c
discontinued obsolete last_execs (cf. cd3ab7625519);
wenzelm
parents:
47347
diff
changeset

536 
in (command_execs, state') end; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

537 

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

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

539 

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

540 

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

541 

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

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

543 

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

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

545 

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

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

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

548 

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

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

550 