author  wenzelm 
Tue, 31 Aug 2010 23:46:49 +0200  
changeset 38888  8248cda328de 
parent 38873  278f552b2e97 
child 39232  69c6d3e87660 
permissions  rwrr 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

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

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

3 

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

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

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

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

7 

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

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

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

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

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

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

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

17 
val print_id: id > string 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

18 
type edit = string * ((command_id option * command_id option) list) option 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

21 
val define_command: command_id > string > state > state 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

23 
val execute: version_id > state > state 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

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

25 

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

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

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

28 

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

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

30 

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

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

33 
type command_id = id; 
38373  34 
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

35 

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

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

37 

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

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

39 
val id_count = Synchronized.var "id" 0; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

40 
in 
38419  41 
fun new_id () = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

42 
Synchronized.change_result id_count 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

43 
(fn i => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

44 
let val i' = i + 1 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

47 

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

48 
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

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

50 

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

51 
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

52 
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

53 

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

54 

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

55 

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

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

57 

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

58 
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

59 

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

60 
abstype node = Node of exec_id option Entries.T (*command entries with excecutions*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

63 

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

64 
val empty_node = Node Entries.empty; 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

65 
val empty_version = Version Graph.empty; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

66 

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

67 
fun fold_entries start f (Node entries) = Entries.fold start f entries; 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

68 
fun first_entry start P (Node entries) = Entries.get_first start P entries; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

69 

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

70 

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

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

72 

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

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

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

75 
(*NONE: remove node, SOME: insert/remove commands*) 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

76 
((command_id option * command_id option) list) option; 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

77 

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

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

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

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

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

82 

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

83 
fun update_entry (id, exec_id) (Node entries) = 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

84 
Node (Entries.update (id, SOME exec_id) entries); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

85 

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

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

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

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

89 
 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

90 

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

91 
fun edit_node (hook, SOME id2) (Node entries) = 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

92 
Node (Entries.insert_after hook (id2, NONE) entries) 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

93 
 edit_node (hook, NONE) (Node entries) = 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

94 
Node (entries > Entries.delete_after hook > reset_after hook); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

95 

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

96 

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

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

98 

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

99 
fun nodes_of (Version nodes) = nodes; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

100 
val node_names_of = Graph.keys o nodes_of; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

101 

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

102 
fun get_node version name = Graph.get_node (nodes_of version) name 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

103 
handle Graph.UNDEF _ => empty_node; 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

104 

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

105 
fun edit_nodes (name, SOME edits) (Version nodes) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

107 
> Graph.default_node (name, empty_node) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

108 
> Graph.map_node name (fold edit_node edits)) 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

109 
 edit_nodes (name, NONE) (Version nodes) = 
38449  110 
Version (Graph.del_node name nodes); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

111 

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

112 
fun put_node name node (Version nodes) = 
38449  113 
Version (Graph.map_node name (K node) nodes); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

114 

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

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

116 

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

117 

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

118 

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

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

120 

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

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

122 
{versions: version Inttab.table, (*version_id > document content*) 
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

123 
commands: Toplevel.transition future Inttab.table, (*command_id > transition (future parsing)*) 
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

124 
execs: Toplevel.state option lazy Inttab.table, (*exec_id > execution process*) 
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

125 
execution: unit future list} (*global execution process*) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

127 

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

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

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

130 

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

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

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

133 

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

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

135 
make_state (Inttab.make [(no_id, empty_version)], 
38449  136 
Inttab.make [(no_id, Future.value Toplevel.empty)], 
137 
Inttab.make [(no_id, Lazy.value (SOME Toplevel.toplevel))], 

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

138 
[]); 
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 

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

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

142 

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

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

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

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

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

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

148 

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

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

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

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

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

153 

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

154 

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

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

156 

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

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

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

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

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

161 
val tr = Future.fork_pri 2 (fn () => 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

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

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

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

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

168 

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

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

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

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

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

173 

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

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

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

176 

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

177 

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

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

179 

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

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

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

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

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

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

185 

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

186 
fun the_exec (State {execs, ...}) (id: exec_id) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

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

190 

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

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

192 

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

193 

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

194 

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

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

196 

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

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

198 

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

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

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

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

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

203 

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

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

205 
if Toplevel.print_of tr then 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

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

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

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

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

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

212 

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

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

214 

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

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

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

217 
(case Toplevel.init_of tr of 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

218 
SOME name => Exn.capture (fn () => Thy_Header.consistent_name thy_name name) () 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

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

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

222 
val int = is_some (Toplevel.init_of tr); 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

223 
val (errs, result) = 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

224 
(case Toplevel.transition int tr st of 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

225 
SOME (st', NONE) => ([], SOME st') 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

226 
 SOME (_, SOME exn_info) => 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

227 
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

228 
[] => raise Exn.Interrupt 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

230 
 NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

231 
val _ = List.app (Toplevel.error_msg tr) errs; 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

233 
(case result of 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

234 
NONE => Toplevel.status tr Markup.failed 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

235 
 SOME st' => 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

236 
(Toplevel.status tr Markup.finished; 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

238 
if int then () else async_state tr st')); 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

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

240 
 Exn.Exn exn => 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

241 
(Toplevel.error_msg tr (ML_Compiler.exn_message exn); Toplevel.status tr Markup.failed; NONE)) 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

242 

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

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

244 

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

245 

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

246 

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

247 

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

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

249 

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

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

251 

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

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

253 

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

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

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

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

257 
 SOME exec' => exec' <> exec); 
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 
fun new_exec name (id: command_id) (exec_id, updates, state) = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

261 
val exec = the_exec state exec_id; 
38419  262 
val exec_id' = new_id (); 
38449  263 
val future_tr = the_command state id; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

265 
Lazy.lazy (fn () => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

266 
(case Lazy.force exec of 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

268 
 SOME st => 
38449  269 
let val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr) 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38873
diff
changeset

270 
in run_command name exec_tr st end)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

272 
in (exec_id', (id, exec_id') :: updates, state') end; 
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 
in 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

275 

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

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

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

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

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

280 

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

281 
fun update_node name (rev_updates, version, st) = 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

282 
let val node = get_node version name in 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

283 
(case first_entry NONE (is_changed (get_node old_version name)) node of 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

284 
NONE => (rev_updates, version, st) 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

285 
 SOME ((prev, id), _) => 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

288 
(case prev of 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

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

290 
 SOME prev_id => the_default no_id (the_entry node prev_id)); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

291 
val (_, rev_upds, st') = 
38448
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

292 
fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st); 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

293 
val node' = fold update_entry rev_upds node; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

294 
in (rev_upds @ rev_updates, put_node name node' version, st') end) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

298 
val (rev_updates, new_version', state') = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

299 
fold update_node (node_names_of new_version) ([], new_version, state); 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

301 

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

302 
val _ = join_commands state''; (* FIXME async!? *) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

303 
in (rev rev_updates, state'') end; 
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 
end; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

306 

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

307 

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

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

309 

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

310 
fun execute version_id state = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

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

314 

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

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

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

317 

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

318 
val _ = List.app Future.cancel execution; 
38873  319 
fun await_cancellation () = 
320 
uninterruptible (fn _ => fn () => Future.join_results execution) (); 

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

321 

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

322 
val execution' = (* FIXME proper node deps *) 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

323 
node_names_of version > map (fn name => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

324 
Future.fork_pri 1 (fn () => 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

326 
fold_entries NONE (fn (_, exec) => fn () => force_exec exec) 
62d16c415019
added functor Linear_Set, based on former adhoc structures in document.ML;
wenzelm
parents:
38421
diff
changeset

327 
(get_node version name) ()))); 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

329 

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

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

331 