support multiple selected print operations instead of slightly odd "menu";

--- a/src/Pure/Tools/print_operation.ML	Tue Jul 22 12:05:53 2014 +0200
+++ b/src/Pure/Tools/print_operation.ML	Tue Jul 22 13:36:51 2014 +0200
@@ -7,7 +7,7 @@
 
 signature PRINT_OPERATION =
 sig
-  val register: string -> string -> (Toplevel.state -> string) -> unit
+  val register: string -> string -> (Toplevel.state -> Pretty.T list) -> unit
 end;
 
 structure Print_Operation: PRINT_OPERATION =
@@ -19,7 +19,7 @@
 
 val print_operations =
   Synchronized.var "print_operations"
-    ([]: (string * (string * (Toplevel.state -> string))) list);
+    ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list);
 
 fun report () =
   Output.try_protocol_message Markup.print_operations
@@ -47,13 +47,13 @@
 val _ =
   Query_Operation.register "print_operation" (fn {state, args, output_result} =>
     let
-      val [name] = args;
-      val pr =
+      val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
+      fun err s = Pretty.mark_str (Markup.bad, s);
+      fun print name =
         (case AList.lookup (op =) (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);
+          SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
+        | NONE => [err ("Unknown print operation: " ^ quote name)]);
+    in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
 
 end;
 
@@ -61,24 +61,21 @@
 (* common print operations *)
 
 val _ =
-  register "context" "context of local theory target"
-    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
+  register "context" "context of local theory target" Toplevel.pretty_context;
 
 val _ =
-  register "cases" "cases of proof context"
-    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
+  register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of);
 
 val _ =
   register "terms" "term bindings of proof context"
-    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of);
+    (Proof_Context.pretty_term_bindings o Toplevel.context_of);
 
 val _ =
   register "theorems" "theorems of local theory or proof context"
-    (Pretty.string_of o Isar_Cmd.pretty_theorems false);
+    (single o Isar_Cmd.pretty_theorems false);
 
 val _ =
-  register "state" "proof state"
-    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state);
+  register "state" "proof state" Toplevel.pretty_state;
 
 end;
 

--- a/src/Tools/jEdit/src/query_dockable.scala	Tue Jul 22 12:05:53 2014 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala	Tue Jul 22 13:36:51 2014 +0200
@@ -184,6 +184,40 @@
 
   private val print_operation = new Query_Dockable.Operation(view)
   {
+    /* items */
+
+    private class Item(val name: String, description: String, sel: Boolean)
+    {
+      val checkbox = new CheckBox(name) {
+        tooltip = "Print " + description
+        selected = sel
+        reactions += { case ButtonClicked(_) => apply_query() }
+      }
+    }
+
+    private var _items: List[Item] = Nil
+
+    private def selected_items(): List[String] =
+      for (item <- _items if item.checkbox.selected) yield item.name
+
+    private def update_items(): List[Item] =
+    {
+      val old_items = _items
+      def was_selected(name: String): Boolean =
+        old_items.find(item => item.name == name) match {
+          case None => false
+          case Some(item) => item.checkbox.selected
+        }
+
+      _items =
+        Print_Operation.print_operations(PIDE.session).map(
+          {
+            case (name, description) => new Item(name, description, was_selected(name))
+          })
+      _items
+    }
+
+
     /* query */
 
     private val process_indicator = new Process_Indicator
@@ -196,50 +230,13 @@
 
     private def apply_query()
     {
-      query_operation.apply_query(List(selector.selection.item))
+      query_operation.apply_query(selected_items())
     }
 
     private val query_label = new Label("Print:")
     def query: JComponent = apply_button.peer
 
-
-    /* items */
-
-    case class Item(name: String, description: String)
-
-    class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
-      extends ListView.Renderer[String]
-    {
-      def componentFor(list: ListView[_],
-        selected: Boolean, focused: Boolean, item: String, index: Int) =
-      {
-        val component = old_renderer.componentFor(list, selected, focused, item, index)
-        try { component.tooltip = items(index).description }
-        catch { case _: IndexOutOfBoundsException => }
-        component
-      }
-    }
-
-    private var selector_item: Option[String] = None
-    private var selector = new ComboBox[String](Nil)
-
-    private def set_selector()
-    {
-      val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
-
-      selector =
-        new ComboBox(items.map(_.name)) {
-          selector_item.foreach(item => selection.item = item)
-          listenTo(selection)
-          reactions += {
-            case SelectionChanged(_) =>
-              selector_item = Some(selection.item)
-              apply_query()
-          }
-        }
-      selector.renderer = new Renderer(selector.renderer, items)
-    }
-    set_selector()
+    update_items()
 
 
     /* GUI page */
@@ -259,10 +256,11 @@
 
     def select
     {
-      set_selector()
       control_panel.contents.clear
+      control_panel.contents += query_label
+      update_items().foreach(item => control_panel.contents += item.checkbox)
       control_panel.contents ++=
-        List(query_label, selector, process_indicator.component, apply_button,
+        List(process_indicator.component, apply_button,
           pretty_text_area.search_label, pretty_text_area.search_field, zoom)
     }