--- 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
--- 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 *)
--- 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 */
--- 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))
--- 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"
--- /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;
+
--- /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 _)
+ }
+}
--- 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
--- 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
{