equal
deleted
inserted
replaced
590 } yield convert(cmd.core_range + start)).toList |
590 } yield convert(cmd.core_range + start)).toList |
591 |
591 |
592 |
592 |
593 /* command as add-on snippet */ |
593 /* command as add-on snippet */ |
594 |
594 |
595 def command_snippet(command: Command): Snapshot = |
595 def snippet(command: Command): Snapshot = |
596 { |
596 { |
597 val node_name = command.node_name |
597 val node_name = command.node_name |
598 |
598 |
599 val nodes0 = version.nodes |
599 val nodes0 = version.nodes |
600 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) |
600 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) |
996 val node_name = command.node_name |
996 val node_name = command.node_name |
997 val command1 = |
997 val command1 = |
998 Command.unparsed(command.source, theory = true, id = id, node_name = node_name, |
998 Command.unparsed(command.source, theory = true, id = id, node_name = node_name, |
999 blobs_info = command.blobs_info, results = st.results, markups = st.markups) |
999 blobs_info = command.blobs_info, results = st.results, markups = st.markups) |
1000 val state1 = copy(theories = theories - id) |
1000 val state1 = copy(theories = theories - id) |
1001 val snapshot = state1.command_snippet(command1) |
1001 (state1.snippet(command1), state1) |
1002 (snapshot, state1) |
|
1003 } |
1002 } |
1004 |
1003 |
1005 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) |
1004 def assign(id: Document_ID.Version, edited: List[String], update: Assign_Update) |
1006 : ((List[Node.Name], List[Command]), State) = |
1005 : ((List[Node.Name], List[Command]), State) = |
1007 { |
1006 { |
1250 }) |
1249 }) |
1251 |
1250 |
1252 new Snapshot(this, version, node_name, edits, snippet_command) |
1251 new Snapshot(this, version, node_name, edits, snippet_command) |
1253 } |
1252 } |
1254 |
1253 |
1255 def command_snippet(command: Command): Snapshot = |
1254 def snippet(command: Command): Snapshot = |
1256 snapshot().command_snippet(command) |
1255 snapshot().snippet(command) |
1257 } |
1256 } |
1258 } |
1257 } |