# HG changeset patch
# User wenzelm
# Date 1399295827 -7200
# Node ID 0446c7ac2e32bb84267866c1e2ef5a7d5b2d3cf2
# Parent  5fdb61a9a010ca3673264eb830c282ed42a168ee
support print operations as asynchronous query;

diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon May 05 15:17:07 2014 +0200
@@ -162,6 +162,7 @@
   val print_syntax: Proof.context -> unit
   val print_abbrevs: Proof.context -> unit
   val print_binds: Proof.context -> unit
+  val pretty_local_facts: Proof.context -> bool -> Pretty.T list
   val print_local_facts: Proof.context -> bool -> unit
   val print_cases: Proof.context -> unit
   val debug: bool Config.T
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon May 05 15:17:07 2014 +0200
@@ -183,6 +183,8 @@
   val loading_theory: string -> Properties.T
   val dest_loading_theory: Properties.T -> string option
   val use_theories_result: string -> bool -> Properties.T
+  val print_operationsN: string
+  val print_operations: Properties.T
   val simp_trace_logN: string
   val simp_trace_stepN: string
   val simp_trace_recurseN: string
@@ -578,6 +580,9 @@
 fun use_theories_result id ok =
   [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
 
+val print_operationsN = "print_operations";
+val print_operations = [(functionN, print_operationsN)];
+
 
 (* simplifier trace *)
 
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/PIDE/markup.scala	Mon May 05 15:17:07 2014 +0200
@@ -459,6 +459,8 @@
       }
   }
 
+  val PRINT_OPERATIONS = "print_operations"
+
 
   /* simplifier trace */
 
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Mon May 05 15:17:07 2014 +0200
@@ -98,6 +98,7 @@
 
   abstract class Protocol_Handler
   {
+    def start(prover: Prover): Unit = {}
     def stop(prover: Prover): Unit = {}
     val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
   }
@@ -122,6 +123,8 @@
       val (handlers2, functions2) =
         try {
           val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
+          new_handler.start(prover)
+
           val new_functions =
             for ((a, f) <- new_handler.functions.toList) yield
               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/Pure.thy	Mon May 05 15:17:07 2014 +0200
@@ -108,6 +108,7 @@
 
 ML_file "ML/ml_antiquotations.ML"
 ML_file "ML/ml_thms.ML"
+ML_file "Tools/print_operation.ML"
 ML_file "Isar/isar_syn.ML"
 ML_file "Isar/calculation.ML"
 ML_file "Tools/rail.ML"
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/Tools/print_operation.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.ML	Mon May 05 15:17:07 2014 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/Tools/print_operation.ML
+    Author:     Makarius
+
+Print operations as asynchronous query.
+*)
+
+
+signature PRINT_OPERATION =
+sig
+  val register: string -> string -> (Toplevel.state -> string) -> unit
+end;
+
+structure Print_Operation: PRINT_OPERATION =
+struct
+
+(* maintain print operations *)
+
+local
+
+val print_operations =
+  Synchronized.var "print_operations"
+    (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
+
+fun report () =
+  Output.try_protocol_message Markup.print_operations
+    let
+      val yxml =
+        Symtab.fold (fn (x, (y, _)) => cons (x, y)) (Synchronized.value print_operations) []
+        |> sort_wrt #1
+        |> let open XML.Encode in list (pair string string) end
+        |> YXML.string_of_body;
+    in [yxml] end;
+
+val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
+
+val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
+
+in
+
+fun register name description pr =
+ (Synchronized.change print_operations (fn tab =>
+   (if not (Symtab.defined tab name) then ()
+    else warning ("Redefining print operation: " ^ quote name);
+    Symtab.update (name, (description, pr)) tab));
+  report ());
+
+val _ =
+  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
+    let
+      val [name] = args;
+      val pr =
+        (case Symtab.lookup (Synchronized.value print_operations) name of
+          SOME (_, pr) => pr
+        | NONE => error ("Unknown print operation: " ^ quote name));
+      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
+    in output_result result end);
+
+end;
+
+
+(* common print operations *)
+
+val _ =
+  register "facts" "print facts of proof context"
+    (fn st =>
+      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
+      |> Pretty.chunks |> Pretty.string_of);
+
+end;
+
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/Tools/print_operation.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/print_operation.scala	Mon May 05 15:17:07 2014 +0200
@@ -0,0 +1,43 @@
+/*  Title:      Pure/System/print_operation.scala
+    Author:     Makarius
+
+Print operations as asynchronous query.
+*/
+
+package isabelle
+
+
+object Print_Operation
+{
+  def print_operations(session: Session): List[(String, String)] =
+    session.protocol_handler("isabelle.Print_Operation$Handler") match {
+      case Some(handler: Handler) => handler.get
+      case _ => Nil
+    }
+
+
+  /* protocol handler */
+
+  class Handler extends Session.Protocol_Handler
+  {
+    private val print_operations = Synchronized(Nil: List[(String, String)])
+
+    def get: List[(String, String)] = print_operations.value
+
+    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    {
+      val ops =
+      {
+        import XML.Decode._
+        list(pair(string, string))(YXML.parse_body(msg.text))
+      }
+      print_operations.change(_ => ops)
+      true
+    }
+
+    override def start(prover: Prover): Unit =
+      prover.protocol_command(Markup.PRINT_OPERATIONS)
+
+    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
+  }
+}
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon May 05 11:53:07 2014 +0200
+++ b/src/Pure/build-jars	Mon May 05 15:17:07 2014 +0200
@@ -89,6 +89,7 @@
   Tools/keywords.scala
   Tools/main.scala
   Tools/ml_statistics.scala
+  Tools/print_operation.scala
   Tools/simplifier_trace.scala
   Tools/task_statistics.scala
   library.scala
diff -r 5fdb61a9a010 -r 0446c7ac2e32 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 11:53:07 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 15:17:07 2014 +0200
@@ -184,9 +184,67 @@
   }
 
 
+  /* print operation */
+
+  private val print_operation = new Find_Dockable.Operation(view)
+  {
+    /* query */
+
+    val query_operation =
+      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+        (snapshot, results, body) =>
+          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+    private var _selector_item = ""
+    private var _selector: ComboBox[String] = null
+
+    private def apply_query()
+    {
+      query_operation.apply_query(List(_selector.selection.item))
+    }
+
+    def query: JComponent = _selector.peer.asInstanceOf[JComponent]
+
+
+    /* GUI page */
+
+    private def update_selector()
+    {
+      _selector =
+        new ComboBox(Print_Operation.print_operations(PIDE.session).map(_._1)) {
+          selection.item = _selector_item
+          listenTo(selection)
+          reactions += {
+            case SelectionChanged(_) =>
+              _selector_item = selection.item
+              apply_query()
+          }
+        }
+    }
+    update_selector()
+
+    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
+
+    def select
+    {
+      update_selector()
+      control_panel.contents.clear
+      control_panel.contents += _selector
+      control_panel.contents += zoom
+      _selector.requestFocus
+    }
+
+    val page =
+      new TabbedPane.Page("Print ...", new BorderPanel {
+        add(control_panel, BorderPanel.Position.North)
+        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+      }, "Print information from context")
+  }
+
+
   /* operations */
 
-  private val operations = List(find_theorems, find_consts)
+  private val operations = List(find_theorems, find_consts, print_operation)
 
   private val operations_pane = new TabbedPane
   {