merged
authorwenzelm
Sat Dec 15 22:19:14 2012 +0100 (2012-12-15)
changeset 50560e4dc37ec1427
parent 50559 89c0d2f13cca
parent 50554 0493efcc97e9
child 50561 9a733bd6c0ba
merged
     1.1 --- a/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 21:34:32 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup_tree.scala	Sat Dec 15 22:19:14 2012 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4  
     1.5  object Markup_Tree
     1.6  {
     1.7 +  /* construct trees */
     1.8 +
     1.9    val empty: Markup_Tree = new Markup_Tree(Branches.empty)
    1.10  
    1.11    def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
    1.12 @@ -35,26 +37,56 @@
    1.13            })
    1.14      }
    1.15  
    1.16 +
    1.17 +  /* tree building blocks */
    1.18 +
    1.19 +  object Elements
    1.20 +  {
    1.21 +    val empty = new Elements(Set.empty)
    1.22 +  }
    1.23 +
    1.24 +  final class Elements private(private val rep: Set[String])
    1.25 +  {
    1.26 +    def contains(name: String): Boolean = rep.contains(name)
    1.27 +
    1.28 +    def + (name: String): Elements =
    1.29 +      if (contains(name)) this
    1.30 +      else new Elements(rep + name)
    1.31 +
    1.32 +    def + (elem: XML.Elem): Elements = this + elem.markup.name
    1.33 +    def ++ (elems: Iterable[XML.Elem]): Elements = (this /: elems.iterator)(_ + _)
    1.34 +
    1.35 +    def ++ (other: Elements): Elements =
    1.36 +      if (this eq other) this
    1.37 +      else if (rep.isEmpty) other
    1.38 +      else (this /: other.rep)(_ + _)
    1.39 +  }
    1.40 +
    1.41    object Entry
    1.42    {
    1.43      def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
    1.44 -      Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
    1.45 +      Entry(markup.range, List(markup.info), Elements.empty + markup.info,
    1.46 +        subtree, subtree.make_elements)
    1.47  
    1.48      def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
    1.49 -      Entry(range, rev_markups, Set.empty ++ rev_markups.iterator.map(_.markup.name), subtree)
    1.50 +      Entry(range, rev_markups, Elements.empty ++ rev_markups,
    1.51 +        subtree, subtree.make_elements)
    1.52    }
    1.53  
    1.54    sealed case class Entry(
    1.55      range: Text.Range,
    1.56      rev_markup: List[XML.Elem],
    1.57 -    elements: Set[String],
    1.58 -    subtree: Markup_Tree)
    1.59 +    elements: Elements,
    1.60 +    subtree: Markup_Tree,
    1.61 +    subtree_elements: Elements)
    1.62    {
    1.63 -    def + (info: XML.Elem): Entry =
    1.64 -      if (elements(info.markup.name)) copy(rev_markup = info :: rev_markup)
    1.65 -      else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
    1.66 +    def markup: List[XML.Elem] = rev_markup.reverse
    1.67  
    1.68 -    def markup: List[XML.Elem] = rev_markup.reverse
    1.69 +    def + (markup: Text.Markup): Entry =
    1.70 +      copy(rev_markup = markup.info :: rev_markup, elements = elements + markup.info)
    1.71 +
    1.72 +    def \ (markup: Text.Markup): Entry =
    1.73 +      copy(subtree = subtree + markup, subtree_elements = subtree_elements + markup.info)
    1.74    }
    1.75  
    1.76    object Branches
    1.77 @@ -121,6 +153,10 @@
    1.78      }
    1.79    }
    1.80  
    1.81 +  def make_elements: Elements =
    1.82 +    (Elements.empty /: branches)(
    1.83 +      { case (elements, (_, entry)) => elements ++ entry.subtree_elements ++ entry.elements })
    1.84 +
    1.85    def + (new_markup: Text.Markup): Markup_Tree =
    1.86    {
    1.87      val new_range = new_markup.range
    1.88 @@ -129,9 +165,9 @@
    1.89        case None => new Markup_Tree(branches, Entry(new_markup, empty))
    1.90        case Some(entry) =>
    1.91          if (entry.range == new_range)
    1.92 -          new Markup_Tree(branches, entry + new_markup.info)
    1.93 +          new Markup_Tree(branches, entry + new_markup)
    1.94          else if (entry.range.contains(new_range))
    1.95 -          new Markup_Tree(branches, entry.copy(subtree = entry.subtree + new_markup))
    1.96 +          new Markup_Tree(branches, entry \ new_markup)
    1.97          else if (new_range.contains(branches.head._1) && new_range.contains(branches.last._1))
    1.98            new Markup_Tree(Branches.empty, Entry(new_markup, this))
    1.99          else {
   1.100 @@ -184,19 +220,25 @@
   1.101    def cumulate[A](root_range: Text.Range, root_info: A, result_elements: Option[Set[String]],
   1.102      result: PartialFunction[(A, Text.Markup), A]): Stream[Text.Info[A]] =
   1.103    {
   1.104 +    val notable: Elements => Boolean =
   1.105 +      result_elements match {
   1.106 +        case Some(res) => (elements: Elements) => res.exists(elements.contains)
   1.107 +        case None => (elements: Elements) => true
   1.108 +      }
   1.109 +
   1.110      def results(x: A, entry: Entry): Option[A] =
   1.111 -      if (result_elements match { case Some(es) => es.exists(entry.elements) case None => true }) {
   1.112 -        val (y, changed) =
   1.113 -          ((x, false) /: entry.rev_markup)((res, info) =>  // FIXME proper order!?
   1.114 -            {
   1.115 -              val (y, changed) = res
   1.116 -              val arg = (y, Text.Info(entry.range, info))
   1.117 -              if (result.isDefinedAt(arg)) (result(arg), true)
   1.118 -              else res
   1.119 -            })
   1.120 -        if (changed) Some(y) else None
   1.121 -      }
   1.122 -      else None
   1.123 +    {
   1.124 +      val (y, changed) =
   1.125 +        // FIXME proper cumulation order (including status markup) (!?)
   1.126 +        ((x, false) /: entry.rev_markup)((res, info) =>
   1.127 +          {
   1.128 +            val (y, changed) = res
   1.129 +            val arg = (y, Text.Info(entry.range, info))
   1.130 +            if (result.isDefinedAt(arg)) (result(arg), true)
   1.131 +            else res
   1.132 +          })
   1.133 +      if (changed) Some(y) else None
   1.134 +    }
   1.135  
   1.136      def stream(
   1.137        last: Text.Offset,
   1.138 @@ -205,10 +247,13 @@
   1.139        stack match {
   1.140          case (parent, (range, entry) #:: more) :: rest =>
   1.141            val subrange = range.restrict(root_range)
   1.142 -          val subtree = entry.subtree.overlapping(subrange).toStream
   1.143 +          val subtree =
   1.144 +            if (notable(entry.subtree_elements))
   1.145 +              entry.subtree.overlapping(subrange).toStream
   1.146 +            else Stream.empty
   1.147            val start = subrange.start
   1.148  
   1.149 -          results(parent.info, entry) match {
   1.150 +          (if (notable(entry.elements)) results(parent.info, entry) else None) match {
   1.151              case Some(res) =>
   1.152                val next = Text.Info(subrange, res)
   1.153                val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
     2.1 --- a/src/Tools/jEdit/etc/options	Sat Dec 15 21:34:32 2012 +0100
     2.2 +++ b/src/Tools/jEdit/etc/options	Sat Dec 15 22:19:14 2012 +0100
     2.3 @@ -12,6 +12,9 @@
     2.4  option jedit_tooltip_margin : int = 60
     2.5    -- "margin for tooltip pretty-printing"
     2.6  
     2.7 +option jedit_tooltip_bounds : real = 0.5
     2.8 +  -- "relative bounds of tooltip window wrt. logical screen size"
     2.9 +
    2.10  option jedit_text_overview_limit : int = 100000
    2.11    -- "maximum amount of text to visualize in overview column"
    2.12  
     3.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 21:34:32 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sat Dec 15 22:19:14 2012 +0100
     3.3 @@ -41,8 +41,8 @@
     3.4  {
     3.5    // FIXME avoid hard-wired stuff
     3.6    private val relevant_options =
     3.7 -    Set("jedit_logic", "jedit_font_scale", "jedit_text_overview_limit",
     3.8 -      "jedit_tooltip_font_scale", "jedit_symbols_search_limit", "jedit_tooltip_margin",
     3.9 +    Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
    3.10 +      "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
    3.11        "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold", "ML_statistics",
    3.12        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
    3.13        "editor_tracing_messages", "editor_update_delay")
     4.1 --- a/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 21:34:32 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/jedit_lib.scala	Sat Dec 15 22:19:14 2012 +0100
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  import isabelle._
     4.6  
     4.7 -import java.awt.{Component, Container, Frame, Window}
     4.8 +import java.awt.{Component, Container, Frame, Window, GraphicsEnvironment, Point, Rectangle}
     4.9  
    4.10  import scala.annotation.tailrec
    4.11  
    4.12 @@ -20,6 +20,19 @@
    4.13  
    4.14  object JEdit_Lib
    4.15  {
    4.16 +  /* bounds within multi-screen environment */
    4.17 +
    4.18 +  def screen_bounds(screen_point: Point): Rectangle =
    4.19 +  {
    4.20 +    val ge = GraphicsEnvironment.getLocalGraphicsEnvironment
    4.21 +    (for {
    4.22 +      device <- ge.getScreenDevices.iterator
    4.23 +      config <- device.getConfigurations.iterator
    4.24 +      bounds = config.getBounds
    4.25 +    } yield bounds).find(_.contains(screen_point)) getOrElse ge.getMaximumWindowBounds
    4.26 +  }
    4.27 +
    4.28 +
    4.29    /* GUI components */
    4.30  
    4.31    def get_parent(component: Component): Option[Container] =
     5.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 21:34:32 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sat Dec 15 22:19:14 2012 +0100
     5.3 @@ -9,7 +9,7 @@
     5.4  
     5.5  import isabelle._
     5.6  
     5.7 -import java.awt.{Toolkit, Color, Point, BorderLayout, Window, Dimension}
     5.8 +import java.awt.{Color, Point, BorderLayout, Window, Dimension}
     5.9  import java.awt.event.{ActionListener, ActionEvent, KeyEvent, WindowEvent, WindowAdapter}
    5.10  import javax.swing.{SwingUtilities, JWindow, JPanel, JComponent, KeyStroke}
    5.11  import javax.swing.border.LineBorder
    5.12 @@ -107,27 +107,27 @@
    5.13  
    5.14    /* window geometry */
    5.15  
    5.16 +  val screen_point = new Point(mouse_x, mouse_y)
    5.17 +  SwingUtilities.convertPointToScreen(screen_point, parent)
    5.18 +  val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
    5.19 +
    5.20    {
    5.21      val font_metrics = pretty_text_area.getPainter.getFontMetrics
    5.22 -    val margin = PIDE.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
    5.23 +    val margin = rendering.tooltip_margin
    5.24      val lines =
    5.25        XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
    5.26          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    5.27  
    5.28 -    val screen = Toolkit.getDefaultToolkit.getScreenSize
    5.29 -    val w = (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen.width / 2)
    5.30 -    val h = (font_metrics.getHeight * (lines + 2)) min (screen.height / 2)
    5.31 +    val bounds = rendering.tooltip_bounds
    5.32 +    val w =
    5.33 +      (font_metrics.charWidth(Pretty.spc) * (margin + 2)) min (screen_bounds.width * bounds).toInt
    5.34 +    val h =
    5.35 +      (font_metrics.getHeight * (lines + 2)) min (screen_bounds.height * bounds).toInt
    5.36      pretty_text_area.setPreferredSize(new Dimension(w, h))
    5.37      window.pack
    5.38 -  }
    5.39  
    5.40 -  {
    5.41 -    val point = new Point(mouse_x, mouse_y)
    5.42 -    SwingUtilities.convertPointToScreen(point, parent)
    5.43 -
    5.44 -    val screen = Toolkit.getDefaultToolkit.getScreenSize
    5.45 -    val x = point.x min (screen.width - window.getWidth)
    5.46 -    val y = point.y min (screen.height - window.getHeight)
    5.47 +    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - window.getWidth)
    5.48 +    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - window.getHeight)
    5.49      window.setLocation(x, y)
    5.50    }
    5.51  
     6.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 21:34:32 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Dec 15 22:19:14 2012 +0100
     6.3 @@ -346,6 +346,9 @@
     6.4      Library.separate(Pretty.FBreak, all_tips.toList)
     6.5    }
     6.6  
     6.7 +  val tooltip_margin: Int = options.int("jedit_tooltip_margin")
     6.8 +  val tooltip_bounds: Double = (options.real("jedit_tooltip_bounds") max 0.2) min 0.8
     6.9 +
    6.10  
    6.11    def gutter_message(range: Text.Range): Option[Icon] =
    6.12    {
     7.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sat Dec 15 21:34:32 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sat Dec 15 22:19:14 2012 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  
     7.5  import isabelle._
     7.6  
     7.7 -import java.awt.{Graphics2D, Shape, Window, Color, Point}
     7.8 +import java.awt.{Graphics2D, Shape, Window, Color, Point, Toolkit}
     7.9  import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
    7.10    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    7.11  import java.awt.font.TextAttribute
    7.12 @@ -168,7 +168,7 @@
    7.13    private val mouse_motion_listener = new MouseMotionAdapter {
    7.14      override def mouseMoved(e: MouseEvent) {
    7.15        robust_body(()) {
    7.16 -        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
    7.17 +        control = (e.getModifiers & Toolkit.getDefaultToolkit.getMenuShortcutKeyMask) != 0
    7.18  
    7.19          if ((control || hovering) && !buffer.isLoading) {
    7.20            JEdit_Lib.buffer_lock(buffer) {