author  wenzelm 
Sun, 18 Sep 2011 19:49:35 +0200  
changeset 44979  68b990e950b1 
parent 44804  3d9ee91394ce 
child 45666  d83797ef0d2d 
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 
44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

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

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

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

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

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

26 
val init_state: state 
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 
44301  28 
val cancel_execution: state > Future.task list 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

29 
val update_perspective: version_id > version_id > string > command_id list > state > state 
44481  30 
val update: version_id > version_id > edit list > state > 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

31 
((command_id * exec_id option) list * (string * command_id option) list) * state 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

32 
val execute: version_id > state > state 
44673  33 
val remove_versions: version_id list > state > state 
43713
1ba5331b4623
moved global state to structure Document (again);
wenzelm
parents:
43668
diff
changeset

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

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

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

37 

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

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

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

40 

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

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

42 

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

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

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

47 

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 
val no_id = 0; 
40449  49 
val new_id = Synchronized.counter (); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

50 

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

51 
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

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

53 

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

54 
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

55 
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

56 

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

57 

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 
(** document structure **) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

60 

44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

61 
type node_header = ((string * string) * string list * (string * bool) list) Exn.result; 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

62 
type perspective = (command_id > bool) * command_id option; (*visible commands, last*) 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

63 
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

64 

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

65 
type exec = exec_id * (Toplevel.state * unit lazy) lazy; (*eval/print process*) 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

66 
val no_print = Lazy.value (); 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

67 
val no_exec = (no_id, Lazy.value (Toplevel.toplevel, no_print)); 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

68 

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

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

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

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

73 
entries: exec option Entries.T, (*command entries with excecutions*) 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

74 
last_exec: command_id option, (*last command with exec state assignment*) 
44197
458573968568
refined Document.edit: less stateful update via Graph.schedule;
wenzelm
parents:
44196
diff
changeset

75 
result: Toplevel.state lazy} 
43668  76 
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

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

78 

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

79 
fun make_node (touched, header, perspective, entries, last_exec, result) = 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

80 
Node {touched = touched, header = header, perspective = perspective, 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

81 
entries = entries, last_exec = last_exec, result = result}; 
43668  82 

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

83 
fun map_node f (Node {touched, header, perspective, entries, last_exec, result}) = 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

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

85 

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

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

87 
(Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids); 
44441  88 

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

89 
val no_header = Exn.Exn (ERROR "Bad theory header"); 
44441  90 
val no_perspective = make_perspective []; 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

91 
val no_result = Lazy.value Toplevel.toplevel; 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

92 

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

93 
val empty_node = make_node (false, no_header, no_perspective, Entries.empty, NONE, no_result); 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

94 
val clear_node = map_node (fn (_, header, _, _, _, _) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

95 
(false, header, no_perspective, Entries.empty, NONE, no_result)); 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

96 

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

97 

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

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

99 

44446  100 
fun is_touched (Node {touched, ...}) = touched; 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

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

102 
map_node (fn (_, header, perspective, entries, last_exec, result) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

103 
(touched, header, perspective, entries, last_exec, result)); 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

104 

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

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

107 
map_node (fn (touched, _, perspective, entries, last_exec, result) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

108 
(touched, header, perspective, entries, last_exec, result)); 
44180  109 

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

110 
fun get_perspective (Node {perspective, ...}) = perspective; 
44441  111 
fun set_perspective ids = 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

112 
map_node (fn (touched, header, _, entries, last_exec, result) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

113 
(touched, header, make_perspective ids, entries, last_exec, result)); 
44385
e7fdb008aa7d
propagate editor perspective through document model;
wenzelm
parents:
44384
diff
changeset

114 

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

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

116 
map_node (fn (touched, header, perspective, entries, last_exec, result) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

117 
(touched, header, perspective, f entries, last_exec, 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

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

119 

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

120 
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

121 
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

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

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

124 
 SOME id => Entries.iterate (SOME id) f entries); 
43668  125 

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

126 
fun get_last_exec (Node {last_exec, ...}) = last_exec; 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

127 
fun set_last_exec last_exec = 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

128 
map_node (fn (touched, header, perspective, entries, _, result) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

129 
(touched, header, perspective, entries, last_exec, result)); 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

130 

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

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

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

133 
map_node (fn (touched, header, perspective, entries, last_exec, _) => 
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

134 
(touched, header, perspective, entries, last_exec, result)); 
44180  135 

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

139 

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

140 

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

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

142 

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

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

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

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

148 

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

150 

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

151 
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

152 

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

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

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

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

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

157 

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

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

160 
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

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

162 

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

163 
fun the_default_entry node (SOME id) = (id, (the_default no_exec (the_entry node id))) 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

165 

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

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

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

168 

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

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

170 
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

171 

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

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

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

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

175 
 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

176 

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

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

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

180 

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

181 

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

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

183 

44185  184 
val empty_version = Version Graph.empty; 
185 

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

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

188 

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

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

190 

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

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

193 
fun touch_node name nodes = 
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

194 
fold (fn desc => 
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

195 
update_node desc 
9987ae55e17b
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
wenzelm
parents:
44614
diff
changeset

196 
(set_touched true #> 
9987ae55e17b
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
wenzelm
parents:
44614
diff
changeset

197 
desc <> name ? (map_entries (reset_after NONE) #> set_result no_result))) 
44202  198 
(Graph.all_succs nodes [name]) nodes; 
199 

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

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

201 

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

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

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

204 
(case node_edit of 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

205 
Clear => 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

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

208 
> touch_node name 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

209 
 Edits edits => 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

211 
> update_node name (edit_node edits) 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

212 
> touch_node name 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

213 
 Header header => 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

215 
val parents = (case header of Exn.Res (_, parents, _) => parents  _ => []); 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

217 
> default_node name 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

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

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

221 
(fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name); 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

222 
val (header', nodes3) = 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

223 
(header, Graph.add_deps_acyclic (name, parents) nodes2) 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

224 
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2); 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

225 
in Graph.map_node name (set_header header') nodes3 end 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

226 
> touch_node name 
44436
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

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

229 

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

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

231 

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

232 
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

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

234 

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

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

236 

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

237 

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 
(** global state  document structure and execution process **) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

240 

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

241 
abstype state = State of 
40398  242 
{versions: version Inttab.table, (*version_id > document content*) 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

243 
commands: (string * Toplevel.transition future) Inttab.table, (*command_id > name * transition*) 
44673  244 
execution: version_id * Future.group} (*current execution process*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

246 

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

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

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

249 

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

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

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

252 

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

253 
val init_state = 
44675
f665a5d35a3d
discontinued predefined empty command (obsolete!?);
wenzelm
parents:
44674
diff
changeset

254 
make_state (Inttab.make [(no_id, empty_version)], Inttab.empty, (no_id, Future.new_group NONE)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

255 

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

256 

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

257 
(* document versions *) 
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 
fun define_version (id: version_id) version = 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

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

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

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

264 

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

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

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

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

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

269 

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

272 

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

273 

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

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

275 

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

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

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

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

279 
val id_string = print_id id; 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

280 
val future = 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

281 
(singleton o Future.forks) 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

282 
{name = "Document.define_command", group = SOME (Future.new_group NONE), 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

283 
deps = [], pri = ~1, interrupts = false} 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

284 
(fn () => 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

285 
Position.setmp_thread_data (Position.id_only id_string) 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

286 
(fn () => Outer_Syntax.read_command (Position.id id_string) text) ()); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

287 
val commands' = 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

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

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

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

291 

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

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

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

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

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

296 

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

297 

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

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

299 

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

301 

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

302 
end; 
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 

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

305 

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

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

307 

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

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

309 

44440  310 
fun timing tr t = 
311 
if Timing.is_relevant t then Toplevel.status tr (Markup.timing t) else (); 

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

312 

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

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

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

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

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

317 

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

318 
fun print_state tr st = 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

319 
(Lazy.lazy o Toplevel.setmp_thread_position tr) 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

320 
(fn () => Toplevel.print_state false st); 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

321 

40390  322 
fun run int tr st = 
323 
(case Toplevel.transition int tr st of 

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

44614
466ea227e00d
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
wenzelm
parents:
44611
diff
changeset

325 
 SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) 
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44247
diff
changeset

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

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

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

329 

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

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

332 
val is_init = Toplevel.is_init tr; 
44185  333 
val is_proof = Keyword.is_proof (Toplevel.name_of tr); 
334 

44614
466ea227e00d
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
wenzelm
parents:
44611
diff
changeset

335 
val _ = Multithreading.interrupted (); 
44611  336 
val _ = Toplevel.status tr Markup.forked; 
44185  337 
val start = Timing.start (); 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

338 
val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; 
44185  339 
val _ = timing tr (Timing.result start); 
44611  340 
val _ = Toplevel.status tr Markup.joined; 
44185  341 
val _ = List.app (Toplevel.error_msg tr) errs; 
342 
in 

343 
(case result of 

44614
466ea227e00d
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
wenzelm
parents:
44611
diff
changeset

344 
NONE => 
44804
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

345 
let 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

346 
val _ = if null errs then Exn.interrupt () else (); 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

347 
val _ = Toplevel.status tr Markup.failed; 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

348 
in (st, no_print) end 
44185  349 
 SOME st' => 
44804
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

350 
let 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

351 
val _ = Toplevel.status tr Markup.finished; 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

352 
val _ = proof_status tr st'; 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

353 
val do_print = 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

354 
not is_init andalso 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

355 
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); 
3d9ee91394ce
no print_state for final proof commands, which return to theory state;
wenzelm
parents:
44675
diff
changeset

356 
in (st', if do_print then print_state tr st' else no_print) end) 
44185  357 
end; 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

358 

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

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

360 

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

361 

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

362 

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

363 

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

365 

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

366 
(* perspective *) 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

367 

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

368 
fun update_perspective (old_id: version_id) (new_id: version_id) name perspective state = 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

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

370 
val old_version = the_version state old_id; 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

371 
val _ = Time.now (); (* FIXME odd workaround for polyml5.4.0/x86_64  needed? *) 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

372 
val new_version = edit_nodes (name, Perspective perspective) old_version; 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

373 
in define_version new_id new_version state end; 
546adfa8a6fc
update_perspective without actual edits, bypassing the full state assignment protocol;
wenzelm
parents:
44435
diff
changeset

374 

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

375 

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

377 

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

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

379 

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

380 
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

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

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

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

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

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

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

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

388 
 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

389 
in (visible', initial') end; 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

390 
fun get_common ((prev, id), exec) (found, (_, flags)) = 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

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

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

393 
let val found' = 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

394 
is_none exec orelse op <> (pairself (Option.map #1) (exec, lookup_entry node0 id)); 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

395 
in SOME (found', (prev, update_flags prev flags)) end; 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

396 
val (found, (common, flags)) = 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

397 
iterate_entries get_common node (false, (NONE, (true, true))); 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

399 
if found then (common, flags) 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

401 
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

402 
in (last, update_flags last flags) end 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

404 

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

405 
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

406 

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

407 
fun new_exec state bad_init command_id' (execs, command_exec, init) = 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

408 
if bad_init andalso is_none init then NONE 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

410 
let 
44660
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

411 
val (name, tr0) = the_command state command_id' > Future.join; 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

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

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

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

416 
val exec_id' = new_id (); 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

417 
val tr = tr0 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

418 
> modify_init 
90bab3febb6c
less agressive parsing of commands (priority ~1);
wenzelm
parents:
44645
diff
changeset

419 
> Toplevel.put_id (print_id exec_id'); 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

420 
val exec' = snd (snd command_exec) > Lazy.map (fn (st, _) => run_command tr st); 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

422 
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

423 

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

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

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

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

427 
Graph.fold (fn (a, (node, _)) => is_some (#2 (get_perspective node)) ? cons a) nodes [] 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

428 
> Graph.all_preds nodes; 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

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

430 
fold (fn a => exists (fn b => Graph.is_edge nodes (a, b)) all_visible ? Symtab.update (a, ())) 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

431 
all_visible Symtab.empty; 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

432 
in Symtab.defined required end; 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

433 

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

434 
fun check_theory nodes name = 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

435 
is_some (Thy_Info.lookup_theory name) orelse (* FIXME more robust!? *) 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

436 
is_some (Exn.get_res (get_header (get_node nodes name))); 
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

437 

44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

438 
fun init_theory deps node = 
44435  439 
let 
44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

440 
(* FIXME provide files via Scala layer, not master_dir *) 
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

441 
val ((master_dir, thy_name), imports, uses) = Exn.release (get_header node); 
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

442 
val files = map (apfst Path.explode) uses; 
44435  443 
val parents = 
444 
imports > map (fn import => 

44441  445 
(case Thy_Info.lookup_theory import of (* FIXME more robust!? *) 
44435  446 
SOME thy => thy 
447 
 NONE => 

448 
get_theory (Position.file_only import) 

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

449 
(snd (Future.join (the (AList.lookup (op =) deps import)))))); 
44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

450 
in Thy_Load.begin_theory (Path.explode master_dir) thy_name imports files parents end; 
44435  451 

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

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

453 

44481  454 
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

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

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

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

459 

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

460 
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

461 
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

462 

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

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

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

465 
(fn deps => fn (name, node) => 
44544
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

466 
if not (is_touched node orelse is_required name) 
da5f0af32c1b
more precise treatment of nodes that are fully required for partially visible ones;
wenzelm
parents:
44483
diff
changeset

467 
then Future.value (([], [], []), node) 
44444
33a5616a7571
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
wenzelm
parents:
44441
diff
changeset

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

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

470 
val node0 = node_of old_version name; 
44979
68b990e950b1
explicit master_dir as part of header  still required (for Cygwin) since Scala layer does not pass file content yet;
wenzelm
parents:
44804
diff
changeset

471 
fun init () = init_theory deps node; 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

473 
not (check_theory nodes name andalso forall (check_theory nodes o #1) deps); 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

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

475 
(singleton o Future.forks) 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

476 
{name = "Document.update", group = NONE, 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

477 
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = false} 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

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

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

480 
val required = is_required name; 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

481 
val last_visible = #2 (get_perspective node); 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

482 
val (common, (visible, initial)) = last_common state last_visible node0 node; 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

483 
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

484 

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

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

486 
([], 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

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

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

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

490 
if not required andalso prev = last_visible then NONE 
44645
5938beb84adc
more precise iterate_entries_after if start refers to last entry;
wenzelm
parents:
44644
diff
changeset

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

492 

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

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

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

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

496 
if is_none exec0 then NONE 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

497 
else if exists (fn (_, (id, _)) => id0 = id) execs then SOME res 
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

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

499 

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

500 
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

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

502 
if is_some (after_entry node last_exec) then no_result 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

503 
else Lazy.map #1 exec; 
44480
38c5b085fb1c
improved Document.edit: more accurate update_start and no_execs;
wenzelm
parents:
44479
diff
changeset

504 

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

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

506 
> fold reset_entry no_execs 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

507 
> fold (fn (id, exec) => update_entry id (SOME exec)) execs 
44482
c7225307acf2
further clarification of Document.updated, based on last_common and after_entry;
wenzelm
parents:
44481
diff
changeset

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

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

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

511 
in ((no_execs, execs, [(name, node')]), node') end) 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

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

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

514 

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

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

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

517 
map (fn (command_id, (exec_id, _)) => (command_id, SOME exec_id)) (maps #2 updated); 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

518 
val updated_nodes = maps #3 updated; 
44476
e8a87398f35d
propagate information about last command with exec state assignment through document model;
wenzelm
parents:
44446
diff
changeset

519 
val last_execs = map (fn (name, node) => (name, get_last_exec node)) updated_nodes; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

520 

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

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

522 
> define_version new_id (fold put_node updated_nodes new_version); 
44479
9a04e7502e22
refined document state assignment: observe perspective, more explicit assignment message;
wenzelm
parents:
44478
diff
changeset

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

524 

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

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

526 

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

527 

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

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

529 

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

530 
fun execute version_id state = 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

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

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

534 

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

535 
fun force_exec _ _ NONE = () 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

536 
 force_exec node command_id (SOME (_, exec)) = 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

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

538 
val (_, print) = Lazy.force exec; 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

539 
val _ = 
44439
2bcd2aefaf7f
print state only for visible command, to avoid wasting resources for the larger part of the text;
wenzelm
parents:
44436
diff
changeset

540 
if #1 (get_perspective node) command_id 
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

541 
then ignore (Lazy.future Future.default_params print) 
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44385
diff
changeset

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

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

544 

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

546 
val _ = 
44201  547 
nodes_of version > Graph.schedule 
548 
(fn deps => fn (name, node) => 

44302  549 
(singleton o Future.forks) 
44673  550 
{name = "theory:" ^ name, group = SOME (Future.new_group (SOME group)), 
44614
466ea227e00d
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
wenzelm
parents:
44611
diff
changeset

551 
deps = map (Future.task_of o #2) deps, pri = 1, interrupts = false} 
44674
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

552 
(iterate_entries (fn ((_, id), exec) => fn () => 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

553 
SOME (force_exec node id exec)) node)); 
40520
77a7b0a7d4b1
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
wenzelm
parents:
40481
diff
changeset

554 

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

555 
in (versions, commands, (version_id, group)) end); 
44673  556 

557 

558 
(* remove versions *) 

559 

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

560 
fun remove_versions ids state = state > map_state (fn (versions, _, execution) => 
44673  561 
let 
562 
val _ = member (op =) ids (#1 execution) andalso 

563 
error ("Attempt to remove execution version " ^ print_id (#1 execution)); 

564 

565 
val versions' = fold delete_version ids versions; 

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

566 
val commands' = 
44675
f665a5d35a3d
discontinued predefined empty command (obsolete!?);
wenzelm
parents:
44674
diff
changeset

567 
(versions', Inttab.empty) > 
44673  568 
Inttab.fold (fn (_, version) => nodes_of version > 
569 
Graph.fold (fn (_, (node, _)) => node > 

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

570 
iterate_entries (fn ((_, id), _) => 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

571 
SOME o Inttab.insert (K true) (id, the_command state id)))); 
bad4f9158c80
discontinued global execs: store exec value directly within entries;
wenzelm
parents:
44673
diff
changeset

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

573 

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

574 

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

575 

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

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

577 

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

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

579 

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

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

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

582 

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

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

584 