equal
deleted
inserted
replaced
29 /* component state -- owned by Swing thread */ |
29 /* component state -- owned by Swing thread */ |
30 |
30 |
31 private var zoom_factor = 100 |
31 private var zoom_factor = 100 |
32 private var show_tracing = false |
32 private var show_tracing = false |
33 private var do_update = true |
33 private var do_update = true |
34 private var current_state = Command.empty.empty_state |
34 private var current_state = Command.empty.init_state |
35 private var current_body: XML.Body = Nil |
35 private var current_body: XML.Body = Nil |
36 |
36 |
37 |
37 |
38 /* HTML panel */ |
38 /* HTML panel */ |
39 |
39 |
89 Document_View(view.getTextArea) match { |
89 Document_View(view.getTextArea) match { |
90 case Some(doc_view) => |
90 case Some(doc_view) => |
91 val snapshot = doc_view.model.snapshot() |
91 val snapshot = doc_view.model.snapshot() |
92 snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
92 snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
93 case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) |
93 case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) |
94 case None => Command.empty.empty_state |
94 case None => Command.empty.init_state |
95 } |
95 } |
96 case None => Command.empty.empty_state |
96 case None => Command.empty.init_state |
97 } |
97 } |
98 } |
98 } |
99 else current_state |
99 else current_state |
100 |
100 |
101 val new_body = |
101 val new_body = |