1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/query_operation.ML	Mon Aug 05 17:14:02 2013 +0200
     1.3 @@ -0,0 +1,30 @@
     1.4 +(*  Title:      Pure/PIDE/query_operation.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +One-shot query operations via asynchronous print functions and temporary
     1.8 +document overlay.
     1.9 +*)
    1.10 +
    1.11 +signature QUERY_OPERATION =
    1.12 +sig
    1.13 +  val register: string -> (Toplevel.state -> string list -> string) -> unit
    1.14 +end;
    1.15 +
    1.16 +structure Query_Operation: QUERY_OPERATION =
    1.17 +struct
    1.18 +
    1.19 +fun register name f =
    1.20 +  Command.print_function name
    1.21 +    (fn {args = instance :: args, ...} =>
    1.22 +        SOME {delay = NONE, pri = 0, persistent = false,
    1.23 +          print_fn = fn _ => fn state =>
    1.24 +            let
    1.25 +              val msg = XML.Elem ((Markup.writelnN, []), [XML.Text (f state args)])
    1.26 +                handle exn =>
    1.27 +                  if Exn.is_interrupt exn then reraise exn
    1.28 +                  else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
    1.29 +            in Output.result [(Markup.instanceN, instance)] (YXML.string_of msg) end}
    1.30 +      | _ => NONE);
    1.31 +
    1.32 +end;
    1.33 +

     2.1 --- a/src/Pure/ROOT	Mon Aug 05 16:12:03 2013 +0200
     2.2 +++ b/src/Pure/ROOT	Mon Aug 05 17:14:02 2013 +0200
     2.3 @@ -158,6 +158,7 @@
     2.4      "PIDE/execution.ML"
     2.5      "PIDE/markup.ML"
     2.6      "PIDE/protocol.ML"
     2.7 +    "PIDE/query_operation.ML"
     2.8      "PIDE/xml.ML"
     2.9      "PIDE/yxml.ML"
    2.10      "Proof/extraction.ML"

     3.1 --- a/src/Pure/ROOT.ML	Mon Aug 05 16:12:03 2013 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Mon Aug 05 17:14:02 2013 +0200
     3.3 @@ -269,6 +269,7 @@
     3.4  use "Thy/present.ML";
     3.5  use "PIDE/execution.ML";
     3.6  use "PIDE/command.ML";
     3.7 +use "PIDE/query_operation.ML";
     3.8  use "Thy/thy_load.ML";
     3.9  use "Thy/thy_info.ML";
    3.10  use "PIDE/document.ML";

     4.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Aug 05 16:12:03 2013 +0200
     4.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Aug 05 17:14:02 2013 +0200
     4.3 @@ -605,7 +605,7 @@
     4.4  
     4.5  
     4.6  
     4.7 -(** command syntax **)
     4.8 +(** Isar command syntax **)
     4.9  
    4.10  local
    4.11  
    4.12 @@ -647,28 +647,10 @@
    4.13  
    4.14  
    4.15  
    4.16 -(** print function **)
    4.17 +(** PIDE query operation **)
    4.18  
    4.19 -val find_theoremsN = "find_theorems";
    4.20 -
    4.21 -val _ = Command.print_function find_theoremsN
    4.22 -  (fn {args, ...} =>
    4.23 -    (case args of
    4.24 -      [instance, query] =>
    4.25 -      SOME {delay = NONE, pri = 0, persistent = false,
    4.26 -        print_fn = fn _ => fn state =>
    4.27 -          let
    4.28 -            val msg =
    4.29 -              XML.Elem ((Markup.writelnN, []),
    4.30 -                [XML.Text
    4.31 -                  (Pretty.string_of (pretty_theorems_cmd state NONE false (parse_query query)))])
    4.32 -              handle exn =>
    4.33 -                if Exn.is_interrupt exn then reraise exn
    4.34 -                else XML.Elem ((Markup.errorN, []), [XML.Text (ML_Compiler.exn_message exn)]);
    4.35 -          in
    4.36 -            Output.result [(Markup.kindN, find_theoremsN), (Markup.instanceN, instance)]
    4.37 -              (YXML.string_of msg)
    4.38 -          end}
    4.39 -    | _ => NONE));
    4.40 +val _ =
    4.41 +  Query_Operation.register "find_theorems" (fn state => fn query =>
    4.42 +    Pretty.string_of (pretty_theorems_cmd state NONE false (maps parse_query query)));
    4.43  
    4.44  end;

     5.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 05 16:12:03 2013 +0200
     5.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Mon Aug 05 17:14:02 2013 +0200
     5.3 @@ -35,6 +35,7 @@
     5.4    "src/pretty_text_area.scala"
     5.5    "src/pretty_tooltip.scala"
     5.6    "src/protocol_dockable.scala"
     5.7 +  "src/query_operation.scala"
     5.8    "src/raw_output_dockable.scala"
     5.9    "src/readme_dockable.scala"
    5.10    "src/rendering.scala"

     6.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 16:12:03 2013 +0200
     6.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Mon Aug 05 17:14:02 2013 +0200
     6.3 @@ -25,27 +25,22 @@
     6.4  {
     6.5    Swing_Thread.require()
     6.6  
     6.7 -
     6.8 -  /* component state -- owned by Swing thread */
     6.9 -
    6.10 -  private val FIND_THEOREMS = "find_theorems"
    6.11 -  private val instance = Document_ID.make().toString
    6.12 -
    6.13 -  private var zoom_factor = 100
    6.14 -  private var current_location: Option[Command] = None
    6.15 -  private var current_query: String = ""
    6.16 -  private var current_result = false
    6.17 -  private var current_snapshot = Document.State.init.snapshot()
    6.18 -  private var current_state = Command.empty.init_state
    6.19 -  private var current_output: List[XML.Tree] = Nil
    6.20 -
    6.21 -
    6.22 -  /* pretty text area */
    6.23 -
    6.24    val pretty_text_area = new Pretty_Text_Area(view)
    6.25    set_content(pretty_text_area)
    6.26  
    6.27  
    6.28 +  /* query operation */
    6.29 +
    6.30 +  private val find_theorems =
    6.31 +    Query_Operation(view, "find_theorems",
    6.32 +      (snapshot, results, body) =>
    6.33 +        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
    6.34 +
    6.35 +
    6.36 +  /* resize */
    6.37 +
    6.38 +  private var zoom_factor = 100
    6.39 +
    6.40    private def handle_resize()
    6.41    {
    6.42      Swing_Thread.require()
    6.43 @@ -54,98 +49,12 @@
    6.44        (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    6.45    }
    6.46  
    6.47 -  private def remove_overlay()
    6.48 -  {
    6.49 -    Swing_Thread.require()
    6.50 +  private val delay_resize =
    6.51 +    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    6.52  
    6.53 -    for {
    6.54 -      command <- current_location
    6.55 -      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    6.56 -      model <- PIDE.document_model(buffer)
    6.57 -    } model.remove_overlay(command, FIND_THEOREMS, List(instance, current_query))
    6.58 -  }
    6.59 -
    6.60 -  private def handle_update()
    6.61 -  {
    6.62 -    Swing_Thread.require()
    6.63 -
    6.64 -    val (new_snapshot, new_state) =
    6.65 -      Document_View(view.getTextArea) match {
    6.66 -        case Some(doc_view) =>
    6.67 -          val snapshot = doc_view.model.snapshot()
    6.68 -          if (!snapshot.is_outdated) {
    6.69 -            current_location match {
    6.70 -              case Some(cmd) =>
    6.71 -                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    6.72 -              case None =>
    6.73 -                (Document.State.init.snapshot(), Command.empty.init_state)
    6.74 -            }
    6.75 -          }
    6.76 -          else (current_snapshot, current_state)
    6.77 -        case None => (current_snapshot, current_state)
    6.78 -      }
    6.79 -
    6.80 -    val new_output =
    6.81 -      (for {
    6.82 -        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
    6.83 -          new_state.results.entries
    6.84 -        if props.contains((Markup.KIND, FIND_THEOREMS))
    6.85 -        if props.contains((Markup.INSTANCE, instance))
    6.86 -      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
    6.87 -
    6.88 -    if (new_output != current_output)
    6.89 -      pretty_text_area.update(new_snapshot, new_state.results, Pretty.separate(new_output))
    6.90 -
    6.91 -    if (!new_output.isEmpty) {
    6.92 -      current_result = true
    6.93 -      remove_overlay()
    6.94 -      PIDE.flush_buffers()
    6.95 -    }
    6.96 -
    6.97 -    current_snapshot = new_snapshot
    6.98 -    current_state = new_state
    6.99 -    current_output = new_output
   6.100 -  }
   6.101 -
   6.102 -  private def apply_query(query: String)
   6.103 -  {
   6.104 -    Swing_Thread.require()
   6.105 -
   6.106 -    Document_View(view.getTextArea) match {
   6.107 -      case Some(doc_view) =>
   6.108 -        val snapshot = doc_view.model.snapshot()
   6.109 -        remove_overlay()
   6.110 -        current_location = None
   6.111 -        current_query = ""
   6.112 -        current_result = false
   6.113 -        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   6.114 -          case Some(command) =>
   6.115 -            current_location = Some(command)
   6.116 -            current_query = query
   6.117 -            doc_view.model.insert_overlay(command, FIND_THEOREMS, List(instance, query))
   6.118 -          case None =>
   6.119 -        }
   6.120 -        PIDE.flush_buffers()
   6.121 -      case None =>
   6.122 -    }
   6.123 -  }
   6.124 -
   6.125 -  private def locate_query()
   6.126 -  {
   6.127 -    Swing_Thread.require()
   6.128 -
   6.129 -    current_location match {
   6.130 -      case Some(command) =>
   6.131 -        val snapshot = PIDE.session.snapshot(command.node_name)
   6.132 -        val commands = snapshot.node.commands
   6.133 -        if (commands.contains(command)) {
   6.134 -          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
   6.135 -          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   6.136 -          Hyperlink(command.node_name.node, line, column).follow(view)
   6.137 -        }
   6.138 -      case None =>
   6.139 -    }
   6.140 -  }
   6.141 +  addComponentListener(new ComponentAdapter {
   6.142 +    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   6.143 +  })
   6.144  
   6.145  
   6.146    /* main actor */
   6.147 @@ -155,12 +64,6 @@
   6.148        react {
   6.149          case _: Session.Global_Options =>
   6.150            Swing_Thread.later { handle_resize() }
   6.151 -        case changed: Session.Commands_Changed =>
   6.152 -          current_location match {
   6.153 -            case Some(command) if !current_result && changed.commands.contains(command) =>
   6.154 -              Swing_Thread.later { handle_update() }
   6.155 -            case _ =>
   6.156 -          }
   6.157          case bad =>
   6.158            java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
   6.159        }
   6.160 @@ -172,30 +75,20 @@
   6.161      Swing_Thread.require()
   6.162  
   6.163      PIDE.session.global_options += main_actor
   6.164 -    PIDE.session.commands_changed += main_actor
   6.165      handle_resize()
   6.166 +    find_theorems.activate()
   6.167    }
   6.168  
   6.169    override def exit()
   6.170    {
   6.171      Swing_Thread.require()
   6.172  
   6.173 +    find_theorems.deactivate()
   6.174      PIDE.session.global_options -= main_actor
   6.175 -    PIDE.session.commands_changed -= main_actor
   6.176      delay_resize.revoke()
   6.177    }
   6.178  
   6.179  
   6.180 -  /* resize */
   6.181 -
   6.182 -  private val delay_resize =
   6.183 -    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   6.184 -
   6.185 -  addComponentListener(new ComponentAdapter {
   6.186 -    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   6.187 -  })
   6.188 -
   6.189 -
   6.190    /* controls */
   6.191  
   6.192    private val query = new HistoryTextArea("isabelle-find-theorems") {
   6.193 @@ -208,12 +101,12 @@
   6.194  
   6.195    private val find = new Button("Find") {
   6.196      tooltip = "Find theorems meeting specified criteria"
   6.197 -    reactions += { case ButtonClicked(_) => apply_query(query.getText) }
   6.198 +    reactions += { case ButtonClicked(_) => find_theorems.apply_query(List(query.getText)) }
   6.199    }
   6.200  
   6.201    private val locate = new Button("Locate") {
   6.202      tooltip = "Locate context of current query within source text"
   6.203 -    reactions += { case ButtonClicked(_) => locate_query() }
   6.204 +    reactions += { case ButtonClicked(_) => find_theorems.locate_query() }
   6.205    }
   6.206  
   6.207    private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/src/query_operation.scala	Mon Aug 05 17:14:02 2013 +0200
     7.3 @@ -0,0 +1,153 @@
     7.4 +/*  Title:      Tools/jEdit/src/query_operation.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +One-shot query operations via asynchronous print functions and temporary
     7.8 +document overlay.
     7.9 +*/
    7.10 +
    7.11 +package isabelle.jedit
    7.12 +
    7.13 +
    7.14 +import isabelle._
    7.15 +
    7.16 +import scala.actors.Actor._
    7.17 +
    7.18 +import org.gjt.sp.jedit.View
    7.19 +
    7.20 +
    7.21 +object Query_Operation
    7.22 +{
    7.23 +  def apply(
    7.24 +      view: View,
    7.25 +      name: String,
    7.26 +      consume: (Document.Snapshot, Command.Results, XML.Body) => Unit) =
    7.27 +    new Query_Operation(view, name, consume)
    7.28 +}
    7.29 +
    7.30 +final class Query_Operation private(
    7.31 +  view: View,
    7.32 +  operation_name: String,
    7.33 +  consume_result: (Document.Snapshot, Command.Results, XML.Body) => Unit)
    7.34 +{
    7.35 +  private val instance = Document_ID.make().toString
    7.36 +
    7.37 +
    7.38 +  /* implicit state -- owned by Swing thread */
    7.39 +
    7.40 +  private var current_location: Option[Command] = None
    7.41 +  private var current_query: List[String] = Nil
    7.42 +  private var current_result = false
    7.43 +  private var current_snapshot = Document.State.init.snapshot()
    7.44 +  private var current_state = Command.empty.init_state
    7.45 +  private var current_output: List[XML.Tree] = Nil
    7.46 +
    7.47 +  private def remove_overlay()
    7.48 +  {
    7.49 +    Swing_Thread.require()
    7.50 +
    7.51 +    for {
    7.52 +      command <- current_location
    7.53 +      buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    7.54 +      model <- PIDE.document_model(buffer)
    7.55 +    } model.remove_overlay(command, operation_name, instance :: current_query)
    7.56 +  }
    7.57 +
    7.58 +  private def handle_result()
    7.59 +  {
    7.60 +    Swing_Thread.require()
    7.61 +
    7.62 +    val (new_snapshot, new_state) =
    7.63 +      Document_View(view.getTextArea) match {
    7.64 +        case Some(doc_view) =>
    7.65 +          val snapshot = doc_view.model.snapshot()
    7.66 +          current_location match {
    7.67 +            case Some(cmd) =>
    7.68 +              (snapshot, snapshot.state.command_state(snapshot.version, cmd))
    7.69 +            case None =>
    7.70 +              (Document.State.init.snapshot(), Command.empty.init_state)
    7.71 +          }
    7.72 +        case None => (current_snapshot, current_state)
    7.73 +      }
    7.74 +
    7.75 +    val new_output =
    7.76 +      (for {
    7.77 +        (_, XML.Elem(Markup(Markup.RESULT, props), List(XML.Elem(markup, body)))) <-
    7.78 +          new_state.results.entries
    7.79 +        if props.contains((Markup.INSTANCE, instance))
    7.80 +      } yield XML.Elem(Markup(Markup.message(markup.name), markup.properties), body)).toList
    7.81 +
    7.82 +    if (new_output != current_output)
    7.83 +      consume_result(new_snapshot, new_state.results, new_output)
    7.84 +
    7.85 +    if (!new_output.isEmpty) {
    7.86 +      current_result = true
    7.87 +      remove_overlay()
    7.88 +      PIDE.flush_buffers()
    7.89 +    }
    7.90 +
    7.91 +    current_snapshot = new_snapshot
    7.92 +    current_state = new_state
    7.93 +    current_output = new_output
    7.94 +  }
    7.95 +
    7.96 +  def apply_query(query: List[String])
    7.97 +  {
    7.98 +    Swing_Thread.require()
    7.99 +
   7.100 +    Document_View(view.getTextArea) match {
   7.101 +      case Some(doc_view) =>
   7.102 +        val snapshot = doc_view.model.snapshot()
   7.103 +        remove_overlay()
   7.104 +        current_location = None
   7.105 +        current_query = Nil
   7.106 +        current_result = false
   7.107 +        snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
   7.108 +          case Some(command) =>
   7.109 +            current_location = Some(command)
   7.110 +            current_query = query
   7.111 +            doc_view.model.insert_overlay(command, operation_name, instance :: query)
   7.112 +          case None =>
   7.113 +        }
   7.114 +        PIDE.flush_buffers()
   7.115 +      case None =>
   7.116 +    }
   7.117 +  }
   7.118 +
   7.119 +  def locate_query()
   7.120 +  {
   7.121 +    Swing_Thread.require()
   7.122 +
   7.123 +    current_location match {
   7.124 +      case Some(command) =>
   7.125 +        val snapshot = PIDE.session.snapshot(command.node_name)
   7.126 +        val commands = snapshot.node.commands
   7.127 +        if (commands.contains(command)) {
   7.128 +          val sources = commands.iterator.takeWhile(_ != command).map(_.source)
   7.129 +          val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   7.130 +          Hyperlink(command.node_name.node, line, column).follow(view)
   7.131 +        }
   7.132 +      case None =>
   7.133 +    }
   7.134 +  }
   7.135 +
   7.136 +
   7.137 +  /* main actor */
   7.138 +
   7.139 +  private val main_actor = actor {
   7.140 +    loop {
   7.141 +      react {
   7.142 +        case changed: Session.Commands_Changed =>
   7.143 +          current_location match {
   7.144 +            case Some(command) if !current_result && changed.commands.contains(command) =>
   7.145 +              Swing_Thread.later { handle_result() }
   7.146 +            case _ =>
   7.147 +          }
   7.148 +        case bad =>
   7.149 +          java.lang.System.err.println("Query_Operation: ignoring bad message " + bad)
   7.150 +      }
   7.151 +    }
   7.152 +  }
   7.153 +
   7.154 +  def activate() { PIDE.session.commands_changed += main_actor }
   7.155 +  def deactivate() { PIDE.session.commands_changed -= main_actor }
   7.156 +}