189 |
189 |
190 /** global state -- document structure, execution process, editing history **/ |
190 /** global state -- document structure, execution process, editing history **/ |
191 |
191 |
192 abstract class Snapshot |
192 abstract class Snapshot |
193 { |
193 { |
|
194 val state: State |
194 val version: Version |
195 val version: Version |
195 val node: Node |
196 val node: Node |
196 val is_outdated: Boolean |
197 val is_outdated: Boolean |
197 def find_command(id: Command_ID): Option[(String, Node, Command)] |
198 def command_state(command: Command): Command.State |
198 def state(command: Command): Command.State |
|
199 def convert(i: Text.Offset): Text.Offset |
199 def convert(i: Text.Offset): Text.Offset |
200 def convert(range: Text.Range): Text.Range |
200 def convert(range: Text.Range): Text.Range |
201 def revert(i: Text.Offset): Text.Offset |
201 def revert(i: Text.Offset): Text.Offset |
202 def revert(range: Text.Range): Text.Range |
202 def revert(range: Text.Range): Text.Range |
203 def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) |
203 def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) |
267 val id = command.id |
267 val id = command.id |
268 if (commands.isDefinedAt(id) || disposed(id)) fail |
268 if (commands.isDefinedAt(id) || disposed(id)) fail |
269 copy(commands = commands + (id -> command.empty_state)) |
269 copy(commands = commands + (id -> command.empty_state)) |
270 } |
270 } |
271 |
271 |
272 def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command) |
272 def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id) |
273 def lookup_exec(id: Exec_ID): Option[Command] = execs.get(id).map(_.command) |
273 |
|
274 def find_command(version: Version, id: ID): Option[(String, Node, Command)] = |
|
275 commands.get(id) orElse execs.get(id) match { |
|
276 case None => None |
|
277 case Some(st) => |
|
278 val command = st.command |
|
279 version.nodes.find({ case (_, node) => node.commands(command) }) |
|
280 .map({ case (name, node) => (name, node, command) }) |
|
281 } |
274 |
282 |
275 def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) |
283 def the_version(id: Version_ID): Version = versions.getOrElse(id, fail) |
276 def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename |
284 def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail) // FIXME rename |
277 def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail) |
285 def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail) |
278 def the_assignment(version: Version): State.Assignment = |
286 def the_assignment(version: Version): State.Assignment = |
365 (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits) |
373 (for ((a, Node.Edits(es)) <- change.edits if a == name) yield es).flatten ::: edits) |
366 lazy val reverse_edits = edits.reverse |
374 lazy val reverse_edits = edits.reverse |
367 |
375 |
368 new Snapshot |
376 new Snapshot |
369 { |
377 { |
|
378 val state = State.this |
370 val version = stable.version.get_finished |
379 val version = stable.version.get_finished |
371 val node = version.nodes(name) |
380 val node = version.nodes(name) |
372 val is_outdated = !(pending_edits.isEmpty && latest == stable) |
381 val is_outdated = !(pending_edits.isEmpty && latest == stable) |
373 |
382 |
374 def find_command(id: ID): Option[(String, Node, Command)] = |
383 def command_state(command: Command): Command.State = |
375 State.this.lookup_command(id) orElse State.this.lookup_exec(id) match { |
|
376 case None => None |
|
377 case Some(command) => |
|
378 version.nodes.find({ case (_, node) => node.commands(command) }) |
|
379 .map({ case (name, node) => (name, node, command) }) |
|
380 } |
|
381 |
|
382 def state(command: Command): Command.State = |
|
383 try { |
384 try { |
384 the_exec(the_assignment(version).check_finished.command_execs |
385 the_exec(the_assignment(version).check_finished.command_execs |
385 .getOrElse(command.id, fail)) |
386 .getOrElse(command.id, fail)) |
386 } |
387 } |
387 catch { case _: State.Fail => command.empty_state } |
388 catch { case _: State.Fail => command.empty_state } |
395 : Stream[Text.Info[Option[A]]] = |
396 : Stream[Text.Info[Option[A]]] = |
396 { |
397 { |
397 val former_range = revert(range) |
398 val former_range = revert(range) |
398 for { |
399 for { |
399 (command, command_start) <- node.command_range(former_range).toStream |
400 (command, command_start) <- node.command_range(former_range).toStream |
400 Text.Info(r0, x) <- state(command).markup. |
401 Text.Info(r0, x) <- command_state(command).markup. |
401 select((former_range - command_start).restrict(command.range)) { |
402 select((former_range - command_start).restrict(command.range)) { |
402 case Text.Info(r0, info) |
403 case Text.Info(r0, info) |
403 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => |
404 if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) => |
404 result(Text.Info(convert(r0 + command_start), info)) |
405 result(Text.Info(convert(r0 + command_start), info)) |
405 } |
406 } |