src/Tools/jEdit/src/find_dockable.scala
changeset 56864 0446c7ac2e32
parent 56759 790f7562cd0e
child 56865 168766e28f5e
equal deleted inserted replaced
56863:5fdb61a9a010 56864:0446c7ac2e32
   182         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
   182         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
   183       }, apply_button.tooltip)
   183       }, apply_button.tooltip)
   184   }
   184   }
   185 
   185 
   186 
   186 
       
   187   /* print operation */
       
   188 
       
   189   private val print_operation = new Find_Dockable.Operation(view)
       
   190   {
       
   191     /* query */
       
   192 
       
   193     val query_operation =
       
   194       new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
       
   195         (snapshot, results, body) =>
       
   196           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
       
   197 
       
   198     private var _selector_item = ""
       
   199     private var _selector: ComboBox[String] = null
       
   200 
       
   201     private def apply_query()
       
   202     {
       
   203       query_operation.apply_query(List(_selector.selection.item))
       
   204     }
       
   205 
       
   206     def query: JComponent = _selector.peer.asInstanceOf[JComponent]
       
   207 
       
   208 
       
   209     /* GUI page */
       
   210 
       
   211     private def update_selector()
       
   212     {
       
   213       _selector =
       
   214         new ComboBox(Print_Operation.print_operations(PIDE.session).map(_._1)) {
       
   215           selection.item = _selector_item
       
   216           listenTo(selection)
       
   217           reactions += {
       
   218             case SelectionChanged(_) =>
       
   219               _selector_item = selection.item
       
   220               apply_query()
       
   221           }
       
   222         }
       
   223     }
       
   224     update_selector()
       
   225 
       
   226     private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
       
   227 
       
   228     def select
       
   229     {
       
   230       update_selector()
       
   231       control_panel.contents.clear
       
   232       control_panel.contents += _selector
       
   233       control_panel.contents += zoom
       
   234       _selector.requestFocus
       
   235     }
       
   236 
       
   237     val page =
       
   238       new TabbedPane.Page("Print ...", new BorderPanel {
       
   239         add(control_panel, BorderPanel.Position.North)
       
   240         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
       
   241       }, "Print information from context")
       
   242   }
       
   243 
       
   244 
   187   /* operations */
   245   /* operations */
   188 
   246 
   189   private val operations = List(find_theorems, find_consts)
   247   private val operations = List(find_theorems, find_consts, print_operation)
   190 
   248 
   191   private val operations_pane = new TabbedPane
   249   private val operations_pane = new TabbedPane
   192   {
   250   {
   193     pages ++= operations.map(_.page)
   251     pages ++= operations.map(_.page)
   194     listenTo(selection)
   252     listenTo(selection)