src/Tools/jEdit/src/find_dockable.scala
changeset 52851 e71b5160f242
parent 52848 9489ca1d55dd
child 52854 92932931bd82
     1.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:00:14 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:02:06 2013 +0200
     1.3 @@ -28,11 +28,16 @@
     1.4  
     1.5    /* component state -- owned by Swing thread */
     1.6  
     1.7 +  private val identification = Document_ID.make().toString
     1.8 +
     1.9    private var zoom_factor = 100
    1.10    private var current_snapshot = Document.State.init.snapshot()
    1.11    private var current_state = Command.empty.init_state
    1.12    private var current_output: List[XML.Tree] = Nil
    1.13    private var current_location: Option[Command] = None
    1.14 +  private var current_query: String = ""
    1.15 +
    1.16 +  private val FIND_THEOREMS = "find_theorems"
    1.17  
    1.18  
    1.19    /* pretty text area */
    1.20 @@ -54,14 +59,35 @@
    1.21      Swing_Thread.require()
    1.22    }
    1.23  
    1.24 -  private def apply_query(text: String)
    1.25 +  private def clear_overlay()
    1.26    {
    1.27      Swing_Thread.require()
    1.28  
    1.29 +    for {
    1.30 +      command <- current_location
    1.31 +      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    1.32 +      model <- PIDE.document_model(buffer)
    1.33 +    } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query))
    1.34 +
    1.35 +    current_location = None
    1.36 +    current_query = ""
    1.37 +  }
    1.38 +
    1.39 +  private def apply_query(query: String)
    1.40 +  {
    1.41 +    Swing_Thread.require()
    1.42 +
    1.43 +    clear_overlay()
    1.44      Document_View(view.getTextArea) match {
    1.45        case Some(doc_view) =>
    1.46          val snapshot = doc_view.model.snapshot()
    1.47 -        current_location = snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1)
    1.48 +        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
    1.49 +          case Some(command) =>
    1.50 +            current_location = Some(command)
    1.51 +            current_query = query
    1.52 +            doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query))
    1.53 +          case None =>
    1.54 +        }
    1.55        case None =>
    1.56      }
    1.57    }