20 |
20 |
21 object Pretty_Text_Area |
21 object Pretty_Text_Area |
22 { |
22 { |
23 def document_state(formatted_body: XML.Body): Document.State = |
23 def document_state(formatted_body: XML.Body): Document.State = |
24 { |
24 { |
25 val text = formatted_body.iterator.flatMap(XML.content).mkString |
25 val command = Command.rich_text(Document.new_id(), formatted_body) |
26 val markup: List[XML.Elem] = Nil // FIXME |
|
27 |
|
28 val command = Command.unparsed(text) |
|
29 val node_name = command.node_name |
26 val node_name = command.node_name |
30 val exec_id = Document.new_id() |
|
31 |
27 |
32 val edits: List[Document.Edit_Text] = |
28 val edits: List[Document.Edit_Text] = |
33 List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, text)))) |
29 List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source)))) |
34 |
30 |
35 val state0 = Document.State.init.define_command(command) |
31 val state0 = Document.State.init.define_command(command) |
36 val version0 = state0.history.tip.version.get_finished |
32 val version0 = state0.history.tip.version.get_finished |
37 val nodes0 = version0.nodes |
33 val nodes0 = version0.nodes |
38 |
34 |
39 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) |
35 val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command))) |
40 val version1 = Document.Version.make(version0.syntax, nodes1) |
36 val version1 = Document.Version.make(version0.syntax, nodes1) |
41 val state1 = |
37 val state1 = |
42 state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 |
38 state0.continue_history(Future.value(version0), edits, Future.value(version1))._2 |
43 .define_version(version1, state0.the_assignment(version0)) |
39 .define_version(version1, state0.the_assignment(version0)) |
44 .assign(version1.id, List(command.id -> Some(exec_id)))._2 |
40 .assign(version1.id, List(command.id -> Some(Document.new_id())))._2 |
45 |
41 |
46 state1 |
42 state1 |
47 } |
43 } |
48 } |
44 } |
49 |
45 |