src/Tools/jEdit/src/jedit_editor.scala
changeset 52974 908e8a36e975
parent 52973 d5f7fa1498b7
child 52977 15254e32d299
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 11:56:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 12:06:48 2013 +0200
     1.3 @@ -17,6 +17,23 @@
     1.4  {
     1.5    def session: Session = PIDE.session
     1.6  
     1.7 +  def flush()
     1.8 +  {
     1.9 +    Swing_Thread.require()
    1.10 +
    1.11 +    session.update(
    1.12 +      (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    1.13 +        case (edits, buffer) =>
    1.14 +          JEdit_Lib.buffer_lock(buffer) {
    1.15 +            PIDE.document_model(buffer) match {
    1.16 +              case Some(model) => model.flushed_edits() ::: edits
    1.17 +              case None => edits
    1.18 +            }
    1.19 +          }
    1.20 +      }
    1.21 +    )
    1.22 +  }
    1.23 +
    1.24    def current_context: View =
    1.25      Swing_Thread.require { jEdit.getActiveView() }
    1.26  
    1.27 @@ -26,6 +43,20 @@
    1.28    def current_snapshot(view: View): Option[Document.Snapshot] =
    1.29      Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) }
    1.30  
    1.31 +  def node_snapshot(name: Document.Node.Name): Document.Snapshot =
    1.32 +  {
    1.33 +    Swing_Thread.require()
    1.34 +
    1.35 +    JEdit_Lib.jedit_buffer(name.node) match {
    1.36 +      case Some(buffer) =>
    1.37 +        PIDE.document_model(buffer) match {
    1.38 +          case Some(model) => model.snapshot
    1.39 +          case None => session.snapshot(name)
    1.40 +        }
    1.41 +      case None => session.snapshot(name)
    1.42 +    }
    1.43 +  }
    1.44 +
    1.45    def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] =
    1.46    {
    1.47      Swing_Thread.require()