moved sources -- eliminated Netbeans artifact of jedit package directory;
authorwenzelm
Wed Jun 08 17:42:07 2011 +0200 (2011-06-08)
changeset 432825d294220ca43
parent 43281 8d8b6ed0588c
child 43283 446e6621762d
moved sources -- eliminated Netbeans artifact of jedit package directory;
src/Tools/jEdit/jedit_build/Tools/jedit
src/Tools/jEdit/src/dockable.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/html_panel.scala
src/Tools/jEdit/src/isabelle_encoding.scala
src/Tools/jEdit/src/isabelle_hyperlinks.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/dockable.scala
src/Tools/jEdit/src/jedit/document_model.scala
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/html_panel.scala
src/Tools/jEdit/src/jedit/isabelle_encoding.scala
src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
src/Tools/jEdit/src/jedit/isabelle_markup.scala
src/Tools/jEdit/src/jedit/isabelle_options.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
src/Tools/jEdit/src/jedit/output_dockable.scala
src/Tools/jEdit/src/jedit/plugin.scala
src/Tools/jEdit/src/jedit/protocol_dockable.scala
src/Tools/jEdit/src/jedit/raw_output_dockable.scala
src/Tools/jEdit/src/jedit/scala_console.scala
src/Tools/jEdit/src/jedit/session_dockable.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/jedit_build/Tools/jedit	Wed Jun 08 17:32:31 2011 +0200
     1.2 +++ b/src/Tools/jEdit/jedit_build/Tools/jedit	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -35,21 +35,21 @@
     1.4  SRC_DIR="$ISABELLE_HOME/src/Tools/jEdit"
     1.5  
     1.6  declare -a SOURCES=(
     1.7 -  "$SRC_DIR/src/jedit/dockable.scala"
     1.8 -  "$SRC_DIR/src/jedit/document_model.scala"
     1.9 -  "$SRC_DIR/src/jedit/document_view.scala"
    1.10 -  "$SRC_DIR/src/jedit/html_panel.scala"
    1.11 -  "$SRC_DIR/src/jedit/isabelle_encoding.scala"
    1.12 -  "$SRC_DIR/src/jedit/isabelle_hyperlinks.scala"
    1.13 -  "$SRC_DIR/src/jedit/isabelle_markup.scala"
    1.14 -  "$SRC_DIR/src/jedit/isabelle_options.scala"
    1.15 -  "$SRC_DIR/src/jedit/isabelle_sidekick.scala"
    1.16 -  "$SRC_DIR/src/jedit/output_dockable.scala"
    1.17 -  "$SRC_DIR/src/jedit/plugin.scala"
    1.18 -  "$SRC_DIR/src/jedit/protocol_dockable.scala"
    1.19 -  "$SRC_DIR/src/jedit/raw_output_dockable.scala"
    1.20 -  "$SRC_DIR/src/jedit/scala_console.scala"
    1.21 -  "$SRC_DIR/src/jedit/session_dockable.scala"
    1.22 +  "$SRC_DIR/src/dockable.scala"
    1.23 +  "$SRC_DIR/src/document_model.scala"
    1.24 +  "$SRC_DIR/src/document_view.scala"
    1.25 +  "$SRC_DIR/src/html_panel.scala"
    1.26 +  "$SRC_DIR/src/isabelle_encoding.scala"
    1.27 +  "$SRC_DIR/src/isabelle_hyperlinks.scala"
    1.28 +  "$SRC_DIR/src/isabelle_markup.scala"
    1.29 +  "$SRC_DIR/src/isabelle_options.scala"
    1.30 +  "$SRC_DIR/src/isabelle_sidekick.scala"
    1.31 +  "$SRC_DIR/src/output_dockable.scala"
    1.32 +  "$SRC_DIR/src/plugin.scala"
    1.33 +  "$SRC_DIR/src/protocol_dockable.scala"
    1.34 +  "$SRC_DIR/src/raw_output_dockable.scala"
    1.35 +  "$SRC_DIR/src/scala_console.scala"
    1.36 +  "$SRC_DIR/src/session_dockable.scala"
    1.37  )
    1.38  
    1.39  declare -a PLUGIN_FILES=(
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Tools/jEdit/src/dockable.scala	Wed Jun 08 17:42:07 2011 +0200
     2.3 @@ -0,0 +1,41 @@
     2.4 +/*  Title:      Tools/jEdit/src/dockable.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Generic dockable window.
     2.8 +*/
     2.9 +
    2.10 +package isabelle.jedit
    2.11 +
    2.12 +
    2.13 +import isabelle._
    2.14 +
    2.15 +import java.awt.{Dimension, Component, BorderLayout}
    2.16 +import javax.swing.JPanel
    2.17 +
    2.18 +import org.gjt.sp.jedit.View
    2.19 +import org.gjt.sp.jedit.gui.DockableWindowManager
    2.20 +
    2.21 +
    2.22 +class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
    2.23 +{
    2.24 +  if (position == DockableWindowManager.FLOATING)
    2.25 +    setPreferredSize(new Dimension(500, 250))
    2.26 +
    2.27 +  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
    2.28 +  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
    2.29 +
    2.30 +  protected def init() { }
    2.31 +  protected def exit() { }
    2.32 +
    2.33 +  override def addNotify()
    2.34 +  {
    2.35 +    super.addNotify()
    2.36 +    init()
    2.37 +  }
    2.38 +
    2.39 +  override def removeNotify()
    2.40 +  {
    2.41 +    exit()
    2.42 +    super.removeNotify()
    2.43 +  }
    2.44 +}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/document_model.scala	Wed Jun 08 17:42:07 2011 +0200
     3.3 @@ -0,0 +1,252 @@
     3.4 +/*  Title:      Tools/jEdit/src/document_model.scala
     3.5 +    Author:     Fabian Immler, TU Munich
     3.6 +    Author:     Makarius
     3.7 +
     3.8 +Document model connected to jEdit buffer -- single node in theory graph.
     3.9 +*/
    3.10 +
    3.11 +package isabelle.jedit
    3.12 +
    3.13 +
    3.14 +import isabelle._
    3.15 +
    3.16 +import scala.collection.mutable
    3.17 +
    3.18 +import org.gjt.sp.jedit.Buffer
    3.19 +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
    3.20 +import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
    3.21 +import org.gjt.sp.jedit.textarea.TextArea
    3.22 +
    3.23 +import java.awt.font.TextAttribute
    3.24 +import javax.swing.text.Segment;
    3.25 +
    3.26 +
    3.27 +object Document_Model
    3.28 +{
    3.29 +  object Token_Markup
    3.30 +  {
    3.31 +    /* extended token styles */
    3.32 +
    3.33 +    private val plain_range: Int = Token.ID_COUNT
    3.34 +    private val full_range: Int = 3 * plain_range
    3.35 +    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
    3.36 +
    3.37 +    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
    3.38 +    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
    3.39 +
    3.40 +    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
    3.41 +    {
    3.42 +      import scala.collection.JavaConversions._
    3.43 +      val script_font =
    3.44 +        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
    3.45 +      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
    3.46 +    }
    3.47 +
    3.48 +    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
    3.49 +    {
    3.50 +      val new_styles = new Array[SyntaxStyle](full_range)
    3.51 +      for (i <- 0 until plain_range) {
    3.52 +        val style = styles(i)
    3.53 +        new_styles(i) = style
    3.54 +        new_styles(subscript(i.toByte)) = script_style(style, -1)
    3.55 +        new_styles(superscript(i.toByte)) = script_style(style, 1)
    3.56 +      }
    3.57 +      new_styles
    3.58 +    }
    3.59 +
    3.60 +
    3.61 +    /* line context */
    3.62 +
    3.63 +    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
    3.64 +
    3.65 +    class Line_Context(val line: Int, prev: Line_Context)
    3.66 +      extends TokenMarker.LineContext(dummy_rules, prev)
    3.67 +    {
    3.68 +      override def hashCode: Int = line
    3.69 +      override def equals(that: Any): Boolean =
    3.70 +        that match {
    3.71 +          case other: Line_Context => line == other.line
    3.72 +          case _ => false
    3.73 +        }
    3.74 +    }
    3.75 +  }
    3.76 +
    3.77 +
    3.78 +  /* document model of buffer */
    3.79 +
    3.80 +  private val key = "isabelle.document_model"
    3.81 +
    3.82 +  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
    3.83 +  {
    3.84 +    Swing_Thread.require()
    3.85 +    val model = new Document_Model(session, buffer, thy_name)
    3.86 +    buffer.setProperty(key, model)
    3.87 +    model.activate()
    3.88 +    model
    3.89 +  }
    3.90 +
    3.91 +  def apply(buffer: Buffer): Option[Document_Model] =
    3.92 +  {
    3.93 +    Swing_Thread.require()
    3.94 +    buffer.getProperty(key) match {
    3.95 +      case model: Document_Model => Some(model)
    3.96 +      case _ => None
    3.97 +    }
    3.98 +  }
    3.99 +
   3.100 +  def exit(buffer: Buffer)
   3.101 +  {
   3.102 +    Swing_Thread.require()
   3.103 +    apply(buffer) match {
   3.104 +      case None =>
   3.105 +      case Some(model) =>
   3.106 +        model.deactivate()
   3.107 +        buffer.unsetProperty(key)
   3.108 +    }
   3.109 +  }
   3.110 +}
   3.111 +
   3.112 +
   3.113 +class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
   3.114 +{
   3.115 +  /* pending text edits */
   3.116 +
   3.117 +  object pending_edits  // owned by Swing thread
   3.118 +  {
   3.119 +    private val pending = new mutable.ListBuffer[Text.Edit]
   3.120 +    def snapshot(): List[Text.Edit] = pending.toList
   3.121 +
   3.122 +    def flush(more_edits: Option[List[Text.Edit]]*)
   3.123 +    {
   3.124 +      Swing_Thread.require()
   3.125 +      val edits = snapshot()
   3.126 +      pending.clear
   3.127 +
   3.128 +      val all_edits =
   3.129 +        if (edits.isEmpty) more_edits.toList
   3.130 +        else Some(edits) :: more_edits.toList
   3.131 +      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
   3.132 +    }
   3.133 +
   3.134 +    def init()
   3.135 +    {
   3.136 +      Swing_Thread.require()
   3.137 +      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
   3.138 +    }
   3.139 +
   3.140 +    private val delay_flush =
   3.141 +      Swing_Thread.delay_last(session.input_delay) { flush() }
   3.142 +
   3.143 +    def +=(edit: Text.Edit)
   3.144 +    {
   3.145 +      Swing_Thread.require()
   3.146 +      pending += edit
   3.147 +      delay_flush()
   3.148 +    }
   3.149 +  }
   3.150 +
   3.151 +
   3.152 +  /* snapshot */
   3.153 +
   3.154 +  def snapshot(): Document.Snapshot =
   3.155 +  {
   3.156 +    Swing_Thread.require()
   3.157 +    session.snapshot(thy_name, pending_edits.snapshot())
   3.158 +  }
   3.159 +
   3.160 +
   3.161 +  /* buffer listener */
   3.162 +
   3.163 +  private val buffer_listener: BufferListener = new BufferAdapter
   3.164 +  {
   3.165 +    override def bufferLoaded(buffer: JEditBuffer)
   3.166 +    {
   3.167 +      pending_edits.init()
   3.168 +    }
   3.169 +
   3.170 +    override def contentInserted(buffer: JEditBuffer,
   3.171 +      start_line: Int, offset: Int, num_lines: Int, length: Int)
   3.172 +    {
   3.173 +      if (!buffer.isLoading)
   3.174 +        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
   3.175 +    }
   3.176 +
   3.177 +    override def preContentRemoved(buffer: JEditBuffer,
   3.178 +      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
   3.179 +    {
   3.180 +      if (!buffer.isLoading)
   3.181 +        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
   3.182 +    }
   3.183 +  }
   3.184 +
   3.185 +
   3.186 +  /* semantic token marker */
   3.187 +
   3.188 +  private val token_marker = new TokenMarker
   3.189 +  {
   3.190 +    override def markTokens(prev: TokenMarker.LineContext,
   3.191 +        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
   3.192 +    {
   3.193 +      Isabelle.swing_buffer_lock(buffer) {
   3.194 +        val snapshot = Document_Model.this.snapshot()
   3.195 +
   3.196 +        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
   3.197 +        val line = if (prev == null) 0 else previous.line + 1
   3.198 +        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
   3.199 +
   3.200 +        val start = buffer.getLineStartOffset(line)
   3.201 +        val stop = start + line_segment.count
   3.202 +
   3.203 +        /* FIXME
   3.204 +        for (text_area <- Isabelle.jedit_text_areas(buffer)
   3.205 +              if Document_View(text_area).isDefined)
   3.206 +          Document_View(text_area).get.set_styles()
   3.207 +        */
   3.208 +
   3.209 +        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
   3.210 +          handler.handleToken(line_segment, style, offset, length, context)
   3.211 +
   3.212 +        val syntax = session.current_syntax()
   3.213 +        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
   3.214 +
   3.215 +        var last = start
   3.216 +        for (token <- tokens.iterator) {
   3.217 +          val Text.Range(token_start, token_stop) = token.range
   3.218 +          if (last < token_start)
   3.219 +            handle_token(Token.COMMENT1, last - start, token_start - last)
   3.220 +          handle_token(token.info getOrElse Token.NULL,
   3.221 +            token_start - start, token_stop - token_start)
   3.222 +          last = token_stop
   3.223 +        }
   3.224 +        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
   3.225 +
   3.226 +        handle_token(Token.END, line_segment.count, 0)
   3.227 +        handler.setLineContext(context)
   3.228 +        context
   3.229 +      }
   3.230 +    }
   3.231 +  }
   3.232 +
   3.233 +
   3.234 +  /* activation */
   3.235 +
   3.236 +  def activate()
   3.237 +  {
   3.238 +    buffer.setTokenMarker(token_marker)
   3.239 +    buffer.addBufferListener(buffer_listener)
   3.240 +    buffer.propertiesChanged()
   3.241 +    pending_edits.init()
   3.242 +  }
   3.243 +
   3.244 +  def refresh()
   3.245 +  {
   3.246 +    buffer.setTokenMarker(token_marker)
   3.247 +  }
   3.248 +
   3.249 +  def deactivate()
   3.250 +  {
   3.251 +    pending_edits.flush()
   3.252 +    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
   3.253 +    buffer.removeBufferListener(buffer_listener)
   3.254 +  }
   3.255 +}
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 08 17:42:07 2011 +0200
     4.3 @@ -0,0 +1,587 @@
     4.4 +/*  Title:      Tools/jEdit/src/document_view.scala
     4.5 +    Author:     Fabian Immler, TU Munich
     4.6 +    Author:     Makarius
     4.7 +
     4.8 +Document view connected to jEdit text area.
     4.9 +*/
    4.10 +
    4.11 +package isabelle.jedit
    4.12 +
    4.13 +
    4.14 +import isabelle._
    4.15 +
    4.16 +import scala.actors.Actor._
    4.17 +
    4.18 +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
    4.19 +import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
    4.20 +  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
    4.21 +import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
    4.22 +import javax.swing.event.{CaretListener, CaretEvent}
    4.23 +import java.util.ArrayList
    4.24 +
    4.25 +import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
    4.26 +import org.gjt.sp.jedit.gui.RolloverButton
    4.27 +import org.gjt.sp.jedit.options.GutterOptionPane
    4.28 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
    4.29 +import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
    4.30 +
    4.31 +
    4.32 +object Document_View
    4.33 +{
    4.34 +  /* document view of text area */
    4.35 +
    4.36 +  private val key = new Object
    4.37 +
    4.38 +  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
    4.39 +  {
    4.40 +    Swing_Thread.require()
    4.41 +    val doc_view = new Document_View(model, text_area)
    4.42 +    text_area.putClientProperty(key, doc_view)
    4.43 +    doc_view.activate()
    4.44 +    doc_view
    4.45 +  }
    4.46 +
    4.47 +  def apply(text_area: JEditTextArea): Option[Document_View] =
    4.48 +  {
    4.49 +    Swing_Thread.require()
    4.50 +    text_area.getClientProperty(key) match {
    4.51 +      case doc_view: Document_View => Some(doc_view)
    4.52 +      case _ => None
    4.53 +    }
    4.54 +  }
    4.55 +
    4.56 +  def exit(text_area: JEditTextArea)
    4.57 +  {
    4.58 +    Swing_Thread.require()
    4.59 +    apply(text_area) match {
    4.60 +      case None =>
    4.61 +      case Some(doc_view) =>
    4.62 +        doc_view.deactivate()
    4.63 +        text_area.putClientProperty(key, null)
    4.64 +    }
    4.65 +  }
    4.66 +}
    4.67 +
    4.68 +
    4.69 +class Document_View(val model: Document_Model, text_area: JEditTextArea)
    4.70 +{
    4.71 +  private val session = model.session
    4.72 +
    4.73 +
    4.74 +  /** token handling **/
    4.75 +
    4.76 +  /* extended token styles */
    4.77 +
    4.78 +  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
    4.79 +
    4.80 +  def extend_styles()
    4.81 +  {
    4.82 +    Swing_Thread.require()
    4.83 +    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
    4.84 +  }
    4.85 +  extend_styles()
    4.86 +
    4.87 +  def set_styles()
    4.88 +  {
    4.89 +    Swing_Thread.require()
    4.90 +    text_area.getPainter.setStyles(styles)
    4.91 +  }
    4.92 +
    4.93 +
    4.94 +  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
    4.95 +
    4.96 +  def wrap_margin(): Int =
    4.97 +  {
    4.98 +    val buffer = text_area.getBuffer
    4.99 +    val painter = text_area.getPainter
   4.100 +    val font = painter.getFont
   4.101 +    val font_context = painter.getFontRenderContext
   4.102 +
   4.103 +    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
   4.104 +    val max = buffer.getIntegerProperty("maxLineLen", 0)
   4.105 +
   4.106 +    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
   4.107 +    else if (soft_wrap)
   4.108 +      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
   4.109 +    else 0
   4.110 +  }
   4.111 +
   4.112 +
   4.113 +  /* chunks */
   4.114 +
   4.115 +  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
   4.116 +  {
   4.117 +    import scala.collection.JavaConversions._
   4.118 +
   4.119 +    val buffer = text_area.getBuffer
   4.120 +    val painter = text_area.getPainter
   4.121 +    val margin = wrap_margin().toFloat
   4.122 +
   4.123 +    val out = new ArrayList[Chunk]
   4.124 +    val handler = new DisplayTokenHandler
   4.125 +
   4.126 +    var result = Map[Text.Offset, Chunk]()
   4.127 +    for (line <- physical_lines) {
   4.128 +      out.clear
   4.129 +      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
   4.130 +      buffer.markTokens(line, handler)
   4.131 +
   4.132 +      val line_start = buffer.getLineStartOffset(line)
   4.133 +      for (chunk <- handler.getChunkList.iterator)
   4.134 +        result += (line_start + chunk.offset -> chunk)
   4.135 +    }
   4.136 +    result
   4.137 +  }
   4.138 +
   4.139 +
   4.140 +  /* visible line ranges */
   4.141 +
   4.142 +  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
   4.143 +  // NB: jEdit already normalizes \r\n and \r to \n
   4.144 +  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
   4.145 +  {
   4.146 +    val stop = if (start < end) end - 1 else end min model.buffer.getLength
   4.147 +    Text.Range(start, stop)
   4.148 +  }
   4.149 +
   4.150 +  def screen_lines_range(): Text.Range =
   4.151 +  {
   4.152 +    val start = text_area.getScreenLineStartOffset(0)
   4.153 +    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
   4.154 +    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
   4.155 +  }
   4.156 +
   4.157 +  def invalidate_line_range(range: Text.Range)
   4.158 +  {
   4.159 +    text_area.invalidateLineRange(
   4.160 +      model.buffer.getLineOfOffset(range.start),
   4.161 +      model.buffer.getLineOfOffset(range.stop))
   4.162 +  }
   4.163 +
   4.164 +
   4.165 +  /* HTML popups */
   4.166 +
   4.167 +  private var html_popup: Option[Popup] = None
   4.168 +
   4.169 +  private def exit_popup() { html_popup.map(_.hide) }
   4.170 +
   4.171 +  private val html_panel =
   4.172 +    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   4.173 +  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
   4.174 +
   4.175 +  private def html_panel_resize()
   4.176 +  {
   4.177 +    Swing_Thread.now {
   4.178 +      html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   4.179 +    }
   4.180 +  }
   4.181 +
   4.182 +  private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
   4.183 +  {
   4.184 +    exit_popup()
   4.185 +/* FIXME broken
   4.186 +    val offset = text_area.xyToOffset(x, y)
   4.187 +    val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
   4.188 +
   4.189 +    // FIXME snapshot.cumulate
   4.190 +    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
   4.191 +      case Text.Info(_, Some(msg)) #:: _ =>
   4.192 +        val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
   4.193 +        html_panel.render_sync(List(msg))
   4.194 +        Thread.sleep(10)  // FIXME !?
   4.195 +        popup.show
   4.196 +        html_popup = Some(popup)
   4.197 +      case _ =>
   4.198 +    }
   4.199 +*/
   4.200 +  }
   4.201 +
   4.202 +
   4.203 +  /* subexpression highlighting */
   4.204 +
   4.205 +  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
   4.206 +    : Option[(Text.Range, Color)] =
   4.207 +  {
   4.208 +    val offset = text_area.xyToOffset(x, y)
   4.209 +    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
   4.210 +      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
   4.211 +      case _ => None
   4.212 +    }
   4.213 +  }
   4.214 +
   4.215 +  private var highlight_range: Option[(Text.Range, Color)] = None
   4.216 +
   4.217 +
   4.218 +  /* CONTROL-mouse management */
   4.219 +
   4.220 +  private var control: Boolean = false
   4.221 +
   4.222 +  private def exit_control()
   4.223 +  {
   4.224 +    exit_popup()
   4.225 +    highlight_range = None
   4.226 +  }
   4.227 +
   4.228 +  private val focus_listener = new FocusAdapter {
   4.229 +    override def focusLost(e: FocusEvent) {
   4.230 +      highlight_range = None // FIXME exit_control !?
   4.231 +    }
   4.232 +  }
   4.233 +
   4.234 +  private val window_listener = new WindowAdapter {
   4.235 +    override def windowIconified(e: WindowEvent) { exit_control() }
   4.236 +    override def windowDeactivated(e: WindowEvent) { exit_control() }
   4.237 +  }
   4.238 +
   4.239 +  private val mouse_motion_listener = new MouseMotionAdapter {
   4.240 +    override def mouseMoved(e: MouseEvent) {
   4.241 +      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
   4.242 +      val x = e.getX()
   4.243 +      val y = e.getY()
   4.244 +
   4.245 +      if (!model.buffer.isLoaded) exit_control()
   4.246 +      else
   4.247 +        Isabelle.swing_buffer_lock(model.buffer) {
   4.248 +          val snapshot = model.snapshot
   4.249 +
   4.250 +          if (control) init_popup(snapshot, x, y)
   4.251 +
   4.252 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   4.253 +          highlight_range = if (control) subexp_range(snapshot, x, y) else None
   4.254 +          highlight_range map { case (range, _) => invalidate_line_range(range) }
   4.255 +        }
   4.256 +    }
   4.257 +  }
   4.258 +
   4.259 +
   4.260 +  /* TextArea painters */
   4.261 +
   4.262 +  private val background_painter = new TextAreaExtension
   4.263 +  {
   4.264 +    override def paintScreenLineRange(gfx: Graphics2D,
   4.265 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
   4.266 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   4.267 +    {
   4.268 +      Isabelle.swing_buffer_lock(model.buffer) {
   4.269 +        val snapshot = model.snapshot()
   4.270 +        val ascent = text_area.getPainter.getFontMetrics.getAscent
   4.271 +
   4.272 +        for (i <- 0 until physical_lines.length) {
   4.273 +          if (physical_lines(i) != -1) {
   4.274 +            val line_range = proper_line_range(start(i), end(i))
   4.275 +
   4.276 +            // background color: status
   4.277 +            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
   4.278 +            for {
   4.279 +              (command, command_start) <- cmds if !command.is_ignored
   4.280 +              val range = line_range.restrict(snapshot.convert(command.range + command_start))
   4.281 +              r <- Isabelle.gfx_range(text_area, range)
   4.282 +              color <- Isabelle_Markup.status_color(snapshot, command)
   4.283 +            } {
   4.284 +              gfx.setColor(color)
   4.285 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   4.286 +            }
   4.287 +
   4.288 +            // background color (1): markup
   4.289 +            for {
   4.290 +              Text.Info(range, Some(color)) <-
   4.291 +                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
   4.292 +              r <- Isabelle.gfx_range(text_area, range)
   4.293 +            } {
   4.294 +              gfx.setColor(color)
   4.295 +              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
   4.296 +            }
   4.297 +
   4.298 +            // background color (2): markup
   4.299 +            for {
   4.300 +              Text.Info(range, Some(color)) <-
   4.301 +                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
   4.302 +              r <- Isabelle.gfx_range(text_area, range)
   4.303 +            } {
   4.304 +              gfx.setColor(color)
   4.305 +              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
   4.306 +            }
   4.307 +
   4.308 +            // sub-expression highlighting -- potentially from other snapshot
   4.309 +            highlight_range match {
   4.310 +              case Some((range, color)) if line_range.overlaps(range) =>
   4.311 +                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
   4.312 +                  case None =>
   4.313 +                  case Some(r) =>
   4.314 +                    gfx.setColor(color)
   4.315 +                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
   4.316 +                }
   4.317 +              case _ =>
   4.318 +            }
   4.319 +
   4.320 +            // squiggly underline
   4.321 +            for {
   4.322 +              Text.Info(range, Some(color)) <-
   4.323 +                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
   4.324 +              r <- Isabelle.gfx_range(text_area, range)
   4.325 +            } {
   4.326 +              gfx.setColor(color)
   4.327 +              val x0 = (r.x / 2) * 2
   4.328 +              val y0 = r.y + ascent + 1
   4.329 +              for (x1 <- Range(x0, x0 + r.length, 2)) {
   4.330 +                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
   4.331 +                gfx.drawLine(x1, y1, x1 + 1, y1)
   4.332 +              }
   4.333 +            }
   4.334 +          }
   4.335 +        }
   4.336 +      }
   4.337 +    }
   4.338 +
   4.339 +    override def getToolTipText(x: Int, y: Int): String =
   4.340 +    {
   4.341 +      Isabelle.swing_buffer_lock(model.buffer) {
   4.342 +        val snapshot = model.snapshot()
   4.343 +        val offset = text_area.xyToOffset(x, y)
   4.344 +        if (control) {
   4.345 +          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
   4.346 +          {
   4.347 +            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   4.348 +            case _ => null
   4.349 +          }
   4.350 +        }
   4.351 +        else {
   4.352 +          // FIXME snapshot.cumulate
   4.353 +          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
   4.354 +          {
   4.355 +            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
   4.356 +            case _ => null
   4.357 +          }
   4.358 +        }
   4.359 +      }
   4.360 +    }
   4.361 +  }
   4.362 +
   4.363 +  var use_text_painter = false
   4.364 +
   4.365 +  private val text_painter = new TextAreaExtension
   4.366 +  {
   4.367 +    override def paintScreenLineRange(gfx: Graphics2D,
   4.368 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
   4.369 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   4.370 +    {
   4.371 +      if (use_text_painter) {
   4.372 +        Isabelle.swing_buffer_lock(model.buffer) {
   4.373 +          val painter = text_area.getPainter
   4.374 +          val fm = painter.getFontMetrics
   4.375 +
   4.376 +          val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
   4.377 +
   4.378 +          val x0 = text_area.getHorizontalOffset
   4.379 +          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
   4.380 +          for (i <- 0 until physical_lines.length) {
   4.381 +            if (physical_lines(i) != -1) {
   4.382 +              all_chunks.get(start(i)) match {
   4.383 +                case Some(chunk) =>
   4.384 +                  Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
   4.385 +                case None =>
   4.386 +              }
   4.387 +            }
   4.388 +            y0 += line_height
   4.389 +          }
   4.390 +        }
   4.391 +      }
   4.392 +    }
   4.393 +  }
   4.394 +
   4.395 +  private val gutter_painter = new TextAreaExtension
   4.396 +  {
   4.397 +    override def paintScreenLineRange(gfx: Graphics2D,
   4.398 +      first_line: Int, last_line: Int, physical_lines: Array[Int],
   4.399 +      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
   4.400 +    {
   4.401 +      val gutter = text_area.getGutter
   4.402 +      val width = GutterOptionPane.getSelectionAreaWidth
   4.403 +      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
   4.404 +      val FOLD_MARKER_SIZE = 12
   4.405 +
   4.406 +      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
   4.407 +        Isabelle.swing_buffer_lock(model.buffer) {
   4.408 +          val snapshot = model.snapshot()
   4.409 +          for (i <- 0 until physical_lines.length) {
   4.410 +            if (physical_lines(i) != -1) {
   4.411 +              val line_range = proper_line_range(start(i), end(i))
   4.412 +
   4.413 +              // gutter icons
   4.414 +              val icons =
   4.415 +                (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
   4.416 +                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
   4.417 +                yield icon).toList.sortWith(_ >= _)
   4.418 +              icons match {
   4.419 +                case icon :: _ =>
   4.420 +                  val icn = icon.icon
   4.421 +                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
   4.422 +                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
   4.423 +                  icn.paintIcon(gutter, gfx, x0, y0)
   4.424 +                case Nil =>
   4.425 +              }
   4.426 +            }
   4.427 +          }
   4.428 +        }
   4.429 +      }
   4.430 +    }
   4.431 +  }
   4.432 +
   4.433 +
   4.434 +  /* caret handling */
   4.435 +
   4.436 +  def selected_command(): Option[Command] =
   4.437 +  {
   4.438 +    Swing_Thread.require()
   4.439 +    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
   4.440 +  }
   4.441 +
   4.442 +  private val caret_listener = new CaretListener {
   4.443 +    private val delay = Swing_Thread.delay_last(session.input_delay) {
   4.444 +      session.perspective.event(Session.Perspective)
   4.445 +    }
   4.446 +    override def caretUpdate(e: CaretEvent) { delay() }
   4.447 +  }
   4.448 +
   4.449 +
   4.450 +  /* overview of command status left of scrollbar */
   4.451 +
   4.452 +  private val overview = new JPanel(new BorderLayout)
   4.453 +  {
   4.454 +    private val WIDTH = 10
   4.455 +    private val HEIGHT = 2
   4.456 +
   4.457 +    setPreferredSize(new Dimension(WIDTH, 0))
   4.458 +
   4.459 +    setRequestFocusEnabled(false)
   4.460 +
   4.461 +    addMouseListener(new MouseAdapter {
   4.462 +      override def mousePressed(event: MouseEvent) {
   4.463 +        val line = y_to_line(event.getY)
   4.464 +        if (line >= 0 && line < text_area.getLineCount)
   4.465 +          text_area.setCaretPosition(text_area.getLineStartOffset(line))
   4.466 +      }
   4.467 +    })
   4.468 +
   4.469 +    override def addNotify() {
   4.470 +      super.addNotify()
   4.471 +      ToolTipManager.sharedInstance.registerComponent(this)
   4.472 +    }
   4.473 +
   4.474 +    override def removeNotify() {
   4.475 +      ToolTipManager.sharedInstance.unregisterComponent(this)
   4.476 +      super.removeNotify
   4.477 +    }
   4.478 +
   4.479 +    override def paintComponent(gfx: Graphics)
   4.480 +    {
   4.481 +      super.paintComponent(gfx)
   4.482 +      Swing_Thread.assert()
   4.483 +
   4.484 +      val buffer = model.buffer
   4.485 +      Isabelle.buffer_lock(buffer) {
   4.486 +        val snapshot = model.snapshot()
   4.487 +
   4.488 +        def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
   4.489 +        {
   4.490 +          try {
   4.491 +            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
   4.492 +            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
   4.493 +            Some((line1, line2))
   4.494 +          }
   4.495 +          catch { case e: ArrayIndexOutOfBoundsException => None }
   4.496 +        }
   4.497 +        for {
   4.498 +          (command, start) <- snapshot.node.command_starts
   4.499 +          if !command.is_ignored
   4.500 +          (line1, line2) <- line_range(command, start)
   4.501 +          val y = line_to_y(line1)
   4.502 +          val height = HEIGHT * (line2 - line1)
   4.503 +          color <- Isabelle_Markup.overview_color(snapshot, command)
   4.504 +        } {
   4.505 +          gfx.setColor(color)
   4.506 +          gfx.fillRect(0, y, getWidth - 1, height)
   4.507 +        }
   4.508 +      }
   4.509 +    }
   4.510 +
   4.511 +    private def line_to_y(line: Int): Int =
   4.512 +      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
   4.513 +
   4.514 +    private def y_to_line(y: Int): Int =
   4.515 +      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
   4.516 +  }
   4.517 +
   4.518 +
   4.519 +  /* main actor */
   4.520 +
   4.521 +  private val main_actor = actor {
   4.522 +    loop {
   4.523 +      react {
   4.524 +        case Session.Commands_Changed(changed) =>
   4.525 +          val buffer = model.buffer
   4.526 +          Isabelle.swing_buffer_lock(buffer) {
   4.527 +            val snapshot = model.snapshot()
   4.528 +
   4.529 +            if (changed.exists(snapshot.node.commands.contains))
   4.530 +              overview.repaint()
   4.531 +
   4.532 +            val visible_range = screen_lines_range()
   4.533 +            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
   4.534 +            if (visible_cmds.exists(changed)) {
   4.535 +              for {
   4.536 +                line <- 0 until text_area.getVisibleLines
   4.537 +                val start = text_area.getScreenLineStartOffset(line) if start >= 0
   4.538 +                val end = text_area.getScreenLineEndOffset(line) if end >= 0
   4.539 +                val range = proper_line_range(start, end)
   4.540 +                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
   4.541 +                if line_cmds.exists(changed)
   4.542 +              } text_area.invalidateScreenLineRange(line, line)
   4.543 +
   4.544 +              // FIXME danger of deadlock!?
   4.545 +              // FIXME potentially slow!?
   4.546 +              model.buffer.propertiesChanged()
   4.547 +            }
   4.548 +          }
   4.549 +
   4.550 +        case Session.Global_Settings => html_panel_resize()
   4.551 +
   4.552 +        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
   4.553 +      }
   4.554 +    }
   4.555 +  }
   4.556 +
   4.557 +
   4.558 +  /* activation */
   4.559 +
   4.560 +  private def activate()
   4.561 +  {
   4.562 +    val painter = text_area.getPainter
   4.563 +    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
   4.564 +    painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
   4.565 +    text_area.getGutter.addExtension(gutter_painter)
   4.566 +    text_area.addFocusListener(focus_listener)
   4.567 +    text_area.getView.addWindowListener(window_listener)
   4.568 +    painter.addMouseMotionListener(mouse_motion_listener)
   4.569 +    text_area.addCaretListener(caret_listener)
   4.570 +    text_area.addLeftOfScrollBar(overview)
   4.571 +    session.commands_changed += main_actor
   4.572 +    session.global_settings += main_actor
   4.573 +  }
   4.574 +
   4.575 +  private def deactivate()
   4.576 +  {
   4.577 +    val painter = text_area.getPainter
   4.578 +    session.commands_changed -= main_actor
   4.579 +    session.global_settings -= main_actor
   4.580 +    text_area.removeFocusListener(focus_listener)
   4.581 +    text_area.getView.removeWindowListener(window_listener)
   4.582 +    painter.removeMouseMotionListener(mouse_motion_listener)
   4.583 +    text_area.removeCaretListener(caret_listener)
   4.584 +    text_area.removeLeftOfScrollBar(overview)
   4.585 +    text_area.getGutter.removeExtension(gutter_painter)
   4.586 +    painter.removeExtension(text_painter)
   4.587 +    painter.removeExtension(background_painter)
   4.588 +    exit_popup()
   4.589 +  }
   4.590 +}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Wed Jun 08 17:42:07 2011 +0200
     5.3 @@ -0,0 +1,206 @@
     5.4 +/*  Title:      Tools/jEdit/src/html_panel.scala
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +HTML panel based on Lobo/Cobra.
     5.8 +*/
     5.9 +
    5.10 +package isabelle.jedit
    5.11 +
    5.12 +
    5.13 +import isabelle._
    5.14 +
    5.15 +import java.io.StringReader
    5.16 +import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
    5.17 +import java.awt.event.MouseEvent
    5.18 +
    5.19 +import java.util.logging.{Logger, Level}
    5.20 +
    5.21 +import org.w3c.dom.html2.HTMLElement
    5.22 +
    5.23 +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
    5.24 +import org.lobobrowser.html.gui.HtmlPanel
    5.25 +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
    5.26 +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
    5.27 +
    5.28 +import scala.actors.Actor._
    5.29 +
    5.30 +
    5.31 +object HTML_Panel
    5.32 +{
    5.33 +  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
    5.34 +  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
    5.35 +  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    5.36 +  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
    5.37 +  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
    5.38 +  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
    5.39 +}
    5.40 +
    5.41 +
    5.42 +class HTML_Panel(
    5.43 +    system: Isabelle_System,
    5.44 +    initial_font_family: String,
    5.45 +    initial_font_size: Int)
    5.46 +  extends HtmlPanel
    5.47 +{
    5.48 +  /** Lobo setup **/
    5.49 +
    5.50 +  /* global logging */
    5.51 +
    5.52 +  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
    5.53 +
    5.54 +
    5.55 +  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
    5.56 +
    5.57 +  val screen_resolution =
    5.58 +    if (GraphicsEnvironment.isHeadless()) 72
    5.59 +    else Toolkit.getDefaultToolkit().getScreenResolution()
    5.60 +
    5.61 +  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
    5.62 +  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
    5.63 +
    5.64 +
    5.65 +  /* contexts and event handling */
    5.66 +
    5.67 +  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
    5.68 +
    5.69 +  private val ucontext = new SimpleUserAgentContext
    5.70 +  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
    5.71 +  {
    5.72 +    private def handle(event: HTML_Panel.Event): Boolean =
    5.73 +      if (handler.isDefinedAt(event)) { handler(event); false }
    5.74 +      else true
    5.75 +
    5.76 +    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
    5.77 +      handle(HTML_Panel.Context_Menu(elem, event))
    5.78 +    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
    5.79 +      handle(HTML_Panel.Mouse_Click(elem, event))
    5.80 +    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
    5.81 +      handle(HTML_Panel.Double_Click(elem, event))
    5.82 +    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
    5.83 +      { handle(HTML_Panel.Mouse_Over(elem, event)) }
    5.84 +    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
    5.85 +      { handle(HTML_Panel.Mouse_Out(elem, event)) }
    5.86 +  }
    5.87 +
    5.88 +  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
    5.89 +
    5.90 +
    5.91 +  /* document template with style sheets */
    5.92 +
    5.93 +  private val template_head =
    5.94 +    """<?xml version="1.0" encoding="utf-8"?>
    5.95 +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
    5.96 +  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
    5.97 +<html xmlns="http://www.w3.org/1999/xhtml">
    5.98 +<head>
    5.99 +<style media="all" type="text/css">
   5.100 +""" +
   5.101 +  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
   5.102 +
   5.103 +  private val template_tail =
   5.104 +"""
   5.105 +</style>
   5.106 +</head>
   5.107 +<body/>
   5.108 +</html>
   5.109 +"""
   5.110 +
   5.111 +  private def template(font_family: String, font_size: Int): String =
   5.112 +    template_head +
   5.113 +    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
   5.114 +    template_tail
   5.115 +
   5.116 +
   5.117 +  /** main actor **/
   5.118 +
   5.119 +  /* internal messages */
   5.120 +
   5.121 +  private case class Resize(font_family: String, font_size: Int)
   5.122 +  private case class Render_Document(text: String)
   5.123 +  private case class Render(body: XML.Body)
   5.124 +  private case class Render_Sync(body: XML.Body)
   5.125 +  private case object Refresh
   5.126 +
   5.127 +  private val main_actor = actor {
   5.128 +
   5.129 +    /* internal state */
   5.130 +
   5.131 +    var current_font_metrics: FontMetrics = null
   5.132 +    var current_font_family = ""
   5.133 +    var current_font_size: Int = 0
   5.134 +    var current_margin: Int = 0
   5.135 +    var current_body: XML.Body = Nil
   5.136 +
   5.137 +    def resize(font_family: String, font_size: Int)
   5.138 +    {
   5.139 +      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
   5.140 +      val (font_metrics, margin) =
   5.141 +        Swing_Thread.now {
   5.142 +          val metrics = getFontMetrics(font)
   5.143 +          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
   5.144 +        }
   5.145 +      if (current_font_metrics == null ||
   5.146 +          current_font_family != font_family ||
   5.147 +          current_font_size != font_size ||
   5.148 +          current_margin != margin)
   5.149 +      {
   5.150 +        current_font_metrics = font_metrics
   5.151 +        current_font_family = font_family
   5.152 +        current_font_size = font_size
   5.153 +        current_margin = margin
   5.154 +        refresh()
   5.155 +      }
   5.156 +    }
   5.157 +
   5.158 +    def refresh() { render(current_body) }
   5.159 +
   5.160 +    def render_document(text: String)
   5.161 +    {
   5.162 +      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
   5.163 +      Swing_Thread.later { setDocument(doc, rcontext) }
   5.164 +    }
   5.165 +
   5.166 +    def render(body: XML.Body)
   5.167 +    {
   5.168 +      current_body = body
   5.169 +      val html_body =
   5.170 +        current_body.flatMap(div =>
   5.171 +          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
   5.172 +            .map(t =>
   5.173 +              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
   5.174 +                HTML.spans(t, true))))
   5.175 +      val doc =
   5.176 +        builder.parse(
   5.177 +          new InputSourceImpl(
   5.178 +            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
   5.179 +      doc.removeChild(doc.getLastChild())
   5.180 +      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
   5.181 +      Swing_Thread.later { setDocument(doc, rcontext) }
   5.182 +    }
   5.183 +
   5.184 +
   5.185 +    /* main loop */
   5.186 +
   5.187 +    resize(initial_font_family, initial_font_size)
   5.188 +
   5.189 +    loop {
   5.190 +      react {
   5.191 +        case Resize(font_family, font_size) => resize(font_family, font_size)
   5.192 +        case Refresh => refresh()
   5.193 +        case Render_Document(text) => render_document(text)
   5.194 +        case Render(body) => render(body)
   5.195 +        case Render_Sync(body) => render(body); reply(())
   5.196 +        case bad => System.err.println("main_actor: ignoring bad message " + bad)
   5.197 +      }
   5.198 +    }
   5.199 +  }
   5.200 +
   5.201 +
   5.202 +  /* external methods */
   5.203 +
   5.204 +  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   5.205 +  def refresh() { main_actor ! Refresh }
   5.206 +  def render_document(text: String) { main_actor ! Render_Document(text) }
   5.207 +  def render(body: XML.Body) { main_actor ! Render(body) }
   5.208 +  def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
   5.209 +}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala	Wed Jun 08 17:42:07 2011 +0200
     6.3 @@ -0,0 +1,65 @@
     6.4 +/*  Title:      Tools/jEdit/src/isabelle_encoding.scala
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +Isabelle encoding -- based on UTF-8.
     6.8 +*/
     6.9 +
    6.10 +package isabelle.jedit
    6.11 +
    6.12 +
    6.13 +import isabelle._
    6.14 +
    6.15 +import org.gjt.sp.jedit.io.Encoding
    6.16 +import org.gjt.sp.jedit.buffer.JEditBuffer
    6.17 +
    6.18 +import java.nio.charset.{Charset, CodingErrorAction}
    6.19 +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
    6.20 +  CharArrayReader, ByteArrayOutputStream}
    6.21 +
    6.22 +import scala.io.{Codec, Source, BufferedSource}
    6.23 +
    6.24 +
    6.25 +object Isabelle_Encoding
    6.26 +{
    6.27 +  val NAME = "UTF-8-Isabelle"
    6.28 +
    6.29 +  def is_active(buffer: JEditBuffer): Boolean =
    6.30 +    buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
    6.31 +}
    6.32 +
    6.33 +class Isabelle_Encoding extends Encoding
    6.34 +{
    6.35 +  private val charset = Charset.forName(Standard_System.charset)
    6.36 +  val BUFSIZE = 32768
    6.37 +
    6.38 +  private def text_reader(in: InputStream, codec: Codec): Reader =
    6.39 +  {
    6.40 +    val source = new BufferedSource(in)(codec)
    6.41 +    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
    6.42 +  }
    6.43 +
    6.44 +  override def getTextReader(in: InputStream): Reader =
    6.45 +    text_reader(in, Standard_System.codec())
    6.46 +
    6.47 +  override def getPermissiveTextReader(in: InputStream): Reader =
    6.48 +  {
    6.49 +    val codec = Standard_System.codec()
    6.50 +    codec.onMalformedInput(CodingErrorAction.REPLACE)
    6.51 +    codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
    6.52 +    text_reader(in, codec)
    6.53 +  }
    6.54 +
    6.55 +  override def getTextWriter(out: OutputStream): Writer =
    6.56 +  {
    6.57 +    val buffer = new ByteArrayOutputStream(BUFSIZE) {
    6.58 +      override def flush()
    6.59 +      {
    6.60 +        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
    6.61 +        out.write(text.getBytes(Standard_System.charset))
    6.62 +        out.flush()
    6.63 +      }
    6.64 +      override def close() { out.close() }
    6.65 +    }
    6.66 +    new OutputStreamWriter(buffer, charset.newEncoder())
    6.67 +  }
    6.68 +}
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala	Wed Jun 08 17:42:07 2011 +0200
     7.3 @@ -0,0 +1,88 @@
     7.4 +/*  Title:      Tools/jEdit/src/isabelle_hyperlinks.scala
     7.5 +    Author:     Fabian Immler, TU Munich
     7.6 +
     7.7 +Hyperlink setup for Isabelle proof documents.
     7.8 +*/
     7.9 +
    7.10 +package isabelle.jedit
    7.11 +
    7.12 +
    7.13 +import isabelle._
    7.14 +
    7.15 +import java.io.File
    7.16 +
    7.17 +import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
    7.18 +
    7.19 +import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
    7.20 +
    7.21 +
    7.22 +private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
    7.23 +  extends AbstractHyperlink(start, end, line, "")
    7.24 +{
    7.25 +  override def click(view: View) {
    7.26 +    view.getTextArea.moveCaretPosition(def_offset)
    7.27 +  }
    7.28 +}
    7.29 +
    7.30 +class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
    7.31 +  extends AbstractHyperlink(start, end, line, "")
    7.32 +{
    7.33 +  override def click(view: View) = {
    7.34 +    Isabelle.system.source_file(def_file) match {
    7.35 +      case None =>
    7.36 +        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
    7.37 +      case Some(file) =>
    7.38 +        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
    7.39 +    }
    7.40 +  }
    7.41 +}
    7.42 +
    7.43 +class Isabelle_Hyperlinks extends HyperlinkSource
    7.44 +{
    7.45 +  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
    7.46 +  {
    7.47 +    Swing_Thread.assert()
    7.48 +    Isabelle.buffer_lock(buffer) {
    7.49 +      Document_Model(buffer) match {
    7.50 +        case Some(model) =>
    7.51 +          val snapshot = model.snapshot()
    7.52 +          val markup =
    7.53 +            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
    7.54 +              // FIXME Isar_Document.Hyperlink extractor
    7.55 +              case Text.Info(info_range,
    7.56 +                  XML.Elem(Markup(Markup.ENTITY, props), _))
    7.57 +                if (props.find(
    7.58 +                  { case (Markup.KIND, Markup.ML_OPEN) => true
    7.59 +                    case (Markup.KIND, Markup.ML_STRUCT) => true
    7.60 +                    case _ => false }).isEmpty) =>
    7.61 +                val Text.Range(begin, end) = info_range
    7.62 +                val line = buffer.getLineOfOffset(begin)
    7.63 +                (Position.File.unapply(props), Position.Line.unapply(props)) match {
    7.64 +                  case (Some(def_file), Some(def_line)) =>
    7.65 +                    new External_Hyperlink(begin, end, line, def_file, def_line)
    7.66 +                  case _ =>
    7.67 +                    (props, props) match {
    7.68 +                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
    7.69 +                        snapshot.lookup_command(def_id) match {
    7.70 +                          case Some(def_cmd) =>
    7.71 +                            snapshot.node.command_start(def_cmd) match {
    7.72 +                              case Some(def_cmd_start) =>
    7.73 +                                new Internal_Hyperlink(begin, end, line,
    7.74 +                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
    7.75 +                              case None => null
    7.76 +                            }
    7.77 +                          case None => null
    7.78 +                        }
    7.79 +                      case _ => null
    7.80 +                    }
    7.81 +                }
    7.82 +            }
    7.83 +          markup match {
    7.84 +            case Text.Info(_, Some(link)) #:: _ => link
    7.85 +            case _ => null
    7.86 +          }
    7.87 +        case None => null
    7.88 +      }
    7.89 +    }
    7.90 +  }
    7.91 +}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Wed Jun 08 17:42:07 2011 +0200
     8.3 @@ -0,0 +1,216 @@
     8.4 +/*  Title:      Tools/jEdit/src/isabelle_markup.scala
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +Isabelle specific physical rendering and markup selection.
     8.8 +*/
     8.9 +
    8.10 +package isabelle.jedit
    8.11 +
    8.12 +
    8.13 +import isabelle._
    8.14 +
    8.15 +import java.awt.Color
    8.16 +
    8.17 +import org.gjt.sp.jedit.syntax.Token
    8.18 +
    8.19 +
    8.20 +object Isabelle_Markup
    8.21 +{
    8.22 +  /* physical rendering */
    8.23 +
    8.24 +  val outdated_color = new Color(240, 240, 240)
    8.25 +  val unfinished_color = new Color(255, 228, 225)
    8.26 +
    8.27 +  val light_color = new Color(240, 240, 240)
    8.28 +  val regular_color = new Color(192, 192, 192)
    8.29 +  val warning_color = new Color(255, 140, 0)
    8.30 +  val error_color = new Color(178, 34, 34)
    8.31 +  val bad_color = new Color(255, 106, 106, 100)
    8.32 +  val hilite_color = new Color(255, 204, 102, 100)
    8.33 +
    8.34 +  class Icon(val priority: Int, val icon: javax.swing.Icon)
    8.35 +  {
    8.36 +    def >= (that: Icon): Boolean = this.priority >= that.priority
    8.37 +  }
    8.38 +  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
    8.39 +  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
    8.40 +
    8.41 +
    8.42 +  /* command status */
    8.43 +
    8.44 +  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    8.45 +  {
    8.46 +    val state = snapshot.state(command)
    8.47 +    if (snapshot.is_outdated) Some(outdated_color)
    8.48 +    else
    8.49 +      Isar_Document.command_status(state.status) match {
    8.50 +        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
    8.51 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    8.52 +        case _ => None
    8.53 +      }
    8.54 +  }
    8.55 +
    8.56 +  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
    8.57 +  {
    8.58 +    val state = snapshot.state(command)
    8.59 +    if (snapshot.is_outdated) None
    8.60 +    else
    8.61 +      Isar_Document.command_status(state.status) match {
    8.62 +        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
    8.63 +        case Isar_Document.Unprocessed => Some(unfinished_color)
    8.64 +        case Isar_Document.Failed => Some(error_color)
    8.65 +        case Isar_Document.Finished =>
    8.66 +          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
    8.67 +          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
    8.68 +          else None
    8.69 +      }
    8.70 +  }
    8.71 +
    8.72 +
    8.73 +  /* markup selectors */
    8.74 +
    8.75 +  val message: Markup_Tree.Select[Color] =
    8.76 +  {
    8.77 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
    8.78 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
    8.79 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
    8.80 +  }
    8.81 +
    8.82 +  val popup: Markup_Tree.Select[String] =
    8.83 +  {
    8.84 +    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
    8.85 +    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
    8.86 +      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
    8.87 +  }
    8.88 +
    8.89 +  val gutter_message: Markup_Tree.Select[Icon] =
    8.90 +  {
    8.91 +    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
    8.92 +    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
    8.93 +  }
    8.94 +
    8.95 +  val background1: Markup_Tree.Select[Color] =
    8.96 +  {
    8.97 +    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
    8.98 +    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
    8.99 +  }
   8.100 +
   8.101 +  val background2: Markup_Tree.Select[Color] =
   8.102 +  {
   8.103 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   8.104 +  }
   8.105 +
   8.106 +  val tooltip: Markup_Tree.Select[String] =
   8.107 +  {
   8.108 +    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
   8.109 +    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
   8.110 +      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
   8.111 +        margin = Isabelle.Int_Property("tooltip-margin"))
   8.112 +    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
   8.113 +    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
   8.114 +    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
   8.115 +    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
   8.116 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
   8.117 +    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
   8.118 +    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
   8.119 +    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
   8.120 +    case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
   8.121 +    case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
   8.122 +    case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
   8.123 +  }
   8.124 +
   8.125 +  private val subexp_include =
   8.126 +    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
   8.127 +      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
   8.128 +      Markup.TFREE, Markup.TVAR)
   8.129 +
   8.130 +  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
   8.131 +  {
   8.132 +    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
   8.133 +      (range, Color.black)
   8.134 +  }
   8.135 +
   8.136 +
   8.137 +  /* token markup -- text styles */
   8.138 +
   8.139 +  private val command_style: Map[String, Byte] =
   8.140 +  {
   8.141 +    import Token._
   8.142 +    Map[String, Byte](
   8.143 +      Keyword.THY_END -> KEYWORD2,
   8.144 +      Keyword.THY_SCRIPT -> LABEL,
   8.145 +      Keyword.PRF_SCRIPT -> LABEL,
   8.146 +      Keyword.PRF_ASM -> KEYWORD3,
   8.147 +      Keyword.PRF_ASM_GOAL -> KEYWORD3
   8.148 +    ).withDefaultValue(KEYWORD1)
   8.149 +  }
   8.150 +
   8.151 +  private val token_style: Map[String, Byte] =
   8.152 +  {
   8.153 +    import Token._
   8.154 +    Map[String, Byte](
   8.155 +      // logical entities
   8.156 +      Markup.TCLASS -> NULL,
   8.157 +      Markup.TYCON -> NULL,
   8.158 +      Markup.FIXED -> NULL,
   8.159 +      Markup.CONST -> LITERAL2,
   8.160 +      Markup.DYNAMIC_FACT -> LABEL,
   8.161 +      // inner syntax
   8.162 +      Markup.TFREE -> NULL,
   8.163 +      Markup.FREE -> MARKUP,
   8.164 +      Markup.TVAR -> NULL,
   8.165 +      Markup.SKOLEM -> COMMENT2,
   8.166 +      Markup.BOUND -> LABEL,
   8.167 +      Markup.VAR -> NULL,
   8.168 +      Markup.NUM -> DIGIT,
   8.169 +      Markup.FLOAT -> DIGIT,
   8.170 +      Markup.XNUM -> DIGIT,
   8.171 +      Markup.XSTR -> LITERAL4,
   8.172 +      Markup.LITERAL -> OPERATOR,
   8.173 +      Markup.INNER_COMMENT -> COMMENT1,
   8.174 +      Markup.SORT -> NULL,
   8.175 +      Markup.TYP -> NULL,
   8.176 +      Markup.TERM -> NULL,
   8.177 +      Markup.PROP -> NULL,
   8.178 +      // ML syntax
   8.179 +      Markup.ML_KEYWORD -> KEYWORD1,
   8.180 +      Markup.ML_DELIMITER -> OPERATOR,
   8.181 +      Markup.ML_IDENT -> NULL,
   8.182 +      Markup.ML_TVAR -> NULL,
   8.183 +      Markup.ML_NUMERAL -> DIGIT,
   8.184 +      Markup.ML_CHAR -> LITERAL1,
   8.185 +      Markup.ML_STRING -> LITERAL1,
   8.186 +      Markup.ML_COMMENT -> COMMENT1,
   8.187 +      Markup.ML_MALFORMED -> INVALID,
   8.188 +      // embedded source text
   8.189 +      Markup.ML_SOURCE -> COMMENT3,
   8.190 +      Markup.DOC_SOURCE -> COMMENT3,
   8.191 +      Markup.ANTIQ -> COMMENT4,
   8.192 +      Markup.ML_ANTIQ -> COMMENT4,
   8.193 +      Markup.DOC_ANTIQ -> COMMENT4,
   8.194 +      // outer syntax
   8.195 +      Markup.KEYWORD -> KEYWORD2,
   8.196 +      Markup.OPERATOR -> OPERATOR,
   8.197 +      Markup.COMMAND -> KEYWORD1,
   8.198 +      Markup.IDENT -> NULL,
   8.199 +      Markup.VERBATIM -> COMMENT3,
   8.200 +      Markup.COMMENT -> COMMENT1,
   8.201 +      Markup.CONTROL -> COMMENT3,
   8.202 +      Markup.MALFORMED -> INVALID,
   8.203 +      Markup.STRING -> LITERAL3,
   8.204 +      Markup.ALTSTRING -> LITERAL1
   8.205 +    ).withDefaultValue(NULL)
   8.206 +  }
   8.207 +
   8.208 +  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
   8.209 +  {
   8.210 +    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
   8.211 +    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
   8.212 +
   8.213 +    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
   8.214 +    if token_style(kind) != Token.NULL => token_style(kind)
   8.215 +
   8.216 +    case Text.Info(_, XML.Elem(Markup(name, _), _))
   8.217 +    if token_style(name) != Token.NULL => token_style(name)
   8.218 +  }
   8.219 +}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Wed Jun 08 17:42:07 2011 +0200
     9.3 @@ -0,0 +1,67 @@
     9.4 +/*  Title:      Tools/jEdit/src/isabelle_options.scala
     9.5 +    Author:     Johannes Hölzl, TU Munich
     9.6 +
     9.7 +Editor pane for plugin options.
     9.8 +*/
     9.9 +
    9.10 +package isabelle.jedit
    9.11 +
    9.12 +
    9.13 +import isabelle._
    9.14 +
    9.15 +import javax.swing.JSpinner
    9.16 +
    9.17 +import scala.swing.CheckBox
    9.18 +
    9.19 +import org.gjt.sp.jedit.AbstractOptionPane
    9.20 +
    9.21 +
    9.22 +class Isabelle_Options extends AbstractOptionPane("isabelle")
    9.23 +{
    9.24 +  private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
    9.25 +  private val auto_start = new CheckBox()
    9.26 +  private val relative_font_size = new JSpinner()
    9.27 +  private val tooltip_font_size = new JSpinner()
    9.28 +  private val tooltip_margin = new JSpinner()
    9.29 +  private val tooltip_dismiss_delay = new JSpinner()
    9.30 +
    9.31 +  override def _init()
    9.32 +  {
    9.33 +    addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
    9.34 +
    9.35 +    addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
    9.36 +    auto_start.selected = Isabelle.Boolean_Property("auto-start")
    9.37 +
    9.38 +    relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
    9.39 +    addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
    9.40 +
    9.41 +    tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
    9.42 +    addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
    9.43 +
    9.44 +    tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
    9.45 +    addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
    9.46 +
    9.47 +    tooltip_dismiss_delay.setValue(
    9.48 +      Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
    9.49 +    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
    9.50 +  }
    9.51 +
    9.52 +  override def _save()
    9.53 +  {
    9.54 +    Isabelle.Property("logic") = logic_selector.selection.item.name
    9.55 +
    9.56 +    Isabelle.Boolean_Property("auto-start") = auto_start.selected
    9.57 +
    9.58 +    Isabelle.Int_Property("relative-font-size") =
    9.59 +      relative_font_size.getValue().asInstanceOf[Int]
    9.60 +
    9.61 +    Isabelle.Int_Property("tooltip-font-size") =
    9.62 +      tooltip_font_size.getValue().asInstanceOf[Int]
    9.63 +
    9.64 +    Isabelle.Int_Property("tooltip-margin") =
    9.65 +      tooltip_margin.getValue().asInstanceOf[Int]
    9.66 +
    9.67 +    Isabelle.Time_Property("tooltip-dismiss-delay") =
    9.68 +      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
    9.69 +  }
    9.70 +}
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Jun 08 17:42:07 2011 +0200
    10.3 @@ -0,0 +1,176 @@
    10.4 +/*  Title:      Tools/jEdit/src/isabelle_sidekick.scala
    10.5 +    Author:     Fabian Immler, TU Munich
    10.6 +    Author:     Makarius
    10.7 +
    10.8 +SideKick parsers for Isabelle proof documents.
    10.9 +*/
   10.10 +
   10.11 +package isabelle.jedit
   10.12 +
   10.13 +
   10.14 +import isabelle._
   10.15 +
   10.16 +import scala.collection.Set
   10.17 +import scala.collection.immutable.TreeSet
   10.18 +
   10.19 +import javax.swing.tree.DefaultMutableTreeNode
   10.20 +import javax.swing.text.Position
   10.21 +import javax.swing.Icon
   10.22 +
   10.23 +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
   10.24 +import errorlist.DefaultErrorSource
   10.25 +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
   10.26 +
   10.27 +
   10.28 +object Isabelle_Sidekick
   10.29 +{
   10.30 +  def int_to_pos(offset: Text.Offset): Position =
   10.31 +    new Position { def getOffset = offset; override def toString = offset.toString }
   10.32 +
   10.33 +  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
   10.34 +  {
   10.35 +    protected var _name = name
   10.36 +    protected var _start = int_to_pos(start)
   10.37 +    protected var _end = int_to_pos(end)
   10.38 +    override def getIcon: Icon = null
   10.39 +    override def getShortString: String = _name
   10.40 +    override def getLongString: String = _name
   10.41 +    override def getName: String = _name
   10.42 +    override def setName(name: String) = _name = name
   10.43 +    override def getStart: Position = _start
   10.44 +    override def setStart(start: Position) = _start = start
   10.45 +    override def getEnd: Position = _end
   10.46 +    override def setEnd(end: Position) = _end = end
   10.47 +    override def toString = _name
   10.48 +  }
   10.49 +}
   10.50 +
   10.51 +
   10.52 +abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
   10.53 +{
   10.54 +  /* parsing */
   10.55 +
   10.56 +  @volatile protected var stopped = false
   10.57 +  override def stop() = { stopped = true }
   10.58 +
   10.59 +  def parser(data: SideKickParsedData, model: Document_Model): Unit
   10.60 +
   10.61 +  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   10.62 +  {
   10.63 +    stopped = false
   10.64 +
   10.65 +    // FIXME lock buffer (!??)
   10.66 +    val data = new SideKickParsedData(buffer.getName)
   10.67 +    val root = data.root
   10.68 +    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
   10.69 +
   10.70 +    Swing_Thread.now { Document_Model(buffer) } match {
   10.71 +      case Some(model) =>
   10.72 +        parser(data, model)
   10.73 +        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
   10.74 +      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
   10.75 +    }
   10.76 +    data
   10.77 +  }
   10.78 +
   10.79 +
   10.80 +  /* completion */
   10.81 +
   10.82 +  override def supportsCompletion = true
   10.83 +  override def canCompleteAnywhere = true
   10.84 +
   10.85 +  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
   10.86 +  {
   10.87 +    val buffer = pane.getBuffer
   10.88 +    Isabelle.swing_buffer_lock(buffer) {
   10.89 +      Document_Model(buffer) match {
   10.90 +        case None => null
   10.91 +        case Some(model) =>
   10.92 +          val line = buffer.getLineOfOffset(caret)
   10.93 +          val start = buffer.getLineStartOffset(line)
   10.94 +          val text = buffer.getSegment(start, caret - start)
   10.95 +
   10.96 +          val completion = model.session.current_syntax().completion
   10.97 +          completion.complete(text) match {
   10.98 +            case None => null
   10.99 +            case Some((word, cs)) =>
  10.100 +              val ds =
  10.101 +                (if (Isabelle_Encoding.is_active(buffer))
  10.102 +                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
  10.103 +                 else cs).filter(_ != word)
  10.104 +              if (ds.isEmpty) null
  10.105 +              else new SideKickCompletion(
  10.106 +                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
  10.107 +          }
  10.108 +      }
  10.109 +    }
  10.110 +  }
  10.111 +}
  10.112 +
  10.113 +
  10.114 +class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
  10.115 +{
  10.116 +  import Thy_Syntax.Structure
  10.117 +
  10.118 +  def parser(data: SideKickParsedData, model: Document_Model)
  10.119 +  {
  10.120 +    val syntax = model.session.current_syntax()
  10.121 +
  10.122 +    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
  10.123 +      entry match {
  10.124 +        case Structure.Block(name, body) =>
  10.125 +          val node =
  10.126 +            new DefaultMutableTreeNode(
  10.127 +              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
  10.128 +          (offset /: body)((i, e) =>
  10.129 +            {
  10.130 +              make_tree(i, e) foreach (nd => node.add(nd))
  10.131 +              i + e.length
  10.132 +            })
  10.133 +          List(node)
  10.134 +        case Structure.Atom(command)
  10.135 +        if command.is_command && syntax.heading_level(command).isEmpty =>
  10.136 +          val node =
  10.137 +            new DefaultMutableTreeNode(
  10.138 +              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
  10.139 +          List(node)
  10.140 +        case _ => Nil
  10.141 +      }
  10.142 +
  10.143 +    val text = Isabelle.buffer_text(model.buffer)
  10.144 +    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
  10.145 +
  10.146 +    make_tree(0, structure) foreach (node => data.root.add(node))
  10.147 +  }
  10.148 +}
  10.149 +
  10.150 +
  10.151 +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
  10.152 +{
  10.153 +  def parser(data: SideKickParsedData, model: Document_Model)
  10.154 +  {
  10.155 +    val root = data.root
  10.156 +    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
  10.157 +    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
  10.158 +      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
  10.159 +          {
  10.160 +            val range = info.range + command_start
  10.161 +            val content = command.source(info.range).replace('\n', ' ')
  10.162 +            val info_text =
  10.163 +              info.info match {
  10.164 +                case elem @ XML.Elem(_, _) =>
  10.165 +                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
  10.166 +                case x => x.toString
  10.167 +              }
  10.168 +
  10.169 +            new DefaultMutableTreeNode(
  10.170 +              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
  10.171 +                override def getShortString: String = content
  10.172 +                override def getLongString: String = info_text
  10.173 +                override def toString = "\"" + content + "\" " + range.toString
  10.174 +              })
  10.175 +          })
  10.176 +    }
  10.177 +  }
  10.178 +}
  10.179 +
    11.1 --- a/src/Tools/jEdit/src/jedit/dockable.scala	Wed Jun 08 17:32:31 2011 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,41 +0,0 @@
    11.4 -/*  Title:      Tools/jEdit/src/jedit/dockable.scala
    11.5 -    Author:     Makarius
    11.6 -
    11.7 -Generic dockable window.
    11.8 -*/
    11.9 -
   11.10 -package isabelle.jedit
   11.11 -
   11.12 -
   11.13 -import isabelle._
   11.14 -
   11.15 -import java.awt.{Dimension, Component, BorderLayout}
   11.16 -import javax.swing.JPanel
   11.17 -
   11.18 -import org.gjt.sp.jedit.View
   11.19 -import org.gjt.sp.jedit.gui.DockableWindowManager
   11.20 -
   11.21 -
   11.22 -class Dockable(view: View, position: String) extends JPanel(new BorderLayout)
   11.23 -{
   11.24 -  if (position == DockableWindowManager.FLOATING)
   11.25 -    setPreferredSize(new Dimension(500, 250))
   11.26 -
   11.27 -  def set_content(c: Component) { add(c, BorderLayout.CENTER) }
   11.28 -  def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) }
   11.29 -
   11.30 -  protected def init() { }
   11.31 -  protected def exit() { }
   11.32 -
   11.33 -  override def addNotify()
   11.34 -  {
   11.35 -    super.addNotify()
   11.36 -    init()
   11.37 -  }
   11.38 -
   11.39 -  override def removeNotify()
   11.40 -  {
   11.41 -    exit()
   11.42 -    super.removeNotify()
   11.43 -  }
   11.44 -}
    12.1 --- a/src/Tools/jEdit/src/jedit/document_model.scala	Wed Jun 08 17:32:31 2011 +0200
    12.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.3 @@ -1,252 +0,0 @@
    12.4 -/*  Title:      Tools/jEdit/src/jedit/document_model.scala
    12.5 -    Author:     Fabian Immler, TU Munich
    12.6 -    Author:     Makarius
    12.7 -
    12.8 -Document model connected to jEdit buffer -- single node in theory graph.
    12.9 -*/
   12.10 -
   12.11 -package isabelle.jedit
   12.12 -
   12.13 -
   12.14 -import isabelle._
   12.15 -
   12.16 -import scala.collection.mutable
   12.17 -
   12.18 -import org.gjt.sp.jedit.Buffer
   12.19 -import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
   12.20 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
   12.21 -import org.gjt.sp.jedit.textarea.TextArea
   12.22 -
   12.23 -import java.awt.font.TextAttribute
   12.24 -import javax.swing.text.Segment;
   12.25 -
   12.26 -
   12.27 -object Document_Model
   12.28 -{
   12.29 -  object Token_Markup
   12.30 -  {
   12.31 -    /* extended token styles */
   12.32 -
   12.33 -    private val plain_range: Int = Token.ID_COUNT
   12.34 -    private val full_range: Int = 3 * plain_range
   12.35 -    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
   12.36 -
   12.37 -    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
   12.38 -    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
   12.39 -
   12.40 -    private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
   12.41 -    {
   12.42 -      import scala.collection.JavaConversions._
   12.43 -      val script_font =
   12.44 -        style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
   12.45 -      new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font)
   12.46 -    }
   12.47 -
   12.48 -    def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
   12.49 -    {
   12.50 -      val new_styles = new Array[SyntaxStyle](full_range)
   12.51 -      for (i <- 0 until plain_range) {
   12.52 -        val style = styles(i)
   12.53 -        new_styles(i) = style
   12.54 -        new_styles(subscript(i.toByte)) = script_style(style, -1)
   12.55 -        new_styles(superscript(i.toByte)) = script_style(style, 1)
   12.56 -      }
   12.57 -      new_styles
   12.58 -    }
   12.59 -
   12.60 -
   12.61 -    /* line context */
   12.62 -
   12.63 -    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
   12.64 -
   12.65 -    class Line_Context(val line: Int, prev: Line_Context)
   12.66 -      extends TokenMarker.LineContext(dummy_rules, prev)
   12.67 -    {
   12.68 -      override def hashCode: Int = line
   12.69 -      override def equals(that: Any): Boolean =
   12.70 -        that match {
   12.71 -          case other: Line_Context => line == other.line
   12.72 -          case _ => false
   12.73 -        }
   12.74 -    }
   12.75 -  }
   12.76 -
   12.77 -
   12.78 -  /* document model of buffer */
   12.79 -
   12.80 -  private val key = "isabelle.document_model"
   12.81 -
   12.82 -  def init(session: Session, buffer: Buffer, thy_name: String): Document_Model =
   12.83 -  {
   12.84 -    Swing_Thread.require()
   12.85 -    val model = new Document_Model(session, buffer, thy_name)
   12.86 -    buffer.setProperty(key, model)
   12.87 -    model.activate()
   12.88 -    model
   12.89 -  }
   12.90 -
   12.91 -  def apply(buffer: Buffer): Option[Document_Model] =
   12.92 -  {
   12.93 -    Swing_Thread.require()
   12.94 -    buffer.getProperty(key) match {
   12.95 -      case model: Document_Model => Some(model)
   12.96 -      case _ => None
   12.97 -    }
   12.98 -  }
   12.99 -
  12.100 -  def exit(buffer: Buffer)
  12.101 -  {
  12.102 -    Swing_Thread.require()
  12.103 -    apply(buffer) match {
  12.104 -      case None =>
  12.105 -      case Some(model) =>
  12.106 -        model.deactivate()
  12.107 -        buffer.unsetProperty(key)
  12.108 -    }
  12.109 -  }
  12.110 -}
  12.111 -
  12.112 -
  12.113 -class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String)
  12.114 -{
  12.115 -  /* pending text edits */
  12.116 -
  12.117 -  object pending_edits  // owned by Swing thread
  12.118 -  {
  12.119 -    private val pending = new mutable.ListBuffer[Text.Edit]
  12.120 -    def snapshot(): List[Text.Edit] = pending.toList
  12.121 -
  12.122 -    def flush(more_edits: Option[List[Text.Edit]]*)
  12.123 -    {
  12.124 -      Swing_Thread.require()
  12.125 -      val edits = snapshot()
  12.126 -      pending.clear
  12.127 -
  12.128 -      val all_edits =
  12.129 -        if (edits.isEmpty) more_edits.toList
  12.130 -        else Some(edits) :: more_edits.toList
  12.131 -      if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _)))
  12.132 -    }
  12.133 -
  12.134 -    def init()
  12.135 -    {
  12.136 -      Swing_Thread.require()
  12.137 -      flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer)))))
  12.138 -    }
  12.139 -
  12.140 -    private val delay_flush =
  12.141 -      Swing_Thread.delay_last(session.input_delay) { flush() }
  12.142 -
  12.143 -    def +=(edit: Text.Edit)
  12.144 -    {
  12.145 -      Swing_Thread.require()
  12.146 -      pending += edit
  12.147 -      delay_flush()
  12.148 -    }
  12.149 -  }
  12.150 -
  12.151 -
  12.152 -  /* snapshot */
  12.153 -
  12.154 -  def snapshot(): Document.Snapshot =
  12.155 -  {
  12.156 -    Swing_Thread.require()
  12.157 -    session.snapshot(thy_name, pending_edits.snapshot())
  12.158 -  }
  12.159 -
  12.160 -
  12.161 -  /* buffer listener */
  12.162 -
  12.163 -  private val buffer_listener: BufferListener = new BufferAdapter
  12.164 -  {
  12.165 -    override def bufferLoaded(buffer: JEditBuffer)
  12.166 -    {
  12.167 -      pending_edits.init()
  12.168 -    }
  12.169 -
  12.170 -    override def contentInserted(buffer: JEditBuffer,
  12.171 -      start_line: Int, offset: Int, num_lines: Int, length: Int)
  12.172 -    {
  12.173 -      if (!buffer.isLoading)
  12.174 -        pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length))
  12.175 -    }
  12.176 -
  12.177 -    override def preContentRemoved(buffer: JEditBuffer,
  12.178 -      start_line: Int, offset: Int, num_lines: Int, removed_length: Int)
  12.179 -    {
  12.180 -      if (!buffer.isLoading)
  12.181 -        pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length))
  12.182 -    }
  12.183 -  }
  12.184 -
  12.185 -
  12.186 -  /* semantic token marker */
  12.187 -
  12.188 -  private val token_marker = new TokenMarker
  12.189 -  {
  12.190 -    override def markTokens(prev: TokenMarker.LineContext,
  12.191 -        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
  12.192 -    {
  12.193 -      Isabelle.swing_buffer_lock(buffer) {
  12.194 -        val snapshot = Document_Model.this.snapshot()
  12.195 -
  12.196 -        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
  12.197 -        val line = if (prev == null) 0 else previous.line + 1
  12.198 -        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
  12.199 -
  12.200 -        val start = buffer.getLineStartOffset(line)
  12.201 -        val stop = start + line_segment.count
  12.202 -
  12.203 -        /* FIXME
  12.204 -        for (text_area <- Isabelle.jedit_text_areas(buffer)
  12.205 -              if Document_View(text_area).isDefined)
  12.206 -          Document_View(text_area).get.set_styles()
  12.207 -        */
  12.208 -
  12.209 -        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
  12.210 -          handler.handleToken(line_segment, style, offset, length, context)
  12.211 -
  12.212 -        val syntax = session.current_syntax()
  12.213 -        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
  12.214 -
  12.215 -        var last = start
  12.216 -        for (token <- tokens.iterator) {
  12.217 -          val Text.Range(token_start, token_stop) = token.range
  12.218 -          if (last < token_start)
  12.219 -            handle_token(Token.COMMENT1, last - start, token_start - last)
  12.220 -          handle_token(token.info getOrElse Token.NULL,
  12.221 -            token_start - start, token_stop - token_start)
  12.222 -          last = token_stop
  12.223 -        }
  12.224 -        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
  12.225 -
  12.226 -        handle_token(Token.END, line_segment.count, 0)
  12.227 -        handler.setLineContext(context)
  12.228 -        context
  12.229 -      }
  12.230 -    }
  12.231 -  }
  12.232 -
  12.233 -
  12.234 -  /* activation */
  12.235 -
  12.236 -  def activate()
  12.237 -  {
  12.238 -    buffer.setTokenMarker(token_marker)
  12.239 -    buffer.addBufferListener(buffer_listener)
  12.240 -    buffer.propertiesChanged()
  12.241 -    pending_edits.init()
  12.242 -  }
  12.243 -
  12.244 -  def refresh()
  12.245 -  {
  12.246 -    buffer.setTokenMarker(token_marker)
  12.247 -  }
  12.248 -
  12.249 -  def deactivate()
  12.250 -  {
  12.251 -    pending_edits.flush()
  12.252 -    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
  12.253 -    buffer.removeBufferListener(buffer_listener)
  12.254 -  }
  12.255 -}
    13.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Wed Jun 08 17:32:31 2011 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,587 +0,0 @@
    13.4 -/*  Title:      Tools/jEdit/src/jedit/document_view.scala
    13.5 -    Author:     Fabian Immler, TU Munich
    13.6 -    Author:     Makarius
    13.7 -
    13.8 -Document view connected to jEdit text area.
    13.9 -*/
   13.10 -
   13.11 -package isabelle.jedit
   13.12 -
   13.13 -
   13.14 -import isabelle._
   13.15 -
   13.16 -import scala.actors.Actor._
   13.17 -
   13.18 -import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point}
   13.19 -import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent,
   13.20 -  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
   13.21 -import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory}
   13.22 -import javax.swing.event.{CaretListener, CaretEvent}
   13.23 -import java.util.ArrayList
   13.24 -
   13.25 -import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
   13.26 -import org.gjt.sp.jedit.gui.RolloverButton
   13.27 -import org.gjt.sp.jedit.options.GutterOptionPane
   13.28 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
   13.29 -import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token}
   13.30 -
   13.31 -
   13.32 -object Document_View
   13.33 -{
   13.34 -  /* document view of text area */
   13.35 -
   13.36 -  private val key = new Object
   13.37 -
   13.38 -  def init(model: Document_Model, text_area: JEditTextArea): Document_View =
   13.39 -  {
   13.40 -    Swing_Thread.require()
   13.41 -    val doc_view = new Document_View(model, text_area)
   13.42 -    text_area.putClientProperty(key, doc_view)
   13.43 -    doc_view.activate()
   13.44 -    doc_view
   13.45 -  }
   13.46 -
   13.47 -  def apply(text_area: JEditTextArea): Option[Document_View] =
   13.48 -  {
   13.49 -    Swing_Thread.require()
   13.50 -    text_area.getClientProperty(key) match {
   13.51 -      case doc_view: Document_View => Some(doc_view)
   13.52 -      case _ => None
   13.53 -    }
   13.54 -  }
   13.55 -
   13.56 -  def exit(text_area: JEditTextArea)
   13.57 -  {
   13.58 -    Swing_Thread.require()
   13.59 -    apply(text_area) match {
   13.60 -      case None =>
   13.61 -      case Some(doc_view) =>
   13.62 -        doc_view.deactivate()
   13.63 -        text_area.putClientProperty(key, null)
   13.64 -    }
   13.65 -  }
   13.66 -}
   13.67 -
   13.68 -
   13.69 -class Document_View(val model: Document_Model, text_area: JEditTextArea)
   13.70 -{
   13.71 -  private val session = model.session
   13.72 -
   13.73 -
   13.74 -  /** token handling **/
   13.75 -
   13.76 -  /* extended token styles */
   13.77 -
   13.78 -  private var styles: Array[SyntaxStyle] = null  // owned by Swing thread
   13.79 -
   13.80 -  def extend_styles()
   13.81 -  {
   13.82 -    Swing_Thread.require()
   13.83 -    styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles)
   13.84 -  }
   13.85 -  extend_styles()
   13.86 -
   13.87 -  def set_styles()
   13.88 -  {
   13.89 -    Swing_Thread.require()
   13.90 -    text_area.getPainter.setStyles(styles)
   13.91 -  }
   13.92 -
   13.93 -
   13.94 -  /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */
   13.95 -
   13.96 -  def wrap_margin(): Int =
   13.97 -  {
   13.98 -    val buffer = text_area.getBuffer
   13.99 -    val painter = text_area.getPainter
  13.100 -    val font = painter.getFont
  13.101 -    val font_context = painter.getFontRenderContext
  13.102 -
  13.103 -    val soft_wrap = buffer.getStringProperty("wrap") == "soft"
  13.104 -    val max = buffer.getIntegerProperty("maxLineLen", 0)
  13.105 -
  13.106 -    if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt
  13.107 -    else if (soft_wrap)
  13.108 -      painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3
  13.109 -    else 0
  13.110 -  }
  13.111 -
  13.112 -
  13.113 -  /* chunks */
  13.114 -
  13.115 -  def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] =
  13.116 -  {
  13.117 -    import scala.collection.JavaConversions._
  13.118 -
  13.119 -    val buffer = text_area.getBuffer
  13.120 -    val painter = text_area.getPainter
  13.121 -    val margin = wrap_margin().toFloat
  13.122 -
  13.123 -    val out = new ArrayList[Chunk]
  13.124 -    val handler = new DisplayTokenHandler
  13.125 -
  13.126 -    var result = Map[Text.Offset, Chunk]()
  13.127 -    for (line <- physical_lines) {
  13.128 -      out.clear
  13.129 -      handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin)
  13.130 -      buffer.markTokens(line, handler)
  13.131 -
  13.132 -      val line_start = buffer.getLineStartOffset(line)
  13.133 -      for (chunk <- handler.getChunkList.iterator)
  13.134 -        result += (line_start + chunk.offset -> chunk)
  13.135 -    }
  13.136 -    result
  13.137 -  }
  13.138 -
  13.139 -
  13.140 -  /* visible line ranges */
  13.141 -
  13.142 -  // simplify slightly odd result of TextArea.getScreenLineEndOffset etc.
  13.143 -  // NB: jEdit already normalizes \r\n and \r to \n
  13.144 -  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
  13.145 -  {
  13.146 -    val stop = if (start < end) end - 1 else end min model.buffer.getLength
  13.147 -    Text.Range(start, stop)
  13.148 -  }
  13.149 -
  13.150 -  def screen_lines_range(): Text.Range =
  13.151 -  {
  13.152 -    val start = text_area.getScreenLineStartOffset(0)
  13.153 -    val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0)
  13.154 -    proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength)
  13.155 -  }
  13.156 -
  13.157 -  def invalidate_line_range(range: Text.Range)
  13.158 -  {
  13.159 -    text_area.invalidateLineRange(
  13.160 -      model.buffer.getLineOfOffset(range.start),
  13.161 -      model.buffer.getLineOfOffset(range.stop))
  13.162 -  }
  13.163 -
  13.164 -
  13.165 -  /* HTML popups */
  13.166 -
  13.167 -  private var html_popup: Option[Popup] = None
  13.168 -
  13.169 -  private def exit_popup() { html_popup.map(_.hide) }
  13.170 -
  13.171 -  private val html_panel =
  13.172 -    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
  13.173 -  html_panel.setBorder(BorderFactory.createLineBorder(Color.black))
  13.174 -
  13.175 -  private def html_panel_resize()
  13.176 -  {
  13.177 -    Swing_Thread.now {
  13.178 -      html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
  13.179 -    }
  13.180 -  }
  13.181 -
  13.182 -  private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int)
  13.183 -  {
  13.184 -    exit_popup()
  13.185 -/* FIXME broken
  13.186 -    val offset = text_area.xyToOffset(x, y)
  13.187 -    val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter)
  13.188 -
  13.189 -    // FIXME snapshot.cumulate
  13.190 -    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match {
  13.191 -      case Text.Info(_, Some(msg)) #:: _ =>
  13.192 -        val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60)
  13.193 -        html_panel.render_sync(List(msg))
  13.194 -        Thread.sleep(10)  // FIXME !?
  13.195 -        popup.show
  13.196 -        html_popup = Some(popup)
  13.197 -      case _ =>
  13.198 -    }
  13.199 -*/
  13.200 -  }
  13.201 -
  13.202 -
  13.203 -  /* subexpression highlighting */
  13.204 -
  13.205 -  private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
  13.206 -    : Option[(Text.Range, Color)] =
  13.207 -  {
  13.208 -    val offset = text_area.xyToOffset(x, y)
  13.209 -    snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
  13.210 -      case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
  13.211 -      case _ => None
  13.212 -    }
  13.213 -  }
  13.214 -
  13.215 -  private var highlight_range: Option[(Text.Range, Color)] = None
  13.216 -
  13.217 -
  13.218 -  /* CONTROL-mouse management */
  13.219 -
  13.220 -  private var control: Boolean = false
  13.221 -
  13.222 -  private def exit_control()
  13.223 -  {
  13.224 -    exit_popup()
  13.225 -    highlight_range = None
  13.226 -  }
  13.227 -
  13.228 -  private val focus_listener = new FocusAdapter {
  13.229 -    override def focusLost(e: FocusEvent) {
  13.230 -      highlight_range = None // FIXME exit_control !?
  13.231 -    }
  13.232 -  }
  13.233 -
  13.234 -  private val window_listener = new WindowAdapter {
  13.235 -    override def windowIconified(e: WindowEvent) { exit_control() }
  13.236 -    override def windowDeactivated(e: WindowEvent) { exit_control() }
  13.237 -  }
  13.238 -
  13.239 -  private val mouse_motion_listener = new MouseMotionAdapter {
  13.240 -    override def mouseMoved(e: MouseEvent) {
  13.241 -      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
  13.242 -      val x = e.getX()
  13.243 -      val y = e.getY()
  13.244 -
  13.245 -      if (!model.buffer.isLoaded) exit_control()
  13.246 -      else
  13.247 -        Isabelle.swing_buffer_lock(model.buffer) {
  13.248 -          val snapshot = model.snapshot
  13.249 -
  13.250 -          if (control) init_popup(snapshot, x, y)
  13.251 -
  13.252 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
  13.253 -          highlight_range = if (control) subexp_range(snapshot, x, y) else None
  13.254 -          highlight_range map { case (range, _) => invalidate_line_range(range) }
  13.255 -        }
  13.256 -    }
  13.257 -  }
  13.258 -
  13.259 -
  13.260 -  /* TextArea painters */
  13.261 -
  13.262 -  private val background_painter = new TextAreaExtension
  13.263 -  {
  13.264 -    override def paintScreenLineRange(gfx: Graphics2D,
  13.265 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
  13.266 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  13.267 -    {
  13.268 -      Isabelle.swing_buffer_lock(model.buffer) {
  13.269 -        val snapshot = model.snapshot()
  13.270 -        val ascent = text_area.getPainter.getFontMetrics.getAscent
  13.271 -
  13.272 -        for (i <- 0 until physical_lines.length) {
  13.273 -          if (physical_lines(i) != -1) {
  13.274 -            val line_range = proper_line_range(start(i), end(i))
  13.275 -
  13.276 -            // background color: status
  13.277 -            val cmds = snapshot.node.command_range(snapshot.revert(line_range))
  13.278 -            for {
  13.279 -              (command, command_start) <- cmds if !command.is_ignored
  13.280 -              val range = line_range.restrict(snapshot.convert(command.range + command_start))
  13.281 -              r <- Isabelle.gfx_range(text_area, range)
  13.282 -              color <- Isabelle_Markup.status_color(snapshot, command)
  13.283 -            } {
  13.284 -              gfx.setColor(color)
  13.285 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  13.286 -            }
  13.287 -
  13.288 -            // background color (1): markup
  13.289 -            for {
  13.290 -              Text.Info(range, Some(color)) <-
  13.291 -                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
  13.292 -              r <- Isabelle.gfx_range(text_area, range)
  13.293 -            } {
  13.294 -              gfx.setColor(color)
  13.295 -              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
  13.296 -            }
  13.297 -
  13.298 -            // background color (2): markup
  13.299 -            for {
  13.300 -              Text.Info(range, Some(color)) <-
  13.301 -                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
  13.302 -              r <- Isabelle.gfx_range(text_area, range)
  13.303 -            } {
  13.304 -              gfx.setColor(color)
  13.305 -              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
  13.306 -            }
  13.307 -
  13.308 -            // sub-expression highlighting -- potentially from other snapshot
  13.309 -            highlight_range match {
  13.310 -              case Some((range, color)) if line_range.overlaps(range) =>
  13.311 -                Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
  13.312 -                  case None =>
  13.313 -                  case Some(r) =>
  13.314 -                    gfx.setColor(color)
  13.315 -                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
  13.316 -                }
  13.317 -              case _ =>
  13.318 -            }
  13.319 -
  13.320 -            // squiggly underline
  13.321 -            for {
  13.322 -              Text.Info(range, Some(color)) <-
  13.323 -                snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
  13.324 -              r <- Isabelle.gfx_range(text_area, range)
  13.325 -            } {
  13.326 -              gfx.setColor(color)
  13.327 -              val x0 = (r.x / 2) * 2
  13.328 -              val y0 = r.y + ascent + 1
  13.329 -              for (x1 <- Range(x0, x0 + r.length, 2)) {
  13.330 -                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
  13.331 -                gfx.drawLine(x1, y1, x1 + 1, y1)
  13.332 -              }
  13.333 -            }
  13.334 -          }
  13.335 -        }
  13.336 -      }
  13.337 -    }
  13.338 -
  13.339 -    override def getToolTipText(x: Int, y: Int): String =
  13.340 -    {
  13.341 -      Isabelle.swing_buffer_lock(model.buffer) {
  13.342 -        val snapshot = model.snapshot()
  13.343 -        val offset = text_area.xyToOffset(x, y)
  13.344 -        if (control) {
  13.345 -          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
  13.346 -          {
  13.347 -            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
  13.348 -            case _ => null
  13.349 -          }
  13.350 -        }
  13.351 -        else {
  13.352 -          // FIXME snapshot.cumulate
  13.353 -          snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match
  13.354 -          {
  13.355 -            case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
  13.356 -            case _ => null
  13.357 -          }
  13.358 -        }
  13.359 -      }
  13.360 -    }
  13.361 -  }
  13.362 -
  13.363 -  var use_text_painter = false
  13.364 -
  13.365 -  private val text_painter = new TextAreaExtension
  13.366 -  {
  13.367 -    override def paintScreenLineRange(gfx: Graphics2D,
  13.368 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
  13.369 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  13.370 -    {
  13.371 -      if (use_text_painter) {
  13.372 -        Isabelle.swing_buffer_lock(model.buffer) {
  13.373 -          val painter = text_area.getPainter
  13.374 -          val fm = painter.getFontMetrics
  13.375 -
  13.376 -          val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1))
  13.377 -
  13.378 -          val x0 = text_area.getHorizontalOffset
  13.379 -          var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
  13.380 -          for (i <- 0 until physical_lines.length) {
  13.381 -            if (physical_lines(i) != -1) {
  13.382 -              all_chunks.get(start(i)) match {
  13.383 -                case Some(chunk) =>
  13.384 -                  Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR)
  13.385 -                case None =>
  13.386 -              }
  13.387 -            }
  13.388 -            y0 += line_height
  13.389 -          }
  13.390 -        }
  13.391 -      }
  13.392 -    }
  13.393 -  }
  13.394 -
  13.395 -  private val gutter_painter = new TextAreaExtension
  13.396 -  {
  13.397 -    override def paintScreenLineRange(gfx: Graphics2D,
  13.398 -      first_line: Int, last_line: Int, physical_lines: Array[Int],
  13.399 -      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
  13.400 -    {
  13.401 -      val gutter = text_area.getGutter
  13.402 -      val width = GutterOptionPane.getSelectionAreaWidth
  13.403 -      val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
  13.404 -      val FOLD_MARKER_SIZE = 12
  13.405 -
  13.406 -      if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
  13.407 -        Isabelle.swing_buffer_lock(model.buffer) {
  13.408 -          val snapshot = model.snapshot()
  13.409 -          for (i <- 0 until physical_lines.length) {
  13.410 -            if (physical_lines(i) != -1) {
  13.411 -              val line_range = proper_line_range(start(i), end(i))
  13.412 -
  13.413 -              // gutter icons
  13.414 -              val icons =
  13.415 -                (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate
  13.416 -                  snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
  13.417 -                yield icon).toList.sortWith(_ >= _)
  13.418 -              icons match {
  13.419 -                case icon :: _ =>
  13.420 -                  val icn = icon.icon
  13.421 -                  val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
  13.422 -                  val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
  13.423 -                  icn.paintIcon(gutter, gfx, x0, y0)
  13.424 -                case Nil =>
  13.425 -              }
  13.426 -            }
  13.427 -          }
  13.428 -        }
  13.429 -      }
  13.430 -    }
  13.431 -  }
  13.432 -
  13.433 -
  13.434 -  /* caret handling */
  13.435 -
  13.436 -  def selected_command(): Option[Command] =
  13.437 -  {
  13.438 -    Swing_Thread.require()
  13.439 -    model.snapshot().node.proper_command_at(text_area.getCaretPosition)
  13.440 -  }
  13.441 -
  13.442 -  private val caret_listener = new CaretListener {
  13.443 -    private val delay = Swing_Thread.delay_last(session.input_delay) {
  13.444 -      session.perspective.event(Session.Perspective)
  13.445 -    }
  13.446 -    override def caretUpdate(e: CaretEvent) { delay() }
  13.447 -  }
  13.448 -
  13.449 -
  13.450 -  /* overview of command status left of scrollbar */
  13.451 -
  13.452 -  private val overview = new JPanel(new BorderLayout)
  13.453 -  {
  13.454 -    private val WIDTH = 10
  13.455 -    private val HEIGHT = 2
  13.456 -
  13.457 -    setPreferredSize(new Dimension(WIDTH, 0))
  13.458 -
  13.459 -    setRequestFocusEnabled(false)
  13.460 -
  13.461 -    addMouseListener(new MouseAdapter {
  13.462 -      override def mousePressed(event: MouseEvent) {
  13.463 -        val line = y_to_line(event.getY)
  13.464 -        if (line >= 0 && line < text_area.getLineCount)
  13.465 -          text_area.setCaretPosition(text_area.getLineStartOffset(line))
  13.466 -      }
  13.467 -    })
  13.468 -
  13.469 -    override def addNotify() {
  13.470 -      super.addNotify()
  13.471 -      ToolTipManager.sharedInstance.registerComponent(this)
  13.472 -    }
  13.473 -
  13.474 -    override def removeNotify() {
  13.475 -      ToolTipManager.sharedInstance.unregisterComponent(this)
  13.476 -      super.removeNotify
  13.477 -    }
  13.478 -
  13.479 -    override def paintComponent(gfx: Graphics)
  13.480 -    {
  13.481 -      super.paintComponent(gfx)
  13.482 -      Swing_Thread.assert()
  13.483 -
  13.484 -      val buffer = model.buffer
  13.485 -      Isabelle.buffer_lock(buffer) {
  13.486 -        val snapshot = model.snapshot()
  13.487 -
  13.488 -        def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] =
  13.489 -        {
  13.490 -          try {
  13.491 -            val line1 = buffer.getLineOfOffset(snapshot.convert(start))
  13.492 -            val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
  13.493 -            Some((line1, line2))
  13.494 -          }
  13.495 -          catch { case e: ArrayIndexOutOfBoundsException => None }
  13.496 -        }
  13.497 -        for {
  13.498 -          (command, start) <- snapshot.node.command_starts
  13.499 -          if !command.is_ignored
  13.500 -          (line1, line2) <- line_range(command, start)
  13.501 -          val y = line_to_y(line1)
  13.502 -          val height = HEIGHT * (line2 - line1)
  13.503 -          color <- Isabelle_Markup.overview_color(snapshot, command)
  13.504 -        } {
  13.505 -          gfx.setColor(color)
  13.506 -          gfx.fillRect(0, y, getWidth - 1, height)
  13.507 -        }
  13.508 -      }
  13.509 -    }
  13.510 -
  13.511 -    private def line_to_y(line: Int): Int =
  13.512 -      (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines)
  13.513 -
  13.514 -    private def y_to_line(y: Int): Int =
  13.515 -      (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight
  13.516 -  }
  13.517 -
  13.518 -
  13.519 -  /* main actor */
  13.520 -
  13.521 -  private val main_actor = actor {
  13.522 -    loop {
  13.523 -      react {
  13.524 -        case Session.Commands_Changed(changed) =>
  13.525 -          val buffer = model.buffer
  13.526 -          Isabelle.swing_buffer_lock(buffer) {
  13.527 -            val snapshot = model.snapshot()
  13.528 -
  13.529 -            if (changed.exists(snapshot.node.commands.contains))
  13.530 -              overview.repaint()
  13.531 -
  13.532 -            val visible_range = screen_lines_range()
  13.533 -            val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1)
  13.534 -            if (visible_cmds.exists(changed)) {
  13.535 -              for {
  13.536 -                line <- 0 until text_area.getVisibleLines
  13.537 -                val start = text_area.getScreenLineStartOffset(line) if start >= 0
  13.538 -                val end = text_area.getScreenLineEndOffset(line) if end >= 0
  13.539 -                val range = proper_line_range(start, end)
  13.540 -                val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
  13.541 -                if line_cmds.exists(changed)
  13.542 -              } text_area.invalidateScreenLineRange(line, line)
  13.543 -
  13.544 -              // FIXME danger of deadlock!?
  13.545 -              // FIXME potentially slow!?
  13.546 -              model.buffer.propertiesChanged()
  13.547 -            }
  13.548 -          }
  13.549 -
  13.550 -        case Session.Global_Settings => html_panel_resize()
  13.551 -
  13.552 -        case bad => System.err.println("command_change_actor: ignoring bad message " + bad)
  13.553 -      }
  13.554 -    }
  13.555 -  }
  13.556 -
  13.557 -
  13.558 -  /* activation */
  13.559 -
  13.560 -  private def activate()
  13.561 -  {
  13.562 -    val painter = text_area.getPainter
  13.563 -    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
  13.564 -    painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter)
  13.565 -    text_area.getGutter.addExtension(gutter_painter)
  13.566 -    text_area.addFocusListener(focus_listener)
  13.567 -    text_area.getView.addWindowListener(window_listener)
  13.568 -    painter.addMouseMotionListener(mouse_motion_listener)
  13.569 -    text_area.addCaretListener(caret_listener)
  13.570 -    text_area.addLeftOfScrollBar(overview)
  13.571 -    session.commands_changed += main_actor
  13.572 -    session.global_settings += main_actor
  13.573 -  }
  13.574 -
  13.575 -  private def deactivate()
  13.576 -  {
  13.577 -    val painter = text_area.getPainter
  13.578 -    session.commands_changed -= main_actor
  13.579 -    session.global_settings -= main_actor
  13.580 -    text_area.removeFocusListener(focus_listener)
  13.581 -    text_area.getView.removeWindowListener(window_listener)
  13.582 -    painter.removeMouseMotionListener(mouse_motion_listener)
  13.583 -    text_area.removeCaretListener(caret_listener)
  13.584 -    text_area.removeLeftOfScrollBar(overview)
  13.585 -    text_area.getGutter.removeExtension(gutter_painter)
  13.586 -    painter.removeExtension(text_painter)
  13.587 -    painter.removeExtension(background_painter)
  13.588 -    exit_popup()
  13.589 -  }
  13.590 -}
    14.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Wed Jun 08 17:32:31 2011 +0200
    14.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.3 @@ -1,206 +0,0 @@
    14.4 -/*  Title:      Tools/jEdit/src/jedit/html_panel.scala
    14.5 -    Author:     Makarius
    14.6 -
    14.7 -HTML panel based on Lobo/Cobra.
    14.8 -*/
    14.9 -
   14.10 -package isabelle.jedit
   14.11 -
   14.12 -
   14.13 -import isabelle._
   14.14 -
   14.15 -import java.io.StringReader
   14.16 -import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
   14.17 -import java.awt.event.MouseEvent
   14.18 -
   14.19 -import java.util.logging.{Logger, Level}
   14.20 -
   14.21 -import org.w3c.dom.html2.HTMLElement
   14.22 -
   14.23 -import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
   14.24 -import org.lobobrowser.html.gui.HtmlPanel
   14.25 -import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl}
   14.26 -import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
   14.27 -
   14.28 -import scala.actors.Actor._
   14.29 -
   14.30 -
   14.31 -object HTML_Panel
   14.32 -{
   14.33 -  sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent }
   14.34 -  case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event
   14.35 -  case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
   14.36 -  case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event
   14.37 -  case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event
   14.38 -  case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event
   14.39 -}
   14.40 -
   14.41 -
   14.42 -class HTML_Panel(
   14.43 -    system: Isabelle_System,
   14.44 -    initial_font_family: String,
   14.45 -    initial_font_size: Int)
   14.46 -  extends HtmlPanel
   14.47 -{
   14.48 -  /** Lobo setup **/
   14.49 -
   14.50 -  /* global logging */
   14.51 -
   14.52 -  Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
   14.53 -
   14.54 -
   14.55 -  /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */
   14.56 -
   14.57 -  val screen_resolution =
   14.58 -    if (GraphicsEnvironment.isHeadless()) 72
   14.59 -    else Toolkit.getDefaultToolkit().getScreenResolution()
   14.60 -
   14.61 -  def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution
   14.62 -  def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96
   14.63 -
   14.64 -
   14.65 -  /* contexts and event handling */
   14.66 -
   14.67 -  protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined
   14.68 -
   14.69 -  private val ucontext = new SimpleUserAgentContext
   14.70 -  private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
   14.71 -  {
   14.72 -    private def handle(event: HTML_Panel.Event): Boolean =
   14.73 -      if (handler.isDefinedAt(event)) { handler(event); false }
   14.74 -      else true
   14.75 -
   14.76 -    override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean =
   14.77 -      handle(HTML_Panel.Context_Menu(elem, event))
   14.78 -    override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean =
   14.79 -      handle(HTML_Panel.Mouse_Click(elem, event))
   14.80 -    override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean =
   14.81 -      handle(HTML_Panel.Double_Click(elem, event))
   14.82 -    override def onMouseOver(elem: HTMLElement, event: MouseEvent)
   14.83 -      { handle(HTML_Panel.Mouse_Over(elem, event)) }
   14.84 -    override def onMouseOut(elem: HTMLElement, event: MouseEvent)
   14.85 -      { handle(HTML_Panel.Mouse_Out(elem, event)) }
   14.86 -  }
   14.87 -
   14.88 -  private val builder = new DocumentBuilderImpl(ucontext, rcontext)
   14.89 -
   14.90 -
   14.91 -  /* document template with style sheets */
   14.92 -
   14.93 -  private val template_head =
   14.94 -    """<?xml version="1.0" encoding="utf-8"?>
   14.95 -<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
   14.96 -  "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
   14.97 -<html xmlns="http://www.w3.org/1999/xhtml">
   14.98 -<head>
   14.99 -<style media="all" type="text/css">
  14.100 -""" +
  14.101 -  system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
  14.102 -
  14.103 -  private val template_tail =
  14.104 -"""
  14.105 -</style>
  14.106 -</head>
  14.107 -<body/>
  14.108 -</html>
  14.109 -"""
  14.110 -
  14.111 -  private def template(font_family: String, font_size: Int): String =
  14.112 -    template_head +
  14.113 -    "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" +
  14.114 -    template_tail
  14.115 -
  14.116 -
  14.117 -  /** main actor **/
  14.118 -
  14.119 -  /* internal messages */
  14.120 -
  14.121 -  private case class Resize(font_family: String, font_size: Int)
  14.122 -  private case class Render_Document(text: String)
  14.123 -  private case class Render(body: XML.Body)
  14.124 -  private case class Render_Sync(body: XML.Body)
  14.125 -  private case object Refresh
  14.126 -
  14.127 -  private val main_actor = actor {
  14.128 -
  14.129 -    /* internal state */
  14.130 -
  14.131 -    var current_font_metrics: FontMetrics = null
  14.132 -    var current_font_family = ""
  14.133 -    var current_font_size: Int = 0
  14.134 -    var current_margin: Int = 0
  14.135 -    var current_body: XML.Body = Nil
  14.136 -
  14.137 -    def resize(font_family: String, font_size: Int)
  14.138 -    {
  14.139 -      val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
  14.140 -      val (font_metrics, margin) =
  14.141 -        Swing_Thread.now {
  14.142 -          val metrics = getFontMetrics(font)
  14.143 -          (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20)
  14.144 -        }
  14.145 -      if (current_font_metrics == null ||
  14.146 -          current_font_family != font_family ||
  14.147 -          current_font_size != font_size ||
  14.148 -          current_margin != margin)
  14.149 -      {
  14.150 -        current_font_metrics = font_metrics
  14.151 -        current_font_family = font_family
  14.152 -        current_font_size = font_size
  14.153 -        current_margin = margin
  14.154 -        refresh()
  14.155 -      }
  14.156 -    }
  14.157 -
  14.158 -    def refresh() { render(current_body) }
  14.159 -
  14.160 -    def render_document(text: String)
  14.161 -    {
  14.162 -      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
  14.163 -      Swing_Thread.later { setDocument(doc, rcontext) }
  14.164 -    }
  14.165 -
  14.166 -    def render(body: XML.Body)
  14.167 -    {
  14.168 -      current_body = body
  14.169 -      val html_body =
  14.170 -        current_body.flatMap(div =>
  14.171 -          Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
  14.172 -            .map(t =>
  14.173 -              XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
  14.174 -                HTML.spans(t, true))))
  14.175 -      val doc =
  14.176 -        builder.parse(
  14.177 -          new InputSourceImpl(
  14.178 -            new StringReader(template(current_font_family, current_font_size)), "http://localhost"))
  14.179 -      doc.removeChild(doc.getLastChild())
  14.180 -      doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body)))
  14.181 -      Swing_Thread.later { setDocument(doc, rcontext) }
  14.182 -    }
  14.183 -
  14.184 -
  14.185 -    /* main loop */
  14.186 -
  14.187 -    resize(initial_font_family, initial_font_size)
  14.188 -
  14.189 -    loop {
  14.190 -      react {
  14.191 -        case Resize(font_family, font_size) => resize(font_family, font_size)
  14.192 -        case Refresh => refresh()
  14.193 -        case Render_Document(text) => render_document(text)
  14.194 -        case Render(body) => render(body)
  14.195 -        case Render_Sync(body) => render(body); reply(())
  14.196 -        case bad => System.err.println("main_actor: ignoring bad message " + bad)
  14.197 -      }
  14.198 -    }
  14.199 -  }
  14.200 -
  14.201 -
  14.202 -  /* external methods */
  14.203 -
  14.204 -  def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
  14.205 -  def refresh() { main_actor ! Refresh }
  14.206 -  def render_document(text: String) { main_actor ! Render_Document(text) }
  14.207 -  def render(body: XML.Body) { main_actor ! Render(body) }
  14.208 -  def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
  14.209 -}
    15.1 --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala	Wed Jun 08 17:32:31 2011 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,65 +0,0 @@
    15.4 -/*  Title:      Tools/jEdit/src/jedit/isabelle_encoding.scala
    15.5 -    Author:     Makarius
    15.6 -
    15.7 -Isabelle encoding -- based on UTF-8.
    15.8 -*/
    15.9 -
   15.10 -package isabelle.jedit
   15.11 -
   15.12 -
   15.13 -import isabelle._
   15.14 -
   15.15 -import org.gjt.sp.jedit.io.Encoding
   15.16 -import org.gjt.sp.jedit.buffer.JEditBuffer
   15.17 -
   15.18 -import java.nio.charset.{Charset, CodingErrorAction}
   15.19 -import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
   15.20 -  CharArrayReader, ByteArrayOutputStream}
   15.21 -
   15.22 -import scala.io.{Codec, Source, BufferedSource}
   15.23 -
   15.24 -
   15.25 -object Isabelle_Encoding
   15.26 -{
   15.27 -  val NAME = "UTF-8-Isabelle"
   15.28 -
   15.29 -  def is_active(buffer: JEditBuffer): Boolean =
   15.30 -    buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
   15.31 -}
   15.32 -
   15.33 -class Isabelle_Encoding extends Encoding
   15.34 -{
   15.35 -  private val charset = Charset.forName(Standard_System.charset)
   15.36 -  val BUFSIZE = 32768
   15.37 -
   15.38 -  private def text_reader(in: InputStream, codec: Codec): Reader =
   15.39 -  {
   15.40 -    val source = new BufferedSource(in)(codec)
   15.41 -    new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray)
   15.42 -  }
   15.43 -
   15.44 -  override def getTextReader(in: InputStream): Reader =
   15.45 -    text_reader(in, Standard_System.codec())
   15.46 -
   15.47 -  override def getPermissiveTextReader(in: InputStream): Reader =
   15.48 -  {
   15.49 -    val codec = Standard_System.codec()
   15.50 -    codec.onMalformedInput(CodingErrorAction.REPLACE)
   15.51 -    codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
   15.52 -    text_reader(in, codec)
   15.53 -  }
   15.54 -
   15.55 -  override def getTextWriter(out: OutputStream): Writer =
   15.56 -  {
   15.57 -    val buffer = new ByteArrayOutputStream(BUFSIZE) {
   15.58 -      override def flush()
   15.59 -      {
   15.60 -        val text = Isabelle.system.symbols.encode(toString(Standard_System.charset))
   15.61 -        out.write(text.getBytes(Standard_System.charset))
   15.62 -        out.flush()
   15.63 -      }
   15.64 -      override def close() { out.close() }
   15.65 -    }
   15.66 -    new OutputStreamWriter(buffer, charset.newEncoder())
   15.67 -  }
   15.68 -}
    16.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Jun 08 17:32:31 2011 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,88 +0,0 @@
    16.4 -/*  Title:      Tools/jEdit/src/jedit/isabelle_hyperlinks.scala
    16.5 -    Author:     Fabian Immler, TU Munich
    16.6 -
    16.7 -Hyperlink setup for Isabelle proof documents.
    16.8 -*/
    16.9 -
   16.10 -package isabelle.jedit
   16.11 -
   16.12 -
   16.13 -import isabelle._
   16.14 -
   16.15 -import java.io.File
   16.16 -
   16.17 -import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink}
   16.18 -
   16.19 -import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities}
   16.20 -
   16.21 -
   16.22 -private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int)
   16.23 -  extends AbstractHyperlink(start, end, line, "")
   16.24 -{
   16.25 -  override def click(view: View) {
   16.26 -    view.getTextArea.moveCaretPosition(def_offset)
   16.27 -  }
   16.28 -}
   16.29 -
   16.30 -class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int)
   16.31 -  extends AbstractHyperlink(start, end, line, "")
   16.32 -{
   16.33 -  override def click(view: View) = {
   16.34 -    Isabelle.system.source_file(def_file) match {
   16.35 -      case None =>
   16.36 -        Library.error_dialog(view, "File not found", "Could not find source file " + def_file)
   16.37 -      case Some(file) =>
   16.38 -        jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line))
   16.39 -    }
   16.40 -  }
   16.41 -}
   16.42 -
   16.43 -class Isabelle_Hyperlinks extends HyperlinkSource
   16.44 -{
   16.45 -  def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink =
   16.46 -  {
   16.47 -    Swing_Thread.assert()
   16.48 -    Isabelle.buffer_lock(buffer) {
   16.49 -      Document_Model(buffer) match {
   16.50 -        case Some(model) =>
   16.51 -          val snapshot = model.snapshot()
   16.52 -          val markup =
   16.53 -            snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) {
   16.54 -              // FIXME Isar_Document.Hyperlink extractor
   16.55 -              case Text.Info(info_range,
   16.56 -                  XML.Elem(Markup(Markup.ENTITY, props), _))
   16.57 -                if (props.find(
   16.58 -                  { case (Markup.KIND, Markup.ML_OPEN) => true
   16.59 -                    case (Markup.KIND, Markup.ML_STRUCT) => true
   16.60 -                    case _ => false }).isEmpty) =>
   16.61 -                val Text.Range(begin, end) = info_range
   16.62 -                val line = buffer.getLineOfOffset(begin)
   16.63 -                (Position.File.unapply(props), Position.Line.unapply(props)) match {
   16.64 -                  case (Some(def_file), Some(def_line)) =>
   16.65 -                    new External_Hyperlink(begin, end, line, def_file, def_line)
   16.66 -                  case _ =>
   16.67 -                    (props, props) match {
   16.68 -                      case (Position.Id(def_id), Position.Offset(def_offset)) =>
   16.69 -                        snapshot.lookup_command(def_id) match {
   16.70 -                          case Some(def_cmd) =>
   16.71 -                            snapshot.node.command_start(def_cmd) match {
   16.72 -                              case Some(def_cmd_start) =>
   16.73 -                                new Internal_Hyperlink(begin, end, line,
   16.74 -                                  snapshot.convert(def_cmd_start + def_cmd.decode(def_offset)))
   16.75 -                              case None => null
   16.76 -                            }
   16.77 -                          case None => null
   16.78 -                        }
   16.79 -                      case _ => null
   16.80 -                    }
   16.81 -                }
   16.82 -            }
   16.83 -          markup match {
   16.84 -            case Text.Info(_, Some(link)) #:: _ => link
   16.85 -            case _ => null
   16.86 -          }
   16.87 -        case None => null
   16.88 -      }
   16.89 -    }
   16.90 -  }
   16.91 -}
    17.1 --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Wed Jun 08 17:32:31 2011 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,216 +0,0 @@
    17.4 -/*  Title:      Tools/jEdit/src/jedit/isabelle_markup.scala
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Isabelle specific physical rendering and markup selection.
    17.8 -*/
    17.9 -
   17.10 -package isabelle.jedit
   17.11 -
   17.12 -
   17.13 -import isabelle._
   17.14 -
   17.15 -import java.awt.Color
   17.16 -
   17.17 -import org.gjt.sp.jedit.syntax.Token
   17.18 -
   17.19 -
   17.20 -object Isabelle_Markup
   17.21 -{
   17.22 -  /* physical rendering */
   17.23 -
   17.24 -  val outdated_color = new Color(240, 240, 240)
   17.25 -  val unfinished_color = new Color(255, 228, 225)
   17.26 -
   17.27 -  val light_color = new Color(240, 240, 240)
   17.28 -  val regular_color = new Color(192, 192, 192)
   17.29 -  val warning_color = new Color(255, 140, 0)
   17.30 -  val error_color = new Color(178, 34, 34)
   17.31 -  val bad_color = new Color(255, 106, 106, 100)
   17.32 -  val hilite_color = new Color(255, 204, 102, 100)
   17.33 -
   17.34 -  class Icon(val priority: Int, val icon: javax.swing.Icon)
   17.35 -  {
   17.36 -    def >= (that: Icon): Boolean = this.priority >= that.priority
   17.37 -  }
   17.38 -  val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png"))
   17.39 -  val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png"))
   17.40 -
   17.41 -
   17.42 -  /* command status */
   17.43 -
   17.44 -  def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   17.45 -  {
   17.46 -    val state = snapshot.state(command)
   17.47 -    if (snapshot.is_outdated) Some(outdated_color)
   17.48 -    else
   17.49 -      Isar_Document.command_status(state.status) match {
   17.50 -        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
   17.51 -        case Isar_Document.Unprocessed => Some(unfinished_color)
   17.52 -        case _ => None
   17.53 -      }
   17.54 -  }
   17.55 -
   17.56 -  def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   17.57 -  {
   17.58 -    val state = snapshot.state(command)
   17.59 -    if (snapshot.is_outdated) None
   17.60 -    else
   17.61 -      Isar_Document.command_status(state.status) match {
   17.62 -        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
   17.63 -        case Isar_Document.Unprocessed => Some(unfinished_color)
   17.64 -        case Isar_Document.Failed => Some(error_color)
   17.65 -        case Isar_Document.Finished =>
   17.66 -          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
   17.67 -          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
   17.68 -          else None
   17.69 -      }
   17.70 -  }
   17.71 -
   17.72 -
   17.73 -  /* markup selectors */
   17.74 -
   17.75 -  val message: Markup_Tree.Select[Color] =
   17.76 -  {
   17.77 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
   17.78 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
   17.79 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   17.80 -  }
   17.81 -
   17.82 -  val popup: Markup_Tree.Select[String] =
   17.83 -  {
   17.84 -    case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
   17.85 -    if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
   17.86 -      Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
   17.87 -  }
   17.88 -
   17.89 -  val gutter_message: Markup_Tree.Select[Icon] =
   17.90 -  {
   17.91 -    case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
   17.92 -    case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
   17.93 -  }
   17.94 -
   17.95 -  val background1: Markup_Tree.Select[Color] =
   17.96 -  {
   17.97 -    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
   17.98 -    case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
   17.99 -  }
  17.100 -
  17.101 -  val background2: Markup_Tree.Select[Color] =
  17.102 -  {
  17.103 -    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
  17.104 -  }
  17.105 -
  17.106 -  val tooltip: Markup_Tree.Select[String] =
  17.107 -  {
  17.108 -    case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
  17.109 -    case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
  17.110 -      Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
  17.111 -        margin = Isabelle.Int_Property("tooltip-margin"))
  17.112 -    case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
  17.113 -    case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
  17.114 -    case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
  17.115 -    case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
  17.116 -    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token"
  17.117 -    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)"
  17.118 -    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)"
  17.119 -    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)"
  17.120 -    case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable"
  17.121 -    case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable"
  17.122 -    case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable"
  17.123 -  }
  17.124 -
  17.125 -  private val subexp_include =
  17.126 -    Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
  17.127 -      Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
  17.128 -      Markup.TFREE, Markup.TVAR)
  17.129 -
  17.130 -  val subexp: Markup_Tree.Select[(Text.Range, Color)] =
  17.131 -  {
  17.132 -    case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
  17.133 -      (range, Color.black)
  17.134 -  }
  17.135 -
  17.136 -
  17.137 -  /* token markup -- text styles */
  17.138 -
  17.139 -  private val command_style: Map[String, Byte] =
  17.140 -  {
  17.141 -    import Token._
  17.142 -    Map[String, Byte](
  17.143 -      Keyword.THY_END -> KEYWORD2,
  17.144 -      Keyword.THY_SCRIPT -> LABEL,
  17.145 -      Keyword.PRF_SCRIPT -> LABEL,
  17.146 -      Keyword.PRF_ASM -> KEYWORD3,
  17.147 -      Keyword.PRF_ASM_GOAL -> KEYWORD3
  17.148 -    ).withDefaultValue(KEYWORD1)
  17.149 -  }
  17.150 -
  17.151 -  private val token_style: Map[String, Byte] =
  17.152 -  {
  17.153 -    import Token._
  17.154 -    Map[String, Byte](
  17.155 -      // logical entities
  17.156 -      Markup.TCLASS -> NULL,
  17.157 -      Markup.TYCON -> NULL,
  17.158 -      Markup.FIXED -> NULL,
  17.159 -      Markup.CONST -> LITERAL2,
  17.160 -      Markup.DYNAMIC_FACT -> LABEL,
  17.161 -      // inner syntax
  17.162 -      Markup.TFREE -> NULL,
  17.163 -      Markup.FREE -> MARKUP,
  17.164 -      Markup.TVAR -> NULL,
  17.165 -      Markup.SKOLEM -> COMMENT2,
  17.166 -      Markup.BOUND -> LABEL,
  17.167 -      Markup.VAR -> NULL,
  17.168 -      Markup.NUM -> DIGIT,
  17.169 -      Markup.FLOAT -> DIGIT,
  17.170 -      Markup.XNUM -> DIGIT,
  17.171 -      Markup.XSTR -> LITERAL4,
  17.172 -      Markup.LITERAL -> OPERATOR,
  17.173 -      Markup.INNER_COMMENT -> COMMENT1,
  17.174 -      Markup.SORT -> NULL,
  17.175 -      Markup.TYP -> NULL,
  17.176 -      Markup.TERM -> NULL,
  17.177 -      Markup.PROP -> NULL,
  17.178 -      // ML syntax
  17.179 -      Markup.ML_KEYWORD -> KEYWORD1,
  17.180 -      Markup.ML_DELIMITER -> OPERATOR,
  17.181 -      Markup.ML_IDENT -> NULL,
  17.182 -      Markup.ML_TVAR -> NULL,
  17.183 -      Markup.ML_NUMERAL -> DIGIT,
  17.184 -      Markup.ML_CHAR -> LITERAL1,
  17.185 -      Markup.ML_STRING -> LITERAL1,
  17.186 -      Markup.ML_COMMENT -> COMMENT1,
  17.187 -      Markup.ML_MALFORMED -> INVALID,
  17.188 -      // embedded source text
  17.189 -      Markup.ML_SOURCE -> COMMENT3,
  17.190 -      Markup.DOC_SOURCE -> COMMENT3,
  17.191 -      Markup.ANTIQ -> COMMENT4,
  17.192 -      Markup.ML_ANTIQ -> COMMENT4,
  17.193 -      Markup.DOC_ANTIQ -> COMMENT4,
  17.194 -      // outer syntax
  17.195 -      Markup.KEYWORD -> KEYWORD2,
  17.196 -      Markup.OPERATOR -> OPERATOR,
  17.197 -      Markup.COMMAND -> KEYWORD1,
  17.198 -      Markup.IDENT -> NULL,
  17.199 -      Markup.VERBATIM -> COMMENT3,
  17.200 -      Markup.COMMENT -> COMMENT1,
  17.201 -      Markup.CONTROL -> COMMENT3,
  17.202 -      Markup.MALFORMED -> INVALID,
  17.203 -      Markup.STRING -> LITERAL3,
  17.204 -      Markup.ALTSTRING -> LITERAL1
  17.205 -    ).withDefaultValue(NULL)
  17.206 -  }
  17.207 -
  17.208 -  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
  17.209 -  {
  17.210 -    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
  17.211 -    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
  17.212 -
  17.213 -    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
  17.214 -    if token_style(kind) != Token.NULL => token_style(kind)
  17.215 -
  17.216 -    case Text.Info(_, XML.Elem(Markup(name, _), _))
  17.217 -    if token_style(name) != Token.NULL => token_style(name)
  17.218 -  }
  17.219 -}
    18.1 --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala	Wed Jun 08 17:32:31 2011 +0200
    18.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.3 @@ -1,67 +0,0 @@
    18.4 -/*  Title:      Tools/jEdit/src/jedit/isabelle_options.scala
    18.5 -    Author:     Johannes Hölzl, TU Munich
    18.6 -
    18.7 -Editor pane for plugin options.
    18.8 -*/
    18.9 -
   18.10 -package isabelle.jedit
   18.11 -
   18.12 -
   18.13 -import isabelle._
   18.14 -
   18.15 -import javax.swing.JSpinner
   18.16 -
   18.17 -import scala.swing.CheckBox
   18.18 -
   18.19 -import org.gjt.sp.jedit.AbstractOptionPane
   18.20 -
   18.21 -
   18.22 -class Isabelle_Options extends AbstractOptionPane("isabelle")
   18.23 -{
   18.24 -  private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic"))
   18.25 -  private val auto_start = new CheckBox()
   18.26 -  private val relative_font_size = new JSpinner()
   18.27 -  private val tooltip_font_size = new JSpinner()
   18.28 -  private val tooltip_margin = new JSpinner()
   18.29 -  private val tooltip_dismiss_delay = new JSpinner()
   18.30 -
   18.31 -  override def _init()
   18.32 -  {
   18.33 -    addComponent(Isabelle.Property("logic.title"), logic_selector.peer)
   18.34 -
   18.35 -    addComponent(Isabelle.Property("auto-start.title"), auto_start.peer)
   18.36 -    auto_start.selected = Isabelle.Boolean_Property("auto-start")
   18.37 -
   18.38 -    relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100))
   18.39 -    addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size)
   18.40 -
   18.41 -    tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10))
   18.42 -    addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size)
   18.43 -
   18.44 -    tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40))
   18.45 -    addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin)
   18.46 -
   18.47 -    tooltip_dismiss_delay.setValue(
   18.48 -      Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt)
   18.49 -    addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay)
   18.50 -  }
   18.51 -
   18.52 -  override def _save()
   18.53 -  {
   18.54 -    Isabelle.Property("logic") = logic_selector.selection.item.name
   18.55 -
   18.56 -    Isabelle.Boolean_Property("auto-start") = auto_start.selected
   18.57 -
   18.58 -    Isabelle.Int_Property("relative-font-size") =
   18.59 -      relative_font_size.getValue().asInstanceOf[Int]
   18.60 -
   18.61 -    Isabelle.Int_Property("tooltip-font-size") =
   18.62 -      tooltip_font_size.getValue().asInstanceOf[Int]
   18.63 -
   18.64 -    Isabelle.Int_Property("tooltip-margin") =
   18.65 -      tooltip_margin.getValue().asInstanceOf[Int]
   18.66 -
   18.67 -    Isabelle.Time_Property("tooltip-dismiss-delay") =
   18.68 -      Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int])
   18.69 -  }
   18.70 -}
    19.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Jun 08 17:32:31 2011 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,176 +0,0 @@
    19.4 -/*  Title:      Tools/jEdit/src/jedit/isabelle_sidekick.scala
    19.5 -    Author:     Fabian Immler, TU Munich
    19.6 -    Author:     Makarius
    19.7 -
    19.8 -SideKick parsers for Isabelle proof documents.
    19.9 -*/
   19.10 -
   19.11 -package isabelle.jedit
   19.12 -
   19.13 -
   19.14 -import isabelle._
   19.15 -
   19.16 -import scala.collection.Set
   19.17 -import scala.collection.immutable.TreeSet
   19.18 -
   19.19 -import javax.swing.tree.DefaultMutableTreeNode
   19.20 -import javax.swing.text.Position
   19.21 -import javax.swing.Icon
   19.22 -
   19.23 -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View}
   19.24 -import errorlist.DefaultErrorSource
   19.25 -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset}
   19.26 -
   19.27 -
   19.28 -object Isabelle_Sidekick
   19.29 -{
   19.30 -  def int_to_pos(offset: Text.Offset): Position =
   19.31 -    new Position { def getOffset = offset; override def toString = offset.toString }
   19.32 -
   19.33 -  class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset
   19.34 -  {
   19.35 -    protected var _name = name
   19.36 -    protected var _start = int_to_pos(start)
   19.37 -    protected var _end = int_to_pos(end)
   19.38 -    override def getIcon: Icon = null
   19.39 -    override def getShortString: String = _name
   19.40 -    override def getLongString: String = _name
   19.41 -    override def getName: String = _name
   19.42 -    override def setName(name: String) = _name = name
   19.43 -    override def getStart: Position = _start
   19.44 -    override def setStart(start: Position) = _start = start
   19.45 -    override def getEnd: Position = _end
   19.46 -    override def setEnd(end: Position) = _end = end
   19.47 -    override def toString = _name
   19.48 -  }
   19.49 -}
   19.50 -
   19.51 -
   19.52 -abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name)
   19.53 -{
   19.54 -  /* parsing */
   19.55 -
   19.56 -  @volatile protected var stopped = false
   19.57 -  override def stop() = { stopped = true }
   19.58 -
   19.59 -  def parser(data: SideKickParsedData, model: Document_Model): Unit
   19.60 -
   19.61 -  def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData =
   19.62 -  {
   19.63 -    stopped = false
   19.64 -
   19.65 -    // FIXME lock buffer (!??)
   19.66 -    val data = new SideKickParsedData(buffer.getName)
   19.67 -    val root = data.root
   19.68 -    data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength))
   19.69 -
   19.70 -    Swing_Thread.now { Document_Model(buffer) } match {
   19.71 -      case Some(model) =>
   19.72 -        parser(data, model)
   19.73 -        if (stopped) root.add(new DefaultMutableTreeNode("<parser stopped>"))
   19.74 -      case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
   19.75 -    }
   19.76 -    data
   19.77 -  }
   19.78 -
   19.79 -
   19.80 -  /* completion */
   19.81 -
   19.82 -  override def supportsCompletion = true
   19.83 -  override def canCompleteAnywhere = true
   19.84 -
   19.85 -  override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion =
   19.86 -  {
   19.87 -    val buffer = pane.getBuffer
   19.88 -    Isabelle.swing_buffer_lock(buffer) {
   19.89 -      Document_Model(buffer) match {
   19.90 -        case None => null
   19.91 -        case Some(model) =>
   19.92 -          val line = buffer.getLineOfOffset(caret)
   19.93 -          val start = buffer.getLineStartOffset(line)
   19.94 -          val text = buffer.getSegment(start, caret - start)
   19.95 -
   19.96 -          val completion = model.session.current_syntax().completion
   19.97 -          completion.complete(text) match {
   19.98 -            case None => null
   19.99 -            case Some((word, cs)) =>
  19.100 -              val ds =
  19.101 -                (if (Isabelle_Encoding.is_active(buffer))
  19.102 -                  cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _)
  19.103 -                 else cs).filter(_ != word)
  19.104 -              if (ds.isEmpty) null
  19.105 -              else new SideKickCompletion(
  19.106 -                pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { }
  19.107 -          }
  19.108 -      }
  19.109 -    }
  19.110 -  }
  19.111 -}
  19.112 -
  19.113 -
  19.114 -class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
  19.115 -{
  19.116 -  import Thy_Syntax.Structure
  19.117 -
  19.118 -  def parser(data: SideKickParsedData, model: Document_Model)
  19.119 -  {
  19.120 -    val syntax = model.session.current_syntax()
  19.121 -
  19.122 -    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
  19.123 -      entry match {
  19.124 -        case Structure.Block(name, body) =>
  19.125 -          val node =
  19.126 -            new DefaultMutableTreeNode(
  19.127 -              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
  19.128 -          (offset /: body)((i, e) =>
  19.129 -            {
  19.130 -              make_tree(i, e) foreach (nd => node.add(nd))
  19.131 -              i + e.length
  19.132 -            })
  19.133 -          List(node)
  19.134 -        case Structure.Atom(command)
  19.135 -        if command.is_command && syntax.heading_level(command).isEmpty =>
  19.136 -          val node =
  19.137 -            new DefaultMutableTreeNode(
  19.138 -              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
  19.139 -          List(node)
  19.140 -        case _ => Nil
  19.141 -      }
  19.142 -
  19.143 -    val text = Isabelle.buffer_text(model.buffer)
  19.144 -    val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
  19.145 -
  19.146 -    make_tree(0, structure) foreach (node => data.root.add(node))
  19.147 -  }
  19.148 -}
  19.149 -
  19.150 -
  19.151 -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw")
  19.152 -{
  19.153 -  def parser(data: SideKickParsedData, model: Document_Model)
  19.154 -  {
  19.155 -    val root = data.root
  19.156 -    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
  19.157 -    for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
  19.158 -      snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
  19.159 -          {
  19.160 -            val range = info.range + command_start
  19.161 -            val content = command.source(info.range).replace('\n', ' ')
  19.162 -            val info_text =
  19.163 -              info.info match {
  19.164 -                case elem @ XML.Elem(_, _) =>
  19.165 -                  Pretty.formatted(List(elem), margin = 40).mkString("\n")
  19.166 -                case x => x.toString
  19.167 -              }
  19.168 -
  19.169 -            new DefaultMutableTreeNode(
  19.170 -              new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) {
  19.171 -                override def getShortString: String = content
  19.172 -                override def getLongString: String = info_text
  19.173 -                override def toString = "\"" + content + "\" " + range.toString
  19.174 -              })
  19.175 -          })
  19.176 -    }
  19.177 -  }
  19.178 -}
  19.179 -
    20.1 --- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Wed Jun 08 17:32:31 2011 +0200
    20.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.3 @@ -1,163 +0,0 @@
    20.4 -/*  Title:      Tools/jEdit/src/jedit/output_dockable.scala
    20.5 -    Author:     Makarius
    20.6 -
    20.7 -Dockable window with result message output.
    20.8 -*/
    20.9 -
   20.10 -package isabelle.jedit
   20.11 -
   20.12 -
   20.13 -import isabelle._
   20.14 -
   20.15 -import scala.actors.Actor._
   20.16 -
   20.17 -import scala.swing.{FlowPanel, Button, CheckBox}
   20.18 -import scala.swing.event.ButtonClicked
   20.19 -
   20.20 -import java.awt.BorderLayout
   20.21 -import java.awt.event.{ComponentEvent, ComponentAdapter}
   20.22 -
   20.23 -import org.gjt.sp.jedit.View
   20.24 -
   20.25 -
   20.26 -class Output_Dockable(view: View, position: String) extends Dockable(view, position)
   20.27 -{
   20.28 -  Swing_Thread.require()
   20.29 -
   20.30 -  private val html_panel =
   20.31 -    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   20.32 -  {
   20.33 -    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
   20.34 -      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
   20.35 -        val text = elem.getFirstChild().getNodeValue()
   20.36 -
   20.37 -        Document_View(view.getTextArea) match {
   20.38 -          case Some(doc_view) =>
   20.39 -            val cmd = current_command.get
   20.40 -            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
   20.41 -            val buffer = view.getBuffer
   20.42 -            buffer.beginCompoundEdit()
   20.43 -            buffer.remove(start_ofs, cmd.length)
   20.44 -            buffer.insert(start_ofs, text)
   20.45 -            buffer.endCompoundEdit()
   20.46 -          case None =>
   20.47 -        }
   20.48 -    }       
   20.49 -  }
   20.50 -
   20.51 -  set_content(html_panel)
   20.52 -
   20.53 -
   20.54 -  /* component state -- owned by Swing thread */
   20.55 -
   20.56 -  private var zoom_factor = 100
   20.57 -  private var show_tracing = false
   20.58 -  private var follow_caret = true
   20.59 -  private var current_command: Option[Command] = None
   20.60 -
   20.61 -
   20.62 -  private def handle_resize()
   20.63 -  {
   20.64 -    Swing_Thread.now {
   20.65 -      html_panel.resize(Isabelle.font_family(),
   20.66 -        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
   20.67 -    }
   20.68 -  }
   20.69 -
   20.70 -  private def handle_perspective(): Boolean =
   20.71 -    Swing_Thread.now {
   20.72 -      Document_View(view.getTextArea) match {
   20.73 -        case Some(doc_view) =>
   20.74 -          val cmd = doc_view.selected_command()
   20.75 -          if (current_command == cmd) false
   20.76 -          else { current_command = cmd; true }
   20.77 -        case None => false
   20.78 -      }
   20.79 -    }
   20.80 -
   20.81 -  private def handle_update(restriction: Option[Set[Command]] = None)
   20.82 -  {
   20.83 -    Swing_Thread.now {
   20.84 -      if (follow_caret) handle_perspective()
   20.85 -      Document_View(view.getTextArea) match {
   20.86 -        case Some(doc_view) =>
   20.87 -          current_command match {
   20.88 -            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
   20.89 -              val snapshot = doc_view.model.snapshot()
   20.90 -              val filtered_results =
   20.91 -                snapshot.state(cmd).results.iterator.map(_._2) filter {
   20.92 -                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
   20.93 -                  case _ => true
   20.94 -                }
   20.95 -              html_panel.render(filtered_results.toList)
   20.96 -            case _ =>
   20.97 -          }
   20.98 -        case None =>
   20.99 -      }
  20.100 -    }
  20.101 -  }
  20.102 -
  20.103 -
  20.104 -  /* main actor */
  20.105 -
  20.106 -  private val main_actor = actor {
  20.107 -    loop {
  20.108 -      react {
  20.109 -        case Session.Global_Settings => handle_resize()
  20.110 -        case Session.Commands_Changed(changed) => handle_update(Some(changed))
  20.111 -        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
  20.112 -        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
  20.113 -      }
  20.114 -    }
  20.115 -  }
  20.116 -
  20.117 -  override def init()
  20.118 -  {
  20.119 -    Isabelle.session.global_settings += main_actor
  20.120 -    Isabelle.session.commands_changed += main_actor
  20.121 -    Isabelle.session.perspective += main_actor
  20.122 -  }
  20.123 -
  20.124 -  override def exit()
  20.125 -  {
  20.126 -    Isabelle.session.global_settings -= main_actor
  20.127 -    Isabelle.session.commands_changed -= main_actor
  20.128 -    Isabelle.session.perspective -= main_actor
  20.129 -  }
  20.130 -
  20.131 -
  20.132 -  /* resize */
  20.133 -
  20.134 -  addComponentListener(new ComponentAdapter {
  20.135 -    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
  20.136 -    override def componentResized(e: ComponentEvent) { delay() }
  20.137 -  })
  20.138 -
  20.139 -
  20.140 -  /* controls */
  20.141 -
  20.142 -  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
  20.143 -  zoom.tooltip = "Zoom factor for basic font size"
  20.144 -
  20.145 -  private val tracing = new CheckBox("Tracing") {
  20.146 -    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
  20.147 -  }
  20.148 -  tracing.selected = show_tracing
  20.149 -  tracing.tooltip = "Indicate output of tracing messages"
  20.150 -
  20.151 -  private val auto_update = new CheckBox("Auto update") {
  20.152 -    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
  20.153 -  }
  20.154 -  auto_update.selected = follow_caret
  20.155 -  auto_update.tooltip = "Indicate automatic update following cursor movement"
  20.156 -
  20.157 -  private val update = new Button("Update") {
  20.158 -    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
  20.159 -  }
  20.160 -  update.tooltip = "Update display according to the command at cursor position"
  20.161 -
  20.162 -  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
  20.163 -  add(controls.peer, BorderLayout.NORTH)
  20.164 -
  20.165 -  handle_update()
  20.166 -}
    21.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Wed Jun 08 17:32:31 2011 +0200
    21.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.3 @@ -1,401 +0,0 @@
    21.4 -/*  Title:      Tools/jEdit/src/jedit/plugin.scala
    21.5 -    Author:     Makarius
    21.6 -
    21.7 -Main Isabelle/jEdit plugin setup.
    21.8 -*/
    21.9 -
   21.10 -package isabelle.jedit
   21.11 -
   21.12 -
   21.13 -import isabelle._
   21.14 -
   21.15 -import java.io.{FileInputStream, IOException}
   21.16 -import java.awt.Font
   21.17 -
   21.18 -import scala.collection.mutable
   21.19 -import scala.swing.ComboBox
   21.20 -
   21.21 -import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   21.22 -  Buffer, EditPane, ServiceManager, View}
   21.23 -import org.gjt.sp.jedit.buffer.JEditBuffer
   21.24 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
   21.25 -import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
   21.26 -import org.gjt.sp.jedit.gui.DockableWindowManager
   21.27 -
   21.28 -import org.gjt.sp.util.Log
   21.29 -
   21.30 -import scala.actors.Actor
   21.31 -import Actor._
   21.32 -
   21.33 -
   21.34 -object Isabelle
   21.35 -{
   21.36 -  /* plugin instance */
   21.37 -
   21.38 -  var system: Isabelle_System = null
   21.39 -  var session: Session = null
   21.40 -
   21.41 -
   21.42 -  /* properties */
   21.43 -
   21.44 -  val OPTION_PREFIX = "options.isabelle."
   21.45 -
   21.46 -  object Property
   21.47 -  {
   21.48 -    def apply(name: String): String =
   21.49 -      jEdit.getProperty(OPTION_PREFIX + name)
   21.50 -    def apply(name: String, default: String): String =
   21.51 -      jEdit.getProperty(OPTION_PREFIX + name, default)
   21.52 -    def update(name: String, value: String) =
   21.53 -      jEdit.setProperty(OPTION_PREFIX + name, value)
   21.54 -  }
   21.55 -
   21.56 -  object Boolean_Property
   21.57 -  {
   21.58 -    def apply(name: String): Boolean =
   21.59 -      jEdit.getBooleanProperty(OPTION_PREFIX + name)
   21.60 -    def apply(name: String, default: Boolean): Boolean =
   21.61 -      jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
   21.62 -    def update(name: String, value: Boolean) =
   21.63 -      jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
   21.64 -  }
   21.65 -
   21.66 -  object Int_Property
   21.67 -  {
   21.68 -    def apply(name: String): Int =
   21.69 -      jEdit.getIntegerProperty(OPTION_PREFIX + name)
   21.70 -    def apply(name: String, default: Int): Int =
   21.71 -      jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
   21.72 -    def update(name: String, value: Int) =
   21.73 -      jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   21.74 -  }
   21.75 -
   21.76 -  object Double_Property
   21.77 -  {
   21.78 -    def apply(name: String): Double =
   21.79 -      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
   21.80 -    def apply(name: String, default: Double): Double =
   21.81 -      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
   21.82 -    def update(name: String, value: Double) =
   21.83 -      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
   21.84 -  }
   21.85 -
   21.86 -  object Time_Property
   21.87 -  {
   21.88 -    def apply(name: String): Time =
   21.89 -      Time.seconds(Double_Property(name))
   21.90 -    def apply(name: String, default: Time): Time =
   21.91 -      Time.seconds(Double_Property(name, default.seconds))
   21.92 -    def update(name: String, value: Time) =
   21.93 -      Double_Property.update(name, value.seconds)
   21.94 -  }
   21.95 -
   21.96 -
   21.97 -  /* font */
   21.98 -
   21.99 -  def font_family(): String = jEdit.getProperty("view.font")
  21.100 -
  21.101 -  def font_size(): Float =
  21.102 -    (jEdit.getIntegerProperty("view.fontsize", 16) *
  21.103 -      Int_Property("relative-font-size", 100)).toFloat / 100
  21.104 -
  21.105 -
  21.106 -  /* text area ranges */
  21.107 -
  21.108 -  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
  21.109 -
  21.110 -  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
  21.111 -  {
  21.112 -    val p = text_area.offsetToXY(range.start)
  21.113 -    val q = text_area.offsetToXY(range.stop)
  21.114 -    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
  21.115 -    else None
  21.116 -  }
  21.117 -
  21.118 -
  21.119 -  /* tooltip markup */
  21.120 -
  21.121 -  def tooltip(text: String): String =
  21.122 -    "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
  21.123 -        Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
  21.124 -      HTML.encode(text) + "</pre></html>"
  21.125 -
  21.126 -  def tooltip_dismiss_delay(): Time =
  21.127 -    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
  21.128 -
  21.129 -  def setup_tooltips()
  21.130 -  {
  21.131 -    Swing_Thread.now {
  21.132 -      val manager = javax.swing.ToolTipManager.sharedInstance
  21.133 -      manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
  21.134 -    }
  21.135 -  }
  21.136 -
  21.137 -
  21.138 -  /* icons */
  21.139 -
  21.140 -  def load_icon(name: String): javax.swing.Icon =
  21.141 -  {
  21.142 -    val icon = GUIUtilities.loadIcon(name)
  21.143 -    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
  21.144 -      Log.log(Log.ERROR, icon, "Bad icon: " + name)
  21.145 -    icon
  21.146 -  }
  21.147 -
  21.148 -
  21.149 -  /* check JVM */
  21.150 -
  21.151 -  def check_jvm()
  21.152 -  {
  21.153 -    if (!Platform.is_hotspot) {
  21.154 -      Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
  21.155 -        "This is " + Platform.jvm_name,
  21.156 -        "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
  21.157 -    }
  21.158 -  }
  21.159 -
  21.160 -
  21.161 -  /* main jEdit components */
  21.162 -
  21.163 -  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
  21.164 -
  21.165 -  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
  21.166 -
  21.167 -  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
  21.168 -    view.getEditPanes().iterator.map(_.getTextArea)
  21.169 -
  21.170 -  def jedit_text_areas(): Iterator[JEditTextArea] =
  21.171 -    jedit_views().flatMap(jedit_text_areas(_))
  21.172 -
  21.173 -  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
  21.174 -    jedit_text_areas().filter(_.getBuffer == buffer)
  21.175 -
  21.176 -  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
  21.177 -  {
  21.178 -    try { buffer.readLock(); body }
  21.179 -    finally { buffer.readUnlock() }
  21.180 -  }
  21.181 -
  21.182 -  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
  21.183 -    Swing_Thread.now { buffer_lock(buffer) { body } }
  21.184 -
  21.185 -  def buffer_text(buffer: JEditBuffer): String =
  21.186 -    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
  21.187 -
  21.188 -
  21.189 -  /* dockable windows */
  21.190 -
  21.191 -  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
  21.192 -
  21.193 -  def docked_session(view: View): Option[Session_Dockable] =
  21.194 -    wm(view).getDockableWindow("isabelle-session") match {
  21.195 -      case dockable: Session_Dockable => Some(dockable)
  21.196 -      case _ => None
  21.197 -    }
  21.198 -
  21.199 -  def docked_output(view: View): Option[Output_Dockable] =
  21.200 -    wm(view).getDockableWindow("isabelle-output") match {
  21.201 -      case dockable: Output_Dockable => Some(dockable)
  21.202 -      case _ => None
  21.203 -    }
  21.204 -
  21.205 -  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
  21.206 -    wm(view).getDockableWindow("isabelle-raw-output") match {
  21.207 -      case dockable: Raw_Output_Dockable => Some(dockable)
  21.208 -      case _ => None
  21.209 -    }
  21.210 -
  21.211 -  def docked_protocol(view: View): Option[Protocol_Dockable] =
  21.212 -    wm(view).getDockableWindow("isabelle-protocol") match {
  21.213 -      case dockable: Protocol_Dockable => Some(dockable)
  21.214 -      case _ => None
  21.215 -    }
  21.216 -
  21.217 -
  21.218 -  /* logic image */
  21.219 -
  21.220 -  def default_logic(): String =
  21.221 -  {
  21.222 -    val logic = system.getenv("JEDIT_LOGIC")
  21.223 -    if (logic != "") logic
  21.224 -    else system.getenv_strict("ISABELLE_LOGIC")
  21.225 -  }
  21.226 -
  21.227 -  class Logic_Entry(val name: String, val description: String)
  21.228 -  {
  21.229 -    override def toString = description
  21.230 -  }
  21.231 -
  21.232 -  def logic_selector(logic: String): ComboBox[Logic_Entry] =
  21.233 -  {
  21.234 -    val entries =
  21.235 -      new Logic_Entry("", "default (" + default_logic() + ")") ::
  21.236 -        system.find_logics().map(name => new Logic_Entry(name, name))
  21.237 -    val component = new ComboBox(entries)
  21.238 -    entries.find(_.name == logic) match {
  21.239 -      case None =>
  21.240 -      case Some(entry) => component.selection.item = entry
  21.241 -    }
  21.242 -    component.tooltip = "Isabelle logic image"
  21.243 -    component
  21.244 -  }
  21.245 -
  21.246 -  def start_session()
  21.247 -  {
  21.248 -    val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
  21.249 -    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
  21.250 -    val logic = {
  21.251 -      val logic = Property("logic")
  21.252 -      if (logic != null && logic != "") logic
  21.253 -      else Isabelle.default_logic()
  21.254 -    }
  21.255 -    session.start(timeout, modes ::: List(logic))
  21.256 -  }
  21.257 -}
  21.258 -
  21.259 -
  21.260 -class Plugin extends EBPlugin
  21.261 -{
  21.262 -  /* session management */
  21.263 -
  21.264 -  private def init_model(buffer: Buffer)
  21.265 -  {
  21.266 -    Isabelle.swing_buffer_lock(buffer) {
  21.267 -      val opt_model =
  21.268 -        Document_Model(buffer) match {
  21.269 -          case Some(model) => model.refresh; Some(model)
  21.270 -          case None =>
  21.271 -            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
  21.272 -              case Some((dir, thy_name)) =>
  21.273 -                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
  21.274 -              case None => None
  21.275 -            }
  21.276 -        }
  21.277 -      if (opt_model.isDefined) {
  21.278 -        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
  21.279 -          if (Document_View(text_area).map(_.model) != opt_model)
  21.280 -            Document_View.init(opt_model.get, text_area)
  21.281 -        }
  21.282 -      }
  21.283 -    }
  21.284 -  }
  21.285 -
  21.286 -  private def exit_model(buffer: Buffer)
  21.287 -  {
  21.288 -    Isabelle.swing_buffer_lock(buffer) {
  21.289 -      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
  21.290 -      Document_Model.exit(buffer)
  21.291 -    }
  21.292 -  }
  21.293 -
  21.294 -  private case class Init_Model(buffer: Buffer)
  21.295 -  private case class Exit_Model(buffer: Buffer)
  21.296 -  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
  21.297 -  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
  21.298 -
  21.299 -  private val session_manager = actor {
  21.300 -    var ready = false
  21.301 -    loop {
  21.302 -      react {
  21.303 -        case phase: Session.Phase =>
  21.304 -          ready = phase == Session.Ready
  21.305 -          phase match {
  21.306 -            case Session.Failed =>
  21.307 -              Swing_Thread.now {
  21.308 -                val text = new scala.swing.TextArea(Isabelle.session.syslog())
  21.309 -                text.editable = false
  21.310 -                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
  21.311 -              }
  21.312 -
  21.313 -            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
  21.314 -            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
  21.315 -            case _ =>
  21.316 -          }
  21.317 -
  21.318 -        case Init_Model(buffer) =>
  21.319 -          if (ready) init_model(buffer)
  21.320 -
  21.321 -        case Exit_Model(buffer) =>
  21.322 -          exit_model(buffer)
  21.323 -
  21.324 -        case Init_View(buffer, text_area) =>
  21.325 -          if (ready) {
  21.326 -            Isabelle.swing_buffer_lock(buffer) {
  21.327 -              Document_Model(buffer) match {
  21.328 -                case Some(model) => Document_View.init(model, text_area)
  21.329 -                case None =>
  21.330 -              }
  21.331 -            }
  21.332 -          }
  21.333 -
  21.334 -        case Exit_View(buffer, text_area) =>
  21.335 -          Isabelle.swing_buffer_lock(buffer) {
  21.336 -            Document_View.exit(text_area)
  21.337 -          }
  21.338 -
  21.339 -        case bad => System.err.println("session_manager: ignoring bad message " + bad)
  21.340 -      }
  21.341 -    }
  21.342 -  }
  21.343 -
  21.344 -
  21.345 -  /* main plugin plumbing */
  21.346 -
  21.347 -  override def handleMessage(message: EBMessage)
  21.348 -  {
  21.349 -    message match {
  21.350 -      case msg: EditorStarted =>
  21.351 -      Isabelle.check_jvm()
  21.352 -      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
  21.353 -
  21.354 -      case msg: BufferUpdate
  21.355 -      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
  21.356 -
  21.357 -        val buffer = msg.getBuffer
  21.358 -        if (buffer != null) session_manager ! Init_Model(buffer)
  21.359 -
  21.360 -      case msg: EditPaneUpdate
  21.361 -      if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
  21.362 -          msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
  21.363 -          msg.getWhat == EditPaneUpdate.CREATED ||
  21.364 -          msg.getWhat == EditPaneUpdate.DESTROYED) =>
  21.365 -
  21.366 -        val edit_pane = msg.getEditPane
  21.367 -        val buffer = edit_pane.getBuffer
  21.368 -        val text_area = edit_pane.getTextArea
  21.369 -
  21.370 -        if (buffer != null && text_area != null) {
  21.371 -          if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
  21.372 -              msg.getWhat == EditPaneUpdate.CREATED)
  21.373 -            session_manager ! Init_View(buffer, text_area)
  21.374 -          else
  21.375 -            session_manager ! Exit_View(buffer, text_area)
  21.376 -        }
  21.377 -
  21.378 -      case msg: PropertiesChanged =>
  21.379 -        Swing_Thread.now {
  21.380 -          Isabelle.setup_tooltips()
  21.381 -          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
  21.382 -            Document_View(text_area).get.extend_styles()
  21.383 -        }
  21.384 -        Isabelle.session.global_settings.event(Session.Global_Settings)
  21.385 -
  21.386 -      case _ =>
  21.387 -    }
  21.388 -  }
  21.389 -
  21.390 -  override def start()
  21.391 -  {
  21.392 -    Isabelle.setup_tooltips()
  21.393 -    Isabelle.system = new Isabelle_System
  21.394 -    Isabelle.system.install_fonts()
  21.395 -    Isabelle.session = new Session(Isabelle.system)
  21.396 -    Isabelle.session.phase_changed += session_manager
  21.397 -  }
  21.398 -
  21.399 -  override def stop()
  21.400 -  {
  21.401 -    Isabelle.session.stop()
  21.402 -    Isabelle.session.phase_changed -= session_manager
  21.403 -  }
  21.404 -}
    22.1 --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala	Wed Jun 08 17:32:31 2011 +0200
    22.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.3 @@ -1,39 +0,0 @@
    22.4 -/*  Title:      Tools/jEdit/src/jedit/protocol_dockable.scala
    22.5 -    Author:     Makarius
    22.6 -
    22.7 -Dockable window for protocol messages.
    22.8 -*/
    22.9 -
   22.10 -package isabelle.jedit
   22.11 -
   22.12 -
   22.13 -import isabelle._
   22.14 -
   22.15 -import scala.actors.Actor._
   22.16 -import scala.swing.{TextArea, ScrollPane}
   22.17 -
   22.18 -import org.gjt.sp.jedit.View
   22.19 -
   22.20 -
   22.21 -class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
   22.22 -{
   22.23 -  private val text_area = new TextArea
   22.24 -  set_content(new ScrollPane(text_area))
   22.25 -
   22.26 -
   22.27 -  /* main actor */
   22.28 -
   22.29 -  private val main_actor = actor {
   22.30 -    loop {
   22.31 -      react {
   22.32 -        case result: Isabelle_Process.Result =>
   22.33 -          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
   22.34 -
   22.35 -        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
   22.36 -      }
   22.37 -    }
   22.38 -  }
   22.39 -
   22.40 -  override def init() { Isabelle.session.raw_messages += main_actor }
   22.41 -  override def exit() { Isabelle.session.raw_messages -= main_actor }
   22.42 -}
    23.1 --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala	Wed Jun 08 17:32:31 2011 +0200
    23.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.3 @@ -1,42 +0,0 @@
    23.4 -/*  Title:      Tools/jEdit/src/jedit/raw_output_dockable.scala
    23.5 -    Author:     Makarius
    23.6 -
    23.7 -Dockable window for raw process output (stdout).
    23.8 -*/
    23.9 -
   23.10 -package isabelle.jedit
   23.11 -
   23.12 -
   23.13 -import isabelle._
   23.14 -
   23.15 -import scala.actors.Actor._
   23.16 -import scala.swing.{TextArea, ScrollPane}
   23.17 -
   23.18 -import org.gjt.sp.jedit.View
   23.19 -
   23.20 -
   23.21 -class Raw_Output_Dockable(view: View, position: String)
   23.22 -  extends Dockable(view: View, position: String)
   23.23 -{
   23.24 -  private val text_area = new TextArea
   23.25 -  text_area.editable = false
   23.26 -  set_content(new ScrollPane(text_area))
   23.27 -
   23.28 -
   23.29 -  /* main actor */
   23.30 -
   23.31 -  private val main_actor = actor {
   23.32 -    loop {
   23.33 -      react {
   23.34 -        case result: Isabelle_Process.Result =>
   23.35 -          if (result.is_stdout)
   23.36 -            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
   23.37 -
   23.38 -        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
   23.39 -      }
   23.40 -    }
   23.41 -  }
   23.42 -
   23.43 -  override def init() { Isabelle.session.raw_messages += main_actor }
   23.44 -  override def exit() { Isabelle.session.raw_messages -= main_actor }
   23.45 -}
    24.1 --- a/src/Tools/jEdit/src/jedit/scala_console.scala	Wed Jun 08 17:32:31 2011 +0200
    24.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.3 @@ -1,155 +0,0 @@
    24.4 -/*  Title:      Tools/jEdit/src/jedit/scala_console.scala
    24.5 -    Author:     Makarius
    24.6 -
    24.7 -Scala instance of Console plugin.
    24.8 -*/
    24.9 -
   24.10 -package isabelle.jedit
   24.11 -
   24.12 -
   24.13 -import isabelle._
   24.14 -
   24.15 -import console.{Console, ConsolePane, Shell, Output}
   24.16 -
   24.17 -import org.gjt.sp.jedit.{jEdit, JARClassLoader}
   24.18 -import org.gjt.sp.jedit.MiscUtilities
   24.19 -
   24.20 -import java.io.{File, OutputStream, Writer, PrintWriter}
   24.21 -
   24.22 -import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
   24.23 -import scala.collection.mutable
   24.24 -
   24.25 -
   24.26 -class Scala_Console extends Shell("Scala")
   24.27 -{
   24.28 -  /* reconstructed jEdit/plugin classpath */
   24.29 -
   24.30 -  private def reconstruct_classpath(): String =
   24.31 -  {
   24.32 -    def find_jars(start: String): List[String] =
   24.33 -      if (start != null)
   24.34 -        Standard_System.find_files(new File(start),
   24.35 -          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
   24.36 -      else Nil
   24.37 -    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
   24.38 -    path.mkString(File.pathSeparator)
   24.39 -  }
   24.40 -
   24.41 -
   24.42 -  /* global state -- owned by Swing thread */
   24.43 -
   24.44 -  private var interpreters = Map[Console, Interpreter]()
   24.45 -
   24.46 -  private var global_console: Console = null
   24.47 -  private var global_out: Output = null
   24.48 -  private var global_err: Output = null
   24.49 -
   24.50 -  private val console_stream = new OutputStream
   24.51 -  {
   24.52 -    val buf = new StringBuilder
   24.53 -    override def flush()
   24.54 -    {
   24.55 -      val str = Standard_System.decode_permissive_utf8(buf.toString)
   24.56 -      buf.clear
   24.57 -      if (global_out == null) System.out.print(str)
   24.58 -      else Swing_Thread.now { global_out.writeAttrs(null, str) }
   24.59 -    }
   24.60 -    override def close() { flush () }
   24.61 -    def write(byte: Int) { buf.append(byte.toChar) }
   24.62 -  }
   24.63 -
   24.64 -  private val console_writer = new Writer
   24.65 -  {
   24.66 -    def flush() {}
   24.67 -    def close() {}
   24.68 -
   24.69 -    def write(cbuf: Array[Char], off: Int, len: Int)
   24.70 -    {
   24.71 -      if (len > 0) write(new String(cbuf.slice(off, off + len)))
   24.72 -    }
   24.73 -
   24.74 -    override def write(str: String)
   24.75 -    {
   24.76 -      if (global_out == null) System.out.println(str)
   24.77 -      else global_out.print(null, str)
   24.78 -    }
   24.79 -  }
   24.80 -
   24.81 -  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
   24.82 -  {
   24.83 -    global_console = console
   24.84 -    global_out = out
   24.85 -    global_err = if (err == null) out else err
   24.86 -    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
   24.87 -    console_stream.flush
   24.88 -    global_console = null
   24.89 -    global_out = null
   24.90 -    global_err = null
   24.91 -    Exn.release(res)
   24.92 -  }
   24.93 -
   24.94 -  private def report_error(str: String)
   24.95 -  {
   24.96 -    if (global_console == null || global_err == null) System.err.println(str)
   24.97 -    else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
   24.98 -  }
   24.99 -
  24.100 -
  24.101 -  /* jEdit console methods */
  24.102 -
  24.103 -  override def openConsole(console: Console)
  24.104 -  {
  24.105 -    val settings = new GenericRunnerSettings(report_error)
  24.106 -    settings.classpath.value = reconstruct_classpath()
  24.107 -
  24.108 -    val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
  24.109 -    {
  24.110 -      override def parentClassLoader = new JARClassLoader
  24.111 -    }
  24.112 -    interp.setContextClassLoader
  24.113 -    interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
  24.114 -    interp.bind("console", "console.Console", console)
  24.115 -    interp.interpret("import isabelle.jedit.Isabelle")
  24.116 -
  24.117 -    interpreters += (console -> interp)
  24.118 -  }
  24.119 -
  24.120 -  override def closeConsole(console: Console)
  24.121 -  {
  24.122 -    interpreters -= console
  24.123 -  }
  24.124 -
  24.125 -  override def printInfoMessage(out: Output)
  24.126 -  {
  24.127 -    out.print(null,
  24.128 -     "This shell evaluates Isabelle/Scala expressions.\n\n" +
  24.129 -     "The following special toplevel bindings are provided:\n" +
  24.130 -     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
  24.131 -     "  console   -- jEdit Console plugin instance\n" +
  24.132 -     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
  24.133 -  }
  24.134 -
  24.135 -  override def printPrompt(console: Console, out: Output)
  24.136 -  {
  24.137 -    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
  24.138 -    out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
  24.139 -  }
  24.140 -
  24.141 -  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
  24.142 -  {
  24.143 -    val interp = interpreters(console)
  24.144 -    with_console(console, out, err) { interp.interpret(command) }
  24.145 -    if (err != null) err.commandDone()
  24.146 -    out.commandDone()
  24.147 -  }
  24.148 -
  24.149 -  override def stop(console: Console)
  24.150 -  {
  24.151 -    closeConsole(console)
  24.152 -    console.clear
  24.153 -    openConsole(console)
  24.154 -    val out = console.getOutput
  24.155 -    out.commandDone
  24.156 -    printPrompt(console, out)
  24.157 -  }
  24.158 -}
    25.1 --- a/src/Tools/jEdit/src/jedit/session_dockable.scala	Wed Jun 08 17:32:31 2011 +0200
    25.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.3 @@ -1,104 +0,0 @@
    25.4 -/*  Title:      Tools/jEdit/src/jedit/session_dockable.scala
    25.5 -    Author:     Makarius
    25.6 -
    25.7 -Dockable window for prover session management.
    25.8 -*/
    25.9 -
   25.10 -package isabelle.jedit
   25.11 -
   25.12 -
   25.13 -import isabelle._
   25.14 -
   25.15 -import scala.actors.Actor._
   25.16 -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
   25.17 -import scala.swing.event.{ButtonClicked, SelectionChanged}
   25.18 -
   25.19 -import java.awt.BorderLayout
   25.20 -import javax.swing.border.{BevelBorder, SoftBevelBorder}
   25.21 -
   25.22 -import org.gjt.sp.jedit.View
   25.23 -
   25.24 -
   25.25 -class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
   25.26 -{
   25.27 -  /* main tabs */
   25.28 -
   25.29 -  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
   25.30 -  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
   25.31 -
   25.32 -  private val syslog = new TextArea(Isabelle.session.syslog())
   25.33 -  syslog.editable = false
   25.34 -
   25.35 -  private val tabs = new TabbedPane {
   25.36 -    pages += new TabbedPane.Page("README", Component.wrap(readme))
   25.37 -    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
   25.38 -
   25.39 -    selection.index =
   25.40 -    {
   25.41 -      val index = Isabelle.Int_Property("session-panel.selection", 0)
   25.42 -      if (index >= pages.length) 0 else index
   25.43 -    }
   25.44 -    listenTo(selection)
   25.45 -    reactions += {
   25.46 -      case SelectionChanged(_) =>
   25.47 -        Isabelle.Int_Property("session-panel.selection") = selection.index
   25.48 -    }
   25.49 -  }
   25.50 -
   25.51 -  set_content(tabs)
   25.52 -
   25.53 -
   25.54 -  /* controls */
   25.55 -
   25.56 -  val session_phase = new Label(Isabelle.session.phase.toString)
   25.57 -  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   25.58 -  session_phase.tooltip = "Prover status"
   25.59 -
   25.60 -  private val interrupt = new Button("Interrupt") {
   25.61 -    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
   25.62 -  }
   25.63 -  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
   25.64 -
   25.65 -  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   25.66 -  logic.listenTo(logic.selection)
   25.67 -  logic.reactions += {
   25.68 -    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
   25.69 -  }
   25.70 -
   25.71 -  private val controls =
   25.72 -    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
   25.73 -  add(controls.peer, BorderLayout.NORTH)
   25.74 -
   25.75 -
   25.76 -  /* main actor */
   25.77 -
   25.78 -  private val main_actor = actor {
   25.79 -    loop {
   25.80 -      react {
   25.81 -        case result: Isabelle_Process.Result =>
   25.82 -          if (result.is_syslog)
   25.83 -            Swing_Thread.now {
   25.84 -              val text = Isabelle.session.syslog()
   25.85 -              if (text != syslog.text) {
   25.86 -                syslog.text = text
   25.87 -              }
   25.88 -            }
   25.89 -
   25.90 -        case phase: Session.Phase =>
   25.91 -          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
   25.92 -
   25.93 -        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
   25.94 -      }
   25.95 -    }
   25.96 -  }
   25.97 -
   25.98 -  override def init() {
   25.99 -    Isabelle.session.raw_messages += main_actor
  25.100 -    Isabelle.session.phase_changed += main_actor
  25.101 -  }
  25.102 -
  25.103 -  override def exit() {
  25.104 -    Isabelle.session.raw_messages -= main_actor
  25.105 -    Isabelle.session.phase_changed -= main_actor
  25.106 -  }
  25.107 -}
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
    26.3 @@ -0,0 +1,163 @@
    26.4 +/*  Title:      Tools/jEdit/src/output_dockable.scala
    26.5 +    Author:     Makarius
    26.6 +
    26.7 +Dockable window with result message output.
    26.8 +*/
    26.9 +
   26.10 +package isabelle.jedit
   26.11 +
   26.12 +
   26.13 +import isabelle._
   26.14 +
   26.15 +import scala.actors.Actor._
   26.16 +
   26.17 +import scala.swing.{FlowPanel, Button, CheckBox}
   26.18 +import scala.swing.event.ButtonClicked
   26.19 +
   26.20 +import java.awt.BorderLayout
   26.21 +import java.awt.event.{ComponentEvent, ComponentAdapter}
   26.22 +
   26.23 +import org.gjt.sp.jedit.View
   26.24 +
   26.25 +
   26.26 +class Output_Dockable(view: View, position: String) extends Dockable(view, position)
   26.27 +{
   26.28 +  Swing_Thread.require()
   26.29 +
   26.30 +  private val html_panel =
   26.31 +    new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
   26.32 +  {
   26.33 +    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
   26.34 +      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
   26.35 +        val text = elem.getFirstChild().getNodeValue()
   26.36 +
   26.37 +        Document_View(view.getTextArea) match {
   26.38 +          case Some(doc_view) =>
   26.39 +            val cmd = current_command.get
   26.40 +            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
   26.41 +            val buffer = view.getBuffer
   26.42 +            buffer.beginCompoundEdit()
   26.43 +            buffer.remove(start_ofs, cmd.length)
   26.44 +            buffer.insert(start_ofs, text)
   26.45 +            buffer.endCompoundEdit()
   26.46 +          case None =>
   26.47 +        }
   26.48 +    }       
   26.49 +  }
   26.50 +
   26.51 +  set_content(html_panel)
   26.52 +
   26.53 +
   26.54 +  /* component state -- owned by Swing thread */
   26.55 +
   26.56 +  private var zoom_factor = 100
   26.57 +  private var show_tracing = false
   26.58 +  private var follow_caret = true
   26.59 +  private var current_command: Option[Command] = None
   26.60 +
   26.61 +
   26.62 +  private def handle_resize()
   26.63 +  {
   26.64 +    Swing_Thread.now {
   26.65 +      html_panel.resize(Isabelle.font_family(),
   26.66 +        scala.math.round(Isabelle.font_size() * zoom_factor / 100))
   26.67 +    }
   26.68 +  }
   26.69 +
   26.70 +  private def handle_perspective(): Boolean =
   26.71 +    Swing_Thread.now {
   26.72 +      Document_View(view.getTextArea) match {
   26.73 +        case Some(doc_view) =>
   26.74 +          val cmd = doc_view.selected_command()
   26.75 +          if (current_command == cmd) false
   26.76 +          else { current_command = cmd; true }
   26.77 +        case None => false
   26.78 +      }
   26.79 +    }
   26.80 +
   26.81 +  private def handle_update(restriction: Option[Set[Command]] = None)
   26.82 +  {
   26.83 +    Swing_Thread.now {
   26.84 +      if (follow_caret) handle_perspective()
   26.85 +      Document_View(view.getTextArea) match {
   26.86 +        case Some(doc_view) =>
   26.87 +          current_command match {
   26.88 +            case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) =>
   26.89 +              val snapshot = doc_view.model.snapshot()
   26.90 +              val filtered_results =
   26.91 +                snapshot.state(cmd).results.iterator.map(_._2) filter {
   26.92 +                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing  // FIXME not scalable
   26.93 +                  case _ => true
   26.94 +                }
   26.95 +              html_panel.render(filtered_results.toList)
   26.96 +            case _ =>
   26.97 +          }
   26.98 +        case None =>
   26.99 +      }
  26.100 +    }
  26.101 +  }
  26.102 +
  26.103 +
  26.104 +  /* main actor */
  26.105 +
  26.106 +  private val main_actor = actor {
  26.107 +    loop {
  26.108 +      react {
  26.109 +        case Session.Global_Settings => handle_resize()
  26.110 +        case Session.Commands_Changed(changed) => handle_update(Some(changed))
  26.111 +        case Session.Perspective => if (follow_caret && handle_perspective()) handle_update()
  26.112 +        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
  26.113 +      }
  26.114 +    }
  26.115 +  }
  26.116 +
  26.117 +  override def init()
  26.118 +  {
  26.119 +    Isabelle.session.global_settings += main_actor
  26.120 +    Isabelle.session.commands_changed += main_actor
  26.121 +    Isabelle.session.perspective += main_actor
  26.122 +  }
  26.123 +
  26.124 +  override def exit()
  26.125 +  {
  26.126 +    Isabelle.session.global_settings -= main_actor
  26.127 +    Isabelle.session.commands_changed -= main_actor
  26.128 +    Isabelle.session.perspective -= main_actor
  26.129 +  }
  26.130 +
  26.131 +
  26.132 +  /* resize */
  26.133 +
  26.134 +  addComponentListener(new ComponentAdapter {
  26.135 +    val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() }
  26.136 +    override def componentResized(e: ComponentEvent) { delay() }
  26.137 +  })
  26.138 +
  26.139 +
  26.140 +  /* controls */
  26.141 +
  26.142 +  private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
  26.143 +  zoom.tooltip = "Zoom factor for basic font size"
  26.144 +
  26.145 +  private val tracing = new CheckBox("Tracing") {
  26.146 +    reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() }
  26.147 +  }
  26.148 +  tracing.selected = show_tracing
  26.149 +  tracing.tooltip = "Indicate output of tracing messages"
  26.150 +
  26.151 +  private val auto_update = new CheckBox("Auto update") {
  26.152 +    reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() }
  26.153 +  }
  26.154 +  auto_update.selected = follow_caret
  26.155 +  auto_update.tooltip = "Indicate automatic update following cursor movement"
  26.156 +
  26.157 +  private val update = new Button("Update") {
  26.158 +    reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() }
  26.159 +  }
  26.160 +  update.tooltip = "Update display according to the command at cursor position"
  26.161 +
  26.162 +  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update)
  26.163 +  add(controls.peer, BorderLayout.NORTH)
  26.164 +
  26.165 +  handle_update()
  26.166 +}
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jun 08 17:42:07 2011 +0200
    27.3 @@ -0,0 +1,401 @@
    27.4 +/*  Title:      Tools/jEdit/src/plugin.scala
    27.5 +    Author:     Makarius
    27.6 +
    27.7 +Main Isabelle/jEdit plugin setup.
    27.8 +*/
    27.9 +
   27.10 +package isabelle.jedit
   27.11 +
   27.12 +
   27.13 +import isabelle._
   27.14 +
   27.15 +import java.io.{FileInputStream, IOException}
   27.16 +import java.awt.Font
   27.17 +
   27.18 +import scala.collection.mutable
   27.19 +import scala.swing.ComboBox
   27.20 +
   27.21 +import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
   27.22 +  Buffer, EditPane, ServiceManager, View}
   27.23 +import org.gjt.sp.jedit.buffer.JEditBuffer
   27.24 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
   27.25 +import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
   27.26 +import org.gjt.sp.jedit.gui.DockableWindowManager
   27.27 +
   27.28 +import org.gjt.sp.util.Log
   27.29 +
   27.30 +import scala.actors.Actor
   27.31 +import Actor._
   27.32 +
   27.33 +
   27.34 +object Isabelle
   27.35 +{
   27.36 +  /* plugin instance */
   27.37 +
   27.38 +  var system: Isabelle_System = null
   27.39 +  var session: Session = null
   27.40 +
   27.41 +
   27.42 +  /* properties */
   27.43 +
   27.44 +  val OPTION_PREFIX = "options.isabelle."
   27.45 +
   27.46 +  object Property
   27.47 +  {
   27.48 +    def apply(name: String): String =
   27.49 +      jEdit.getProperty(OPTION_PREFIX + name)
   27.50 +    def apply(name: String, default: String): String =
   27.51 +      jEdit.getProperty(OPTION_PREFIX + name, default)
   27.52 +    def update(name: String, value: String) =
   27.53 +      jEdit.setProperty(OPTION_PREFIX + name, value)
   27.54 +  }
   27.55 +
   27.56 +  object Boolean_Property
   27.57 +  {
   27.58 +    def apply(name: String): Boolean =
   27.59 +      jEdit.getBooleanProperty(OPTION_PREFIX + name)
   27.60 +    def apply(name: String, default: Boolean): Boolean =
   27.61 +      jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
   27.62 +    def update(name: String, value: Boolean) =
   27.63 +      jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
   27.64 +  }
   27.65 +
   27.66 +  object Int_Property
   27.67 +  {
   27.68 +    def apply(name: String): Int =
   27.69 +      jEdit.getIntegerProperty(OPTION_PREFIX + name)
   27.70 +    def apply(name: String, default: Int): Int =
   27.71 +      jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
   27.72 +    def update(name: String, value: Int) =
   27.73 +      jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
   27.74 +  }
   27.75 +
   27.76 +  object Double_Property
   27.77 +  {
   27.78 +    def apply(name: String): Double =
   27.79 +      jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
   27.80 +    def apply(name: String, default: Double): Double =
   27.81 +      jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
   27.82 +    def update(name: String, value: Double) =
   27.83 +      jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
   27.84 +  }
   27.85 +
   27.86 +  object Time_Property
   27.87 +  {
   27.88 +    def apply(name: String): Time =
   27.89 +      Time.seconds(Double_Property(name))
   27.90 +    def apply(name: String, default: Time): Time =
   27.91 +      Time.seconds(Double_Property(name, default.seconds))
   27.92 +    def update(name: String, value: Time) =
   27.93 +      Double_Property.update(name, value.seconds)
   27.94 +  }
   27.95 +
   27.96 +
   27.97 +  /* font */
   27.98 +
   27.99 +  def font_family(): String = jEdit.getProperty("view.font")
  27.100 +
  27.101 +  def font_size(): Float =
  27.102 +    (jEdit.getIntegerProperty("view.fontsize", 16) *
  27.103 +      Int_Property("relative-font-size", 100)).toFloat / 100
  27.104 +
  27.105 +
  27.106 +  /* text area ranges */
  27.107 +
  27.108 +  case class Gfx_Range(val x: Int, val y: Int, val length: Int)
  27.109 +
  27.110 +  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
  27.111 +  {
  27.112 +    val p = text_area.offsetToXY(range.start)
  27.113 +    val q = text_area.offsetToXY(range.stop)
  27.114 +    if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
  27.115 +    else None
  27.116 +  }
  27.117 +
  27.118 +
  27.119 +  /* tooltip markup */
  27.120 +
  27.121 +  def tooltip(text: String): String =
  27.122 +    "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
  27.123 +        Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
  27.124 +      HTML.encode(text) + "</pre></html>"
  27.125 +
  27.126 +  def tooltip_dismiss_delay(): Time =
  27.127 +    Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
  27.128 +
  27.129 +  def setup_tooltips()
  27.130 +  {
  27.131 +    Swing_Thread.now {
  27.132 +      val manager = javax.swing.ToolTipManager.sharedInstance
  27.133 +      manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
  27.134 +    }
  27.135 +  }
  27.136 +
  27.137 +
  27.138 +  /* icons */
  27.139 +
  27.140 +  def load_icon(name: String): javax.swing.Icon =
  27.141 +  {
  27.142 +    val icon = GUIUtilities.loadIcon(name)
  27.143 +    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
  27.144 +      Log.log(Log.ERROR, icon, "Bad icon: " + name)
  27.145 +    icon
  27.146 +  }
  27.147 +
  27.148 +
  27.149 +  /* check JVM */
  27.150 +
  27.151 +  def check_jvm()
  27.152 +  {
  27.153 +    if (!Platform.is_hotspot) {
  27.154 +      Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
  27.155 +        "This is " + Platform.jvm_name,
  27.156 +        "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
  27.157 +    }
  27.158 +  }
  27.159 +
  27.160 +
  27.161 +  /* main jEdit components */
  27.162 +
  27.163 +  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
  27.164 +
  27.165 +  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
  27.166 +
  27.167 +  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
  27.168 +    view.getEditPanes().iterator.map(_.getTextArea)
  27.169 +
  27.170 +  def jedit_text_areas(): Iterator[JEditTextArea] =
  27.171 +    jedit_views().flatMap(jedit_text_areas(_))
  27.172 +
  27.173 +  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
  27.174 +    jedit_text_areas().filter(_.getBuffer == buffer)
  27.175 +
  27.176 +  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
  27.177 +  {
  27.178 +    try { buffer.readLock(); body }
  27.179 +    finally { buffer.readUnlock() }
  27.180 +  }
  27.181 +
  27.182 +  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
  27.183 +    Swing_Thread.now { buffer_lock(buffer) { body } }
  27.184 +
  27.185 +  def buffer_text(buffer: JEditBuffer): String =
  27.186 +    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
  27.187 +
  27.188 +
  27.189 +  /* dockable windows */
  27.190 +
  27.191 +  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
  27.192 +
  27.193 +  def docked_session(view: View): Option[Session_Dockable] =
  27.194 +    wm(view).getDockableWindow("isabelle-session") match {
  27.195 +      case dockable: Session_Dockable => Some(dockable)
  27.196 +      case _ => None
  27.197 +    }
  27.198 +
  27.199 +  def docked_output(view: View): Option[Output_Dockable] =
  27.200 +    wm(view).getDockableWindow("isabelle-output") match {
  27.201 +      case dockable: Output_Dockable => Some(dockable)
  27.202 +      case _ => None
  27.203 +    }
  27.204 +
  27.205 +  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
  27.206 +    wm(view).getDockableWindow("isabelle-raw-output") match {
  27.207 +      case dockable: Raw_Output_Dockable => Some(dockable)
  27.208 +      case _ => None
  27.209 +    }
  27.210 +
  27.211 +  def docked_protocol(view: View): Option[Protocol_Dockable] =
  27.212 +    wm(view).getDockableWindow("isabelle-protocol") match {
  27.213 +      case dockable: Protocol_Dockable => Some(dockable)
  27.214 +      case _ => None
  27.215 +    }
  27.216 +
  27.217 +
  27.218 +  /* logic image */
  27.219 +
  27.220 +  def default_logic(): String =
  27.221 +  {
  27.222 +    val logic = system.getenv("JEDIT_LOGIC")
  27.223 +    if (logic != "") logic
  27.224 +    else system.getenv_strict("ISABELLE_LOGIC")
  27.225 +  }
  27.226 +
  27.227 +  class Logic_Entry(val name: String, val description: String)
  27.228 +  {
  27.229 +    override def toString = description
  27.230 +  }
  27.231 +
  27.232 +  def logic_selector(logic: String): ComboBox[Logic_Entry] =
  27.233 +  {
  27.234 +    val entries =
  27.235 +      new Logic_Entry("", "default (" + default_logic() + ")") ::
  27.236 +        system.find_logics().map(name => new Logic_Entry(name, name))
  27.237 +    val component = new ComboBox(entries)
  27.238 +    entries.find(_.name == logic) match {
  27.239 +      case None =>
  27.240 +      case Some(entry) => component.selection.item = entry
  27.241 +    }
  27.242 +    component.tooltip = "Isabelle logic image"
  27.243 +    component
  27.244 +  }
  27.245 +
  27.246 +  def start_session()
  27.247 +  {
  27.248 +    val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
  27.249 +    val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
  27.250 +    val logic = {
  27.251 +      val logic = Property("logic")
  27.252 +      if (logic != null && logic != "") logic
  27.253 +      else Isabelle.default_logic()
  27.254 +    }
  27.255 +    session.start(timeout, modes ::: List(logic))
  27.256 +  }
  27.257 +}
  27.258 +
  27.259 +
  27.260 +class Plugin extends EBPlugin
  27.261 +{
  27.262 +  /* session management */
  27.263 +
  27.264 +  private def init_model(buffer: Buffer)
  27.265 +  {
  27.266 +    Isabelle.swing_buffer_lock(buffer) {
  27.267 +      val opt_model =
  27.268 +        Document_Model(buffer) match {
  27.269 +          case Some(model) => model.refresh; Some(model)
  27.270 +          case None =>
  27.271 +            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
  27.272 +              case Some((dir, thy_name)) =>
  27.273 +                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
  27.274 +              case None => None
  27.275 +            }
  27.276 +        }
  27.277 +      if (opt_model.isDefined) {
  27.278 +        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
  27.279 +          if (Document_View(text_area).map(_.model) != opt_model)
  27.280 +            Document_View.init(opt_model.get, text_area)
  27.281 +        }
  27.282 +      }
  27.283 +    }
  27.284 +  }
  27.285 +
  27.286 +  private def exit_model(buffer: Buffer)
  27.287 +  {
  27.288 +    Isabelle.swing_buffer_lock(buffer) {
  27.289 +      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
  27.290 +      Document_Model.exit(buffer)
  27.291 +    }
  27.292 +  }
  27.293 +
  27.294 +  private case class Init_Model(buffer: Buffer)
  27.295 +  private case class Exit_Model(buffer: Buffer)
  27.296 +  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
  27.297 +  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
  27.298 +
  27.299 +  private val session_manager = actor {
  27.300 +    var ready = false
  27.301 +    loop {
  27.302 +      react {
  27.303 +        case phase: Session.Phase =>
  27.304 +          ready = phase == Session.Ready
  27.305 +          phase match {
  27.306 +            case Session.Failed =>
  27.307 +              Swing_Thread.now {
  27.308 +                val text = new scala.swing.TextArea(Isabelle.session.syslog())
  27.309 +                text.editable = false
  27.310 +                Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
  27.311 +              }
  27.312 +
  27.313 +            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
  27.314 +            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
  27.315 +            case _ =>
  27.316 +          }
  27.317 +
  27.318 +        case Init_Model(buffer) =>
  27.319 +          if (ready) init_model(buffer)
  27.320 +
  27.321 +        case Exit_Model(buffer) =>
  27.322 +          exit_model(buffer)
  27.323 +
  27.324 +        case Init_View(buffer, text_area) =>
  27.325 +          if (ready) {
  27.326 +            Isabelle.swing_buffer_lock(buffer) {
  27.327 +              Document_Model(buffer) match {
  27.328 +                case Some(model) => Document_View.init(model, text_area)
  27.329 +                case None =>
  27.330 +              }
  27.331 +            }
  27.332 +          }
  27.333 +
  27.334 +        case Exit_View(buffer, text_area) =>
  27.335 +          Isabelle.swing_buffer_lock(buffer) {
  27.336 +            Document_View.exit(text_area)
  27.337 +          }
  27.338 +
  27.339 +        case bad => System.err.println("session_manager: ignoring bad message " + bad)
  27.340 +      }
  27.341 +    }
  27.342 +  }
  27.343 +
  27.344 +
  27.345 +  /* main plugin plumbing */
  27.346 +
  27.347 +  override def handleMessage(message: EBMessage)
  27.348 +  {
  27.349 +    message match {
  27.350 +      case msg: EditorStarted =>
  27.351 +      Isabelle.check_jvm()
  27.352 +      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
  27.353 +
  27.354 +      case msg: BufferUpdate
  27.355 +      if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
  27.356 +
  27.357 +        val buffer = msg.getBuffer
  27.358 +        if (buffer != null) session_manager ! Init_Model(buffer)
  27.359 +
  27.360 +      case msg: EditPaneUpdate
  27.361 +      if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
  27.362 +          msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
  27.363 +          msg.getWhat == EditPaneUpdate.CREATED ||
  27.364 +          msg.getWhat == EditPaneUpdate.DESTROYED) =>
  27.365 +
  27.366 +        val edit_pane = msg.getEditPane
  27.367 +        val buffer = edit_pane.getBuffer
  27.368 +        val text_area = edit_pane.getTextArea
  27.369 +
  27.370 +        if (buffer != null && text_area != null) {
  27.371 +          if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
  27.372 +              msg.getWhat == EditPaneUpdate.CREATED)
  27.373 +            session_manager ! Init_View(buffer, text_area)
  27.374 +          else
  27.375 +            session_manager ! Exit_View(buffer, text_area)
  27.376 +        }
  27.377 +
  27.378 +      case msg: PropertiesChanged =>
  27.379 +        Swing_Thread.now {
  27.380 +          Isabelle.setup_tooltips()
  27.381 +          for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
  27.382 +            Document_View(text_area).get.extend_styles()
  27.383 +        }
  27.384 +        Isabelle.session.global_settings.event(Session.Global_Settings)
  27.385 +
  27.386 +      case _ =>
  27.387 +    }
  27.388 +  }
  27.389 +
  27.390 +  override def start()
  27.391 +  {
  27.392 +    Isabelle.setup_tooltips()
  27.393 +    Isabelle.system = new Isabelle_System
  27.394 +    Isabelle.system.install_fonts()
  27.395 +    Isabelle.session = new Session(Isabelle.system)
  27.396 +    Isabelle.session.phase_changed += session_manager
  27.397 +  }
  27.398 +
  27.399 +  override def stop()
  27.400 +  {
  27.401 +    Isabelle.session.stop()
  27.402 +    Isabelle.session.phase_changed -= session_manager
  27.403 +  }
  27.404 +}
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
    28.3 @@ -0,0 +1,39 @@
    28.4 +/*  Title:      Tools/jEdit/src/protocol_dockable.scala
    28.5 +    Author:     Makarius
    28.6 +
    28.7 +Dockable window for protocol messages.
    28.8 +*/
    28.9 +
   28.10 +package isabelle.jedit
   28.11 +
   28.12 +
   28.13 +import isabelle._
   28.14 +
   28.15 +import scala.actors.Actor._
   28.16 +import scala.swing.{TextArea, ScrollPane}
   28.17 +
   28.18 +import org.gjt.sp.jedit.View
   28.19 +
   28.20 +
   28.21 +class Protocol_Dockable(view: View, position: String) extends Dockable(view, position)
   28.22 +{
   28.23 +  private val text_area = new TextArea
   28.24 +  set_content(new ScrollPane(text_area))
   28.25 +
   28.26 +
   28.27 +  /* main actor */
   28.28 +
   28.29 +  private val main_actor = actor {
   28.30 +    loop {
   28.31 +      react {
   28.32 +        case result: Isabelle_Process.Result =>
   28.33 +          Swing_Thread.now { text_area.append(result.message.toString + "\n") }
   28.34 +
   28.35 +        case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad)
   28.36 +      }
   28.37 +    }
   28.38 +  }
   28.39 +
   28.40 +  override def init() { Isabelle.session.raw_messages += main_actor }
   28.41 +  override def exit() { Isabelle.session.raw_messages -= main_actor }
   28.42 +}
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
    29.3 @@ -0,0 +1,42 @@
    29.4 +/*  Title:      Tools/jEdit/src/raw_output_dockable.scala
    29.5 +    Author:     Makarius
    29.6 +
    29.7 +Dockable window for raw process output (stdout).
    29.8 +*/
    29.9 +
   29.10 +package isabelle.jedit
   29.11 +
   29.12 +
   29.13 +import isabelle._
   29.14 +
   29.15 +import scala.actors.Actor._
   29.16 +import scala.swing.{TextArea, ScrollPane}
   29.17 +
   29.18 +import org.gjt.sp.jedit.View
   29.19 +
   29.20 +
   29.21 +class Raw_Output_Dockable(view: View, position: String)
   29.22 +  extends Dockable(view: View, position: String)
   29.23 +{
   29.24 +  private val text_area = new TextArea
   29.25 +  text_area.editable = false
   29.26 +  set_content(new ScrollPane(text_area))
   29.27 +
   29.28 +
   29.29 +  /* main actor */
   29.30 +
   29.31 +  private val main_actor = actor {
   29.32 +    loop {
   29.33 +      react {
   29.34 +        case result: Isabelle_Process.Result =>
   29.35 +          if (result.is_stdout)
   29.36 +            Swing_Thread.now { text_area.append(XML.content(result.message).mkString) }
   29.37 +
   29.38 +        case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
   29.39 +      }
   29.40 +    }
   29.41 +  }
   29.42 +
   29.43 +  override def init() { Isabelle.session.raw_messages += main_actor }
   29.44 +  override def exit() { Isabelle.session.raw_messages -= main_actor }
   29.45 +}
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Wed Jun 08 17:42:07 2011 +0200
    30.3 @@ -0,0 +1,155 @@
    30.4 +/*  Title:      Tools/jEdit/src/scala_console.scala
    30.5 +    Author:     Makarius
    30.6 +
    30.7 +Scala instance of Console plugin.
    30.8 +*/
    30.9 +
   30.10 +package isabelle.jedit
   30.11 +
   30.12 +
   30.13 +import isabelle._
   30.14 +
   30.15 +import console.{Console, ConsolePane, Shell, Output}
   30.16 +
   30.17 +import org.gjt.sp.jedit.{jEdit, JARClassLoader}
   30.18 +import org.gjt.sp.jedit.MiscUtilities
   30.19 +
   30.20 +import java.io.{File, OutputStream, Writer, PrintWriter}
   30.21 +
   30.22 +import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
   30.23 +import scala.collection.mutable
   30.24 +
   30.25 +
   30.26 +class Scala_Console extends Shell("Scala")
   30.27 +{
   30.28 +  /* reconstructed jEdit/plugin classpath */
   30.29 +
   30.30 +  private def reconstruct_classpath(): String =
   30.31 +  {
   30.32 +    def find_jars(start: String): List[String] =
   30.33 +      if (start != null)
   30.34 +        Standard_System.find_files(new File(start),
   30.35 +          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
   30.36 +      else Nil
   30.37 +    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
   30.38 +    path.mkString(File.pathSeparator)
   30.39 +  }
   30.40 +
   30.41 +
   30.42 +  /* global state -- owned by Swing thread */
   30.43 +
   30.44 +  private var interpreters = Map[Console, Interpreter]()
   30.45 +
   30.46 +  private var global_console: Console = null
   30.47 +  private var global_out: Output = null
   30.48 +  private var global_err: Output = null
   30.49 +
   30.50 +  private val console_stream = new OutputStream
   30.51 +  {
   30.52 +    val buf = new StringBuilder
   30.53 +    override def flush()
   30.54 +    {
   30.55 +      val str = Standard_System.decode_permissive_utf8(buf.toString)
   30.56 +      buf.clear
   30.57 +      if (global_out == null) System.out.print(str)
   30.58 +      else Swing_Thread.now { global_out.writeAttrs(null, str) }
   30.59 +    }
   30.60 +    override def close() { flush () }
   30.61 +    def write(byte: Int) { buf.append(byte.toChar) }
   30.62 +  }
   30.63 +
   30.64 +  private val console_writer = new Writer
   30.65 +  {
   30.66 +    def flush() {}
   30.67 +    def close() {}
   30.68 +
   30.69 +    def write(cbuf: Array[Char], off: Int, len: Int)
   30.70 +    {
   30.71 +      if (len > 0) write(new String(cbuf.slice(off, off + len)))
   30.72 +    }
   30.73 +
   30.74 +    override def write(str: String)
   30.75 +    {
   30.76 +      if (global_out == null) System.out.println(str)
   30.77 +      else global_out.print(null, str)
   30.78 +    }
   30.79 +  }
   30.80 +
   30.81 +  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
   30.82 +  {
   30.83 +    global_console = console
   30.84 +    global_out = out
   30.85 +    global_err = if (err == null) out else err
   30.86 +    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
   30.87 +    console_stream.flush
   30.88 +    global_console = null
   30.89 +    global_out = null
   30.90 +    global_err = null
   30.91 +    Exn.release(res)
   30.92 +  }
   30.93 +
   30.94 +  private def report_error(str: String)
   30.95 +  {
   30.96 +    if (global_console == null || global_err == null) System.err.println(str)
   30.97 +    else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
   30.98 +  }
   30.99 +
  30.100 +
  30.101 +  /* jEdit console methods */
  30.102 +
  30.103 +  override def openConsole(console: Console)
  30.104 +  {
  30.105 +    val settings = new GenericRunnerSettings(report_error)
  30.106 +    settings.classpath.value = reconstruct_classpath()
  30.107 +
  30.108 +    val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
  30.109 +    {
  30.110 +      override def parentClassLoader = new JARClassLoader
  30.111 +    }
  30.112 +    interp.setContextClassLoader
  30.113 +    interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
  30.114 +    interp.bind("console", "console.Console", console)
  30.115 +    interp.interpret("import isabelle.jedit.Isabelle")
  30.116 +
  30.117 +    interpreters += (console -> interp)
  30.118 +  }
  30.119 +
  30.120 +  override def closeConsole(console: Console)
  30.121 +  {
  30.122 +    interpreters -= console
  30.123 +  }
  30.124 +
  30.125 +  override def printInfoMessage(out: Output)
  30.126 +  {
  30.127 +    out.print(null,
  30.128 +     "This shell evaluates Isabelle/Scala expressions.\n\n" +
  30.129 +     "The following special toplevel bindings are provided:\n" +
  30.130 +     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
  30.131 +     "  console   -- jEdit Console plugin instance\n" +
  30.132 +     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
  30.133 +  }
  30.134 +
  30.135 +  override def printPrompt(console: Console, out: Output)
  30.136 +  {
  30.137 +    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
  30.138 +    out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
  30.139 +  }
  30.140 +
  30.141 +  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
  30.142 +  {
  30.143 +    val interp = interpreters(console)
  30.144 +    with_console(console, out, err) { interp.interpret(command) }
  30.145 +    if (err != null) err.commandDone()
  30.146 +    out.commandDone()
  30.147 +  }
  30.148 +
  30.149 +  override def stop(console: Console)
  30.150 +  {
  30.151 +    closeConsole(console)
  30.152 +    console.clear
  30.153 +    openConsole(console)
  30.154 +    val out = console.getOutput
  30.155 +    out.commandDone
  30.156 +    printPrompt(console, out)
  30.157 +  }
  30.158 +}
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Wed Jun 08 17:42:07 2011 +0200
    31.3 @@ -0,0 +1,104 @@
    31.4 +/*  Title:      Tools/jEdit/src/session_dockable.scala
    31.5 +    Author:     Makarius
    31.6 +
    31.7 +Dockable window for prover session management.
    31.8 +*/
    31.9 +
   31.10 +package isabelle.jedit
   31.11 +
   31.12 +
   31.13 +import isabelle._
   31.14 +
   31.15 +import scala.actors.Actor._
   31.16 +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing}
   31.17 +import scala.swing.event.{ButtonClicked, SelectionChanged}
   31.18 +
   31.19 +import java.awt.BorderLayout
   31.20 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
   31.21 +
   31.22 +import org.gjt.sp.jedit.View
   31.23 +
   31.24 +
   31.25 +class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
   31.26 +{
   31.27 +  /* main tabs */
   31.28 +
   31.29 +  private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14)
   31.30 +  readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html")))
   31.31 +
   31.32 +  private val syslog = new TextArea(Isabelle.session.syslog())
   31.33 +  syslog.editable = false
   31.34 +
   31.35 +  private val tabs = new TabbedPane {
   31.36 +    pages += new TabbedPane.Page("README", Component.wrap(readme))
   31.37 +    pages += new TabbedPane.Page("System log", new ScrollPane(syslog))
   31.38 +
   31.39 +    selection.index =
   31.40 +    {
   31.41 +      val index = Isabelle.Int_Property("session-panel.selection", 0)
   31.42 +      if (index >= pages.length) 0 else index
   31.43 +    }
   31.44 +    listenTo(selection)
   31.45 +    reactions += {
   31.46 +      case SelectionChanged(_) =>
   31.47 +        Isabelle.Int_Property("session-panel.selection") = selection.index
   31.48 +    }
   31.49 +  }
   31.50 +
   31.51 +  set_content(tabs)
   31.52 +
   31.53 +
   31.54 +  /* controls */
   31.55 +
   31.56 +  val session_phase = new Label(Isabelle.session.phase.toString)
   31.57 +  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   31.58 +  session_phase.tooltip = "Prover status"
   31.59 +
   31.60 +  private val interrupt = new Button("Interrupt") {
   31.61 +    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
   31.62 +  }
   31.63 +  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
   31.64 +
   31.65 +  private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   31.66 +  logic.listenTo(logic.selection)
   31.67 +  logic.reactions += {
   31.68 +    case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
   31.69 +  }
   31.70 +
   31.71 +  private val controls =
   31.72 +    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
   31.73 +  add(controls.peer, BorderLayout.NORTH)
   31.74 +
   31.75 +
   31.76 +  /* main actor */
   31.77 +
   31.78 +  private val main_actor = actor {
   31.79 +    loop {
   31.80 +      react {
   31.81 +        case result: Isabelle_Process.Result =>
   31.82 +          if (result.is_syslog)
   31.83 +            Swing_Thread.now {
   31.84 +              val text = Isabelle.session.syslog()
   31.85 +              if (text != syslog.text) {
   31.86 +                syslog.text = text
   31.87 +              }
   31.88 +            }
   31.89 +
   31.90 +        case phase: Session.Phase =>
   31.91 +          Swing_Thread.now { session_phase.text = " " + phase.toString + " " }
   31.92 +
   31.93 +        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
   31.94 +      }
   31.95 +    }
   31.96 +  }
   31.97 +
   31.98 +  override def init() {
   31.99 +    Isabelle.session.raw_messages += main_actor
  31.100 +    Isabelle.session.phase_changed += main_actor
  31.101 +  }
  31.102 +
  31.103 +  override def exit() {
  31.104 +    Isabelle.session.raw_messages -= main_actor
  31.105 +    Isabelle.session.phase_changed -= main_actor
  31.106 +  }
  31.107 +}