minimal print function "find_theorems", which merely echos its arguments;
authorwenzelm
Fri Aug 02 16:02:06 2013 +0200 (2013-08-02)
changeset 52851e71b5160f242
parent 52850 9fff9f78240a
child 52852 08ecbffaf25c
minimal print function "find_theorems", which merely echos its arguments;
src/Pure/Tools/find_theorems.ML
src/Tools/jEdit/src/find_dockable.scala
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Aug 02 16:00:14 2013 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Aug 02 16:02:06 2013 +0200
     1.3 @@ -636,4 +636,16 @@
     1.4  
     1.5  end;
     1.6  
     1.7 +
     1.8 +
     1.9 +(** print function **)
    1.10 +
    1.11 +val _ = Command.print_function "find_theorems"
    1.12 +  (fn {args, ...} =>
    1.13 +    if null args then NONE
    1.14 +    else
    1.15 +      SOME {delay = NONE, pri = 0, persistent = false,
    1.16 +        print_fn = fn _ => fn st =>
    1.17 +          writeln (cat_lines ("find_theorems" :: args))});
    1.18 +
    1.19  end;
     2.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:00:14 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Fri Aug 02 16:02:06 2013 +0200
     2.3 @@ -28,11 +28,16 @@
     2.4  
     2.5    /* component state -- owned by Swing thread */
     2.6  
     2.7 +  private val identification = Document_ID.make().toString
     2.8 +
     2.9    private var zoom_factor = 100
    2.10    private var current_snapshot = Document.State.init.snapshot()
    2.11    private var current_state = Command.empty.init_state
    2.12    private var current_output: List[XML.Tree] = Nil
    2.13    private var current_location: Option[Command] = None
    2.14 +  private var current_query: String = ""
    2.15 +
    2.16 +  private val FIND_THEOREMS = "find_theorems"
    2.17  
    2.18  
    2.19    /* pretty text area */
    2.20 @@ -54,14 +59,35 @@
    2.21      Swing_Thread.require()
    2.22    }
    2.23  
    2.24 -  private def apply_query(text: String)
    2.25 +  private def clear_overlay()
    2.26    {
    2.27      Swing_Thread.require()
    2.28  
    2.29 +    for {
    2.30 +      command <- current_location
    2.31 +      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    2.32 +      model <- PIDE.document_model(buffer)
    2.33 +    } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query))
    2.34 +
    2.35 +    current_location = None
    2.36 +    current_query = ""
    2.37 +  }
    2.38 +
    2.39 +  private def apply_query(query: String)
    2.40 +  {
    2.41 +    Swing_Thread.require()
    2.42 +
    2.43 +    clear_overlay()
    2.44      Document_View(view.getTextArea) match {
    2.45        case Some(doc_view) =>
    2.46          val snapshot = doc_view.model.snapshot()
    2.47 -        current_location = snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1)
    2.48 +        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
    2.49 +          case Some(command) =>
    2.50 +            current_location = Some(command)
    2.51 +            current_query = query
    2.52 +            doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query))
    2.53 +          case None =>
    2.54 +        }
    2.55        case None =>
    2.56      }
    2.57    }