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 /* pretty text panel */ |
38 /* pretty text panel */ |
39 |
39 |
58 Document_View(view.getTextArea) match { |
58 Document_View(view.getTextArea) match { |
59 case Some(doc_view) => |
59 case Some(doc_view) => |
60 val snapshot = doc_view.model.snapshot() |
60 val snapshot = doc_view.model.snapshot() |
61 snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
61 snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match { |
62 case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) |
62 case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd) |
63 case None => Command.empty.empty_state |
63 case None => Command.empty.init_state |
64 } |
64 } |
65 case None => Command.empty.empty_state |
65 case None => Command.empty.init_state |
66 } |
66 } |
67 } |
67 } |
68 else current_state |
68 else current_state |
69 |
69 |
70 val new_body = |
70 val new_body = |