# HG changeset patch # User wenzelm # Date 1307547727 -7200 # Node ID 5d294220ca437133f506b8c63518869121f2941a # Parent 8d8b6ed0588cf140794f9eb0818af880f82c886d moved sources -- eliminated Netbeans artifact of jedit package directory; diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/jedit_build/Tools/jedit --- a/src/Tools/jEdit/jedit_build/Tools/jedit Wed Jun 08 17:32:31 2011 +0200 +++ b/src/Tools/jEdit/jedit_build/Tools/jedit Wed Jun 08 17:42:07 2011 +0200 @@ -35,21 +35,21 @@ SRC_DIR="$ISABELLE_HOME/src/Tools/jEdit" declare -a SOURCES=( - "$SRC_DIR/src/jedit/dockable.scala" - "$SRC_DIR/src/jedit/document_model.scala" - "$SRC_DIR/src/jedit/document_view.scala" - "$SRC_DIR/src/jedit/html_panel.scala" - "$SRC_DIR/src/jedit/isabelle_encoding.scala" - "$SRC_DIR/src/jedit/isabelle_hyperlinks.scala" - "$SRC_DIR/src/jedit/isabelle_markup.scala" - "$SRC_DIR/src/jedit/isabelle_options.scala" - "$SRC_DIR/src/jedit/isabelle_sidekick.scala" - "$SRC_DIR/src/jedit/output_dockable.scala" - "$SRC_DIR/src/jedit/plugin.scala" - "$SRC_DIR/src/jedit/protocol_dockable.scala" - "$SRC_DIR/src/jedit/raw_output_dockable.scala" - "$SRC_DIR/src/jedit/scala_console.scala" - "$SRC_DIR/src/jedit/session_dockable.scala" + "$SRC_DIR/src/dockable.scala" + "$SRC_DIR/src/document_model.scala" + "$SRC_DIR/src/document_view.scala" + "$SRC_DIR/src/html_panel.scala" + "$SRC_DIR/src/isabelle_encoding.scala" + "$SRC_DIR/src/isabelle_hyperlinks.scala" + "$SRC_DIR/src/isabelle_markup.scala" + "$SRC_DIR/src/isabelle_options.scala" + "$SRC_DIR/src/isabelle_sidekick.scala" + "$SRC_DIR/src/output_dockable.scala" + "$SRC_DIR/src/plugin.scala" + "$SRC_DIR/src/protocol_dockable.scala" + "$SRC_DIR/src/raw_output_dockable.scala" + "$SRC_DIR/src/scala_console.scala" + "$SRC_DIR/src/session_dockable.scala" ) declare -a PLUGIN_FILES=( diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/dockable.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,41 @@ +/* Title: Tools/jEdit/src/dockable.scala + Author: Makarius + +Generic dockable window. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.{Dimension, Component, BorderLayout} +import javax.swing.JPanel + +import org.gjt.sp.jedit.View +import org.gjt.sp.jedit.gui.DockableWindowManager + + +class Dockable(view: View, position: String) extends JPanel(new BorderLayout) +{ + if (position == DockableWindowManager.FLOATING) + setPreferredSize(new Dimension(500, 250)) + + def set_content(c: Component) { add(c, BorderLayout.CENTER) } + def set_content(c: scala.swing.Component) { add(c.peer, BorderLayout.CENTER) } + + protected def init() { } + protected def exit() { } + + override def addNotify() + { + super.addNotify() + init() + } + + override def removeNotify() + { + exit() + super.removeNotify() + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/document_model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/document_model.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,252 @@ +/* Title: Tools/jEdit/src/document_model.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Document model connected to jEdit buffer -- single node in theory graph. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.collection.mutable + +import org.gjt.sp.jedit.Buffer +import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} +import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet} +import org.gjt.sp.jedit.textarea.TextArea + +import java.awt.font.TextAttribute +import javax.swing.text.Segment; + + +object Document_Model +{ + object Token_Markup + { + /* extended token styles */ + + private val plain_range: Int = Token.ID_COUNT + private val full_range: Int = 3 * plain_range + private def check_range(i: Int) { require(0 <= i && i < plain_range) } + + def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } + def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } + + private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = + { + import scala.collection.JavaConversions._ + val script_font = + style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))) + new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, script_font) + } + + def extend_styles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = + { + val new_styles = new Array[SyntaxStyle](full_range) + for (i <- 0 until plain_range) { + val style = styles(i) + new_styles(i) = style + new_styles(subscript(i.toByte)) = script_style(style, -1) + new_styles(superscript(i.toByte)) = script_style(style, 1) + } + new_styles + } + + + /* line context */ + + private val dummy_rules = new ParserRuleSet("isabelle", "MAIN") + + class Line_Context(val line: Int, prev: Line_Context) + extends TokenMarker.LineContext(dummy_rules, prev) + { + override def hashCode: Int = line + override def equals(that: Any): Boolean = + that match { + case other: Line_Context => line == other.line + case _ => false + } + } + } + + + /* document model of buffer */ + + private val key = "isabelle.document_model" + + def init(session: Session, buffer: Buffer, thy_name: String): Document_Model = + { + Swing_Thread.require() + val model = new Document_Model(session, buffer, thy_name) + buffer.setProperty(key, model) + model.activate() + model + } + + def apply(buffer: Buffer): Option[Document_Model] = + { + Swing_Thread.require() + buffer.getProperty(key) match { + case model: Document_Model => Some(model) + case _ => None + } + } + + def exit(buffer: Buffer) + { + Swing_Thread.require() + apply(buffer) match { + case None => + case Some(model) => + model.deactivate() + buffer.unsetProperty(key) + } + } +} + + +class Document_Model(val session: Session, val buffer: Buffer, val thy_name: String) +{ + /* pending text edits */ + + object pending_edits // owned by Swing thread + { + private val pending = new mutable.ListBuffer[Text.Edit] + def snapshot(): List[Text.Edit] = pending.toList + + def flush(more_edits: Option[List[Text.Edit]]*) + { + Swing_Thread.require() + val edits = snapshot() + pending.clear + + val all_edits = + if (edits.isEmpty) more_edits.toList + else Some(edits) :: more_edits.toList + if (!all_edits.isEmpty) session.edit_version(all_edits.map((thy_name, _))) + } + + def init() + { + Swing_Thread.require() + flush(None, Some(List(Text.Edit.insert(0, Isabelle.buffer_text(buffer))))) + } + + private val delay_flush = + Swing_Thread.delay_last(session.input_delay) { flush() } + + def +=(edit: Text.Edit) + { + Swing_Thread.require() + pending += edit + delay_flush() + } + } + + + /* snapshot */ + + def snapshot(): Document.Snapshot = + { + Swing_Thread.require() + session.snapshot(thy_name, pending_edits.snapshot()) + } + + + /* buffer listener */ + + private val buffer_listener: BufferListener = new BufferAdapter + { + override def bufferLoaded(buffer: JEditBuffer) + { + pending_edits.init() + } + + override def contentInserted(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, length: Int) + { + if (!buffer.isLoading) + pending_edits += Text.Edit.insert(offset, buffer.getText(offset, length)) + } + + override def preContentRemoved(buffer: JEditBuffer, + start_line: Int, offset: Int, num_lines: Int, removed_length: Int) + { + if (!buffer.isLoading) + pending_edits += Text.Edit.remove(offset, buffer.getText(offset, removed_length)) + } + } + + + /* semantic token marker */ + + private val token_marker = new TokenMarker + { + override def markTokens(prev: TokenMarker.LineContext, + handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext = + { + Isabelle.swing_buffer_lock(buffer) { + val snapshot = Document_Model.this.snapshot() + + val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context] + val line = if (prev == null) 0 else previous.line + 1 + val context = new Document_Model.Token_Markup.Line_Context(line, previous) + + val start = buffer.getLineStartOffset(line) + val stop = start + line_segment.count + + /* FIXME + for (text_area <- Isabelle.jedit_text_areas(buffer) + if Document_View(text_area).isDefined) + Document_View(text_area).get.set_styles() + */ + + def handle_token(style: Byte, offset: Text.Offset, length: Int) = + handler.handleToken(line_segment, style, offset, length, context) + + val syntax = session.current_syntax() + val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax)) + + var last = start + for (token <- tokens.iterator) { + val Text.Range(token_start, token_stop) = token.range + if (last < token_start) + handle_token(Token.COMMENT1, last - start, token_start - last) + handle_token(token.info getOrElse Token.NULL, + token_start - start, token_stop - token_start) + last = token_stop + } + if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last) + + handle_token(Token.END, line_segment.count, 0) + handler.setLineContext(context) + context + } + } + } + + + /* activation */ + + def activate() + { + buffer.setTokenMarker(token_marker) + buffer.addBufferListener(buffer_listener) + buffer.propertiesChanged() + pending_edits.init() + } + + def refresh() + { + buffer.setTokenMarker(token_marker) + } + + def deactivate() + { + pending_edits.flush() + buffer.setTokenMarker(buffer.getMode.getTokenMarker) + buffer.removeBufferListener(buffer_listener) + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/document_view.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/document_view.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,587 @@ +/* Title: Tools/jEdit/src/document_view.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +Document view connected to jEdit text area. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ + +import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D, Point} +import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, + FocusAdapter, FocusEvent, WindowEvent, WindowAdapter} +import javax.swing.{JPanel, ToolTipManager, Popup, PopupFactory, SwingUtilities, BorderFactory} +import javax.swing.event.{CaretListener, CaretEvent} +import java.util.ArrayList + +import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug} +import org.gjt.sp.jedit.gui.RolloverButton +import org.gjt.sp.jedit.options.GutterOptionPane +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter} +import org.gjt.sp.jedit.syntax.{SyntaxStyle, DisplayTokenHandler, Chunk, Token} + + +object Document_View +{ + /* document view of text area */ + + private val key = new Object + + def init(model: Document_Model, text_area: JEditTextArea): Document_View = + { + Swing_Thread.require() + val doc_view = new Document_View(model, text_area) + text_area.putClientProperty(key, doc_view) + doc_view.activate() + doc_view + } + + def apply(text_area: JEditTextArea): Option[Document_View] = + { + Swing_Thread.require() + text_area.getClientProperty(key) match { + case doc_view: Document_View => Some(doc_view) + case _ => None + } + } + + def exit(text_area: JEditTextArea) + { + Swing_Thread.require() + apply(text_area) match { + case None => + case Some(doc_view) => + doc_view.deactivate() + text_area.putClientProperty(key, null) + } + } +} + + +class Document_View(val model: Document_Model, text_area: JEditTextArea) +{ + private val session = model.session + + + /** token handling **/ + + /* extended token styles */ + + private var styles: Array[SyntaxStyle] = null // owned by Swing thread + + def extend_styles() + { + Swing_Thread.require() + styles = Document_Model.Token_Markup.extend_styles(text_area.getPainter.getStyles) + } + extend_styles() + + def set_styles() + { + Swing_Thread.require() + text_area.getPainter.setStyles(styles) + } + + + /* wrap_margin -- cf. org.gjt.sp.jedit.textarea.TextArea.propertiesChanged */ + + def wrap_margin(): Int = + { + val buffer = text_area.getBuffer + val painter = text_area.getPainter + val font = painter.getFont + val font_context = painter.getFontRenderContext + + val soft_wrap = buffer.getStringProperty("wrap") == "soft" + val max = buffer.getIntegerProperty("maxLineLen", 0) + + if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt + else if (soft_wrap) + painter.getWidth - (font.getStringBounds(" ", font_context).getWidth.round.toInt) * 3 + else 0 + } + + + /* chunks */ + + def line_chunks(physical_lines: Set[Int]): Map[Text.Offset, Chunk] = + { + import scala.collection.JavaConversions._ + + val buffer = text_area.getBuffer + val painter = text_area.getPainter + val margin = wrap_margin().toFloat + + val out = new ArrayList[Chunk] + val handler = new DisplayTokenHandler + + var result = Map[Text.Offset, Chunk]() + for (line <- physical_lines) { + out.clear + handler.init(painter.getStyles, painter.getFontRenderContext, painter, out, margin) + buffer.markTokens(line, handler) + + val line_start = buffer.getLineStartOffset(line) + for (chunk <- handler.getChunkList.iterator) + result += (line_start + chunk.offset -> chunk) + } + result + } + + + /* visible line ranges */ + + // simplify slightly odd result of TextArea.getScreenLineEndOffset etc. + // NB: jEdit already normalizes \r\n and \r to \n + def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range = + { + val stop = if (start < end) end - 1 else end min model.buffer.getLength + Text.Range(start, stop) + } + + def screen_lines_range(): Text.Range = + { + val start = text_area.getScreenLineStartOffset(0) + val raw_end = text_area.getScreenLineEndOffset(text_area.getVisibleLines - 1 max 0) + proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength) + } + + def invalidate_line_range(range: Text.Range) + { + text_area.invalidateLineRange( + model.buffer.getLineOfOffset(range.start), + model.buffer.getLineOfOffset(range.stop)) + } + + + /* HTML popups */ + + private var html_popup: Option[Popup] = None + + private def exit_popup() { html_popup.map(_.hide) } + + private val html_panel = + new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) + html_panel.setBorder(BorderFactory.createLineBorder(Color.black)) + + private def html_panel_resize() + { + Swing_Thread.now { + html_panel.resize(Isabelle.font_family(), scala.math.round(Isabelle.font_size())) + } + } + + private def init_popup(snapshot: Document.Snapshot, x: Int, y: Int) + { + exit_popup() +/* FIXME broken + val offset = text_area.xyToOffset(x, y) + val p = new Point(x, y); SwingUtilities.convertPointToScreen(p, text_area.getPainter) + + // FIXME snapshot.cumulate + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match { + case Text.Info(_, Some(msg)) #:: _ => + val popup = PopupFactory.getSharedInstance().getPopup(text_area, html_panel, p.x, p.y + 60) + html_panel.render_sync(List(msg)) + Thread.sleep(10) // FIXME !? + popup.show + html_popup = Some(popup) + case _ => + } +*/ + } + + + /* subexpression highlighting */ + + private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int) + : Option[(Text.Range, Color)] = + { + val offset = text_area.xyToOffset(x, y) + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match { + case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color)) + case _ => None + } + } + + private var highlight_range: Option[(Text.Range, Color)] = None + + + /* CONTROL-mouse management */ + + private var control: Boolean = false + + private def exit_control() + { + exit_popup() + highlight_range = None + } + + private val focus_listener = new FocusAdapter { + override def focusLost(e: FocusEvent) { + highlight_range = None // FIXME exit_control !? + } + } + + private val window_listener = new WindowAdapter { + override def windowIconified(e: WindowEvent) { exit_control() } + override def windowDeactivated(e: WindowEvent) { exit_control() } + } + + private val mouse_motion_listener = new MouseMotionAdapter { + override def mouseMoved(e: MouseEvent) { + control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown + val x = e.getX() + val y = e.getY() + + if (!model.buffer.isLoaded) exit_control() + else + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot + + if (control) init_popup(snapshot, x, y) + + highlight_range map { case (range, _) => invalidate_line_range(range) } + highlight_range = if (control) subexp_range(snapshot, x, y) else None + highlight_range map { case (range, _) => invalidate_line_range(range) } + } + } + } + + + /* TextArea painters */ + + private val background_painter = new TextAreaExtension + { + override def paintScreenLineRange(gfx: Graphics2D, + first_line: Int, last_line: Int, physical_lines: Array[Int], + start: Array[Int], end: Array[Int], y: Int, line_height: Int) + { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() + val ascent = text_area.getPainter.getFontMetrics.getAscent + + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_range = proper_line_range(start(i), end(i)) + + // background color: status + val cmds = snapshot.node.command_range(snapshot.revert(line_range)) + for { + (command, command_start) <- cmds if !command.is_ignored + val range = line_range.restrict(snapshot.convert(command.range + command_start)) + r <- Isabelle.gfx_range(text_area, range) + color <- Isabelle_Markup.status_color(snapshot, command) + } { + gfx.setColor(color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + + // background color (1): markup + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.fillRect(r.x, y + i * line_height, r.length, line_height) + } + + // background color (2): markup + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4) + } + + // sub-expression highlighting -- potentially from other snapshot + highlight_range match { + case Some((range, color)) if line_range.overlaps(range) => + Isabelle.gfx_range(text_area, line_range.restrict(range)) match { + case None => + case Some(r) => + gfx.setColor(color) + gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1) + } + case _ => + } + + // squiggly underline + for { + Text.Info(range, Some(color)) <- + snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator + r <- Isabelle.gfx_range(text_area, range) + } { + gfx.setColor(color) + val x0 = (r.x / 2) * 2 + val y0 = r.y + ascent + 1 + for (x1 <- Range(x0, x0 + r.length, 2)) { + val y1 = if (x1 % 4 < 2) y0 else y0 + 1 + gfx.drawLine(x1, y1, x1 + 1, y1) + } + } + } + } + } + } + + override def getToolTipText(x: Int, y: Int): String = + { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() + val offset = text_area.xyToOffset(x, y) + if (control) { + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match + { + case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) + case _ => null + } + } + else { + // FIXME snapshot.cumulate + snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.popup) match + { + case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text) + case _ => null + } + } + } + } + } + + var use_text_painter = false + + private val text_painter = new TextAreaExtension + { + override def paintScreenLineRange(gfx: Graphics2D, + first_line: Int, last_line: Int, physical_lines: Array[Int], + start: Array[Int], end: Array[Int], y: Int, line_height: Int) + { + if (use_text_painter) { + Isabelle.swing_buffer_lock(model.buffer) { + val painter = text_area.getPainter + val fm = painter.getFontMetrics + + val all_chunks = line_chunks(Set[Int]() ++ physical_lines.iterator.filter(i => i != -1)) + + val x0 = text_area.getHorizontalOffset + var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + all_chunks.get(start(i)) match { + case Some(chunk) => + Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR) + case None => + } + } + y0 += line_height + } + } + } + } + } + + private val gutter_painter = new TextAreaExtension + { + override def paintScreenLineRange(gfx: Graphics2D, + first_line: Int, last_line: Int, physical_lines: Array[Int], + start: Array[Int], end: Array[Int], y: Int, line_height: Int) + { + val gutter = text_area.getGutter + val width = GutterOptionPane.getSelectionAreaWidth + val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3) + val FOLD_MARKER_SIZE = 12 + + if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) { + Isabelle.swing_buffer_lock(model.buffer) { + val snapshot = model.snapshot() + for (i <- 0 until physical_lines.length) { + if (physical_lines(i) != -1) { + val line_range = proper_line_range(start(i), end(i)) + + // gutter icons + val icons = + (for (Text.Info(_, Some(icon)) <- // FIXME snapshot.cumulate + snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator) + yield icon).toList.sortWith(_ >= _) + icons match { + case icon :: _ => + val icn = icon.icon + val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10 + val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0) + icn.paintIcon(gutter, gfx, x0, y0) + case Nil => + } + } + } + } + } + } + } + + + /* caret handling */ + + def selected_command(): Option[Command] = + { + Swing_Thread.require() + model.snapshot().node.proper_command_at(text_area.getCaretPosition) + } + + private val caret_listener = new CaretListener { + private val delay = Swing_Thread.delay_last(session.input_delay) { + session.perspective.event(Session.Perspective) + } + override def caretUpdate(e: CaretEvent) { delay() } + } + + + /* overview of command status left of scrollbar */ + + private val overview = new JPanel(new BorderLayout) + { + private val WIDTH = 10 + private val HEIGHT = 2 + + setPreferredSize(new Dimension(WIDTH, 0)) + + setRequestFocusEnabled(false) + + addMouseListener(new MouseAdapter { + override def mousePressed(event: MouseEvent) { + val line = y_to_line(event.getY) + if (line >= 0 && line < text_area.getLineCount) + text_area.setCaretPosition(text_area.getLineStartOffset(line)) + } + }) + + override def addNotify() { + super.addNotify() + ToolTipManager.sharedInstance.registerComponent(this) + } + + override def removeNotify() { + ToolTipManager.sharedInstance.unregisterComponent(this) + super.removeNotify + } + + override def paintComponent(gfx: Graphics) + { + super.paintComponent(gfx) + Swing_Thread.assert() + + val buffer = model.buffer + Isabelle.buffer_lock(buffer) { + val snapshot = model.snapshot() + + def line_range(command: Command, start: Text.Offset): Option[(Int, Int)] = + { + try { + val line1 = buffer.getLineOfOffset(snapshot.convert(start)) + val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1 + Some((line1, line2)) + } + catch { case e: ArrayIndexOutOfBoundsException => None } + } + for { + (command, start) <- snapshot.node.command_starts + if !command.is_ignored + (line1, line2) <- line_range(command, start) + val y = line_to_y(line1) + val height = HEIGHT * (line2 - line1) + color <- Isabelle_Markup.overview_color(snapshot, command) + } { + gfx.setColor(color) + gfx.fillRect(0, y, getWidth - 1, height) + } + } + } + + private def line_to_y(line: Int): Int = + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) + + private def y_to_line(y: Int): Int = + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case Session.Commands_Changed(changed) => + val buffer = model.buffer + Isabelle.swing_buffer_lock(buffer) { + val snapshot = model.snapshot() + + if (changed.exists(snapshot.node.commands.contains)) + overview.repaint() + + val visible_range = screen_lines_range() + val visible_cmds = snapshot.node.command_range(snapshot.revert(visible_range)).map(_._1) + if (visible_cmds.exists(changed)) { + for { + line <- 0 until text_area.getVisibleLines + val start = text_area.getScreenLineStartOffset(line) if start >= 0 + val end = text_area.getScreenLineEndOffset(line) if end >= 0 + val range = proper_line_range(start, end) + val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1) + if line_cmds.exists(changed) + } text_area.invalidateScreenLineRange(line, line) + + // FIXME danger of deadlock!? + // FIXME potentially slow!? + model.buffer.propertiesChanged() + } + } + + case Session.Global_Settings => html_panel_resize() + + case bad => System.err.println("command_change_actor: ignoring bad message " + bad) + } + } + } + + + /* activation */ + + private def activate() + { + val painter = text_area.getPainter + painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter) + painter.addExtension(TextAreaPainter.TEXT_LAYER + 1, text_painter) + text_area.getGutter.addExtension(gutter_painter) + text_area.addFocusListener(focus_listener) + text_area.getView.addWindowListener(window_listener) + painter.addMouseMotionListener(mouse_motion_listener) + text_area.addCaretListener(caret_listener) + text_area.addLeftOfScrollBar(overview) + session.commands_changed += main_actor + session.global_settings += main_actor + } + + private def deactivate() + { + val painter = text_area.getPainter + session.commands_changed -= main_actor + session.global_settings -= main_actor + text_area.removeFocusListener(focus_listener) + text_area.getView.removeWindowListener(window_listener) + painter.removeMouseMotionListener(mouse_motion_listener) + text_area.removeCaretListener(caret_listener) + text_area.removeLeftOfScrollBar(overview) + text_area.getGutter.removeExtension(gutter_painter) + painter.removeExtension(text_painter) + painter.removeExtension(background_painter) + exit_popup() + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/html_panel.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/html_panel.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,206 @@ +/* Title: Tools/jEdit/src/html_panel.scala + Author: Makarius + +HTML panel based on Lobo/Cobra. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.io.StringReader +import java.awt.{Font, BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics} +import java.awt.event.MouseEvent + +import java.util.logging.{Logger, Level} + +import org.w3c.dom.html2.HTMLElement + +import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl} +import org.lobobrowser.html.gui.HtmlPanel +import org.lobobrowser.html.domimpl.{HTMLDocumentImpl, HTMLStyleElementImpl, NodeImpl} +import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext} + +import scala.actors.Actor._ + + +object HTML_Panel +{ + sealed abstract class Event { val element: HTMLElement; val mouse: MouseEvent } + case class Context_Menu(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Click(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Double_Click(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Over(val element: HTMLElement, mouse: MouseEvent) extends Event + case class Mouse_Out(val element: HTMLElement, mouse: MouseEvent) extends Event +} + + +class HTML_Panel( + system: Isabelle_System, + initial_font_family: String, + initial_font_size: Int) + extends HtmlPanel +{ + /** Lobo setup **/ + + /* global logging */ + + Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING) + + + /* pixel size -- cf. org.lobobrowser.html.style.HtmlValues.getFontSize */ + + val screen_resolution = + if (GraphicsEnvironment.isHeadless()) 72 + else Toolkit.getDefaultToolkit().getScreenResolution() + + def lobo_px(raw_px: Int): Int = raw_px * 96 / screen_resolution + def raw_px(lobo_px: Int): Int = (lobo_px * screen_resolution + 95) / 96 + + + /* contexts and event handling */ + + protected val handler: PartialFunction[HTML_Panel.Event, Unit] = Library.undefined + + private val ucontext = new SimpleUserAgentContext + private val rcontext = new SimpleHtmlRendererContext(this, ucontext) + { + private def handle(event: HTML_Panel.Event): Boolean = + if (handler.isDefinedAt(event)) { handler(event); false } + else true + + override def onContextMenu(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Context_Menu(elem, event)) + override def onMouseClick(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Mouse_Click(elem, event)) + override def onDoubleClick(elem: HTMLElement, event: MouseEvent): Boolean = + handle(HTML_Panel.Double_Click(elem, event)) + override def onMouseOver(elem: HTMLElement, event: MouseEvent) + { handle(HTML_Panel.Mouse_Over(elem, event)) } + override def onMouseOut(elem: HTMLElement, event: MouseEvent) + { handle(HTML_Panel.Mouse_Out(elem, event)) } + } + + private val builder = new DocumentBuilderImpl(ucontext, rcontext) + + + /* document template with style sheets */ + + private val template_head = + """ + + +
+ + +