merged
authorwenzelm
Fri Sep 14 21:23:06 2012 +0200 (2012-09-14)
changeset 49373ab677b04cbf4
parent 49372 c62165188971
parent 49360 37c1297aa562
child 49374 b08c6312782b
merged
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 14 12:09:27 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Fri Sep 14 21:23:06 2012 +0200
     1.3 @@ -245,7 +245,7 @@
     1.4        if mode = Auto_Try then
     1.5          Unsynchronized.change state_ref o Proof.goal_message o K
     1.6          o Pretty.chunks o cons (Pretty.str "") o single
     1.7 -        o Pretty.mark Isabelle_Markup.hilite
     1.8 +        o Pretty.mark Isabelle_Markup.intensify
     1.9        else
    1.10          print o Pretty.string_of
    1.11      val pprint_a = pprint Output.urgent_message
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Sep 14 12:09:27 2012 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Fri Sep 14 21:23:06 2012 +0200
     2.3 @@ -137,7 +137,7 @@
     2.4           |> outcome_code = someN
     2.5              ? Proof.goal_message (fn () =>
     2.6                    [Pretty.str "",
     2.7 -                   Pretty.mark Isabelle_Markup.hilite (Pretty.str (message ()))]
     2.8 +                   Pretty.mark Isabelle_Markup.intensify (Pretty.str (message ()))]
     2.9                    |> Pretty.chunks))
    2.10        end
    2.11      else if blocking then
     3.1 --- a/src/HOL/Tools/try0.ML	Fri Sep 14 12:09:27 2012 +0200
     3.2 +++ b/src/HOL/Tools/try0.ML	Fri Sep 14 21:23:06 2012 +0200
     3.3 @@ -146,7 +146,7 @@
     3.4          (true, (s, st |> (if mode = Auto_Try then
     3.5                              Proof.goal_message
     3.6                                  (fn () => Pretty.chunks [Pretty.str "",
     3.7 -                                          Pretty.markup Isabelle_Markup.hilite
     3.8 +                                          Pretty.markup Isabelle_Markup.intensify
     3.9                                                          [Pretty.str message]])
    3.10                            else
    3.11                              tap (fn _ => Output.urgent_message message))))
     4.1 --- a/src/Pure/General/name_space.ML	Fri Sep 14 12:09:27 2012 +0200
     4.2 +++ b/src/Pure/General/name_space.ML	Fri Sep 14 21:23:06 2012 +0200
     4.3 @@ -133,7 +133,7 @@
     4.4  
     4.5  fun markup (Name_Space {kind, entries, ...}) name =
     4.6    (case Symtab.lookup entries name of
     4.7 -    NONE => Isabelle_Markup.hilite
     4.8 +    NONE => Isabelle_Markup.intensify
     4.9    | SOME (_, entry) => entry_markup false kind (name, entry));
    4.10  
    4.11  fun is_concealed space name = #concealed (the_entry space name);
     5.1 --- a/src/Pure/PIDE/command.scala	Fri Sep 14 12:09:27 2012 +0200
     5.2 +++ b/src/Pure/PIDE/command.scala	Fri Sep 14 21:23:06 2012 +0200
     5.3 @@ -102,6 +102,8 @@
     5.4    def unparsed(source: String): Command =
     5.5      Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
     5.6  
     5.7 +  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
     5.8 +
     5.9  
    5.10    /* perspective */
    5.11  
     6.1 --- a/src/Pure/PIDE/isabelle_markup.ML	Fri Sep 14 12:09:27 2012 +0200
     6.2 +++ b/src/Pure/PIDE/isabelle_markup.ML	Fri Sep 14 21:23:06 2012 +0200
     6.3 @@ -84,7 +84,7 @@
     6.4    val stateN: string val state: Markup.T
     6.5    val subgoalN: string val subgoal: Markup.T
     6.6    val sendbackN: string val sendback: Markup.T
     6.7 -  val hiliteN: string val hilite: Markup.T
     6.8 +  val intensifyN: string val intensify: Markup.T
     6.9    val taskN: string
    6.10    val acceptedN: string val accepted: Markup.T
    6.11    val forkedN: string val forked: Markup.T
    6.12 @@ -264,7 +264,7 @@
    6.13  val (stateN, state) = markup_elem "state";
    6.14  val (subgoalN, subgoal) = markup_elem "subgoal";
    6.15  val (sendbackN, sendback) = markup_elem "sendback";
    6.16 -val (hiliteN, hilite) = markup_elem "hilite";
    6.17 +val (intensifyN, intensify) = markup_elem "intensify";
    6.18  
    6.19  
    6.20  (* command status *)
     7.1 --- a/src/Pure/PIDE/isabelle_markup.scala	Fri Sep 14 12:09:27 2012 +0200
     7.2 +++ b/src/Pure/PIDE/isabelle_markup.scala	Fri Sep 14 21:23:06 2012 +0200
     7.3 @@ -185,7 +185,7 @@
     7.4    val STATE = "state"
     7.5    val SUBGOAL = "subgoal"
     7.6    val SENDBACK = "sendback"
     7.7 -  val HILITE = "hilite"
     7.8 +  val INTENSIFY = "intensify"
     7.9  
    7.10  
    7.11    /* command status */
     8.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 14 12:09:27 2012 +0200
     8.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 14 21:23:06 2012 +0200
     8.3 @@ -41,7 +41,7 @@
     8.4            if null ts then Markup.no_output
     8.5            else if name = Isabelle_Markup.stateN then (special "O" ^ "\n", "\n" ^ special "P")
     8.6            else if name = Isabelle_Markup.sendbackN then (special "W", special "X")
     8.7 -          else if name = Isabelle_Markup.hiliteN then (special "0", special "1")
     8.8 +          else if name = Isabelle_Markup.intensifyN then (special "0", special "1")
     8.9            else if name = Isabelle_Markup.tfreeN then (special "C", special "A")
    8.10            else if name = Isabelle_Markup.tvarN then (special "D", special "A")
    8.11            else if name = Isabelle_Markup.freeN then (special "E", special "A")
     9.1 --- a/src/Pure/Syntax/syntax_phases.ML	Fri Sep 14 12:09:27 2012 +0200
     9.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Fri Sep 14 21:23:06 2012 +0200
     9.3 @@ -586,7 +586,7 @@
     9.4      val m =
     9.5        if Variable.is_fixed ctxt x orelse Syntax.is_pretty_global ctxt
     9.6        then Isabelle_Markup.fixed x
     9.7 -      else Isabelle_Markup.hilite;
     9.8 +      else Isabelle_Markup.intensify;
     9.9    in
    9.10      if can Name.dest_skolem x
    9.11      then ([m, Isabelle_Markup.skolem], Variable.revert_fixed ctxt x)
    10.1 --- a/src/Tools/jEdit/etc/isabelle-jedit.css	Fri Sep 14 12:09:27 2012 +0200
    10.2 +++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Fri Sep 14 21:23:06 2012 +0200
    10.3 @@ -9,7 +9,7 @@
    10.4  
    10.5  .report { display: none; }
    10.6  
    10.7 -.hilite { background-color: #FFCC66; }
    10.8 +.intensify { background-color: #FFCC66; }
    10.9  
   10.10  .keyword { font-weight: bold; color: #009966; }
   10.11  .operator { font-weight: bold; }
    11.1 --- a/src/Tools/jEdit/etc/options	Fri Sep 14 12:09:27 2012 +0200
    11.2 +++ b/src/Tools/jEdit/etc/options	Fri Sep 14 21:23:06 2012 +0200
    11.3 @@ -21,32 +21,33 @@
    11.4  
    11.5  section "Rendering of Document Content"
    11.6  
    11.7 -option color_outdated : string = "EEE3E3FF"
    11.8 -option color_unprocessed : string = "FFA0A0FF"
    11.9 -option color_unprocessed1 : string = "FFA0A032"
   11.10 -option color_running : string = "610061FF"
   11.11 -option color_running1 : string = "61006164"
   11.12 -option color_light : string = "F0F0F0FF"
   11.13 -option color_writeln : string = "C0C0C0FF"
   11.14 -option color_warning : string = "FF8C00FF"
   11.15 -option color_error : string = "B22222FF"
   11.16 -option color_error1 : string = "B2222232"
   11.17 -option color_bad : string = "FF6A6A64"
   11.18 -option color_hilite : string = "FFCC6664"
   11.19 -option color_quoted : string = "8B8B8B19"
   11.20 -option color_subexp : string = "50505032"
   11.21 -option color_hyperlink : string = "000000FF"
   11.22 -option color_keyword1 : string = "006699FF"
   11.23 -option color_keyword2 : string = "009966FF"
   11.24 +option outdated_color : string = "EEE3E3FF"
   11.25 +option unprocessed_color : string = "FFA0A0FF"
   11.26 +option unprocessed1_color : string = "FFA0A032"
   11.27 +option running_color : string = "610061FF"
   11.28 +option running1_color : string = "61006164"
   11.29 +option light_color : string = "F0F0F0FF"
   11.30 +option writeln_color : string = "C0C0C0FF"
   11.31 +option warning_color : string = "FF8C00FF"
   11.32 +option error_color : string = "B22222FF"
   11.33 +option error1_color : string = "B2222232"
   11.34 +option bad_color : string = "FF6A6A64"
   11.35 +option intensify_color : string = "FFCC6664"
   11.36 +option quoted_color : string = "8B8B8B19"
   11.37 +option highlight_color : string = "50505032"
   11.38 +option hyperlink_color : string = "000000FF"
   11.39 +option keyword1_color : string = "006699FF"
   11.40 +option keyword2_color : string = "009966FF"
   11.41  
   11.42 -option color_variable_free : string = "0000FFFF"
   11.43 -option color_variable_type : string = "A020F0FF"
   11.44 -option color_variable_skolem : string = "D2691EFF"
   11.45 -option color_variable_bound : string = "008000FF"
   11.46 -option color_variable_schematic : string = "00009BFF"
   11.47 -option color_inner_quoted : string = "D2691EFF"
   11.48 -option color_inner_comment : string = "8B0000FF"
   11.49 -option color_inner_numeral : string = "FF0000FF"
   11.50 -option color_antiquotation : string = "0000FFFF"
   11.51 -option color_dynamic : string = "7BA428FF"
   11.52 +option tfree_color : string = "A020F0FF"
   11.53 +option tvar_color : string = "A020F0FF"
   11.54 +option free_color : string = "0000FFFF"
   11.55 +option skolem_color : string = "D2691EFF"
   11.56 +option bound_color : string = "008000FF"
   11.57 +option var_color : string = "00009BFF"
   11.58 +option inner_numeral_color : string = "FF0000FF"
   11.59 +option inner_quoted_color : string = "D2691EFF"
   11.60 +option inner_comment_color : string = "8B0000FF"
   11.61 +option antiquotation_color : string = "0000FFFF"
   11.62 +option dynamic_color : string = "7BA428FF"
   11.63  
    12.1 --- a/src/Tools/jEdit/src/Isabelle.props	Fri Sep 14 12:09:27 2012 +0200
    12.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Fri Sep 14 21:23:06 2012 +0200
    12.3 @@ -20,9 +20,11 @@
    12.4  plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 0.8
    12.5  
    12.6  #options
    12.7 -plugin.isabelle.jedit.Plugin.option-pane=isabelle
    12.8 -options.isabelle.label=Isabelle
    12.9 -options.isabelle.code=new isabelle.jedit.Isabelle_Options();
   12.10 +plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
   12.11 +options.isabelle-general.label=General
   12.12 +options.isabelle-general.code=new isabelle.jedit.Isabelle_Options1();
   12.13 +options.isabelle-rendering.label=Rendering
   12.14 +options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
   12.15  
   12.16  #actions
   12.17  isabelle.check-buffer.label=Commence full proof checking of current buffer
    13.1 --- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 14 12:09:27 2012 +0200
    13.2 +++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 14 21:23:06 2012 +0200
    13.3 @@ -92,6 +92,24 @@
    13.4    }
    13.5  
    13.6  
    13.7 +
    13.8 +  /* point range */
    13.9 +
   13.10 +  def point_range(offset: Text.Offset): Text.Range =
   13.11 +    Isabelle.buffer_lock(buffer) {
   13.12 +      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
   13.13 +      try {
   13.14 +        val c = text(offset)
   13.15 +        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
   13.16 +          Text.Range(offset, offset + 2)
   13.17 +        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
   13.18 +          Text.Range(offset - 1, offset + 1)
   13.19 +        else Text.Range(offset, offset + 1)
   13.20 +      }
   13.21 +      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
   13.22 +    }
   13.23 +
   13.24 +
   13.25    /* pending text edits */
   13.26  
   13.27    private object pending_edits  // owned by Swing thread
    14.1 --- a/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 12:09:27 2012 +0200
    14.2 +++ b/src/Tools/jEdit/src/document_view.scala	Fri Sep 14 21:23:06 2012 +0200
    14.3 @@ -19,7 +19,6 @@
    14.4  import java.awt.{Color, Graphics2D, Point}
    14.5  import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
    14.6    FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    14.7 -import javax.swing.{Popup, PopupFactory, SwingUtilities, BorderFactory}
    14.8  import javax.swing.event.{CaretListener, CaretEvent}
    14.9  
   14.10  import org.gjt.sp.util.Log
   14.11 @@ -143,77 +142,56 @@
   14.12    }
   14.13  
   14.14  
   14.15 -  /* HTML popups */
   14.16 +  /* active areas within the text */
   14.17  
   14.18 -  private var html_popup: Option[Popup] = None
   14.19 +  private class Active_Area[A](
   14.20 +    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
   14.21 +  {
   14.22 +    private var the_info: Option[Text.Info[A]] = None
   14.23  
   14.24 -  private def exit_popup() { html_popup.map(_.hide) }
   14.25 +    def info: Option[Text.Info[A]] = the_info
   14.26  
   14.27 -  private val html_panel =
   14.28 -    new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   14.29 -  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
   14.30 +    def update(new_info: Option[Text.Info[A]])
   14.31 +    {
   14.32 +      val old_info = the_info
   14.33 +      if (new_info != old_info) {
   14.34 +        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
   14.35 +          invalidate_range(range)
   14.36 +        the_info = new_info
   14.37 +      }
   14.38 +    }
   14.39  
   14.40 -  private def html_panel_resize()
   14.41 -  {
   14.42 -    Swing_Thread.now {
   14.43 -      html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   14.44 -    }
   14.45 +    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
   14.46 +    { update(rendering(r)(range)) }
   14.47 +
   14.48 +    def reset { update(None) }
   14.49    }
   14.50  
   14.51 -  private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
   14.52 -  {
   14.53 -    exit_popup()
   14.54 -/* FIXME broken
   14.55 -    val offset = text_area.xyToOffset(x, y)
   14.56 -    val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
   14.57 -
   14.58 -    // FIXME snapshot.cumulate
   14.59 -    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Rendering.popup) match {
   14.60 -      case Text.Info(_, Some(msg)) #:: _ =>
   14.61 -        val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
   14.62 -        html_panel.render_sync(List(msg))
   14.63 -        Thread.sleep(10)  // FIXME !?
   14.64 -        popup.show
   14.65 -        html_popup = Some(popup)
   14.66 -      case _ =>
   14.67 -    }
   14.68 -*/
   14.69 -  }
   14.70 -
   14.71 -
   14.72 -  /* subexpression highlighting and hyperlinks */
   14.73 -
   14.74 -  @volatile private var _highlight_range: Option[Text.Info[Color]] = None
   14.75 -  def highlight_range(): Option[Text.Info[Color]] = _highlight_range
   14.76 -
   14.77 -  @volatile private var _hyperlink_range: Option[Text.Info[Hyperlink]] = None
   14.78 -  def hyperlink_range(): Option[Text.Info[Hyperlink]] = _hyperlink_range
   14.79 +  // owned by Swing thread
   14.80  
   14.81    private var control: Boolean = false
   14.82  
   14.83 -  private def exit_control()
   14.84 -  {
   14.85 -    exit_popup()
   14.86 -    _highlight_range = None
   14.87 -    _hyperlink_range = None
   14.88 -  }
   14.89 +  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
   14.90 +  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
   14.91 +
   14.92 +  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
   14.93 +  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
   14.94 +
   14.95 +  private val active_areas = List(highlight_area, hyperlink_area)
   14.96 +  private def active_reset(): Unit = active_areas.foreach(_.reset)
   14.97  
   14.98    private val focus_listener = new FocusAdapter {
   14.99 -    override def focusLost(e: FocusEvent) {
  14.100 -      // FIXME exit_control !?
  14.101 -      _highlight_range = None
  14.102 -      _hyperlink_range = None
  14.103 -    }
  14.104 +    override def focusLost(e: FocusEvent) { active_reset() }
  14.105    }
  14.106  
  14.107    private val window_listener = new WindowAdapter {
  14.108 -    override def windowIconified(e: WindowEvent) { exit_control() }
  14.109 -    override def windowDeactivated(e: WindowEvent) { exit_control() }
  14.110 +    override def windowIconified(e: WindowEvent) { active_reset() }
  14.111 +    override def windowDeactivated(e: WindowEvent) { active_reset() }
  14.112    }
  14.113  
  14.114    private val mouse_listener = new MouseAdapter {
  14.115      override def mouseClicked(e: MouseEvent) {
  14.116 -      hyperlink_range match {
  14.117 +      hyperlink_area.info match {
  14.118          case Some(Text.Info(range, link)) => link.follow(text_area.getView)
  14.119          case None =>
  14.120        }
  14.121 @@ -222,36 +200,15 @@
  14.122  
  14.123    private val mouse_motion_listener = new MouseMotionAdapter {
  14.124      override def mouseMoved(e: MouseEvent) {
  14.125 -      Swing_Thread.assert()
  14.126 -
  14.127        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
  14.128 -      val x = e.getX()
  14.129 -      val y = e.getY()
  14.130 -
  14.131 -      if (!model.buffer.isLoaded) exit_control()
  14.132 -      else
  14.133 +      if (control && model.buffer.isLoaded) {
  14.134          Isabelle.buffer_lock(model.buffer) {
  14.135 -          val snapshot = model.snapshot()
  14.136 -
  14.137 -          if (control) init_popup(snapshot, x, y)
  14.138 -
  14.139 -          def update_range[A](
  14.140 -            rendering: (Document.Snapshot, Text.Range) => Option[Text.Info[A]],
  14.141 -            info: Option[Text.Info[A]]): Option[Text.Info[A]] =
  14.142 -          {
  14.143 -            for (Text.Info(range, _) <- info) invalidate_range(range)
  14.144 -            val new_info =
  14.145 -              if (control) {
  14.146 -                val offset = text_area.xyToOffset(x, y)
  14.147 -                rendering(snapshot, Text.Range(offset, offset + 1))
  14.148 -              }
  14.149 -              else None
  14.150 -            for (Text.Info(range, _) <- info) invalidate_range(range)
  14.151 -            new_info
  14.152 -          }
  14.153 -          _highlight_range = update_range(Isabelle_Rendering.subexp, _highlight_range)
  14.154 -          _hyperlink_range = update_range(Isabelle_Rendering.hyperlink, _hyperlink_range)
  14.155 +          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
  14.156 +          val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
  14.157 +          active_areas.foreach(_.update_rendering(rendering, mouse_range))
  14.158          }
  14.159 +      }
  14.160 +      else active_reset()
  14.161      }
  14.162    }
  14.163  
  14.164 @@ -265,12 +222,12 @@
  14.165      override def getToolTipText(x: Int, y: Int): String =
  14.166      {
  14.167        robust_body(null: String) {
  14.168 -        val snapshot = model.snapshot()
  14.169 +        val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
  14.170          val offset = text_area.xyToOffset(x, y)
  14.171          val range = Text.Range(offset, offset + 1)
  14.172          val tip =
  14.173 -          if (control) Isabelle_Rendering.tooltip(snapshot, range)
  14.174 -          else Isabelle_Rendering.tooltip_message(snapshot, range)
  14.175 +          if (control) rendering.tooltip(range)
  14.176 +          else rendering.tooltip_message(range)
  14.177          tip.map(Isabelle.tooltip(_)) getOrElse null
  14.178        }
  14.179      }
  14.180 @@ -292,13 +249,14 @@
  14.181  
  14.182          if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
  14.183            Isabelle.buffer_lock(model.buffer) {
  14.184 -            val snapshot = model.snapshot()
  14.185 +            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
  14.186 +
  14.187              for (i <- 0 until physical_lines.length) {
  14.188                if (physical_lines(i) != -1) {
  14.189                  val line_range = proper_line_range(start(i), end(i))
  14.190  
  14.191                  // gutter icons
  14.192 -                Isabelle_Rendering.gutter_message(snapshot, line_range) match {
  14.193 +                rendering.gutter_message(line_range) match {
  14.194                    case Some(icon) =>
  14.195                      val x0 = (FOLD_MARKER_SIZE + width - border_width - icon.getIconWidth) max 10
  14.196                      val y0 = y + i * line_height + (((line_height - icon.getIconHeight) / 2) max 0)
  14.197 @@ -314,32 +272,8 @@
  14.198    }
  14.199  
  14.200  
  14.201 -  /* caret range */
  14.202 -
  14.203 -  def caret_range(): Text.Range =
  14.204 -    Isabelle.buffer_lock(model.buffer) {
  14.205 -      def text(i: Text.Offset): Char = model.buffer.getText(i, 1).charAt(0)
  14.206 -      val caret = text_area.getCaretPosition
  14.207 -      try {
  14.208 -        val c = text(caret)
  14.209 -        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(caret + 1)))
  14.210 -          Text.Range(caret, caret + 2)
  14.211 -        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(caret - 1)))
  14.212 -          Text.Range(caret - 1, caret + 1)
  14.213 -        else Text.Range(caret, caret + 1)
  14.214 -      }
  14.215 -      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(caret, caret + 1) }
  14.216 -    }
  14.217 -
  14.218 -
  14.219    /* caret handling */
  14.220  
  14.221 -  def selected_command(): Option[Command] =
  14.222 -  {
  14.223 -    Swing_Thread.require()
  14.224 -    model.snapshot().node.command_at(text_area.getCaretPosition).map(_._1)
  14.225 -  }
  14.226 -
  14.227    private val delay_caret_update =
  14.228      Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
  14.229        session.caret_focus.event(Session.Caret_Focus)
  14.230 @@ -406,8 +340,6 @@
  14.231              }
  14.232            }
  14.233  
  14.234 -        case Session.Global_Settings => html_panel_resize()
  14.235 -
  14.236          case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
  14.237        }
  14.238      }
  14.239 @@ -431,7 +363,6 @@
  14.240      text_area.addLeftOfScrollBar(overview)
  14.241      session.raw_edits += main_actor
  14.242      session.commands_changed += main_actor
  14.243 -    session.global_settings += main_actor
  14.244    }
  14.245  
  14.246    private def deactivate()
  14.247 @@ -439,7 +370,6 @@
  14.248      val painter = text_area.getPainter
  14.249      session.raw_edits -= main_actor
  14.250      session.commands_changed -= main_actor
  14.251 -    session.global_settings -= main_actor
  14.252      text_area.removeFocusListener(focus_listener)
  14.253      text_area.getView.removeWindowListener(window_listener)
  14.254      painter.removeMouseMotionListener(mouse_motion_listener)
  14.255 @@ -450,6 +380,5 @@
  14.256      text_area_painter.deactivate()
  14.257      painter.removeExtension(tooltip_painter)
  14.258      painter.removeExtension(update_perspective)
  14.259 -    exit_popup()
  14.260    }
  14.261  }
    15.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Fri Sep 14 12:09:27 2012 +0200
    15.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Fri Sep 14 21:23:06 2012 +0200
    15.3 @@ -12,25 +12,9 @@
    15.4  import org.gjt.sp.jedit.{jEdit, AbstractOptionPane}
    15.5  
    15.6  
    15.7 -class Isabelle_Options extends AbstractOptionPane("isabelle")
    15.8 +abstract class Isabelle_Options(name: String) extends AbstractOptionPane(name)
    15.9  {
   15.10 -  // FIXME avoid hard-wired stuff
   15.11 -  private val relevant_options =
   15.12 -    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
   15.13 -      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
   15.14 -      "editor_input_delay", "editor_output_delay", "editor_update_delay")
   15.15 -
   15.16 -  relevant_options.foreach(Isabelle.options.value.check_name _)
   15.17 -
   15.18 -  private val predefined =
   15.19 -    Isabelle_Logic.logic_selector(false) ::
   15.20 -      (for {
   15.21 -        (name, opt) <- Isabelle.options.value.options.toList
   15.22 -        // FIXME avoid hard-wired stuff
   15.23 -        if (name.startsWith("color_") && opt.section == "Rendering of Document Content")
   15.24 -      } yield Isabelle.options.make_color_component(opt))
   15.25 -
   15.26 -  private val components = Isabelle.options.make_components(predefined, relevant_options)
   15.27 +  protected val components: List[(String, List[Option_Component])]
   15.28  
   15.29    override def _init()
   15.30    {
   15.31 @@ -51,3 +35,34 @@
   15.32      for ((_, cs) <- components) cs.foreach(_.save())
   15.33    }
   15.34  }
   15.35 +
   15.36 +
   15.37 +class Isabelle_Options1 extends Isabelle_Options("isabelle-general")
   15.38 +{
   15.39 +  // FIXME avoid hard-wired stuff
   15.40 +  private val relevant_options =
   15.41 +    Set("jedit_logic", "jedit_auto_start", "jedit_font_scale", "jedit_tooltip_font_size",
   15.42 +      "jedit_tooltip_margin", "jedit_tooltip_dismiss_delay", "editor_load_delay",
   15.43 +      "editor_input_delay", "editor_output_delay", "editor_update_delay")
   15.44 +
   15.45 +  relevant_options.foreach(Isabelle.options.value.check_name _)
   15.46 +
   15.47 +  protected val components =
   15.48 +    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
   15.49 +}
   15.50 +
   15.51 +
   15.52 +class Isabelle_Options2 extends Isabelle_Options("isabelle-rendering")
   15.53 +{
   15.54 +  // FIXME avoid hard-wired stuff
   15.55 +  private val predefined =
   15.56 +    (for {
   15.57 +      (name, opt) <- Isabelle.options.value.options.toList
   15.58 +      if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
   15.59 +    } yield Isabelle.options.make_color_component(opt))
   15.60 +
   15.61 +  assert(!predefined.isEmpty)
   15.62 +
   15.63 +  protected val components = Isabelle.options.make_components(predefined, _ => false)
   15.64 +}
   15.65 +
    16.1 --- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 12:09:27 2012 +0200
    16.2 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 14 21:23:06 2012 +0200
    16.3 @@ -20,326 +20,22 @@
    16.4  
    16.5  object Isabelle_Rendering
    16.6  {
    16.7 -  /* physical rendering */
    16.8 +  def apply(snapshot: Document.Snapshot, options: Options): Isabelle_Rendering =
    16.9 +    new Isabelle_Rendering(snapshot, options)
   16.10  
   16.11 -  def color_value(s: String): Color = Color_Value(Isabelle.options.value.string(s))
   16.12 +
   16.13 +  /* physical rendering */
   16.14  
   16.15    private val writeln_pri = 1
   16.16    private val warning_pri = 2
   16.17    private val legacy_pri = 3
   16.18    private val error_pri = 4
   16.19  
   16.20 -
   16.21 -  /* command overview */
   16.22 -
   16.23 -  def overview_color(snapshot: Document.Snapshot, range: Text.Range): Option[Color] =
   16.24 -  {
   16.25 -    if (snapshot.is_outdated) None
   16.26 -    else {
   16.27 -      val results =
   16.28 -        snapshot.cumulate_markup[(Protocol.Status, Int)](
   16.29 -          range, (Protocol.Status.init, 0),
   16.30 -          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
   16.31 -          {
   16.32 -            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
   16.33 -              if (markup.name == Isabelle_Markup.WARNING) (status, pri max warning_pri)
   16.34 -              else if (markup.name == Isabelle_Markup.ERROR) (status, pri max error_pri)
   16.35 -              else (Protocol.command_status(status, markup), pri)
   16.36 -          })
   16.37 -      if (results.isEmpty) None
   16.38 -      else {
   16.39 -        val (status, pri) =
   16.40 -          ((Protocol.Status.init, 0) /: results) {
   16.41 -            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
   16.42 -
   16.43 -        if (pri == warning_pri) Some(color_value("color_warning"))
   16.44 -        else if (pri == error_pri) Some(color_value("color_error"))
   16.45 -        else if (status.is_unprocessed) Some(color_value("color_unprocessed"))
   16.46 -        else if (status.is_running) Some(color_value("color_running"))
   16.47 -        else if (status.is_failed) Some(color_value("color_error"))
   16.48 -        else None
   16.49 -      }
   16.50 -    }
   16.51 -  }
   16.52 -
   16.53 -
   16.54 -  /* markup selectors */
   16.55 -
   16.56 -  private val subexp_include =
   16.57 -    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
   16.58 -      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
   16.59 -      Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
   16.60 -      Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
   16.61 -      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
   16.62 -
   16.63 -  def subexp(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Color]] =
   16.64 -  {
   16.65 -    snapshot.select_markup(range, Some(subexp_include),
   16.66 -        {
   16.67 -          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   16.68 -            Text.Info(snapshot.convert(info_range), color_value("color_subexp"))
   16.69 -        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
   16.70 -  }
   16.71 -
   16.72 -
   16.73 -  private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
   16.74 -
   16.75 -  def hyperlink(snapshot: Document.Snapshot, range: Text.Range): Option[Text.Info[Hyperlink]] =
   16.76 -  {
   16.77 -    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
   16.78 -        {
   16.79 -          case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
   16.80 -          if Path.is_ok(name) =>
   16.81 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   16.82 -            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   16.83 -
   16.84 -          case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
   16.85 -          if (props.find(
   16.86 -            { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
   16.87 -              case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
   16.88 -              case _ => false }).isEmpty) =>
   16.89 -
   16.90 -            props match {
   16.91 -              case Position.Line_File(line, name) if Path.is_ok(name) =>
   16.92 -                Isabelle_System.source_file(Path.explode(name)) match {
   16.93 -                  case Some(path) =>
   16.94 -                    val jedit_file = Isabelle_System.platform_path(path)
   16.95 -                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
   16.96 -                  case None => links
   16.97 -                }
   16.98 -
   16.99 -              case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
  16.100 -                snapshot.state.find_command(snapshot.version, id) match {
  16.101 -                  case Some((node, command)) =>
  16.102 -                    val sources =
  16.103 -                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
  16.104 -                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
  16.105 -                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
  16.106 -                    Text.Info(snapshot.convert(info_range),
  16.107 -                      Hyperlink(command.node_name.node, line, column)) :: links
  16.108 -                  case None => links
  16.109 -                }
  16.110 -
  16.111 -              case _ => links
  16.112 -            }
  16.113 -        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
  16.114 -  }
  16.115 -
  16.116 -
  16.117 -  private def tooltip_text(msg: XML.Tree): String =
  16.118 -    Pretty.string_of(List(msg), margin = Isabelle.options.int("jedit_tooltip_margin"))
  16.119 -
  16.120 -  def tooltip_message(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
  16.121 -  {
  16.122 -    val msgs =
  16.123 -      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
  16.124 -        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
  16.125 -          Isabelle_Markup.BAD)),
  16.126 -        {
  16.127 -          case (msgs, Text.Info(_, msg @
  16.128 -              XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
  16.129 -          if markup == Isabelle_Markup.WRITELN ||
  16.130 -              markup == Isabelle_Markup.WARNING ||
  16.131 -              markup == Isabelle_Markup.ERROR =>
  16.132 -            msgs + (serial -> tooltip_text(msg))
  16.133 -          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
  16.134 -          if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg))
  16.135 -        }).toList.flatMap(_.info)
  16.136 -    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
  16.137 -  }
  16.138 -
  16.139 -
  16.140 -  private val tooltips: Map[String, String] =
  16.141 -    Map(
  16.142 -      Isabelle_Markup.SORT -> "sort",
  16.143 -      Isabelle_Markup.TYP -> "type",
  16.144 -      Isabelle_Markup.TERM -> "term",
  16.145 -      Isabelle_Markup.PROP -> "proposition",
  16.146 -      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
  16.147 -      Isabelle_Markup.FREE -> "free variable",
  16.148 -      Isabelle_Markup.SKOLEM -> "skolem variable",
  16.149 -      Isabelle_Markup.BOUND -> "bound variable",
  16.150 -      Isabelle_Markup.VAR -> "schematic variable",
  16.151 -      Isabelle_Markup.TFREE -> "free type variable",
  16.152 -      Isabelle_Markup.TVAR -> "schematic type variable",
  16.153 -      Isabelle_Markup.ML_SOURCE -> "ML source",
  16.154 -      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
  16.155 -
  16.156 -  private val tooltip_elements =
  16.157 -    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
  16.158 -      Isabelle_Markup.PATH) ++ tooltips.keys
  16.159 -
  16.160 -  private def string_of_typing(kind: String, body: XML.Body): String =
  16.161 -    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
  16.162 -      margin = Isabelle.options.int("jedit_tooltip_margin"))
  16.163 -
  16.164 -  def tooltip(snapshot: Document.Snapshot, range: Text.Range): Option[String] =
  16.165 -  {
  16.166 -    def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
  16.167 -      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
  16.168 -
  16.169 -    val tips =
  16.170 -      snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
  16.171 -        range, Text.Info(range, Nil), Some(tooltip_elements),
  16.172 -        {
  16.173 -          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
  16.174 -            val kind1 = space_explode('_', kind).mkString(" ")
  16.175 -            add(prev, r, (true, kind1 + " " + quote(name)))
  16.176 -          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
  16.177 -          if Path.is_ok(name) =>
  16.178 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
  16.179 -            add(prev, r, (true, "file " + quote(jedit_file)))
  16.180 -          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
  16.181 -            add(prev, r, (true, string_of_typing("::", body)))
  16.182 -          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
  16.183 -            add(prev, r, (false, string_of_typing("ML:", body)))
  16.184 -          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
  16.185 -          if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
  16.186 -        }).toList.flatMap(_.info.info)
  16.187 -
  16.188 -    val all_tips =
  16.189 -      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
  16.190 -    if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
  16.191 -  }
  16.192 -
  16.193 -
  16.194    private val gutter_icons = Map(
  16.195      warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
  16.196      legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
  16.197      error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
  16.198  
  16.199 -  def gutter_message(snapshot: Document.Snapshot, range: Text.Range): Option[Icon] =
  16.200 -  {
  16.201 -    val results =
  16.202 -      snapshot.cumulate_markup[Int](range, 0,
  16.203 -        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  16.204 -        {
  16.205 -          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
  16.206 -            body match {
  16.207 -              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) => pri max legacy_pri
  16.208 -              case _ => pri max warning_pri
  16.209 -            }
  16.210 -          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
  16.211 -            pri max error_pri
  16.212 -        })
  16.213 -    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
  16.214 -    gutter_icons.get(pri)
  16.215 -  }
  16.216 -
  16.217 -
  16.218 -  def squiggly_underline(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
  16.219 -  {
  16.220 -    val squiggly_colors = Map(
  16.221 -      writeln_pri -> color_value("color_writeln"),
  16.222 -      warning_pri -> color_value("color_warning"),
  16.223 -      error_pri -> color_value("color_error"))
  16.224 -
  16.225 -    val results =
  16.226 -      snapshot.cumulate_markup[Int](range, 0,
  16.227 -        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  16.228 -        {
  16.229 -          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
  16.230 -            name match {
  16.231 -              case Isabelle_Markup.WRITELN => pri max writeln_pri
  16.232 -              case Isabelle_Markup.WARNING => pri max warning_pri
  16.233 -              case Isabelle_Markup.ERROR => pri max error_pri
  16.234 -              case _ => pri
  16.235 -            }
  16.236 -        })
  16.237 -    for {
  16.238 -      Text.Info(r, pri) <- results
  16.239 -      color <- squiggly_colors.get(pri)
  16.240 -    } yield Text.Info(r, color)
  16.241 -  }
  16.242 -
  16.243 -
  16.244 -  def background1(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
  16.245 -  {
  16.246 -    if (snapshot.is_outdated) Stream(Text.Info(range, color_value("color_outdated")))
  16.247 -    else
  16.248 -      for {
  16.249 -        Text.Info(r, result) <-
  16.250 -          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
  16.251 -            range, (Some(Protocol.Status.init), None),
  16.252 -            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.HILITE),
  16.253 -            {
  16.254 -              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
  16.255 -              if (Protocol.command_status_markup(markup.name)) =>
  16.256 -                (Some(Protocol.command_status(status, markup)), color)
  16.257 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
  16.258 -                (None, Some(color_value("color_bad")))
  16.259 -              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.HILITE, _), _))) =>
  16.260 -                (None, Some(color_value("color_hilite")))
  16.261 -            })
  16.262 -        color <-
  16.263 -          (result match {
  16.264 -            case (Some(status), opt_color) =>
  16.265 -              if (status.is_unprocessed) Some(color_value("color_unprocessed1"))
  16.266 -              else if (status.is_running) Some(color_value("color_running1"))
  16.267 -              else opt_color
  16.268 -            case (_, opt_color) => opt_color
  16.269 -          })
  16.270 -      } yield Text.Info(r, color)
  16.271 -  }
  16.272 -
  16.273 -
  16.274 -  def background2(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
  16.275 -    snapshot.select_markup(range,
  16.276 -      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
  16.277 -      {
  16.278 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) =>
  16.279 -          color_value("color_light")
  16.280 -      })
  16.281 -
  16.282 -
  16.283 -  def foreground(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Color]] =
  16.284 -    snapshot.select_markup(range,
  16.285 -      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
  16.286 -      {
  16.287 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) =>
  16.288 -          color_value("color_quoted")
  16.289 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) =>
  16.290 -          color_value("color_quoted")
  16.291 -        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) =>
  16.292 -          color_value("color_quoted")
  16.293 -      })
  16.294 -
  16.295 -
  16.296 -  def text_color(snapshot: Document.Snapshot, range: Text.Range, color: Color)
  16.297 -      : Stream[Text.Info[Color]] =
  16.298 -  {
  16.299 -    val text_colors: Map[String, Color] = Map(
  16.300 -      Isabelle_Markup.STRING -> Color.BLACK,
  16.301 -      Isabelle_Markup.ALTSTRING -> Color.BLACK,
  16.302 -      Isabelle_Markup.VERBATIM -> Color.BLACK,
  16.303 -      Isabelle_Markup.LITERAL -> color_value("color_keyword1"),
  16.304 -      Isabelle_Markup.DELIMITER -> Color.BLACK,
  16.305 -      Isabelle_Markup.TFREE -> color_value("color_variable_type"),
  16.306 -      Isabelle_Markup.TVAR -> color_value("color_variable_type"),
  16.307 -      Isabelle_Markup.FREE -> color_value("color_variable_free"),
  16.308 -      Isabelle_Markup.SKOLEM -> color_value("color_variable_skolem"),
  16.309 -      Isabelle_Markup.BOUND -> color_value("color_variable_bound"),
  16.310 -      Isabelle_Markup.VAR -> color_value("color_variable_schematic"),
  16.311 -      Isabelle_Markup.INNER_STRING -> color_value("color_inner_quoted"),
  16.312 -      Isabelle_Markup.INNER_COMMENT -> color_value("color_inner_comment"),
  16.313 -      Isabelle_Markup.DYNAMIC_FACT -> color_value("color_dynamic"),
  16.314 -      Isabelle_Markup.ML_KEYWORD -> color_value("color_keyword1"),
  16.315 -      Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
  16.316 -      Isabelle_Markup.ML_NUMERAL -> color_value("color_inner_numeral"),
  16.317 -      Isabelle_Markup.ML_CHAR -> color_value("color_inner_quoted"),
  16.318 -      Isabelle_Markup.ML_STRING -> color_value("color_inner_quoted"),
  16.319 -      Isabelle_Markup.ML_COMMENT -> color_value("color_inner_comment"),
  16.320 -      Isabelle_Markup.ANTIQ -> color_value("color_antiquotation"))
  16.321 -
  16.322 -    val text_color_elements = Set.empty[String] ++ text_colors.keys
  16.323 -
  16.324 -    snapshot.cumulate_markup(range, color, Some(text_color_elements),
  16.325 -      {
  16.326 -        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
  16.327 -        if text_colors.isDefinedAt(m) => text_colors(m)
  16.328 -      })
  16.329 -  }
  16.330 -
  16.331  
  16.332    /* token markup -- text styles */
  16.333  
  16.334 @@ -382,3 +78,346 @@
  16.335      else if (token.is_operator) JEditToken.OPERATOR
  16.336      else token_style(token.kind)
  16.337  }
  16.338 +
  16.339 +
  16.340 +class Isabelle_Rendering private(val snapshot: Document.Snapshot, val options: Options)
  16.341 +{
  16.342 +  /* colors */
  16.343 +
  16.344 +  def color_value(s: String): Color = Color_Value(options.string(s))
  16.345 +
  16.346 +  val outdated_color = color_value("outdated_color")
  16.347 +  val unprocessed_color = color_value("unprocessed_color")
  16.348 +  val unprocessed1_color = color_value("unprocessed1_color")
  16.349 +  val running_color = color_value("running_color")
  16.350 +  val running1_color = color_value("running1_color")
  16.351 +  val light_color = color_value("light_color")
  16.352 +  val writeln_color = color_value("writeln_color")
  16.353 +  val warning_color = color_value("warning_color")
  16.354 +  val error_color = color_value("error_color")
  16.355 +  val error1_color = color_value("error1_color")
  16.356 +  val bad_color = color_value("bad_color")
  16.357 +  val intensify_color = color_value("intensify_color")
  16.358 +  val quoted_color = color_value("quoted_color")
  16.359 +  val highlight_color = color_value("highlight_color")
  16.360 +  val hyperlink_color = color_value("hyperlink_color")
  16.361 +  val keyword1_color = color_value("keyword1_color")
  16.362 +  val keyword2_color = color_value("keyword2_color")
  16.363 +
  16.364 +  val tfree_color = color_value("tfree_color")
  16.365 +  val tvar_color = color_value("tvar_color")
  16.366 +  val free_color = color_value("free_color")
  16.367 +  val skolem_color = color_value("skolem_color")
  16.368 +  val bound_color = color_value("bound_color")
  16.369 +  val var_color = color_value("var_color")
  16.370 +  val inner_numeral_color = color_value("inner_numeral_color")
  16.371 +  val inner_quoted_color = color_value("inner_quoted_color")
  16.372 +  val inner_comment_color = color_value("inner_comment_color")
  16.373 +  val antiquotation_color = color_value("antiquotation_color")
  16.374 +  val dynamic_color = color_value("dynamic_color")
  16.375 +
  16.376 +
  16.377 +  /* command overview */
  16.378 +
  16.379 +  def overview_color(range: Text.Range): Option[Color] =
  16.380 +  {
  16.381 +    if (snapshot.is_outdated) None
  16.382 +    else {
  16.383 +      val results =
  16.384 +        snapshot.cumulate_markup[(Protocol.Status, Int)](
  16.385 +          range, (Protocol.Status.init, 0),
  16.386 +          Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
  16.387 +          {
  16.388 +            case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
  16.389 +              if (markup.name == Isabelle_Markup.WARNING)
  16.390 +                (status, pri max Isabelle_Rendering.warning_pri)
  16.391 +              else if (markup.name == Isabelle_Markup.ERROR)
  16.392 +                (status, pri max Isabelle_Rendering.error_pri)
  16.393 +              else (Protocol.command_status(status, markup), pri)
  16.394 +          })
  16.395 +      if (results.isEmpty) None
  16.396 +      else {
  16.397 +        val (status, pri) =
  16.398 +          ((Protocol.Status.init, 0) /: results) {
  16.399 +            case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
  16.400 +
  16.401 +        if (pri == Isabelle_Rendering.warning_pri) Some(warning_color)
  16.402 +        else if (pri == Isabelle_Rendering.error_pri) Some(error_color)
  16.403 +        else if (status.is_unprocessed) Some(unprocessed_color)
  16.404 +        else if (status.is_running) Some(running_color)
  16.405 +        else if (status.is_failed) Some(error_color)
  16.406 +        else None
  16.407 +      }
  16.408 +    }
  16.409 +  }
  16.410 +
  16.411 +
  16.412 +  /* markup selectors */
  16.413 +
  16.414 +  private val highlight_include =
  16.415 +    Set(Isabelle_Markup.SORT, Isabelle_Markup.TYP, Isabelle_Markup.TERM, Isabelle_Markup.PROP,
  16.416 +      Isabelle_Markup.ML_TYPING, Isabelle_Markup.TOKEN_RANGE, Isabelle_Markup.ENTITY,
  16.417 +      Isabelle_Markup.PATH, Isabelle_Markup.TYPING, Isabelle_Markup.FREE, Isabelle_Markup.SKOLEM,
  16.418 +      Isabelle_Markup.BOUND, Isabelle_Markup.VAR, Isabelle_Markup.TFREE, Isabelle_Markup.TVAR,
  16.419 +      Isabelle_Markup.ML_SOURCE, Isabelle_Markup.DOCUMENT_SOURCE)
  16.420 +
  16.421 +  def highlight(range: Text.Range): Option[Text.Info[Color]] =
  16.422 +  {
  16.423 +    snapshot.select_markup(range, Some(highlight_include),
  16.424 +        {
  16.425 +          case Text.Info(info_range, XML.Elem(Markup(name, _), _)) if highlight_include(name) =>
  16.426 +            Text.Info(snapshot.convert(info_range), highlight_color)
  16.427 +        }) match { case Text.Info(_, info) #:: _ => Some(info) case _ => None }
  16.428 +  }
  16.429 +
  16.430 +
  16.431 +  private val hyperlink_include = Set(Isabelle_Markup.ENTITY, Isabelle_Markup.PATH)
  16.432 +
  16.433 +  def hyperlink(range: Text.Range): Option[Text.Info[Hyperlink]] =
  16.434 +  {
  16.435 +    snapshot.cumulate_markup[List[Text.Info[Hyperlink]]](range, Nil, Some(hyperlink_include),
  16.436 +        {
  16.437 +          case (links, Text.Info(info_range, XML.Elem(Isabelle_Markup.Path(name), _)))
  16.438 +          if Path.is_ok(name) =>
  16.439 +            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
  16.440 +            Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
  16.441 +
  16.442 +          case (links, Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.ENTITY, props), _)))
  16.443 +          if (props.find(
  16.444 +            { case (Markup.KIND, Isabelle_Markup.ML_OPEN) => true
  16.445 +              case (Markup.KIND, Isabelle_Markup.ML_STRUCT) => true
  16.446 +              case _ => false }).isEmpty) =>
  16.447 +
  16.448 +            props match {
  16.449 +              case Position.Line_File(line, name) if Path.is_ok(name) =>
  16.450 +                Isabelle_System.source_file(Path.explode(name)) match {
  16.451 +                  case Some(path) =>
  16.452 +                    val jedit_file = Isabelle_System.platform_path(path)
  16.453 +                    Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, line, 0)) :: links
  16.454 +                  case None => links
  16.455 +                }
  16.456 +
  16.457 +              case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
  16.458 +                snapshot.state.find_command(snapshot.version, id) match {
  16.459 +                  case Some((node, command)) =>
  16.460 +                    val sources =
  16.461 +                      node.commands.iterator.takeWhile(_ != command).map(_.source) ++
  16.462 +                        Iterator.single(command.source(Text.Range(0, command.decode(offset))))
  16.463 +                    val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
  16.464 +                    Text.Info(snapshot.convert(info_range),
  16.465 +                      Hyperlink(command.node_name.node, line, column)) :: links
  16.466 +                  case None => links
  16.467 +                }
  16.468 +
  16.469 +              case _ => links
  16.470 +            }
  16.471 +        }) match { case Text.Info(_, info :: _) #:: _ => Some(info) case _ => None }
  16.472 +  }
  16.473 +
  16.474 +
  16.475 +  private def tooltip_text(msg: XML.Tree): String =
  16.476 +    Pretty.string_of(List(msg), margin = options.int("jedit_tooltip_margin"))
  16.477 +
  16.478 +  def tooltip_message(range: Text.Range): Option[String] =
  16.479 +  {
  16.480 +    val msgs =
  16.481 +      snapshot.cumulate_markup[SortedMap[Long, String]](range, SortedMap.empty,
  16.482 +        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR,
  16.483 +          Isabelle_Markup.BAD)),
  16.484 +        {
  16.485 +          case (msgs, Text.Info(_, msg @
  16.486 +              XML.Elem(Markup(markup, Isabelle_Markup.Serial(serial)), _)))
  16.487 +          if markup == Isabelle_Markup.WRITELN ||
  16.488 +              markup == Isabelle_Markup.WARNING ||
  16.489 +              markup == Isabelle_Markup.ERROR =>
  16.490 +            msgs + (serial -> tooltip_text(msg))
  16.491 +          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Isabelle_Markup.BAD, _), body)))
  16.492 +          if !body.isEmpty => msgs + (Document.new_id() -> tooltip_text(msg))
  16.493 +        }).toList.flatMap(_.info)
  16.494 +    if (msgs.isEmpty) None else Some(cat_lines(msgs.iterator.map(_._2)))
  16.495 +  }
  16.496 +
  16.497 +
  16.498 +  private val tooltips: Map[String, String] =
  16.499 +    Map(
  16.500 +      Isabelle_Markup.SORT -> "sort",
  16.501 +      Isabelle_Markup.TYP -> "type",
  16.502 +      Isabelle_Markup.TERM -> "term",
  16.503 +      Isabelle_Markup.PROP -> "proposition",
  16.504 +      Isabelle_Markup.TOKEN_RANGE -> "inner syntax token",
  16.505 +      Isabelle_Markup.FREE -> "free variable",
  16.506 +      Isabelle_Markup.SKOLEM -> "skolem variable",
  16.507 +      Isabelle_Markup.BOUND -> "bound variable",
  16.508 +      Isabelle_Markup.VAR -> "schematic variable",
  16.509 +      Isabelle_Markup.TFREE -> "free type variable",
  16.510 +      Isabelle_Markup.TVAR -> "schematic type variable",
  16.511 +      Isabelle_Markup.ML_SOURCE -> "ML source",
  16.512 +      Isabelle_Markup.DOCUMENT_SOURCE -> "document source")
  16.513 +
  16.514 +  private val tooltip_elements =
  16.515 +    Set(Isabelle_Markup.ENTITY, Isabelle_Markup.TYPING, Isabelle_Markup.ML_TYPING,
  16.516 +      Isabelle_Markup.PATH) ++ tooltips.keys
  16.517 +
  16.518 +  private def string_of_typing(kind: String, body: XML.Body): String =
  16.519 +    Pretty.string_of(List(Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)),
  16.520 +      margin = options.int("jedit_tooltip_margin"))
  16.521 +
  16.522 +  def tooltip(range: Text.Range): Option[String] =
  16.523 +  {
  16.524 +    def add(prev: Text.Info[List[(Boolean, String)]], r: Text.Range, p: (Boolean, String)) =
  16.525 +      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
  16.526 +
  16.527 +    val tips =
  16.528 +      snapshot.cumulate_markup[Text.Info[(List[(Boolean, String)])]](
  16.529 +        range, Text.Info(range, Nil), Some(tooltip_elements),
  16.530 +        {
  16.531 +          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Entity(kind, name), _))) =>
  16.532 +            val kind1 = space_explode('_', kind).mkString(" ")
  16.533 +            add(prev, r, (true, kind1 + " " + quote(name)))
  16.534 +          case (prev, Text.Info(r, XML.Elem(Isabelle_Markup.Path(name), _)))
  16.535 +          if Path.is_ok(name) =>
  16.536 +            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
  16.537 +            add(prev, r, (true, "file " + quote(jedit_file)))
  16.538 +          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.TYPING, _), body))) =>
  16.539 +            add(prev, r, (true, string_of_typing("::", body)))
  16.540 +          case (prev, Text.Info(r, XML.Elem(Markup(Isabelle_Markup.ML_TYPING, _), body))) =>
  16.541 +            add(prev, r, (false, string_of_typing("ML:", body)))
  16.542 +          case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
  16.543 +          if tooltips.isDefinedAt(name) => add(prev, r, (true, tooltips(name)))
  16.544 +        }).toList.flatMap(_.info.info)
  16.545 +
  16.546 +    val all_tips =
  16.547 +      (tips.filter(_._1) ++ tips.filter(!_._1).lastOption.toList).map(_._2)
  16.548 +    if (all_tips.isEmpty) None else Some(cat_lines(all_tips))
  16.549 +  }
  16.550 +
  16.551 +
  16.552 +  def gutter_message(range: Text.Range): Option[Icon] =
  16.553 +  {
  16.554 +    val results =
  16.555 +      snapshot.cumulate_markup[Int](range, 0,
  16.556 +        Some(Set(Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  16.557 +        {
  16.558 +          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING, _), body))) =>
  16.559 +            body match {
  16.560 +              case List(XML.Elem(Markup(Isabelle_Markup.LEGACY, _), _)) =>
  16.561 +                pri max Isabelle_Rendering.legacy_pri
  16.562 +              case _ => pri max Isabelle_Rendering.warning_pri
  16.563 +            }
  16.564 +          case (pri, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR, _), _))) =>
  16.565 +            pri max Isabelle_Rendering.error_pri
  16.566 +        })
  16.567 +    val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
  16.568 +    Isabelle_Rendering.gutter_icons.get(pri)
  16.569 +  }
  16.570 +
  16.571 +
  16.572 +  private val squiggly_colors = Map(
  16.573 +    Isabelle_Rendering.writeln_pri -> writeln_color,
  16.574 +    Isabelle_Rendering.warning_pri -> warning_color,
  16.575 +    Isabelle_Rendering.error_pri -> error_color)
  16.576 +
  16.577 +  def squiggly_underline(range: Text.Range): Stream[Text.Info[Color]] =
  16.578 +  {
  16.579 +    val results =
  16.580 +      snapshot.cumulate_markup[Int](range, 0,
  16.581 +        Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
  16.582 +        {
  16.583 +          case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
  16.584 +            name match {
  16.585 +              case Isabelle_Markup.WRITELN => pri max Isabelle_Rendering.writeln_pri
  16.586 +              case Isabelle_Markup.WARNING => pri max Isabelle_Rendering.warning_pri
  16.587 +              case Isabelle_Markup.ERROR => pri max Isabelle_Rendering.error_pri
  16.588 +              case _ => pri
  16.589 +            }
  16.590 +        })
  16.591 +    for {
  16.592 +      Text.Info(r, pri) <- results
  16.593 +      color <- squiggly_colors.get(pri)
  16.594 +    } yield Text.Info(r, color)
  16.595 +  }
  16.596 +
  16.597 +
  16.598 +  def background1(range: Text.Range): Stream[Text.Info[Color]] =
  16.599 +  {
  16.600 +    if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
  16.601 +    else
  16.602 +      for {
  16.603 +        Text.Info(r, result) <-
  16.604 +          snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
  16.605 +            range, (Some(Protocol.Status.init), None),
  16.606 +            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
  16.607 +            {
  16.608 +              case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
  16.609 +              if (Protocol.command_status_markup(markup.name)) =>
  16.610 +                (Some(Protocol.command_status(status, markup)), color)
  16.611 +              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
  16.612 +                (None, Some(bad_color))
  16.613 +              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
  16.614 +                (None, Some(intensify_color))
  16.615 +            })
  16.616 +        color <-
  16.617 +          (result match {
  16.618 +            case (Some(status), opt_color) =>
  16.619 +              if (status.is_unprocessed) Some(unprocessed1_color)
  16.620 +              else if (status.is_running) Some(running1_color)
  16.621 +              else opt_color
  16.622 +            case (_, opt_color) => opt_color
  16.623 +          })
  16.624 +      } yield Text.Info(r, color)
  16.625 +  }
  16.626 +
  16.627 +
  16.628 +  def background2(range: Text.Range): Stream[Text.Info[Color]] =
  16.629 +    snapshot.select_markup(range,
  16.630 +      Some(Set(Isabelle_Markup.TOKEN_RANGE)),
  16.631 +      {
  16.632 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TOKEN_RANGE, _), _)) => light_color
  16.633 +      })
  16.634 +
  16.635 +
  16.636 +  def foreground(range: Text.Range): Stream[Text.Info[Color]] =
  16.637 +    snapshot.select_markup(range,
  16.638 +      Some(Set(Isabelle_Markup.STRING, Isabelle_Markup.ALTSTRING, Isabelle_Markup.VERBATIM)),
  16.639 +      {
  16.640 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.STRING, _), _)) => quoted_color
  16.641 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ALTSTRING, _), _)) => quoted_color
  16.642 +        case Text.Info(_, XML.Elem(Markup(Isabelle_Markup.VERBATIM, _), _)) => quoted_color
  16.643 +      })
  16.644 +
  16.645 +
  16.646 +  private val text_colors: Map[String, Color] = Map(
  16.647 +      Isabelle_Markup.STRING -> Color.BLACK,
  16.648 +      Isabelle_Markup.ALTSTRING -> Color.BLACK,
  16.649 +      Isabelle_Markup.VERBATIM -> Color.BLACK,
  16.650 +      Isabelle_Markup.LITERAL -> keyword1_color,
  16.651 +      Isabelle_Markup.DELIMITER -> Color.BLACK,
  16.652 +      Isabelle_Markup.TFREE -> tfree_color,
  16.653 +      Isabelle_Markup.TVAR -> tvar_color,
  16.654 +      Isabelle_Markup.FREE -> free_color,
  16.655 +      Isabelle_Markup.SKOLEM -> skolem_color,
  16.656 +      Isabelle_Markup.BOUND -> bound_color,
  16.657 +      Isabelle_Markup.VAR -> var_color,
  16.658 +      Isabelle_Markup.INNER_STRING -> inner_quoted_color,
  16.659 +      Isabelle_Markup.INNER_COMMENT -> inner_comment_color,
  16.660 +      Isabelle_Markup.DYNAMIC_FACT -> dynamic_color,
  16.661 +      Isabelle_Markup.ML_KEYWORD -> keyword1_color,
  16.662 +      Isabelle_Markup.ML_DELIMITER -> Color.BLACK,
  16.663 +      Isabelle_Markup.ML_NUMERAL -> inner_numeral_color,
  16.664 +      Isabelle_Markup.ML_CHAR -> inner_quoted_color,
  16.665 +      Isabelle_Markup.ML_STRING -> inner_quoted_color,
  16.666 +      Isabelle_Markup.ML_COMMENT -> inner_comment_color,
  16.667 +      Isabelle_Markup.ANTIQ -> antiquotation_color)
  16.668 +
  16.669 +  private val text_color_elements = Set.empty[String] ++ text_colors.keys
  16.670 +
  16.671 +  def text_color(range: Text.Range, color: Color)
  16.672 +      : Stream[Text.Info[Color]] =
  16.673 +  {
  16.674 +    snapshot.cumulate_markup(range, color, Some(text_color_elements),
  16.675 +      {
  16.676 +        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
  16.677 +        if text_colors.isDefinedAt(m) => text_colors(m)
  16.678 +      })
  16.679 +  }
  16.680 +}
    17.1 --- a/src/Tools/jEdit/src/jedit_options.scala	Fri Sep 14 12:09:27 2012 +0200
    17.2 +++ b/src/Tools/jEdit/src/jedit_options.scala	Fri Sep 14 21:23:06 2012 +0200
    17.3 @@ -9,6 +9,7 @@
    17.4  
    17.5  import isabelle._
    17.6  
    17.7 +import java.awt.Color
    17.8  import javax.swing.{InputVerifier, JComponent, UIManager}
    17.9  import javax.swing.text.JTextComponent
   17.10  
   17.11 @@ -26,6 +27,8 @@
   17.12  
   17.13  class JEdit_Options extends Options_Variable
   17.14  {
   17.15 +  def color_value(s: String): Color = Color_Value(string(s))
   17.16 +
   17.17    def make_color_component(opt: Options.Opt): Option_Component =
   17.18    {
   17.19      Swing_Thread.require()
    18.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 14 12:09:27 2012 +0200
    18.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Sep 14 21:23:06 2012 +0200
    18.3 @@ -25,6 +25,18 @@
    18.4  {
    18.5    Swing_Thread.require()
    18.6  
    18.7 +
    18.8 +  /* component state -- owned by Swing thread */
    18.9 +
   18.10 +  private var zoom_factor = 100
   18.11 +  private var show_tracing = false
   18.12 +  private var do_update = true
   18.13 +  private var current_state = Command.empty.empty_state
   18.14 +  private var current_body: XML.Body = Nil
   18.15 +
   18.16 +
   18.17 +  /* HTML panel */
   18.18 +
   18.19    private val html_panel =
   18.20      new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   18.21    {
   18.22 @@ -36,23 +48,20 @@
   18.23          Document_View(view.getTextArea) match {
   18.24            case Some(doc_view) =>
   18.25              doc_view.robust_body() {
   18.26 -              current_command match {
   18.27 -                case Some(cmd) =>
   18.28 -                  val model = doc_view.model
   18.29 -                  val buffer = model.buffer
   18.30 -                  val snapshot = model.snapshot()
   18.31 -                  snapshot.node.command_start(cmd) match {
   18.32 -                    case Some(start) if !snapshot.is_outdated =>
   18.33 -                      val text = Pretty.string_of(sendback)
   18.34 -                      try {
   18.35 -                        buffer.beginCompoundEdit()
   18.36 -                        buffer.remove(start, cmd.proper_range.length)
   18.37 -                        buffer.insert(start, text)
   18.38 -                      }
   18.39 -                      finally { buffer.endCompoundEdit() }
   18.40 -                    case _ =>
   18.41 +              val cmd = current_state.command
   18.42 +              val model = doc_view.model
   18.43 +              val buffer = model.buffer
   18.44 +              val snapshot = model.snapshot()
   18.45 +              snapshot.node.command_start(cmd) match {
   18.46 +                case Some(start) if !snapshot.is_outdated =>
   18.47 +                  val text = Pretty.string_of(sendback)
   18.48 +                  try {
   18.49 +                    buffer.beginCompoundEdit()
   18.50 +                    buffer.remove(start, cmd.proper_range.length)
   18.51 +                    buffer.insert(start, text)
   18.52                    }
   18.53 -                case None =>
   18.54 +                  finally { buffer.endCompoundEdit() }
   18.55 +                case _ =>
   18.56                }
   18.57              }
   18.58            case None =>
   18.59 @@ -63,55 +72,45 @@
   18.60    set_content(html_panel)
   18.61  
   18.62  
   18.63 -  /* component state -- owned by Swing thread */
   18.64 -
   18.65 -  private var zoom_factor = 100
   18.66 -  private var show_tracing = false
   18.67 -  private var follow_caret = true
   18.68 -  private var current_command: Option[Command] = None
   18.69 -
   18.70 -
   18.71    private def handle_resize()
   18.72    {
   18.73 -    Swing_Thread.now {
   18.74 -      html_panel.resize(Isabelle.font_family(),
   18.75 -        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
   18.76 -    }
   18.77 +    Swing_Thread.require()
   18.78 +
   18.79 +    html_panel.resize(Isabelle.font_family(),
   18.80 +      scala.math.round(Isabelle.font_size() * zoom_factor / 100))
   18.81    }
   18.82  
   18.83 -  private def handle_perspective(): Boolean =
   18.84 -    Swing_Thread.now {
   18.85 -      Document_View(view.getTextArea) match {
   18.86 -        case Some(doc_view) =>
   18.87 -          val cmd = doc_view.selected_command()
   18.88 -          if (current_command == cmd) false
   18.89 -          else { current_command = cmd; true }
   18.90 -        case None => false
   18.91 -      }
   18.92 -    }
   18.93 -
   18.94 -  private def handle_update(restriction: Option[Set[Command]] = None)
   18.95 +  private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
   18.96    {
   18.97 -    Swing_Thread.now {
   18.98 -      if (follow_caret) handle_perspective()
   18.99 -      Document_View(view.getTextArea) match {
  18.100 -        case Some(doc_view) =>
  18.101 -          current_command match {
  18.102 -            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
  18.103 -              val snapshot = doc_view.model.snapshot()
  18.104 -              val filtered_results =
  18.105 -                snapshot.state.command_state(snapshot.version, cmd).results.iterator
  18.106 -                  .map(_._2).filter(
  18.107 -                  { // FIXME not scalable
  18.108 -                    case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
  18.109 -                    case _ => true
  18.110 -                  }).toList
  18.111 -              html_panel.render(filtered_results)
  18.112 -            case _ => html_panel.render(Nil)
  18.113 -          }
  18.114 -        case None => html_panel.render(Nil)
  18.115 +    Swing_Thread.require()
  18.116 +
  18.117 +    val new_state =
  18.118 +      if (follow) {
  18.119 +        Document_View(view.getTextArea) match {
  18.120 +          case Some(doc_view) =>
  18.121 +            val snapshot = doc_view.model.snapshot()
  18.122 +            snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
  18.123 +              case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
  18.124 +              case None => Command.empty.empty_state
  18.125 +            }
  18.126 +          case None => Command.empty.empty_state
  18.127 +        }
  18.128        }
  18.129 -    }
  18.130 +      else current_state
  18.131 +
  18.132 +    val new_body =
  18.133 +      if (!restriction.isDefined || restriction.get.contains(new_state.command))
  18.134 +        new_state.results.iterator.map(_._2).filter(
  18.135 +        { // FIXME not scalable
  18.136 +          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
  18.137 +          case _ => true
  18.138 +        }).toList
  18.139 +      else current_body
  18.140 +
  18.141 +    if (new_body != current_body) html_panel.render(new_body)
  18.142 +
  18.143 +    current_state = new_state
  18.144 +    current_body = new_body
  18.145    }
  18.146  
  18.147  
  18.148 @@ -120,9 +119,12 @@
  18.149    private val main_actor = actor {
  18.150      loop {
  18.151        react {
  18.152 -        case Session.Global_Settings => handle_resize()
  18.153 -        case changed: Session.Commands_Changed => handle_update(Some(changed.commands))
  18.154 -        case Session.Caret_Focus => if (follow_caret && handle_perspective()) handle_update()
  18.155 +        case Session.Global_Settings =>
  18.156 +          Swing_Thread.later { handle_resize() }
  18.157 +        case changed: Session.Commands_Changed =>
  18.158 +          Swing_Thread.later { handle_update(do_update, Some(changed.commands)) }
  18.159 +        case Session.Caret_Focus =>
  18.160 +          Swing_Thread.later { handle_update(do_update, None) }
  18.161          case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
  18.162        }
  18.163      }
  18.164 @@ -130,14 +132,18 @@
  18.165  
  18.166    override def init()
  18.167    {
  18.168 +    Swing_Thread.require()
  18.169 +
  18.170      Isabelle.session.global_settings += main_actor
  18.171      Isabelle.session.commands_changed += main_actor
  18.172      Isabelle.session.caret_focus += main_actor
  18.173 -    handle_update()
  18.174 +    handle_update(true, None)
  18.175    }
  18.176  
  18.177    override def exit()
  18.178    {
  18.179 +    Swing_Thread.require()
  18.180 +
  18.181      Isabelle.session.global_settings -= main_actor
  18.182      Isabelle.session.commands_changed -= main_actor
  18.183      Isabelle.session.caret_focus -= main_actor
  18.184 @@ -162,19 +168,21 @@
  18.185    zoom.tooltip = "Zoom factor for basic font size"
  18.186  
  18.187    private val tracing = new CheckBox("Tracing") {
  18.188 -    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
  18.189 +    reactions += {
  18.190 +      case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }
  18.191    }
  18.192    tracing.selected = show_tracing
  18.193    tracing.tooltip = "Indicate output of tracing messages"
  18.194  
  18.195    private val auto_update = new CheckBox("Auto update") {
  18.196 -    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
  18.197 +    reactions += {
  18.198 +      case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
  18.199    }
  18.200 -  auto_update.selected = follow_caret
  18.201 +  auto_update.selected = do_update
  18.202    auto_update.tooltip = "Indicate automatic update following cursor movement"
  18.203  
  18.204    private val update = new Button("Update") {
  18.205 -    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
  18.206 +    reactions += { case ButtonClicked(_) => handle_update(true, None) }
  18.207    }
  18.208    update.tooltip = "Update display according to the command at cursor position"
  18.209  
    19.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 14 12:09:27 2012 +0200
    19.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Fri Sep 14 21:23:06 2012 +0200
    19.3 @@ -89,10 +89,10 @@
    19.4            var end = size.width - insets.right
    19.5            for {
    19.6              (n, color) <- List(
    19.7 -              (st.unprocessed, Isabelle_Rendering.color_value("color_unprocessed1")),
    19.8 -              (st.running, Isabelle_Rendering.color_value("color_running")),
    19.9 -              (st.warned, Isabelle_Rendering.color_value("color_warning")),
   19.10 -              (st.failed, Isabelle_Rendering.color_value("color_error"))) }
   19.11 +              (st.unprocessed, Isabelle.options.color_value("unprocessed1_color")),
   19.12 +              (st.running, Isabelle.options.color_value("running_color")),
   19.13 +              (st.warned, Isabelle.options.color_value("warning_color")),
   19.14 +              (st.failed, Isabelle.options.color_value("error_color"))) }
   19.15            {
   19.16              gfx.setColor(color)
   19.17              val v = (n * w / st.total) max (if (n > 0) 2 else 0)
    20.1 --- a/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 14 12:09:27 2012 +0200
    20.2 +++ b/src/Tools/jEdit/src/text_area_painter.scala	Fri Sep 14 21:23:06 2012 +0200
    20.3 @@ -75,7 +75,7 @@
    20.4  
    20.5    /* common painter state */
    20.6  
    20.7 -  @volatile private var painter_snapshot: Document.Snapshot = null
    20.8 +  @volatile private var painter_rendering: Isabelle_Rendering = null
    20.9    @volatile private var painter_clip: Shape = null
   20.10  
   20.11    private val set_state = new TextAreaExtension
   20.12 @@ -84,7 +84,7 @@
   20.13        first_line: Int, last_line: Int, physical_lines: Array[Int],
   20.14        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   20.15      {
   20.16 -      painter_snapshot = model.snapshot()
   20.17 +      painter_rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
   20.18        painter_clip = gfx.getClip
   20.19      }
   20.20    }
   20.21 @@ -95,14 +95,14 @@
   20.22        first_line: Int, last_line: Int, physical_lines: Array[Int],
   20.23        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   20.24      {
   20.25 -      painter_snapshot = null
   20.26 +      painter_rendering = null
   20.27        painter_clip = null
   20.28      }
   20.29    }
   20.30  
   20.31 -  private def robust_snapshot(body: Document.Snapshot => Unit)
   20.32 +  private def robust_rendering(body: Isabelle_Rendering => Unit)
   20.33    {
   20.34 -    doc_view.robust_body(()) { body(painter_snapshot) }
   20.35 +    doc_view.robust_body(()) { body(painter_rendering) }
   20.36    }
   20.37  
   20.38  
   20.39 @@ -114,7 +114,7 @@
   20.40        first_line: Int, last_line: Int, physical_lines: Array[Int],
   20.41        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   20.42      {
   20.43 -      robust_snapshot { snapshot =>
   20.44 +      robust_rendering { rendering =>
   20.45          val ascent = text_area.getPainter.getFontMetrics.getAscent
   20.46  
   20.47          for (i <- 0 until physical_lines.length) {
   20.48 @@ -123,7 +123,7 @@
   20.49  
   20.50              // background color (1)
   20.51              for {
   20.52 -              Text.Info(range, color) <- Isabelle_Rendering.background1(snapshot, line_range)
   20.53 +              Text.Info(range, color) <- rendering.background1(line_range)
   20.54                r <- gfx_range(range)
   20.55              } {
   20.56                gfx.setColor(color)
   20.57 @@ -132,7 +132,7 @@
   20.58  
   20.59              // background color (2)
   20.60              for {
   20.61 -              Text.Info(range, color) <- Isabelle_Rendering.background2(snapshot, line_range)
   20.62 +              Text.Info(range, color) <- rendering.background2(line_range)
   20.63                r <- gfx_range(range)
   20.64              } {
   20.65                gfx.setColor(color)
   20.66 @@ -141,7 +141,7 @@
   20.67  
   20.68              // squiggly underline
   20.69              for {
   20.70 -              Text.Info(range, color) <- Isabelle_Rendering.squiggly_underline(snapshot, line_range)
   20.71 +              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
   20.72                r <- gfx_range(range)
   20.73              } {
   20.74                gfx.setColor(color)
   20.75 @@ -161,7 +161,7 @@
   20.76  
   20.77    /* text */
   20.78  
   20.79 -  private def paint_chunk_list(snapshot: Document.Snapshot,
   20.80 +  private def paint_chunk_list(rendering: Isabelle_Rendering,
   20.81      gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
   20.82    {
   20.83      val clip_rect = gfx.getClipBounds
   20.84 @@ -185,12 +185,12 @@
   20.85            else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
   20.86  
   20.87          val caret_range =
   20.88 -          if (text_area.isCaretVisible) doc_view.caret_range()
   20.89 +          if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition)
   20.90            else Text.Range(-1)
   20.91  
   20.92          val markup =
   20.93            for {
   20.94 -            r1 <- Isabelle_Rendering.text_color(snapshot, chunk_range, chunk_color)
   20.95 +            r1 <- rendering.text_color(chunk_range, chunk_color)
   20.96              r2 <- r1.try_restrict(chunk_range)
   20.97            } yield r2
   20.98  
   20.99 @@ -246,7 +246,7 @@
  20.100        first_line: Int, last_line: Int, physical_lines: Array[Int],
  20.101        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  20.102      {
  20.103 -      robust_snapshot { snapshot =>
  20.104 +      robust_rendering { rendering =>
  20.105          val clip = gfx.getClip
  20.106          val x0 = text_area.getHorizontalOffset
  20.107          val fm = text_area.getPainter.getFontMetrics
  20.108 @@ -260,7 +260,7 @@
  20.109              if (chunks != null) {
  20.110                val line_start = text_area.getBuffer.getLineStartOffset(line)
  20.111                gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
  20.112 -              val w = paint_chunk_list(snapshot, gfx, line_start, chunks, x0, y0).toInt
  20.113 +              val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
  20.114                gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
  20.115                orig_text_painter.paintValidLine(gfx,
  20.116                  screen_line, line, start(i), end(i), y + line_height * i)
  20.117 @@ -282,23 +282,23 @@
  20.118        first_line: Int, last_line: Int, physical_lines: Array[Int],
  20.119        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  20.120      {
  20.121 -      robust_snapshot { snapshot =>
  20.122 +      robust_rendering { rendering =>
  20.123          for (i <- 0 until physical_lines.length) {
  20.124            if (physical_lines(i) != -1) {
  20.125              val line_range = doc_view.proper_line_range(start(i), end(i))
  20.126  
  20.127              // foreground color
  20.128              for {
  20.129 -              Text.Info(range, color) <- Isabelle_Rendering.foreground(snapshot, line_range)
  20.130 +              Text.Info(range, color) <- rendering.foreground(line_range)
  20.131                r <- gfx_range(range)
  20.132              } {
  20.133                gfx.setColor(color)
  20.134                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  20.135              }
  20.136  
  20.137 -            // highlighted range -- potentially from other snapshot
  20.138 +            // highlight range -- potentially from other snapshot
  20.139              for {
  20.140 -              info <- doc_view.highlight_range()
  20.141 +              info <- doc_view.highlight_info()
  20.142                Text.Info(range, color) <- info.try_restrict(line_range)
  20.143                r <- gfx_range(range)
  20.144              } {
  20.145 @@ -308,11 +308,11 @@
  20.146  
  20.147              // hyperlink range -- potentially from other snapshot
  20.148              for {
  20.149 -              info <- doc_view.hyperlink_range()
  20.150 +              info <- doc_view.hyperlink_info()
  20.151                Text.Info(range, _) <- info.try_restrict(line_range)
  20.152                r <- gfx_range(range)
  20.153              } {
  20.154 -              gfx.setColor(Isabelle_Rendering.color_value("color_hyperlink"))
  20.155 +              gfx.setColor(rendering.hyperlink_color)
  20.156                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
  20.157              }
  20.158            }
  20.159 @@ -329,7 +329,7 @@
  20.160      override def paintValidLine(gfx: Graphics2D,
  20.161        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
  20.162      {
  20.163 -      robust_snapshot { _ =>
  20.164 +      robust_rendering { _ =>
  20.165          if (before) gfx.clipRect(0, 0, 0, 0)
  20.166          else gfx.setClip(painter_clip)
  20.167        }
  20.168 @@ -346,7 +346,7 @@
  20.169      override def paintValidLine(gfx: Graphics2D,
  20.170        screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
  20.171      {
  20.172 -      robust_snapshot { _ =>
  20.173 +      robust_rendering { _ =>
  20.174          if (text_area.isCaretVisible) {
  20.175            val caret = text_area.getCaretPosition
  20.176            if (start <= caret && caret == end - 1) {
    21.1 --- a/src/Tools/jEdit/src/text_overview.scala	Fri Sep 14 12:09:27 2012 +0200
    21.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Fri Sep 14 21:23:06 2012 +0200
    21.3 @@ -54,6 +54,7 @@
    21.4    private var cached_colors: List[(Color, Int, Int)] = Nil
    21.5  
    21.6    private var last_snapshot = Document.State.init.snapshot()
    21.7 +  private var last_options = Isabelle.options.value
    21.8    private var last_line_count = 0
    21.9    private var last_char_count = 0
   21.10    private var last_L = 0
   21.11 @@ -69,7 +70,7 @@
   21.12          val snapshot = doc_view.model.snapshot()
   21.13  
   21.14          if (snapshot.is_outdated) {
   21.15 -          gfx.setColor(Isabelle_Rendering.color_value("color_outdated"))
   21.16 +          gfx.setColor(Isabelle.options.color_value("outdated_color"))
   21.17            gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds)
   21.18          }
   21.19          else {
   21.20 @@ -82,9 +83,14 @@
   21.21            val L = lines()
   21.22            val H = getHeight()
   21.23  
   21.24 +          val options = Isabelle.options.value
   21.25 +
   21.26            if (!(line_count == last_line_count && char_count == last_char_count &&
   21.27 -                L == last_L && H == last_H && (snapshot eq_markup last_snapshot)))
   21.28 +                L == last_L && H == last_H && (snapshot eq_markup last_snapshot) &&
   21.29 +                (options eq last_options)))
   21.30            {
   21.31 +            val rendering = Isabelle_Rendering(snapshot, options)
   21.32 +
   21.33              @tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)])
   21.34                : List[(Color, Int, Int)] =
   21.35              {
   21.36 @@ -102,7 +108,7 @@
   21.37                  val range = Text.Range(start, end)
   21.38  
   21.39                  val colors1 =
   21.40 -                  (Isabelle_Rendering.overview_color(snapshot, range), colors) match {
   21.41 +                  (rendering.overview_color(range), colors) match {
   21.42                      case (Some(color), (old_color, old_h, old_h1) :: rest)
   21.43                      if color == old_color && old_h1 == h => (color, old_h, h1) :: rest
   21.44                      case (Some(color), _) => (color, h, h1) :: colors
   21.45 @@ -115,6 +121,7 @@
   21.46              cached_colors = loop(0, 0, 0, 0, Nil)
   21.47  
   21.48              last_snapshot = snapshot
   21.49 +            last_options = options
   21.50              last_line_count = line_count
   21.51              last_char_count = char_count
   21.52              last_L = L
    22.1 --- a/src/Tools/quickcheck.ML	Fri Sep 14 12:09:27 2012 +0200
    22.2 +++ b/src/Tools/quickcheck.ML	Fri Sep 14 21:23:06 2012 +0200
    22.3 @@ -529,7 +529,7 @@
    22.4               state
    22.5               |> (if auto then
    22.6                     Proof.goal_message (K (Pretty.chunks [Pretty.str "",
    22.7 -                       Pretty.mark Isabelle_Markup.hilite msg]))
    22.8 +                       Pretty.mark Isabelle_Markup.intensify msg]))
    22.9                   else
   22.10                     tap (fn _ => Output.urgent_message (Pretty.string_of msg))))
   22.11            else
    23.1 --- a/src/Tools/solve_direct.ML	Fri Sep 14 12:09:27 2012 +0200
    23.2 +++ b/src/Tools/solve_direct.ML	Fri Sep 14 21:23:06 2012 +0200
    23.3 @@ -89,7 +89,7 @@
    23.4                 Proof.goal_message
    23.5                   (fn () =>
    23.6                     Pretty.chunks
    23.7 -                    [Pretty.str "", Pretty.markup Isabelle_Markup.hilite (message results)])
    23.8 +                    [Pretty.str "", Pretty.markup Isabelle_Markup.intensify (message results)])
    23.9               else
   23.10                 tap (fn _ =>
   23.11                   Output.urgent_message (Pretty.string_of (Pretty.chunks (message results))))))