src/Tools/jEdit/src/jedit/html_panel.scala
changeset 42976 9901f877eeb7
parent 39740 0294948ba962
equal deleted inserted replaced
42975:284f9a7af1c9 42976:9901f877eeb7
    65 
    65 
    66   private val ucontext = new SimpleUserAgentContext
    66   private val ucontext = new SimpleUserAgentContext
    67   private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    67   private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    68   {
    68   {
    69     private def handle(event: HTML_Panel.Event): Boolean =
    69     private def handle(event: HTML_Panel.Event): Boolean =
    70       if (handler.isDefinedAt(event)) { handler(event); true }
    70       if (handler.isDefinedAt(event)) { handler(event); false }
    71       else false
    71       else true
    72 
    72 
    73     override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    73     override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    74       handle(HTML_Panel.Context_Menu(elem, event))
    74       handle(HTML_Panel.Context_Menu(elem, event))
    75     override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    75     override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    76       handle(HTML_Panel.Mouse_Click(elem, event))
    76       handle(HTML_Panel.Mouse_Click(elem, event))