support multiple selected print operations instead of slightly odd "menu";
authorwenzelm
Tue Jul 22 13:36:51 2014 +0200 (2014-07-22)
changeset 5760430885e25c6de
parent 57603 0f58af858813
child 57605 8e0a7eaffe47
support multiple selected print operations instead of slightly odd "menu";
src/Pure/Tools/print_operation.ML
src/Tools/jEdit/src/query_dockable.scala
     1.1 --- a/src/Pure/Tools/print_operation.ML	Tue Jul 22 12:05:53 2014 +0200
     1.2 +++ b/src/Pure/Tools/print_operation.ML	Tue Jul 22 13:36:51 2014 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature PRINT_OPERATION =
     1.6  sig
     1.7 -  val register: string -> string -> (Toplevel.state -> string) -> unit
     1.8 +  val register: string -> string -> (Toplevel.state -> Pretty.T list) -> unit
     1.9  end;
    1.10  
    1.11  structure Print_Operation: PRINT_OPERATION =
    1.12 @@ -19,7 +19,7 @@
    1.13  
    1.14  val print_operations =
    1.15    Synchronized.var "print_operations"
    1.16 -    ([]: (string * (string * (Toplevel.state -> string))) list);
    1.17 +    ([]: (string * (string * (Toplevel.state -> Pretty.T list))) list);
    1.18  
    1.19  fun report () =
    1.20    Output.try_protocol_message Markup.print_operations
    1.21 @@ -47,13 +47,13 @@
    1.22  val _ =
    1.23    Query_Operation.register "print_operation" (fn {state, args, output_result} =>
    1.24      let
    1.25 -      val [name] = args;
    1.26 -      val pr =
    1.27 +      val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
    1.28 +      fun err s = Pretty.mark_str (Markup.bad, s);
    1.29 +      fun print name =
    1.30          (case AList.lookup (op =) (Synchronized.value print_operations) name of
    1.31 -          SOME (_, pr) => pr
    1.32 -        | NONE => error ("Unknown print operation: " ^ quote name));
    1.33 -      val result = pr state handle Toplevel.UNDEF => error "Unknown context";
    1.34 -    in output_result result end);
    1.35 +          SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
    1.36 +        | NONE => [err ("Unknown print operation: " ^ quote name)]);
    1.37 +    in output_result (Pretty.string_of (Pretty.chunks (maps print args))) end);
    1.38  
    1.39  end;
    1.40  
    1.41 @@ -61,24 +61,21 @@
    1.42  (* common print operations *)
    1.43  
    1.44  val _ =
    1.45 -  register "context" "context of local theory target"
    1.46 -    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_context);
    1.47 +  register "context" "context of local theory target" Toplevel.pretty_context;
    1.48  
    1.49  val _ =
    1.50 -  register "cases" "cases of proof context"
    1.51 -    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of);
    1.52 +  register "cases" "cases of proof context" (Proof_Context.pretty_cases o Toplevel.context_of);
    1.53  
    1.54  val _ =
    1.55    register "terms" "term bindings of proof context"
    1.56 -    (Pretty.string_of o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of);
    1.57 +    (Proof_Context.pretty_term_bindings o Toplevel.context_of);
    1.58  
    1.59  val _ =
    1.60    register "theorems" "theorems of local theory or proof context"
    1.61 -    (Pretty.string_of o Isar_Cmd.pretty_theorems false);
    1.62 +    (single o Isar_Cmd.pretty_theorems false);
    1.63  
    1.64  val _ =
    1.65 -  register "state" "proof state"
    1.66 -    (Pretty.string_of o Pretty.chunks o Toplevel.pretty_state);
    1.67 +  register "state" "proof state" Toplevel.pretty_state;
    1.68  
    1.69  end;
    1.70  
     2.1 --- a/src/Tools/jEdit/src/query_dockable.scala	Tue Jul 22 12:05:53 2014 +0200
     2.2 +++ b/src/Tools/jEdit/src/query_dockable.scala	Tue Jul 22 13:36:51 2014 +0200
     2.3 @@ -184,6 +184,40 @@
     2.4  
     2.5    private val print_operation = new Query_Dockable.Operation(view)
     2.6    {
     2.7 +    /* items */
     2.8 +
     2.9 +    private class Item(val name: String, description: String, sel: Boolean)
    2.10 +    {
    2.11 +      val checkbox = new CheckBox(name) {
    2.12 +        tooltip = "Print " + description
    2.13 +        selected = sel
    2.14 +        reactions += { case ButtonClicked(_) => apply_query() }
    2.15 +      }
    2.16 +    }
    2.17 +
    2.18 +    private var _items: List[Item] = Nil
    2.19 +
    2.20 +    private def selected_items(): List[String] =
    2.21 +      for (item <- _items if item.checkbox.selected) yield item.name
    2.22 +
    2.23 +    private def update_items(): List[Item] =
    2.24 +    {
    2.25 +      val old_items = _items
    2.26 +      def was_selected(name: String): Boolean =
    2.27 +        old_items.find(item => item.name == name) match {
    2.28 +          case None => false
    2.29 +          case Some(item) => item.checkbox.selected
    2.30 +        }
    2.31 +
    2.32 +      _items =
    2.33 +        Print_Operation.print_operations(PIDE.session).map(
    2.34 +          {
    2.35 +            case (name, description) => new Item(name, description, was_selected(name))
    2.36 +          })
    2.37 +      _items
    2.38 +    }
    2.39 +
    2.40 +
    2.41      /* query */
    2.42  
    2.43      private val process_indicator = new Process_Indicator
    2.44 @@ -196,50 +230,13 @@
    2.45  
    2.46      private def apply_query()
    2.47      {
    2.48 -      query_operation.apply_query(List(selector.selection.item))
    2.49 +      query_operation.apply_query(selected_items())
    2.50      }
    2.51  
    2.52      private val query_label = new Label("Print:")
    2.53      def query: JComponent = apply_button.peer
    2.54  
    2.55 -
    2.56 -    /* items */
    2.57 -
    2.58 -    case class Item(name: String, description: String)
    2.59 -
    2.60 -    class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
    2.61 -      extends ListView.Renderer[String]
    2.62 -    {
    2.63 -      def componentFor(list: ListView[_],
    2.64 -        selected: Boolean, focused: Boolean, item: String, index: Int) =
    2.65 -      {
    2.66 -        val component = old_renderer.componentFor(list, selected, focused, item, index)
    2.67 -        try { component.tooltip = items(index).description }
    2.68 -        catch { case _: IndexOutOfBoundsException => }
    2.69 -        component
    2.70 -      }
    2.71 -    }
    2.72 -
    2.73 -    private var selector_item: Option[String] = None
    2.74 -    private var selector = new ComboBox[String](Nil)
    2.75 -
    2.76 -    private def set_selector()
    2.77 -    {
    2.78 -      val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
    2.79 -
    2.80 -      selector =
    2.81 -        new ComboBox(items.map(_.name)) {
    2.82 -          selector_item.foreach(item => selection.item = item)
    2.83 -          listenTo(selection)
    2.84 -          reactions += {
    2.85 -            case SelectionChanged(_) =>
    2.86 -              selector_item = Some(selection.item)
    2.87 -              apply_query()
    2.88 -          }
    2.89 -        }
    2.90 -      selector.renderer = new Renderer(selector.renderer, items)
    2.91 -    }
    2.92 -    set_selector()
    2.93 +    update_items()
    2.94  
    2.95  
    2.96      /* GUI page */
    2.97 @@ -259,10 +256,11 @@
    2.98  
    2.99      def select
   2.100      {
   2.101 -      set_selector()
   2.102        control_panel.contents.clear
   2.103 +      control_panel.contents += query_label
   2.104 +      update_items().foreach(item => control_panel.contents += item.checkbox)
   2.105        control_panel.contents ++=
   2.106 -        List(query_label, selector, process_indicator.component, apply_button,
   2.107 +        List(process_indicator.component, apply_button,
   2.108            pretty_text_area.search_label, pretty_text_area.search_field, zoom)
   2.109      }
   2.110