# HG changeset patch # User wenzelm # Date 1406029011 -7200 # Node ID 30885e25c6de101c8499a3bf7a6130a29ce2e70b # Parent 0f58af85881307bda7d0396e937a2077d27231a0 support multiple selected print operations instead of slightly odd "menu"; diff -r 0f58af858813 -r 30885e25c6de src/Pure/Tools/print_operation.ML --- 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; diff -r 0f58af858813 -r 30885e25c6de src/Tools/jEdit/src/query_dockable.scala --- 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) }