src/Tools/jEdit/src/jedit_editor.scala
changeset 52977 15254e32d299
parent 52974 908e8a36e975
child 52978 37fbb3fde380
     1.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 13:32:26 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Mon Aug 12 14:27:58 2013 +0200
     1.3 @@ -15,6 +15,8 @@
     1.4  
     1.5  class JEdit_Editor extends Editor[View]
     1.6  {
     1.7 +  /* session */
     1.8 +
     1.9    def session: Session = PIDE.session
    1.10  
    1.11    def flush()
    1.12 @@ -34,6 +36,9 @@
    1.13      )
    1.14    }
    1.15  
    1.16 +
    1.17 +  /* current situation */
    1.18 +
    1.19    def current_context: View =
    1.20      Swing_Thread.require { jEdit.getActiveView() }
    1.21  
    1.22 @@ -72,4 +77,18 @@
    1.23        }
    1.24      }
    1.25    }
    1.26 +
    1.27 +
    1.28 +  /* overlays */
    1.29 +
    1.30 +  private var overlays = Document.Overlays.empty
    1.31 +
    1.32 +  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
    1.33 +    synchronized { overlays(name) }
    1.34 +
    1.35 +  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
    1.36 +    synchronized { overlays = overlays.insert(command, fn, args) }
    1.37 +
    1.38 +  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
    1.39 +    synchronized { overlays = overlays.remove(command, fn, args) }
    1.40  }