author  wenzelm 
Wed, 10 Jul 2013 12:33:28 +0200  
changeset 52573  815461c835b9 
parent 52570  26d84a0b9209 
child 52586  7a0935571a23 
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 
52536  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 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

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

11 
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

12 
Clear  (* FIXME unused !? *) 
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

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

14 
Deps of node_header  
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

15 
Perspective of Document_ID.command list 
44156  16 
type edit = string * node_edit 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

18 
val init_state: state 
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

19 
val define_command: Document_ID.command > string > string > state > state 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

20 
val remove_versions: Document_ID.version 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

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

22 
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

23 
val start_execution: state > unit 
47628  24 
val timing: bool Unsynchronized.ref 
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

25 
val update: Document_ID.version > Document_ID.version > edit list > state > 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

26 
(Document_ID.command * Document_ID.exec list) list * state 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

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

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

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

30 

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

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

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

33 

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

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

35 

52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

36 
fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ Document_ID.print id); 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

37 
fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document_ID.print id); 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

38 

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

39 
type node_header = string * Thy_Header.header * string list; 
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

40 
type perspective = Inttab.set * Document_ID.command option; 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

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

42 

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

44 
{header: node_header, (*master directory, theory header, errors*) 
52508  45 
perspective: perspective, (*visible commands, last visible command*) 
52532  46 
entries: Command.exec option Entries.T * bool, (*command entries with excecutions, stable*) 
52526  47 
result: Command.eval option} (*result of last execution*) 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

48 
and version = Version of node String_Graph.T (*development graph wrt. static imports*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

50 

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

51 
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

52 
Node {header = header, perspective = perspective, entries = entries, result = result}; 
43668  53 

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

54 
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

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

56 

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

57 
fun make_perspective command_ids : perspective = 
52526  58 
(Inttab.make_set command_ids, try List.last command_ids); 
44441  59 

51294
0850d43cb355
discontinued obsolete header "files"  these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset

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

62 

49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

63 
val empty_node = make_node (no_header, no_perspective, (Entries.empty, true), NONE); 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

64 
val clear_node = 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

65 
map_node (fn (header, _, _, _) => (header, no_perspective, (Entries.empty, true), NONE)); 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

66 

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

67 

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

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

69 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

70 
fun set_header header = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

71 
map_node (fn (_, perspective, entries, result) => (header, perspective, entries, result)); 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

72 

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

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

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

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

76 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

77 
fun read_header node span = 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

78 
let 
51294
0850d43cb355
discontinued obsolete header "files"  these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset

79 
val (dir, {name = (name, _), imports, keywords}) = get_header node; 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

80 
val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span; 
51294
0850d43cb355
discontinued obsolete header "files"  these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset

81 
in (dir, Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords) end; 
44180  82 

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

83 
fun get_perspective (Node {perspective, ...}) = perspective; 
44441  84 
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

85 
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

86 

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

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

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

89 
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

90 

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

91 
fun map_entries f = 
49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

92 
map_node (fn (header, perspective, (entries, stable), result) => 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

93 
(header, perspective, (f entries, stable), result)); 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

94 
fun get_entries (Node {entries = (entries, _), ...}) = entries; 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

95 

bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

96 
fun entries_stable stable = 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

97 
map_node (fn (header, perspective, (entries, _), result) => 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

98 
(header, perspective, (entries, stable), result)); 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

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

100 

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

101 
fun iterate_entries f = Entries.iterate NONE f o get_entries; 
49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

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

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

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

105 
 SOME id => Entries.iterate (SOME id) f entries); 
43668  106 

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

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

108 
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

109 
map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); 
44180  110 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

111 
fun changed_result node node' = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

112 
(case (get_result node, get_result node') of 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

113 
(SOME eval, SOME eval') => #exec_id eval <> #exec_id eval' 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

114 
 (NONE, NONE) => false 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

115 
 _ => true); 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

116 

52533  117 
fun finished_theory node = 
52534  118 
(case Exn.capture (Command.eval_result_state o the) (get_result node) of 
119 
Exn.Res st => can (Toplevel.end_theory Position.none) st 

52533  120 
 _ => false); 
121 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

122 
fun get_node nodes name = String_Graph.get_node nodes name 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

123 
handle String_Graph.UNDEF _ => empty_node; 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

124 
fun default_node name = String_Graph.default_node (name, empty_node); 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

125 
fun update_node name f = default_node name #> String_Graph.map_node name f; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

126 

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

127 

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

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

129 

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

130 
datatype node_edit = 
44185  131 
Clear  
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

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

133 
Deps of node_header  
52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

134 
Perspective of Document_ID.command list; 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

135 

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

137 

49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

138 
val after_entry = Entries.get_after o get_entries; 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

139 

49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

140 
fun lookup_entry node id = 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

141 
(case Entries.lookup (get_entries node) id of 
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

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

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

144 

49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

145 
fun the_entry node id = 
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

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

147 
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

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

149 

52532  150 
fun the_default_entry node (SOME id) = (id, the_default Command.no_exec (the_entry node id)) 
151 
 the_default_entry _ NONE = (Document_ID.none, Command.no_exec); 

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

152 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

153 
fun assign_entry (command_id, exec) node = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

154 
if is_none (Entries.lookup (get_entries node) command_id) then node 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

155 
else map_entries (Entries.update (command_id, exec)) node; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

156 

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

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

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

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

160 
 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

161 

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

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

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

165 

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

166 

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

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

168 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

169 
val empty_version = Version String_Graph.empty; 
44185  170 

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

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

173 

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

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

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

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

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

179 
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

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

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

182 
let 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

183 
val imports = map fst (#imports header); 
48707
ba531af91148
simplified Document.Node.Header  internalized errors;
wenzelm
parents:
47633
diff
changeset

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

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

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

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

188 
> default_node name 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

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

190 
val nodes2 = nodes1 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

191 
> String_Graph.Keys.fold 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

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

193 
val (nodes3, errors2) = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

194 
(String_Graph.add_deps_acyclic (name, imports) nodes2, errors1) 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

195 
handle String_Graph.CYCLES cs => (nodes2, errors1 @ map cycle_msg cs); 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

196 
in String_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

197 
 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

198 

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

199 
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

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

201 

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

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

203 

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

204 

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

205 

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

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

207 

52536  208 
type execution = 
209 
{version_id: Document_ID.version, 

210 
group: Future.group, 

211 
running: bool Unsynchronized.ref}; 

212 

213 
val no_execution = 

214 
{version_id = Document_ID.none, 

215 
group = Future.new_group NONE, 

216 
running = Unsynchronized.ref false}; 

217 

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

218 
abstype state = State of 
52536  219 
{versions: version Inttab.table, (*version id > document content*) 
220 
commands: (string * Token.T list lazy) Inttab.table, (*command id > named span*) 

221 
execution: execution} (*current execution process*) 

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

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

223 

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

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

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

226 

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

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

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

229 

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

230 
val init_state = 
52536  231 
make_state (Inttab.make [(Document_ID.none, empty_version)], Inttab.empty, no_execution); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

232 

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

233 
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

234 

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

235 

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

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

237 

52536  238 
fun define_version 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

239 
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

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

242 
handle Inttab.DUP dup => err_dup "document version" dup; 
52536  243 
val execution' = 
244 
{version_id = version_id, 

245 
group = Future.new_group NONE, 

246 
running = Unsynchronized.ref true}; 

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

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

248 

52536  249 
fun the_version (State {versions, ...}) version_id = 
250 
(case Inttab.lookup versions version_id of 

251 
NONE => err_undef "document version" version_id 

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

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

253 

52536  254 
fun delete_version version_id versions = 
255 
Inttab.delete version_id versions 

256 
handle Inttab.UNDEF _ => err_undef "document version" version_id; 

44673  257 

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

258 

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

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

260 

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

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

263 
let 
52536  264 
val id = Document_ID.print command_id; 
265 
val span = 

266 
Lazy.lazy (fn () => 

267 
Position.setmp_thread_data (Position.id_only id) 

268 
(fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id) text) ()); 

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

269 
val _ = 
52536  270 
Position.setmp_thread_data (Position.id_only id) 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49906
diff
changeset

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

272 
val commands' = 
52536  273 
Inttab.update_new (command_id, (name, span)) commands 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

276 

52536  277 
fun the_command (State {commands, ...}) command_id = 
278 
(case Inttab.lookup commands command_id of 

279 
NONE => err_undef "command" command_id 

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

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

281 

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

282 
val the_command_name = #1 oo the_command; 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

283 

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

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

285 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

286 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

287 
(* remove_versions *) 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

288 

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

290 
let 
52536  291 
val _ = 
292 
member (op =) version_ids (#version_id execution) andalso 

293 
error ("Attempt to remove execution version " ^ Document_ID.print (#version_id execution)); 

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

294 

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

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

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

298 
Inttab.fold (fn (_, version) => nodes_of version > 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

299 
String_Graph.fold (fn (_, (node, _)) => node > 
52536  300 
iterate_entries (fn ((_, command_id), _) => 
301 
SOME o Inttab.insert (K true) (command_id, the_command state command_id)))); 

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

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

303 

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

304 

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

305 

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

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

307 

52536  308 
val discontinue_execution = execution_of #> (fn {running, ...} => running := false); 
309 
val cancel_execution = execution_of #> (fn {group, ...} => Future.cancel_group group); 

310 
val terminate_execution = execution_of #> (fn {group, ...} => Future.terminate group); 

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

311 

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

312 
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

313 
let 
52536  314 
val {version_id, group, running} = execution_of state; 
47420
0dbe6c69eda2
just one dedicated execution per document version  NB: nonmonotonicity of cancel always requires fresh update;
wenzelm
parents:
47415
diff
changeset

315 
val _ = 
52573
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

316 
if not (! running) orelse Task_Queue.is_canceled group then [] 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

317 
else 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

318 
nodes_of (the_version state version_id) > String_Graph.schedule 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

319 
(fn deps => fn (name, node) => 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

320 
if not (visible_node node) andalso finished_theory node then 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

321 
Future.value () 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

322 
else 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

323 
(singleton o Future.forks) 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

324 
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

325 
deps = map (Future.task_of o #2) deps, pri = ~2, interrupts = false} 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

326 
(fn () => 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

327 
iterate_entries (fn (_, opt_exec) => fn () => 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

328 
(case opt_exec of 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

329 
SOME exec => if ! running then SOME (Command.execute exec) else NONE 
815461c835b9
tuned start_execution: avoid sleep on worker thread;
wenzelm
parents:
52570
diff
changeset

330 
 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

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

332 

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

333 

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

334 

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

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

336 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

337 
(* exec state assignment *) 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

338 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

339 
type assign_update = Command.exec option Inttab.table; (*command id > exec*) 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

340 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

341 
val assign_update_empty: assign_update = Inttab.empty; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

342 
fun assign_update_null (tab: assign_update) = Inttab.is_empty tab; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

343 
fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

344 
fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

345 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

346 
fun assign_update_new upd (tab: assign_update) = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

347 
Inttab.update_new upd tab 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

348 
handle Inttab.DUP dup => err_dup "exec state assignment" dup; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

349 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

350 
fun assign_update_result (tab: assign_update) = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

351 
Inttab.fold (fn (command_id, exec) => cons (command_id, Command.exec_ids exec)) tab []; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

352 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

353 

52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

354 
(* update *) 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

355 

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

358 

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

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

360 

47335  361 
fun make_required nodes = 
362 
let 

363 
val all_visible = 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

364 
String_Graph.fold (fn (a, (node, _)) => visible_node node ? cons a) nodes [] 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

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

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

367 

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

369 
Symtab.fold (fn (a, ()) => 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

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

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

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

374 
fun init_theory deps node span = 
47335  375 
let 
49173
fa01a202399c
eliminated potentially confusing terminology of Scala "layer";
wenzelm
parents:
49064
diff
changeset

376 
(* FIXME provide files via Isabelle/Scala, not master_dir *) 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

377 
val (dir, header) = read_header node span; 
47335  378 
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

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

380 
SOME (Url.File path) => path 
47335  381 
 _ => Path.current); 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

382 
val imports = #imports header; 
47335  383 
val parents = 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

384 
imports > map (fn (import, _) => 
47407  385 
(case Thy_Info.lookup_theory import of 
47335  386 
SOME thy => thy 
387 
 NONE => 

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

388 
Toplevel.end_theory (Position.file_only import) 
52536  389 
(case get_result (snd (the (AList.lookup (op =) deps import))) of 
390 
NONE => Toplevel.toplevel 

391 
 SOME eval => Command.eval_result_state eval))); 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

392 
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); 
47335  393 
in Thy_Load.begin_theory master_dir header parents end; 
394 

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

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

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

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

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

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

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

402 
let 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

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

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

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

406 
NONE => true 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

407 
 SOME command_id => not (Keyword.is_theory_begin (the_command_name state command_id))); 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

408 
in (visible', initial') end; 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

409 

18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

410 
fun get_common ((prev, command_id), opt_exec) (_, same, flags, assign_update) = 
47630  411 
if same then 
412 
let 

413 
val flags' = update_flags prev flags; 

414 
val same' = 

415 
(case opt_exec of 

416 
NONE => false 

52533  417 
 SOME (eval, _) => 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

418 
(case lookup_entry node0 command_id of 
47630  419 
NONE => false 
52533  420 
 SOME (eval0, _) => 
421 
#exec_id eval = #exec_id eval0 andalso Command.stable_eval eval)); 

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

422 
val assign_update' = assign_update > 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

423 
(case opt_exec of 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

424 
SOME (eval, prints) => 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

425 
let 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

426 
val command_visible = visible_command node command_id; 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

427 
val command_name = the_command_name state command_id; 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

428 
in 
52570  429 
(case Command.print command_visible command_name eval prints of 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

430 
SOME prints' => assign_update_new (command_id, SOME (eval, prints')) 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

431 
 NONE => I) 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

432 
end 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

433 
 NONE => I); 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

434 
in SOME (prev, same', flags', assign_update') end 
47630  435 
else NONE; 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

436 
val (common, same, flags, assign_update') = 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

437 
iterate_entries get_common node (NONE, true, (true, true), assign_update_empty); 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

438 
val (common', flags') = 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

439 
if same then 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

440 
let val last = Entries.get_after (get_entries node) common 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

441 
in (last, update_flags last flags) end 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

442 
else (common, flags); 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

443 
in (assign_update', common', flags') end; 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

444 

52534  445 
fun illegal_init _ = error "Illegal theory header after end of theory"; 
446 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

447 
fun new_exec state proper_init command_visible command_id' (assign_update, command_exec, init) = 
47407  448 
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

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

450 
let 
52534  451 
val (_, (eval, _)) = command_exec; 
52527
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52526
diff
changeset

452 
val (command_name, span) = the_command state command_id' > Lazy.force; 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

453 

52534  454 
val eval' = Command.eval (fn () => the_default illegal_init init span) span eval; 
52570  455 
val prints' = perhaps (Command.print command_visible command_name eval') []; 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

456 
val exec' = (eval', prints'); 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

457 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

458 
val assign_update' = assign_update_new (command_id', SOME exec') assign_update; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

459 
val init' = if Keyword.is_theory_begin command_name then NONE else init; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

460 
in SOME (assign_update', (command_id', (eval', prints')), init') end; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

462 

52536  463 
fun update old_version_id new_version_id edits state = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

464 
let 
52536  465 
val old_version = the_version state old_version_id; 
47628  466 
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

467 

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

468 
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

469 
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

470 

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

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50201
diff
changeset

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

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

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

476 
{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

477 
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

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

479 
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

480 
val imports = map (apsnd Future.join) deps; 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

481 
val imports_changed = exists (#3 o #1 o #2) imports; 
52514  482 
val node_required = is_required name; 
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 
in 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

484 
if imports_changed orelse AList.defined (op =) edits name orelse 
49064
bd6cc0b911a1
maintain stable state of node entries from last round  bypass slightly different Thm.join_theory_proofs;
wenzelm
parents:
49061
diff
changeset

485 
not (stable_entries node) orelse not (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

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

487 
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

488 
val node0 = node_of old_version name; 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48918
diff
changeset

489 
val init = init_theory imports node; 
47407  490 
val proper_init = 
491 
check_theory false name node andalso 

492 
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

493 

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

494 
val (print_execs, common, (still_visible, initial)) = 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

495 
if imports_changed then (assign_update_empty, NONE, (true, true)) 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

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

497 
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

498 

52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

499 
val (updated_execs, (command_id', (eval', _)), _) = 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

500 
(print_execs, common_command_exec, if initial then SOME init else NONE) 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

501 
> (still_visible orelse node_required) ? 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

503 
(fn ((prev, id), _) => fn res => 
52569
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

504 
if not node_required andalso prev = visible_last node then NONE 
18dde2cf7aa7
produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
wenzelm
parents:
52566
diff
changeset

505 
else new_exec state proper_init (visible_command node id) id res) node; 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

506 

52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

507 
val assigned_execs = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

508 
(node0, updated_execs) > iterate_entries_after common 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

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

510 
if is_none exec0 then NONE 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

511 
else if assign_update_defined updated_execs command_id0 then SOME res 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

512 
else SOME (assign_update_new (command_id0, NONE) res)); 
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

513 

52530
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

514 
val last_exec = 
99dd8b4ef3fe
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
wenzelm
parents:
52527
diff
changeset

515 
if command_id' = Document_ID.none 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

516 
val result = 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

517 
if is_none last_exec orelse is_some (after_entry node last_exec) then NONE 
52526  518 
else SOME eval'; 
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

519 

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

520 
val node' = node 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

521 
> assign_update_apply assigned_execs 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

522 
> entries_stable (assign_update_null updated_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

523 
> set_result result; 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

524 
val assigned_node = 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

525 
if assign_update_null assigned_execs then NONE else SOME (name, node'); 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

526 
val result_changed = changed_result node0 node'; 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

527 
in 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

528 
((assign_update_result assigned_execs, assigned_node, result_changed), node') 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

529 
end 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

530 
else (([], NONE, false), 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

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

533 

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

534 
val state' = state 
52566
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

535 
> define_version new_version_id (fold put_node (map_filter #2 updated) new_version); 
52a0eacf04d1
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
wenzelm
parents:
52536
diff
changeset

536 
in (maps #1 updated, 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 

52508  544 
val global_state = Synchronized.var "Document.global_state" init_state; 
43713
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 