author  wenzelm 
Sat, 13 Aug 2011 20:20:36 +0200  
changeset 44185  05641edb5d30 
parent 44182  ecb51b457064 
child 44186  806f0ec1a43d 
permissions  rwrr 
38150
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

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

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

3 

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

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

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

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

7 

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

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

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

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

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

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

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

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

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

21 
Edits of (command_id option * command_id option) list  
44182  22 
Header of node_header 
44156  23 
type edit = string * node_edit 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

25 
val init_state: state 
43668  26 
val get_theory: state > version_id > Position.T > string > theory 
43666  27 
val cancel_execution: state > unit > unit 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

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

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

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

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

34 

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

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

36 
struct 
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 
(* unique identifiers *) 
67fc24df3721
simplified/refined document model: collection of named nodes, without proper dependencies yet;
wenzelm
parents:
diff
changeset

39 

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

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

42 
type command_id = id; 
38373  43 
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

44 

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

45 
val no_id = 0; 
40449  46 
val new_id = Synchronized.counter (); 
38418
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 

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

59 
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

60 

43668  61 
abstype node = Node of 
44182  62 
{header: node_header, 
44180  63 
entries: exec_id option Entries.T, (*command entries with excecutions*) 
64 
last: exec_id} (*last entry with main result*) 

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

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

67 

44180  68 
fun make_node (header, entries, last) = 
69 
Node {header = header, entries = entries, last = last}; 

43668  70 

44180  71 
fun map_node f (Node {header, entries, last}) = 
72 
make_node (f (header, entries, last)); 

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

73 

44180  74 
fun get_header (Node {header, ...}) = header; 
75 
fun set_header header = map_node (fn (_, entries, last) => (header, entries, last)); 

76 

77 
fun map_entries f (Node {header, entries, last}) = make_node (header, f entries, last); 

43668  78 
fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries; 
79 
fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries; 

80 

44180  81 
fun get_last (Node {last, ...}) = last; 
82 
fun set_last last = map_node (fn (header, entries, _) => (header, entries, last)); 

83 

84 
val empty_node = make_node (Exn.Exn (ERROR "Bad theory header"), Entries.empty, no_id); 

44185  85 
val clear_node = map_node (fn (header, _, _) => (header, Entries.empty, no_id)); 
86 

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

88 
fun remove_node name nodes = Graph.del_node name nodes handle Graph.UNDEF _ => nodes; 

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

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

90 

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

91 

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

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

93 

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

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

96 
Edits of (command_id option * command_id option) list  
44182  97 
Header of node_header; 
44157
a21d3e1e64fd
uniform treatment of header edits as document edits;
wenzelm
parents:
44156
diff
changeset

98 

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

100 

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

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

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

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

105 

43668  106 
fun update_entry (id, exec_id) = 
107 
map_entries (Entries.update (id, SOME exec_id)); 

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

108 

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

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

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

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

112 
 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

113 

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

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

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

120 

44185  121 
val empty_version = Version Graph.empty; 
122 

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

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

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

126 

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

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

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

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

131 
(case node_edit of 
44185  132 
Clear => update_node name clear_node nodes 
44180  133 
 Edits edits => update_node name (edit_node edits) nodes 
44185  134 
 Header header => 
135 
let 

136 
val node = get_node nodes name; 

137 
val nodes' = Graph.new_node (name, node) (remove_node name nodes); 

138 
val parents = 

139 
(case header of Exn.Res (_, parents, _) => parents  _ => []) 

140 
> filter (can (Graph.get_node nodes')); 

141 
val (header', nodes'') = 

142 
(header, Graph.add_deps_acyclic (name, parents) nodes') 

143 
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes'); 

144 
in Graph.map_node name (set_header header') nodes'' end); 

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

145 

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

146 
fun put_node name node (Version nodes) = 
40481  147 
Version (nodes 
148 
> Graph.default_node (name, empty_node) 

149 
> Graph.map_node name (K node)); 

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

150 

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

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

152 

38418
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 
(** global state  document structure and execution process **) 
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 
abstype state = State of 
40398  158 
{versions: version Inttab.table, (*version_id > document content*) 
38421
6cfc6fce7bfb
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
wenzelm
parents:
38419
diff
changeset

159 
commands: Toplevel.transition future Inttab.table, (*command_id > transition (future parsing)*) 
40398  160 
execs: (bool * Toplevel.state) lazy Inttab.table, (*exec_id > execution process*) 
161 
execution: unit future list} (*global execution process*) 

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

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

163 

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

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

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

166 

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

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

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

169 

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

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

171 
make_state (Inttab.make [(no_id, empty_version)], 
38449  172 
Inttab.make [(no_id, Future.value Toplevel.empty)], 
40398  173 
Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))], 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

175 

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

176 

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

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

178 

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

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

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

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

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

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

184 

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

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

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

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

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

189 

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 
(* commands *) 
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 
fun define_command (id: command_id) text = 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

196 
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

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

198 
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

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

200 
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

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

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

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

204 

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

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

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

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

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

209 

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

210 
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

211 
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

212 

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

213 

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

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

215 

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

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

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

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

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

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

221 

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

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

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

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

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

226 

43668  227 
fun get_theory state version_id pos name = 
228 
let 

44185  229 
val last = get_last (node_of (the_version state version_id) name); 
44180  230 
val st = 
231 
(case Lazy.peek (the_exec state last) of 

232 
SOME result => #2 (Exn.release result) 

44185  233 
 NONE => error ("Unfinished execution for theory " ^ quote name ^ Position.str_of pos)); 
43668  234 
in Toplevel.end_theory pos st end; 
235 

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

236 

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

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

238 

43666  239 
fun cancel_execution (State {execution, ...}) = 
240 
(List.app Future.cancel execution; 

241 
fn () => ignore (Future.join_results execution)); 

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

242 

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

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

244 

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

245 

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

246 

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

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

248 

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

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

250 

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

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

252 

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

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

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

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

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

257 

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

258 
fun async_state tr st = 
40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset

259 
ignore 
41673  260 
(singleton 
41674  261 
(Future.forks {name = "Document.async_state", 
44113  262 
group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0, interrupts = true}) 
40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset

263 
(fn () => 
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset

264 
Toplevel.setmp_thread_position tr 
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset

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

266 

40390  267 
fun run int tr st = 
268 
(case Toplevel.transition int tr st of 

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

270 
 SOME (_, SOME exn_info) => 

271 
(case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of 

272 
[] => Exn.interrupt () 

273 
 errs => (errs, NONE)) 

274 
 NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); 

275 

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

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

277 

44185  278 
fun run_command (node_name, node_header) raw_tr st = 
279 
let 

280 
val is_init = Toplevel.is_init raw_tr; 

281 
val tr = 

282 
if is_init then 

283 
raw_tr > Toplevel.modify_init (fn _ => 

284 
let 

285 
(* FIXME get theories from document state *) 

286 
(* FIXME provide files via Scala layer *) 

287 
val (name, imports, uses) = Exn.release node_header; 

288 
val master = SOME (Path.dir (Path.explode node_name)); 

289 
in Thy_Info.toplevel_begin_theory master name imports (map (apfst Path.explode) uses) end) 

290 
else raw_tr; 

40534
9e196062bf88
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
wenzelm
parents:
40532
diff
changeset

291 

44185  292 
val is_proof = Keyword.is_proof (Toplevel.name_of tr); 
293 
val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof); 

294 

295 
val start = Timing.start (); 

296 
val (errs, result) = 

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

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

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

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

301 
in 

302 
(case result of 

303 
NONE => (Toplevel.status tr Markup.failed; (false, st)) 

304 
 SOME st' => 

305 
(Toplevel.status tr Markup.finished; 

306 
proof_status tr st'; 

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

308 
(true, st'))) 

309 
end; 

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

310 

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

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

312 

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

313 

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

314 

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

315 

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

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

319 

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

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

321 

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

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

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

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

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

326 

44185  327 
fun new_exec node_info (id: command_id) (exec_id, updates, state) = 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

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

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

333 
Lazy.lazy (fn () => 
40398  334 
let 
335 
val st = #2 (Lazy.force exec); 

336 
val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr); 

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

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

339 
in (exec_id', (id, exec_id') :: updates, state') end; 
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

340 

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

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

342 

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

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

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

345 
val old_version = the_version state old_id; 
44180  346 
val _ = Time.now (); (* FIXME odd workaround for polyml5.4.0/x86_64 *) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

348 

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

349 
fun update_node name (rev_updates, version, st) = 
44185  350 
let 
351 
val node = node_of version name; 

352 
val header = get_header node; 

353 
in 

354 
(case first_entry NONE (is_changed (node_of old_version name)) node of 

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

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

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

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

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

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

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

361 
 SOME prev_id => the_default no_id (the_entry node prev_id)); 
43668  362 
val (last, rev_upds, st') = 
44185  363 
fold_entries (SOME id) (new_exec (name, header) o #2 o #1) node (prev_exec, [], st); 
43668  364 
val node' = node > fold update_entry rev_upds > set_last last; 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

365 
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

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

367 

44185  368 
(* FIXME Graph.schedule *) 
38418
9a7af64d71bb
more explicit / functional ML version of document model;
wenzelm
parents:
38414
diff
changeset

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

370 
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

371 
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

372 

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

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

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

375 

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

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

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

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

380 

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

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

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

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

385 

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

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

387 
 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

388 

44180  389 
val execution' = (* FIXME Graph.schedule *) 
44113  390 
Future.forks 
391 
{name = "Document.execute", group = NONE, deps = [], pri = 1, interrupts = true} 

41673  392 
[fn () => 
43666  393 
node_names_of version > List.app (fn name => 
394 
fold_entries NONE (fn (_, exec) => fn () => force_exec exec) 

44185  395 
(node_of version name) ())]; 
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

396 

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

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

398 

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

399 

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

400 

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

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

402 

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

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

404 

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

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

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

407 

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

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

409 