concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
authorwenzelm
Tue Sep 07 23:06:52 2010 +0200 (2010-09-07)
changeset 3917883e9f3ccea9f
parent 39177 0468964aec11
child 39179 591bbab9ef59
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
src/Pure/PIDE/document.scala
src/Pure/PIDE/markup_tree.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_markup.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Tue Sep 07 22:28:58 2010 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Tue Sep 07 23:06:52 2010 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4      def convert(range: Text.Range): Text.Range
     1.5      def revert(i: Text.Offset): Text.Offset
     1.6      def revert(range: Text.Range): Text.Range
     1.7 -    def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
     1.8 +    def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
     1.9        : Stream[Text.Info[Option[A]]]
    1.10    }
    1.11  
    1.12 @@ -310,7 +310,7 @@
    1.13          def revert(range: Text.Range): Text.Range =
    1.14            if (edits.isEmpty) range else range.map(revert(_))
    1.15  
    1.16 -        def select_markup[A](range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    1.17 +        def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.18            : Stream[Text.Info[Option[A]]] =
    1.19          {
    1.20            val former_range = revert(range)
     2.1 --- a/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 22:28:58 2010 +0200
     2.2 +++ b/src/Pure/PIDE/markup_tree.scala	Tue Sep 07 23:06:52 2010 +0200
     2.3 @@ -43,6 +43,8 @@
     2.4    }
     2.5  
     2.6    val empty = new Markup_Tree(Branches.empty)
     2.7 +
     2.8 +  type Select[A] = PartialFunction[Text.Info[Any], A]
     2.9  }
    2.10  
    2.11  
    2.12 @@ -89,7 +91,7 @@
    2.13    private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
    2.14      Branches.overlapping(range, branches).toStream
    2.15  
    2.16 -  def select[A](root_range: Text.Range)(result: PartialFunction[Text.Info[Any], A])
    2.17 +  def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
    2.18      : Stream[Text.Info[Option[A]]] =
    2.19    {
    2.20      def stream(
     3.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 22:28:58 2010 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/document_model.scala	Tue Sep 07 23:06:52 2010 +0200
     3.3 @@ -272,7 +272,7 @@
     3.4            handler.handleToken(line_segment, style, offset, length, context)
     3.5  
     3.6          val syntax = session.current_syntax()
     3.7 -        val token_markup: PartialFunction[Text.Info[Any], Byte] =
     3.8 +        val token_markup: Markup_Tree.Select[Byte] =
     3.9          {
    3.10            case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
    3.11            if syntax.keyword_kind(name).isDefined =>
     4.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 22:28:58 2010 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 23:06:52 2010 +0200
     4.3 @@ -13,11 +13,11 @@
     4.4  import scala.actors.Actor._
     4.5  
     4.6  import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
     4.7 -import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
     4.8 +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
     4.9  import javax.swing.{JPanel, ToolTipManager}
    4.10  import javax.swing.event.{CaretListener, CaretEvent}
    4.11  
    4.12 -import org.gjt.sp.jedit.{jEdit, GUIUtilities, OperatingSystem}
    4.13 +import org.gjt.sp.jedit.{jEdit, OperatingSystem}
    4.14  import org.gjt.sp.jedit.gui.RolloverButton
    4.15  import org.gjt.sp.jedit.options.GutterOptionPane
    4.16  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    4.17 @@ -26,75 +26,6 @@
    4.18  
    4.19  object Document_View
    4.20  {
    4.21 -  /* physical rendering */
    4.22 -
    4.23 -  val outdated_color = new Color(240, 240, 240)
    4.24 -  val unfinished_color = new Color(255, 228, 225)
    4.25 -
    4.26 -  val regular_color = new Color(192, 192, 192)
    4.27 -  val warning_color = new Color(255, 168, 0)
    4.28 -  val error_color = new Color(255, 80, 80)
    4.29 -  val bad_color = new Color(255, 204, 153, 100)
    4.30 -
    4.31 -  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
    4.32 -  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
    4.33 -
    4.34 -  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    4.35 -  {
    4.36 -    val state = snapshot.state(command)
    4.37 -    if (snapshot.is_outdated) Some(outdated_color)
    4.38 -    else
    4.39 -      Isar_Document.command_status(state.status) match {
    4.40 -        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    4.41 -        case Isar_Document.Unprocessed => Some(unfinished_color)
    4.42 -        case _ => None
    4.43 -      }
    4.44 -  }
    4.45 -
    4.46 -  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    4.47 -  {
    4.48 -    val state = snapshot.state(command)
    4.49 -    if (snapshot.is_outdated) None
    4.50 -    else
    4.51 -      Isar_Document.command_status(state.status) match {
    4.52 -        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    4.53 -        case Isar_Document.Unprocessed => Some(unfinished_color)
    4.54 -        case Isar_Document.Failed => Some(error_color)
    4.55 -        case _ => None
    4.56 -      }
    4.57 -  }
    4.58 -
    4.59 -
    4.60 -  /* markup selectors */
    4.61 -
    4.62 -  private val message_markup: PartialFunction[Text.Info[Any], Color] =
    4.63 -  {
    4.64 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    4.65 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    4.66 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    4.67 -  }
    4.68 -
    4.69 -  private val background_markup: PartialFunction[Text.Info[Any], Color] =
    4.70 -  {
    4.71 -    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    4.72 -  }
    4.73 -
    4.74 -  private val box_markup: PartialFunction[Text.Info[Any], Color] =
    4.75 -  {
    4.76 -    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
    4.77 -  }
    4.78 -
    4.79 -  private val tooltip_markup: PartialFunction[Text.Info[Any], String] =
    4.80 -  {
    4.81 -    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    4.82 -      Pretty.string_of(List(Pretty.block(body)), margin = 40)
    4.83 -    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
    4.84 -    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
    4.85 -    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
    4.86 -    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
    4.87 -  }
    4.88 -
    4.89 -
    4.90    /* document view of text area */
    4.91  
    4.92    private val key = new Object
    4.93 @@ -217,24 +148,17 @@
    4.94  
    4.95    /* subexpression highlighting */
    4.96  
    4.97 -  private val subexp_include =
    4.98 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
    4.99 -
   4.100 -  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
   4.101 +  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   4.102 +    : Option[(Text.Range, Color)] =
   4.103    {
   4.104 -    val subexp_markup: PartialFunction[Text.Info[Any], Text.Range] =
   4.105 -    {
   4.106 -      case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   4.107 -        snapshot.convert(range)
   4.108 -    }
   4.109      val offset = text_area.xyToOffset(x, y)
   4.110 -    snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup) match {
   4.111 -      case Text.Info(_, r) #:: _ => r
   4.112 +    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   4.113 +      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   4.114        case _ => None
   4.115      }
   4.116    }
   4.117  
   4.118 -  private var highlight_range: Option[Text.Range] = None
   4.119 +  private var highlight_range: Option[(Text.Range, Color)] = None
   4.120  
   4.121    private val focus_listener = new FocusAdapter {
   4.122      override def focusLost(e: FocusEvent) { highlight_range = None }
   4.123 @@ -246,10 +170,10 @@
   4.124        if (!model.buffer.isLoaded) highlight_range = None
   4.125        else
   4.126          Isabelle.swing_buffer_lock(model.buffer) {
   4.127 -          highlight_range.map(invalidate_line_range(_))
   4.128 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   4.129            highlight_range =
   4.130              if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
   4.131 -          highlight_range.map(invalidate_line_range(_))
   4.132 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   4.133          }
   4.134      }
   4.135    }
   4.136 @@ -279,7 +203,7 @@
   4.137                  (command, command_start) <- cmds if !command.is_ignored
   4.138                  val range = line_range.restrict(snapshot.convert(command.range + command_start))
   4.139                  r <- Isabelle.gfx_range(text_area, range)
   4.140 -                color <- Document_View.status_color(snapshot, command)
   4.141 +                color <- Isabelle_Markup.status_color(snapshot, command)
   4.142                } {
   4.143                  gfx.setColor(color)
   4.144                  gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   4.145 @@ -288,29 +212,29 @@
   4.146                // background color: markup
   4.147                for {
   4.148                  Text.Info(range, Some(color)) <-
   4.149 -                  snapshot.select_markup(line_range)(Document_View.background_markup).iterator
   4.150 +                  snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
   4.151                  r <- Isabelle.gfx_range(text_area, range)
   4.152                } {
   4.153                  gfx.setColor(color)
   4.154                  gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   4.155                }
   4.156  
   4.157 -              // subexpression highlighting -- potentially from other snapshot
   4.158 -              if (highlight_range.isDefined) {
   4.159 -                if (line_range.overlaps(highlight_range.get)) {
   4.160 -                  Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
   4.161 +              // sub-expression highlighting -- potentially from other snapshot
   4.162 +              highlight_range match {
   4.163 +                case Some((range, color)) if line_range.overlaps(range) =>
   4.164 +                  Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   4.165                      case None =>
   4.166                      case Some(r) =>
   4.167 -                      gfx.setColor(Color.black)
   4.168 +                      gfx.setColor(color)
   4.169                        gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
   4.170                    }
   4.171 -                }
   4.172 +                case _ =>
   4.173                }
   4.174  
   4.175                // boxed text
   4.176                for {
   4.177                  Text.Info(range, Some(color)) <-
   4.178 -                  snapshot.select_markup(line_range)(Document_View.box_markup).iterator
   4.179 +                  snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
   4.180                  r <- Isabelle.gfx_range(text_area, range)
   4.181                } {
   4.182                  gfx.setColor(color)
   4.183 @@ -320,7 +244,7 @@
   4.184                // squiggly underline
   4.185                for {
   4.186                  Text.Info(range, Some(color)) <-
   4.187 -                  snapshot.select_markup(line_range)(Document_View.message_markup).iterator
   4.188 +                  snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   4.189                  if color != null
   4.190                  r <- Isabelle.gfx_range(text_area, range)
   4.191                } {
   4.192 @@ -344,7 +268,8 @@
   4.193        Isabelle.swing_buffer_lock(model.buffer) {
   4.194          val snapshot = model.snapshot()
   4.195          val offset = text_area.xyToOffset(x, y)
   4.196 -        snapshot.select_markup(Text.Range(offset, offset + 1))(Document_View.tooltip_markup) match {
   4.197 +        snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
   4.198 +        {
   4.199            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   4.200            case _ => null
   4.201          }
   4.202 @@ -378,9 +303,9 @@
   4.203                val states = cmds.map(p => snapshot.state(p._1)).toStream
   4.204                val opt_icon =
   4.205                  if (states.exists(_.results.exists(p => Isar_Document.is_error(p._2))))
   4.206 -                  Some(Document_View.error_icon)
   4.207 +                  Some(Isabelle_Markup.error_icon)
   4.208                  else if (states.exists(_.results.exists(p => Isar_Document.is_warning(p._2))))
   4.209 -                  Some(Document_View.warning_icon)
   4.210 +                  Some(Isabelle_Markup.warning_icon)
   4.211                  else None
   4.212                opt_icon match {
   4.213                  case Some(icon) if icon.getIconWidth > 0 && icon.getIconHeight > 0 =>
   4.214 @@ -465,7 +390,7 @@
   4.215              val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
   4.216              val y = line_to_y(line1)
   4.217              val height = HEIGHT * (line2 - line1)
   4.218 -            color <- Document_View.overview_color(snapshot, command)
   4.219 +            color <- Isabelle_Markup.overview_color(snapshot, command)
   4.220            } {
   4.221              gfx.setColor(color)
   4.222              gfx.fillRect(0, y, getWidth - 1, height)
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Tue Sep 07 23:06:52 2010 +0200
     5.3 @@ -0,0 +1,98 @@
     5.4 +/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Isabelle specific physical rendering and markup selection.
     5.8 +*/
     5.9 +
    5.10 +package isabelle.jedit
    5.11 +
    5.12 +
    5.13 +import isabelle._
    5.14 +
    5.15 +import java.awt.Color
    5.16 +
    5.17 +import org.gjt.sp.jedit.GUIUtilities
    5.18 +
    5.19 +
    5.20 +object Isabelle_Markup
    5.21 +{
    5.22 +  /* physical rendering */
    5.23 +
    5.24 +  val outdated_color = new Color(240, 240, 240)
    5.25 +  val unfinished_color = new Color(255, 228, 225)
    5.26 +
    5.27 +  val regular_color = new Color(192, 192, 192)
    5.28 +  val warning_color = new Color(255, 168, 0)
    5.29 +  val error_color = new Color(255, 80, 80)
    5.30 +  val bad_color = new Color(255, 204, 153, 100)
    5.31 +
    5.32 +  val warning_icon = GUIUtilities.loadIcon("16x16/status/dialog-warning.png")
    5.33 +  val error_icon = GUIUtilities.loadIcon("16x16/status/dialog-error.png")
    5.34 +
    5.35 +
    5.36 +  /* command status */
    5.37 +
    5.38 +  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    5.39 +  {
    5.40 +    val state = snapshot.state(command)
    5.41 +    if (snapshot.is_outdated) Some(outdated_color)
    5.42 +    else
    5.43 +      Isar_Document.command_status(state.status) match {
    5.44 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    5.45 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    5.46 +        case _ => None
    5.47 +      }
    5.48 +  }
    5.49 +
    5.50 +  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    5.51 +  {
    5.52 +    val state = snapshot.state(command)
    5.53 +    if (snapshot.is_outdated) None
    5.54 +    else
    5.55 +      Isar_Document.command_status(state.status) match {
    5.56 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    5.57 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    5.58 +        case Isar_Document.Failed => Some(error_color)
    5.59 +        case _ => None
    5.60 +      }
    5.61 +  }
    5.62 +
    5.63 +
    5.64 +  /* markup selectors */
    5.65 +
    5.66 +  private val subexp_include =
    5.67 +    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
    5.68 +
    5.69 +  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
    5.70 +  {
    5.71 +    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
    5.72 +      (range, Color.black)
    5.73 +  }
    5.74 +
    5.75 +  val message: Markup_Tree.Select[Color] =
    5.76 +  {
    5.77 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    5.78 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    5.79 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    5.80 +  }
    5.81 +
    5.82 +  val background: Markup_Tree.Select[Color] =
    5.83 +  {
    5.84 +    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    5.85 +  }
    5.86 +
    5.87 +  val box: Markup_Tree.Select[Color] =
    5.88 +  {
    5.89 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
    5.90 +  }
    5.91 +
    5.92 +  val tooltip: Markup_Tree.Select[String] =
    5.93 +  {
    5.94 +    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
    5.95 +      Pretty.string_of(List(Pretty.block(body)), margin = 40)
    5.96 +    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
    5.97 +    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
    5.98 +    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
    5.99 +    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
   5.100 +  }
   5.101 +}