1.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 05 11:53:07 2014 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 05 15:17:07 2014 +0200
     1.3 @@ -162,6 +162,7 @@
     1.4    val print_syntax: Proof.context -> unit
     1.5    val print_abbrevs: Proof.context -> unit
     1.6    val print_binds: Proof.context -> unit
     1.7 +  val pretty_local_facts: Proof.context -> bool -> Pretty.T list
     1.8    val print_local_facts: Proof.context -> bool -> unit
     1.9    val print_cases: Proof.context -> unit
    1.10    val debug: bool Config.T

     2.1 --- a/src/Pure/PIDE/markup.ML	Mon May 05 11:53:07 2014 +0200
     2.2 +++ b/src/Pure/PIDE/markup.ML	Mon May 05 15:17:07 2014 +0200
     2.3 @@ -183,6 +183,8 @@
     2.4    val loading_theory: string -> Properties.T
     2.5    val dest_loading_theory: Properties.T -> string option
     2.6    val use_theories_result: string -> bool -> Properties.T
     2.7 +  val print_operationsN: string
     2.8 +  val print_operations: Properties.T
     2.9    val simp_trace_logN: string
    2.10    val simp_trace_stepN: string
    2.11    val simp_trace_recurseN: string
    2.12 @@ -578,6 +580,9 @@
    2.13  fun use_theories_result id ok =
    2.14    [("function", "use_theories_result"), ("id", id), ("ok", print_bool ok)];
    2.15  
    2.16 +val print_operationsN = "print_operations";
    2.17 +val print_operations = [(functionN, print_operationsN)];
    2.18 +
    2.19  
    2.20  (* simplifier trace *)
    2.21  

     3.1 --- a/src/Pure/PIDE/markup.scala	Mon May 05 11:53:07 2014 +0200
     3.2 +++ b/src/Pure/PIDE/markup.scala	Mon May 05 15:17:07 2014 +0200
     3.3 @@ -459,6 +459,8 @@
     3.4        }
     3.5    }
     3.6  
     3.7 +  val PRINT_OPERATIONS = "print_operations"
     3.8 +
     3.9  
    3.10    /* simplifier trace */
    3.11  

     4.1 --- a/src/Pure/PIDE/session.scala	Mon May 05 11:53:07 2014 +0200
     4.2 +++ b/src/Pure/PIDE/session.scala	Mon May 05 15:17:07 2014 +0200
     4.3 @@ -98,6 +98,7 @@
     4.4  
     4.5    abstract class Protocol_Handler
     4.6    {
     4.7 +    def start(prover: Prover): Unit = {}
     4.8      def stop(prover: Prover): Unit = {}
     4.9      val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
    4.10    }
    4.11 @@ -122,6 +123,8 @@
    4.12        val (handlers2, functions2) =
    4.13          try {
    4.14            val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler]
    4.15 +          new_handler.start(prover)
    4.16 +
    4.17            val new_functions =
    4.18              for ((a, f) <- new_handler.functions.toList) yield
    4.19                (a, (msg: Prover.Protocol_Output) => f(prover, msg))

     5.1 --- a/src/Pure/Pure.thy	Mon May 05 11:53:07 2014 +0200
     5.2 +++ b/src/Pure/Pure.thy	Mon May 05 15:17:07 2014 +0200
     5.3 @@ -108,6 +108,7 @@
     5.4  
     5.5  ML_file "ML/ml_antiquotations.ML"
     5.6  ML_file "ML/ml_thms.ML"
     5.7 +ML_file "Tools/print_operation.ML"
     5.8  ML_file "Isar/isar_syn.ML"
     5.9  ML_file "Isar/calculation.ML"
    5.10  ML_file "Tools/rail.ML"

     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/Tools/print_operation.ML	Mon May 05 15:17:07 2014 +0200
     6.3 @@ -0,0 +1,70 @@
     6.4 +(*  Title:      Pure/Tools/print_operation.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Print operations as asynchronous query.
     6.8 +*)
     6.9 +
    6.10 +
    6.11 +signature PRINT_OPERATION =
    6.12 +sig
    6.13 +  val register: string -> string -> (Toplevel.state -> string) -> unit
    6.14 +end;
    6.15 +
    6.16 +structure Print_Operation: PRINT_OPERATION =
    6.17 +struct
    6.18 +
    6.19 +(* maintain print operations *)
    6.20 +
    6.21 +local
    6.22 +
    6.23 +val print_operations =
    6.24 +  Synchronized.var "print_operations"
    6.25 +    (Symtab.empty: (string * (Toplevel.state -> string)) Symtab.table);
    6.26 +
    6.27 +fun report () =
    6.28 +  Output.try_protocol_message Markup.print_operations
    6.29 +    let
    6.30 +      val yxml =
    6.31 +        Symtab.fold (fn (x, (y, _)) => cons (x, y)) (Synchronized.value print_operations) []
    6.32 +        |> sort_wrt #1
    6.33 +        |> let open XML.Encode in list (pair string string) end
    6.34 +        |> YXML.string_of_body;
    6.35 +    in [yxml] end;
    6.36 +
    6.37 +val _ = Isabelle_Process.protocol_command "print_operations" (fn [] => report ());
    6.38 +
    6.39 +val _ = Session.protocol_handler "isabelle.Print_Operation$Handler";
    6.40 +
    6.41 +in
    6.42 +
    6.43 +fun register name description pr =
    6.44 + (Synchronized.change print_operations (fn tab =>
    6.45 +   (if not (Symtab.defined tab name) then ()
    6.46 +    else warning ("Redefining print operation: " ^ quote name);
    6.47 +    Symtab.update (name, (description, pr)) tab));
    6.48 +  report ());
    6.49 +
    6.50 +val _ =
    6.51 +  Query_Operation.register "print_operation" (fn {state, args, output_result} =>
    6.52 +    let
    6.53 +      val [name] = args;
    6.54 +      val pr =
    6.55 +        (case Symtab.lookup (Synchronized.value print_operations) name of
    6.56 +          SOME (_, pr) => pr
    6.57 +        | NONE => error ("Unknown print operation: " ^ quote name));
    6.58 +      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
    6.59 +    in output_result result end);
    6.60 +
    6.61 +end;
    6.62 +
    6.63 +
    6.64 +(* common print operations *)
    6.65 +
    6.66 +val _ =
    6.67 +  register "facts" "print facts of proof context"
    6.68 +    (fn st =>
    6.69 +      Proof_Context.pretty_local_facts (Toplevel.context_of st) false
    6.70 +      |> Pretty.chunks |> Pretty.string_of);
    6.71 +
    6.72 +end;
    6.73 +

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Tools/print_operation.scala	Mon May 05 15:17:07 2014 +0200
     7.3 @@ -0,0 +1,43 @@
     7.4 +/*  Title:      Pure/System/print_operation.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +Print operations as asynchronous query.
     7.8 +*/
     7.9 +
    7.10 +package isabelle
    7.11 +
    7.12 +
    7.13 +object Print_Operation
    7.14 +{
    7.15 +  def print_operations(session: Session): List[(String, String)] =
    7.16 +    session.protocol_handler("isabelle.Print_Operation$Handler") match {
    7.17 +      case Some(handler: Handler) => handler.get
    7.18 +      case _ => Nil
    7.19 +    }
    7.20 +
    7.21 +
    7.22 +  /* protocol handler */
    7.23 +
    7.24 +  class Handler extends Session.Protocol_Handler
    7.25 +  {
    7.26 +    private val print_operations = Synchronized(Nil: List[(String, String)])
    7.27 +
    7.28 +    def get: List[(String, String)] = print_operations.value
    7.29 +
    7.30 +    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
    7.31 +    {
    7.32 +      val ops =
    7.33 +      {
    7.34 +        import XML.Decode._
    7.35 +        list(pair(string, string))(YXML.parse_body(msg.text))
    7.36 +      }
    7.37 +      print_operations.change(_ => ops)
    7.38 +      true
    7.39 +    }
    7.40 +
    7.41 +    override def start(prover: Prover): Unit =
    7.42 +      prover.protocol_command(Markup.PRINT_OPERATIONS)
    7.43 +
    7.44 +    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
    7.45 +  }
    7.46 +}

     8.1 --- a/src/Pure/build-jars	Mon May 05 11:53:07 2014 +0200
     8.2 +++ b/src/Pure/build-jars	Mon May 05 15:17:07 2014 +0200
     8.3 @@ -89,6 +89,7 @@
     8.4    Tools/keywords.scala
     8.5    Tools/main.scala
     8.6    Tools/ml_statistics.scala
     8.7 +  Tools/print_operation.scala
     8.8    Tools/simplifier_trace.scala
     8.9    Tools/task_statistics.scala
    8.10    library.scala

     9.1 --- a/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 11:53:07 2014 +0200
     9.2 +++ b/src/Tools/jEdit/src/find_dockable.scala	Mon May 05 15:17:07 2014 +0200
     9.3 @@ -184,9 +184,67 @@
     9.4    }
     9.5  
     9.6  
     9.7 +  /* print operation */
     9.8 +
     9.9 +  private val print_operation = new Find_Dockable.Operation(view)
    9.10 +  {
    9.11 +    /* query */
    9.12 +
    9.13 +    val query_operation =
    9.14 +      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
    9.15 +        (snapshot, results, body) =>
    9.16 +          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
    9.17 +
    9.18 +    private var _selector_item = ""
    9.19 +    private var _selector: ComboBox[String] = null
    9.20 +
    9.21 +    private def apply_query()
    9.22 +    {
    9.23 +      query_operation.apply_query(List(_selector.selection.item))
    9.24 +    }
    9.25 +
    9.26 +    def query: JComponent = _selector.peer.asInstanceOf[JComponent]
    9.27 +
    9.28 +
    9.29 +    /* GUI page */
    9.30 +
    9.31 +    private def update_selector()
    9.32 +    {
    9.33 +      _selector =
    9.34 +        new ComboBox(Print_Operation.print_operations(PIDE.session).map(_._1)) {
    9.35 +          selection.item = _selector_item
    9.36 +          listenTo(selection)
    9.37 +          reactions += {
    9.38 +            case SelectionChanged(_) =>
    9.39 +              _selector_item = selection.item
    9.40 +              apply_query()
    9.41 +          }
    9.42 +        }
    9.43 +    }
    9.44 +    update_selector()
    9.45 +
    9.46 +    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
    9.47 +
    9.48 +    def select
    9.49 +    {
    9.50 +      update_selector()
    9.51 +      control_panel.contents.clear
    9.52 +      control_panel.contents += _selector
    9.53 +      control_panel.contents += zoom
    9.54 +      _selector.requestFocus
    9.55 +    }
    9.56 +
    9.57 +    val page =
    9.58 +      new TabbedPane.Page("Print ...", new BorderPanel {
    9.59 +        add(control_panel, BorderPanel.Position.North)
    9.60 +        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
    9.61 +      }, "Print information from context")
    9.62 +  }
    9.63 +
    9.64 +
    9.65    /* operations */
    9.66  
    9.67 -  private val operations = List(find_theorems, find_consts)
    9.68 +  private val operations = List(find_theorems, find_consts, print_operation)
    9.69  
    9.70    private val operations_pane = new TabbedPane
    9.71    {