equal
deleted
inserted
replaced
68 |
68 |
69 override def current_node(view: View): Option[Document.Node.Name] = |
69 override def current_node(view: View): Option[Document.Node.Name] = |
70 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } |
70 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } |
71 |
71 |
72 override def current_node_snapshot(view: View): Option[Document.Snapshot] = |
72 override def current_node_snapshot(view: View): Option[Document.Snapshot] = |
73 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) } |
73 GUI_Thread.require { Document_Model.get_snapshot(view.getBuffer) } |
74 |
74 |
75 override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { |
75 override def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
76 GUI_Thread.require {} |
76 GUI_Thread.require { Document_Model.get_snapshot(name) getOrElse session.snapshot(name) } |
77 Document_Model.get(name) match { |
|
78 case Some(model) => model.snapshot() |
|
79 case None => session.snapshot(name) |
|
80 } |
|
81 } |
|
82 |
77 |
83 override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = { |
78 override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = { |
84 GUI_Thread.require {} |
79 GUI_Thread.require {} |
85 |
80 |
86 val text_area = view.getTextArea |
81 val text_area = view.getTextArea |