# 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 = + """ + + + + + + + +""" + + private def template(font_family: String, font_size: Int): String = + template_head + + "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" + + template_tail + + + /** main actor **/ + + /* internal messages */ + + private case class Resize(font_family: String, font_size: Int) + private case class Render_Document(text: String) + private case class Render(body: XML.Body) + private case class Render_Sync(body: XML.Body) + private case object Refresh + + private val main_actor = actor { + + /* internal state */ + + var current_font_metrics: FontMetrics = null + var current_font_family = "" + var current_font_size: Int = 0 + var current_margin: Int = 0 + var current_body: XML.Body = Nil + + def resize(font_family: String, font_size: Int) + { + val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size))) + val (font_metrics, margin) = + Swing_Thread.now { + val metrics = getFontMetrics(font) + (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20) + } + if (current_font_metrics == null || + current_font_family != font_family || + current_font_size != font_size || + current_margin != margin) + { + current_font_metrics = font_metrics + current_font_family = font_family + current_font_size = font_size + current_margin = margin + refresh() + } + } + + def refresh() { render(current_body) } + + def render_document(text: String) + { + val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost")) + Swing_Thread.later { setDocument(doc, rcontext) } + } + + def render(body: XML.Body) + { + current_body = body + val html_body = + current_body.flatMap(div => + Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) + .map(t => + XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))), + HTML.spans(t, true)))) + val doc = + builder.parse( + new InputSourceImpl( + new StringReader(template(current_font_family, current_font_size)), "http://localhost")) + doc.removeChild(doc.getLastChild()) + doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body))) + Swing_Thread.later { setDocument(doc, rcontext) } + } + + + /* main loop */ + + resize(initial_font_family, initial_font_size) + + loop { + react { + case Resize(font_family, font_size) => resize(font_family, font_size) + case Refresh => refresh() + case Render_Document(text) => render_document(text) + case Render(body) => render(body) + case Render_Sync(body) => render(body); reply(()) + case bad => System.err.println("main_actor: ignoring bad message " + bad) + } + } + } + + + /* external methods */ + + def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) } + def refresh() { main_actor ! Refresh } + def render_document(text: String) { main_actor ! Render_Document(text) } + def render(body: XML.Body) { main_actor ! Render(body) } + def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/isabelle_encoding.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,65 @@ +/* Title: Tools/jEdit/src/isabelle_encoding.scala + Author: Makarius + +Isabelle encoding -- based on UTF-8. +*/ + +package isabelle.jedit + + +import isabelle._ + +import org.gjt.sp.jedit.io.Encoding +import org.gjt.sp.jedit.buffer.JEditBuffer + +import java.nio.charset.{Charset, CodingErrorAction} +import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, + CharArrayReader, ByteArrayOutputStream} + +import scala.io.{Codec, Source, BufferedSource} + + +object Isabelle_Encoding +{ + val NAME = "UTF-8-Isabelle" + + def is_active(buffer: JEditBuffer): Boolean = + buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME +} + +class Isabelle_Encoding extends Encoding +{ + private val charset = Charset.forName(Standard_System.charset) + val BUFSIZE = 32768 + + private def text_reader(in: InputStream, codec: Codec): Reader = + { + val source = new BufferedSource(in)(codec) + new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) + } + + override def getTextReader(in: InputStream): Reader = + text_reader(in, Standard_System.codec()) + + override def getPermissiveTextReader(in: InputStream): Reader = + { + val codec = Standard_System.codec() + codec.onMalformedInput(CodingErrorAction.REPLACE) + codec.onUnmappableCharacter(CodingErrorAction.REPLACE) + text_reader(in, codec) + } + + override def getTextWriter(out: OutputStream): Writer = + { + val buffer = new ByteArrayOutputStream(BUFSIZE) { + override def flush() + { + val text = Isabelle.system.symbols.encode(toString(Standard_System.charset)) + out.write(text.getBytes(Standard_System.charset)) + out.flush() + } + override def close() { out.close() } + } + new OutputStreamWriter(buffer, charset.newEncoder()) + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/isabelle_hyperlinks.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_hyperlinks.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,88 @@ +/* Title: Tools/jEdit/src/isabelle_hyperlinks.scala + Author: Fabian Immler, TU Munich + +Hyperlink setup for Isabelle proof documents. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.io.File + +import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink} + +import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities} + + +private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int) + extends AbstractHyperlink(start, end, line, "") +{ + override def click(view: View) { + view.getTextArea.moveCaretPosition(def_offset) + } +} + +class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int) + extends AbstractHyperlink(start, end, line, "") +{ + override def click(view: View) = { + Isabelle.system.source_file(def_file) match { + case None => + Library.error_dialog(view, "File not found", "Could not find source file " + def_file) + case Some(file) => + jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line)) + } + } +} + +class Isabelle_Hyperlinks extends HyperlinkSource +{ + def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = + { + Swing_Thread.assert() + Isabelle.buffer_lock(buffer) { + Document_Model(buffer) match { + case Some(model) => + val snapshot = model.snapshot() + val markup = + snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { + // FIXME Isar_Document.Hyperlink extractor + case Text.Info(info_range, + XML.Elem(Markup(Markup.ENTITY, props), _)) + if (props.find( + { case (Markup.KIND, Markup.ML_OPEN) => true + case (Markup.KIND, Markup.ML_STRUCT) => true + case _ => false }).isEmpty) => + val Text.Range(begin, end) = info_range + val line = buffer.getLineOfOffset(begin) + (Position.File.unapply(props), Position.Line.unapply(props)) match { + case (Some(def_file), Some(def_line)) => + new External_Hyperlink(begin, end, line, def_file, def_line) + case _ => + (props, props) match { + case (Position.Id(def_id), Position.Offset(def_offset)) => + snapshot.lookup_command(def_id) match { + case Some(def_cmd) => + snapshot.node.command_start(def_cmd) match { + case Some(def_cmd_start) => + new Internal_Hyperlink(begin, end, line, + snapshot.convert(def_cmd_start + def_cmd.decode(def_offset))) + case None => null + } + case None => null + } + case _ => null + } + } + } + markup match { + case Text.Info(_, Some(link)) #:: _ => link + case _ => null + } + case None => null + } + } + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/isabelle_markup.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_markup.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,216 @@ +/* Title: Tools/jEdit/src/isabelle_markup.scala + Author: Makarius + +Isabelle specific physical rendering and markup selection. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.awt.Color + +import org.gjt.sp.jedit.syntax.Token + + +object Isabelle_Markup +{ + /* physical rendering */ + + val outdated_color = new Color(240, 240, 240) + val unfinished_color = new Color(255, 228, 225) + + val light_color = new Color(240, 240, 240) + val regular_color = new Color(192, 192, 192) + val warning_color = new Color(255, 140, 0) + val error_color = new Color(178, 34, 34) + val bad_color = new Color(255, 106, 106, 100) + val hilite_color = new Color(255, 204, 102, 100) + + class Icon(val priority: Int, val icon: javax.swing.Icon) + { + def >= (that: Icon): Boolean = this.priority >= that.priority + } + val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png")) + val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png")) + + + /* command status */ + + def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = + { + val state = snapshot.state(command) + if (snapshot.is_outdated) Some(outdated_color) + else + Isar_Document.command_status(state.status) match { + case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color) + case Isar_Document.Unprocessed => Some(unfinished_color) + case _ => None + } + } + + def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = + { + val state = snapshot.state(command) + if (snapshot.is_outdated) None + else + Isar_Document.command_status(state.status) match { + case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None + case Isar_Document.Unprocessed => Some(unfinished_color) + case Isar_Document.Failed => Some(error_color) + case Isar_Document.Finished => + if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color) + else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color) + else None + } + } + + + /* markup selectors */ + + val message: Markup_Tree.Select[Color] = + { + case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color + } + + val popup: Markup_Tree.Select[String] = + { + case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) + if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => + Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")) + } + + val gutter_message: Markup_Tree.Select[Icon] = + { + case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon + case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon + } + + val background1: Markup_Tree.Select[Color] = + { + case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color + case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color + } + + val background2: Markup_Tree.Select[Color] = + { + case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color + } + + val tooltip: Markup_Tree.Select[String] = + { + case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" + case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => + Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), + margin = Isabelle.Int_Property("tooltip-margin")) + case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort" + case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type" + case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term" + case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition" + case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token" + case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)" + case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)" + case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)" + case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable" + case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable" + case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable" + } + + private val subexp_include = + Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, + Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, + Markup.TFREE, Markup.TVAR) + + val subexp: Markup_Tree.Select[(Text.Range, Color)] = + { + case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => + (range, Color.black) + } + + + /* token markup -- text styles */ + + private val command_style: Map[String, Byte] = + { + import Token._ + Map[String, Byte]( + Keyword.THY_END -> KEYWORD2, + Keyword.THY_SCRIPT -> LABEL, + Keyword.PRF_SCRIPT -> LABEL, + Keyword.PRF_ASM -> KEYWORD3, + Keyword.PRF_ASM_GOAL -> KEYWORD3 + ).withDefaultValue(KEYWORD1) + } + + private val token_style: Map[String, Byte] = + { + import Token._ + Map[String, Byte]( + // logical entities + Markup.TCLASS -> NULL, + Markup.TYCON -> NULL, + Markup.FIXED -> NULL, + Markup.CONST -> LITERAL2, + Markup.DYNAMIC_FACT -> LABEL, + // inner syntax + Markup.TFREE -> NULL, + Markup.FREE -> MARKUP, + Markup.TVAR -> NULL, + Markup.SKOLEM -> COMMENT2, + Markup.BOUND -> LABEL, + Markup.VAR -> NULL, + Markup.NUM -> DIGIT, + Markup.FLOAT -> DIGIT, + Markup.XNUM -> DIGIT, + Markup.XSTR -> LITERAL4, + Markup.LITERAL -> OPERATOR, + Markup.INNER_COMMENT -> COMMENT1, + Markup.SORT -> NULL, + Markup.TYP -> NULL, + Markup.TERM -> NULL, + Markup.PROP -> NULL, + // ML syntax + Markup.ML_KEYWORD -> KEYWORD1, + Markup.ML_DELIMITER -> OPERATOR, + Markup.ML_IDENT -> NULL, + Markup.ML_TVAR -> NULL, + Markup.ML_NUMERAL -> DIGIT, + Markup.ML_CHAR -> LITERAL1, + Markup.ML_STRING -> LITERAL1, + Markup.ML_COMMENT -> COMMENT1, + Markup.ML_MALFORMED -> INVALID, + // embedded source text + Markup.ML_SOURCE -> COMMENT3, + Markup.DOC_SOURCE -> COMMENT3, + Markup.ANTIQ -> COMMENT4, + Markup.ML_ANTIQ -> COMMENT4, + Markup.DOC_ANTIQ -> COMMENT4, + // outer syntax + Markup.KEYWORD -> KEYWORD2, + Markup.OPERATOR -> OPERATOR, + Markup.COMMAND -> KEYWORD1, + Markup.IDENT -> NULL, + Markup.VERBATIM -> COMMENT3, + Markup.COMMENT -> COMMENT1, + Markup.CONTROL -> COMMENT3, + Markup.MALFORMED -> INVALID, + Markup.STRING -> LITERAL3, + Markup.ALTSTRING -> LITERAL1 + ).withDefaultValue(NULL) + } + + def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] = + { + case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) + if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get) + + case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _)) + if token_style(kind) != Token.NULL => token_style(kind) + + case Text.Info(_, XML.Elem(Markup(name, _), _)) + if token_style(name) != Token.NULL => token_style(name) + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/isabelle_options.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_options.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,67 @@ +/* Title: Tools/jEdit/src/isabelle_options.scala + Author: Johannes Hölzl, TU Munich + +Editor pane for plugin options. +*/ + +package isabelle.jedit + + +import isabelle._ + +import javax.swing.JSpinner + +import scala.swing.CheckBox + +import org.gjt.sp.jedit.AbstractOptionPane + + +class Isabelle_Options extends AbstractOptionPane("isabelle") +{ + private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic")) + private val auto_start = new CheckBox() + private val relative_font_size = new JSpinner() + private val tooltip_font_size = new JSpinner() + private val tooltip_margin = new JSpinner() + private val tooltip_dismiss_delay = new JSpinner() + + override def _init() + { + addComponent(Isabelle.Property("logic.title"), logic_selector.peer) + + addComponent(Isabelle.Property("auto-start.title"), auto_start.peer) + auto_start.selected = Isabelle.Boolean_Property("auto-start") + + relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100)) + addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size) + + tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10)) + addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size) + + tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40)) + addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin) + + tooltip_dismiss_delay.setValue( + Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt) + addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay) + } + + override def _save() + { + Isabelle.Property("logic") = logic_selector.selection.item.name + + Isabelle.Boolean_Property("auto-start") = auto_start.selected + + Isabelle.Int_Property("relative-font-size") = + relative_font_size.getValue().asInstanceOf[Int] + + Isabelle.Int_Property("tooltip-font-size") = + tooltip_font_size.getValue().asInstanceOf[Int] + + Isabelle.Int_Property("tooltip-margin") = + tooltip_margin.getValue().asInstanceOf[Int] + + Isabelle.Time_Property("tooltip-dismiss-delay") = + Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int]) + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/isabelle_sidekick.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,176 @@ +/* Title: Tools/jEdit/src/isabelle_sidekick.scala + Author: Fabian Immler, TU Munich + Author: Makarius + +SideKick parsers for Isabelle proof documents. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.collection.Set +import scala.collection.immutable.TreeSet + +import javax.swing.tree.DefaultMutableTreeNode +import javax.swing.text.Position +import javax.swing.Icon + +import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} +import errorlist.DefaultErrorSource +import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} + + +object Isabelle_Sidekick +{ + def int_to_pos(offset: Text.Offset): Position = + new Position { def getOffset = offset; override def toString = offset.toString } + + class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset + { + protected var _name = name + protected var _start = int_to_pos(start) + protected var _end = int_to_pos(end) + override def getIcon: Icon = null + override def getShortString: String = _name + override def getLongString: String = _name + override def getName: String = _name + override def setName(name: String) = _name = name + override def getStart: Position = _start + override def setStart(start: Position) = _start = start + override def getEnd: Position = _end + override def setEnd(end: Position) = _end = end + override def toString = _name + } +} + + +abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name) +{ + /* parsing */ + + @volatile protected var stopped = false + override def stop() = { stopped = true } + + def parser(data: SideKickParsedData, model: Document_Model): Unit + + def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = + { + stopped = false + + // FIXME lock buffer (!??) + val data = new SideKickParsedData(buffer.getName) + val root = data.root + data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength)) + + Swing_Thread.now { Document_Model(buffer) } match { + case Some(model) => + parser(data, model) + if (stopped) root.add(new DefaultMutableTreeNode("")) + case None => root.add(new DefaultMutableTreeNode("")) + } + data + } + + + /* completion */ + + override def supportsCompletion = true + override def canCompleteAnywhere = true + + override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion = + { + val buffer = pane.getBuffer + Isabelle.swing_buffer_lock(buffer) { + Document_Model(buffer) match { + case None => null + case Some(model) => + val line = buffer.getLineOfOffset(caret) + val start = buffer.getLineStartOffset(line) + val text = buffer.getSegment(start, caret - start) + + val completion = model.session.current_syntax().completion + completion.complete(text) match { + case None => null + case Some((word, cs)) => + val ds = + (if (Isabelle_Encoding.is_active(buffer)) + cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) + else cs).filter(_ != word) + if (ds.isEmpty) null + else new SideKickCompletion( + pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } + } + } + } + } +} + + +class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle") +{ + import Thy_Syntax.Structure + + def parser(data: SideKickParsedData, model: Document_Model) + { + val syntax = model.session.current_syntax() + + def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] = + entry match { + case Structure.Block(name, body) => + val node = + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) + (offset /: body)((i, e) => + { + make_tree(i, e) foreach (nd => node.add(nd)) + i + e.length + }) + List(node) + case Structure.Atom(command) + if command.is_command && syntax.heading_level(command).isEmpty => + val node = + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) + List(node) + case _ => Nil + } + + val text = Isabelle.buffer_text(model.buffer) + val structure = Structure.parse(syntax, "theory " + model.thy_name, text) + + make_tree(0, structure) foreach (node => data.root.add(node)) + } +} + + +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw") +{ + def parser(data: SideKickParsedData, model: Document_Model) + { + val root = data.root + val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) + for ((command, command_start) <- snapshot.node.command_range() if !stopped) { + snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => + { + val range = info.range + command_start + val content = command.source(info.range).replace('\n', ' ') + val info_text = + info.info match { + case elem @ XML.Elem(_, _) => + Pretty.formatted(List(elem), margin = 40).mkString("\n") + case x => x.toString + } + + new DefaultMutableTreeNode( + new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { + override def getShortString: String = content + override def getLongString: String = info_text + override def toString = "\"" + content + "\" " + range.toString + }) + }) + } + } +} + diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/dockable.scala --- a/src/Tools/jEdit/src/jedit/dockable.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,41 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/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/jedit/document_model.scala --- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,252 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/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/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,587 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/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/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,206 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/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 = - """ - - - - - - - -""" - - private def template(font_family: String, font_size: Int): String = - template_head + - "body { font-family: " + font_family + "; font-size: " + raw_px(font_size) + "px; }" + - template_tail - - - /** main actor **/ - - /* internal messages */ - - private case class Resize(font_family: String, font_size: Int) - private case class Render_Document(text: String) - private case class Render(body: XML.Body) - private case class Render_Sync(body: XML.Body) - private case object Refresh - - private val main_actor = actor { - - /* internal state */ - - var current_font_metrics: FontMetrics = null - var current_font_family = "" - var current_font_size: Int = 0 - var current_margin: Int = 0 - var current_body: XML.Body = Nil - - def resize(font_family: String, font_size: Int) - { - val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size))) - val (font_metrics, margin) = - Swing_Thread.now { - val metrics = getFontMetrics(font) - (metrics, (getWidth() / (metrics.charWidth(Symbol.spc) max 1) - 4) max 20) - } - if (current_font_metrics == null || - current_font_family != font_family || - current_font_size != font_size || - current_margin != margin) - { - current_font_metrics = font_metrics - current_font_family = font_family - current_font_size = font_size - current_margin = margin - refresh() - } - } - - def refresh() { render(current_body) } - - def render_document(text: String) - { - val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost")) - Swing_Thread.later { setDocument(doc, rcontext) } - } - - def render(body: XML.Body) - { - current_body = body - val html_body = - current_body.flatMap(div => - Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) - .map(t => - XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))), - HTML.spans(t, true)))) - val doc = - builder.parse( - new InputSourceImpl( - new StringReader(template(current_font_family, current_font_size)), "http://localhost")) - doc.removeChild(doc.getLastChild()) - doc.appendChild(XML.document_node(doc, XML.elem(HTML.BODY, html_body))) - Swing_Thread.later { setDocument(doc, rcontext) } - } - - - /* main loop */ - - resize(initial_font_family, initial_font_size) - - loop { - react { - case Resize(font_family, font_size) => resize(font_family, font_size) - case Refresh => refresh() - case Render_Document(text) => render_document(text) - case Render(body) => render(body) - case Render_Sync(body) => render(body); reply(()) - case bad => System.err.println("main_actor: ignoring bad message " + bad) - } - } - } - - - /* external methods */ - - def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) } - def refresh() { main_actor ! Refresh } - def render_document(text: String) { main_actor ! Render_Document(text) } - def render(body: XML.Body) { main_actor ! Render(body) } - def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/isabelle_encoding.scala --- a/src/Tools/jEdit/src/jedit/isabelle_encoding.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,65 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_encoding.scala - Author: Makarius - -Isabelle encoding -- based on UTF-8. -*/ - -package isabelle.jedit - - -import isabelle._ - -import org.gjt.sp.jedit.io.Encoding -import org.gjt.sp.jedit.buffer.JEditBuffer - -import java.nio.charset.{Charset, CodingErrorAction} -import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter, - CharArrayReader, ByteArrayOutputStream} - -import scala.io.{Codec, Source, BufferedSource} - - -object Isabelle_Encoding -{ - val NAME = "UTF-8-Isabelle" - - def is_active(buffer: JEditBuffer): Boolean = - buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME -} - -class Isabelle_Encoding extends Encoding -{ - private val charset = Charset.forName(Standard_System.charset) - val BUFSIZE = 32768 - - private def text_reader(in: InputStream, codec: Codec): Reader = - { - val source = new BufferedSource(in)(codec) - new CharArrayReader(Isabelle.system.symbols.decode(source.mkString).toArray) - } - - override def getTextReader(in: InputStream): Reader = - text_reader(in, Standard_System.codec()) - - override def getPermissiveTextReader(in: InputStream): Reader = - { - val codec = Standard_System.codec() - codec.onMalformedInput(CodingErrorAction.REPLACE) - codec.onUnmappableCharacter(CodingErrorAction.REPLACE) - text_reader(in, codec) - } - - override def getTextWriter(out: OutputStream): Writer = - { - val buffer = new ByteArrayOutputStream(BUFSIZE) { - override def flush() - { - val text = Isabelle.system.symbols.encode(toString(Standard_System.charset)) - out.write(text.getBytes(Standard_System.charset)) - out.flush() - } - override def close() { out.close() } - } - new OutputStreamWriter(buffer, charset.newEncoder()) - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,88 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_hyperlinks.scala - Author: Fabian Immler, TU Munich - -Hyperlink setup for Isabelle proof documents. -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.io.File - -import gatchan.jedit.hyperlinks.{Hyperlink, HyperlinkSource, AbstractHyperlink} - -import org.gjt.sp.jedit.{View, jEdit, Buffer, TextUtilities} - - -private class Internal_Hyperlink(start: Int, end: Int, line: Int, def_offset: Int) - extends AbstractHyperlink(start, end, line, "") -{ - override def click(view: View) { - view.getTextArea.moveCaretPosition(def_offset) - } -} - -class External_Hyperlink(start: Int, end: Int, line: Int, def_file: String, def_line: Int) - extends AbstractHyperlink(start, end, line, "") -{ - override def click(view: View) = { - Isabelle.system.source_file(def_file) match { - case None => - Library.error_dialog(view, "File not found", "Could not find source file " + def_file) - case Some(file) => - jEdit.openFiles(view, file.getParent, Array(file.getName, "+line:" + def_line)) - } - } -} - -class Isabelle_Hyperlinks extends HyperlinkSource -{ - def getHyperlink(buffer: Buffer, buffer_offset: Int): Hyperlink = - { - Swing_Thread.assert() - Isabelle.buffer_lock(buffer) { - Document_Model(buffer) match { - case Some(model) => - val snapshot = model.snapshot() - val markup = - snapshot.select_markup(Text.Range(buffer_offset, buffer_offset + 1)) { - // FIXME Isar_Document.Hyperlink extractor - case Text.Info(info_range, - XML.Elem(Markup(Markup.ENTITY, props), _)) - if (props.find( - { case (Markup.KIND, Markup.ML_OPEN) => true - case (Markup.KIND, Markup.ML_STRUCT) => true - case _ => false }).isEmpty) => - val Text.Range(begin, end) = info_range - val line = buffer.getLineOfOffset(begin) - (Position.File.unapply(props), Position.Line.unapply(props)) match { - case (Some(def_file), Some(def_line)) => - new External_Hyperlink(begin, end, line, def_file, def_line) - case _ => - (props, props) match { - case (Position.Id(def_id), Position.Offset(def_offset)) => - snapshot.lookup_command(def_id) match { - case Some(def_cmd) => - snapshot.node.command_start(def_cmd) match { - case Some(def_cmd_start) => - new Internal_Hyperlink(begin, end, line, - snapshot.convert(def_cmd_start + def_cmd.decode(def_offset))) - case None => null - } - case None => null - } - case _ => null - } - } - } - markup match { - case Text.Info(_, Some(link)) #:: _ => link - case _ => null - } - case None => null - } - } - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/isabelle_markup.scala --- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,216 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_markup.scala - Author: Makarius - -Isabelle specific physical rendering and markup selection. -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.awt.Color - -import org.gjt.sp.jedit.syntax.Token - - -object Isabelle_Markup -{ - /* physical rendering */ - - val outdated_color = new Color(240, 240, 240) - val unfinished_color = new Color(255, 228, 225) - - val light_color = new Color(240, 240, 240) - val regular_color = new Color(192, 192, 192) - val warning_color = new Color(255, 140, 0) - val error_color = new Color(178, 34, 34) - val bad_color = new Color(255, 106, 106, 100) - val hilite_color = new Color(255, 204, 102, 100) - - class Icon(val priority: Int, val icon: javax.swing.Icon) - { - def >= (that: Icon): Boolean = this.priority >= that.priority - } - val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png")) - val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png")) - - - /* command status */ - - def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = - { - val state = snapshot.state(command) - if (snapshot.is_outdated) Some(outdated_color) - else - Isar_Document.command_status(state.status) match { - case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color) - case Isar_Document.Unprocessed => Some(unfinished_color) - case _ => None - } - } - - def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = - { - val state = snapshot.state(command) - if (snapshot.is_outdated) None - else - Isar_Document.command_status(state.status) match { - case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None - case Isar_Document.Unprocessed => Some(unfinished_color) - case Isar_Document.Failed => Some(error_color) - case Isar_Document.Finished => - if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color) - else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color) - else None - } - } - - - /* markup selectors */ - - val message: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color - } - - val popup: Markup_Tree.Select[String] = - { - case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) - if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => - Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")) - } - - val gutter_message: Markup_Tree.Select[Icon] = - { - case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon - case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon - } - - val background1: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color - case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color - } - - val background2: Markup_Tree.Select[Color] = - { - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color - } - - val tooltip: Markup_Tree.Select[String] = - { - case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" - case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => - Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), - margin = Isabelle.Int_Property("tooltip-margin")) - case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort" - case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type" - case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term" - case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition" - case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => "inner syntax token" - case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => "free variable (globally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => "skolem variable (locally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => "bound variable (internally fixed)" - case Text.Info(_, XML.Elem(Markup(Markup.VAR, _), _)) => "schematic variable" - case Text.Info(_, XML.Elem(Markup(Markup.TFREE, _), _)) => "free type variable" - case Text.Info(_, XML.Elem(Markup(Markup.TVAR, _), _)) => "schematic type variable" - } - - private val subexp_include = - Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, - Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, - Markup.TFREE, Markup.TVAR) - - val subexp: Markup_Tree.Select[(Text.Range, Color)] = - { - case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => - (range, Color.black) - } - - - /* token markup -- text styles */ - - private val command_style: Map[String, Byte] = - { - import Token._ - Map[String, Byte]( - Keyword.THY_END -> KEYWORD2, - Keyword.THY_SCRIPT -> LABEL, - Keyword.PRF_SCRIPT -> LABEL, - Keyword.PRF_ASM -> KEYWORD3, - Keyword.PRF_ASM_GOAL -> KEYWORD3 - ).withDefaultValue(KEYWORD1) - } - - private val token_style: Map[String, Byte] = - { - import Token._ - Map[String, Byte]( - // logical entities - Markup.TCLASS -> NULL, - Markup.TYCON -> NULL, - Markup.FIXED -> NULL, - Markup.CONST -> LITERAL2, - Markup.DYNAMIC_FACT -> LABEL, - // inner syntax - Markup.TFREE -> NULL, - Markup.FREE -> MARKUP, - Markup.TVAR -> NULL, - Markup.SKOLEM -> COMMENT2, - Markup.BOUND -> LABEL, - Markup.VAR -> NULL, - Markup.NUM -> DIGIT, - Markup.FLOAT -> DIGIT, - Markup.XNUM -> DIGIT, - Markup.XSTR -> LITERAL4, - Markup.LITERAL -> OPERATOR, - Markup.INNER_COMMENT -> COMMENT1, - Markup.SORT -> NULL, - Markup.TYP -> NULL, - Markup.TERM -> NULL, - Markup.PROP -> NULL, - // ML syntax - Markup.ML_KEYWORD -> KEYWORD1, - Markup.ML_DELIMITER -> OPERATOR, - Markup.ML_IDENT -> NULL, - Markup.ML_TVAR -> NULL, - Markup.ML_NUMERAL -> DIGIT, - Markup.ML_CHAR -> LITERAL1, - Markup.ML_STRING -> LITERAL1, - Markup.ML_COMMENT -> COMMENT1, - Markup.ML_MALFORMED -> INVALID, - // embedded source text - Markup.ML_SOURCE -> COMMENT3, - Markup.DOC_SOURCE -> COMMENT3, - Markup.ANTIQ -> COMMENT4, - Markup.ML_ANTIQ -> COMMENT4, - Markup.DOC_ANTIQ -> COMMENT4, - // outer syntax - Markup.KEYWORD -> KEYWORD2, - Markup.OPERATOR -> OPERATOR, - Markup.COMMAND -> KEYWORD1, - Markup.IDENT -> NULL, - Markup.VERBATIM -> COMMENT3, - Markup.COMMENT -> COMMENT1, - Markup.CONTROL -> COMMENT3, - Markup.MALFORMED -> INVALID, - Markup.STRING -> LITERAL3, - Markup.ALTSTRING -> LITERAL1 - ).withDefaultValue(NULL) - } - - def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] = - { - case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)) - if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get) - - case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _)) - if token_style(kind) != Token.NULL => token_style(kind) - - case Text.Info(_, XML.Elem(Markup(name, _), _)) - if token_style(name) != Token.NULL => token_style(name) - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/isabelle_options.scala --- a/src/Tools/jEdit/src/jedit/isabelle_options.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,67 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_options.scala - Author: Johannes Hölzl, TU Munich - -Editor pane for plugin options. -*/ - -package isabelle.jedit - - -import isabelle._ - -import javax.swing.JSpinner - -import scala.swing.CheckBox - -import org.gjt.sp.jedit.AbstractOptionPane - - -class Isabelle_Options extends AbstractOptionPane("isabelle") -{ - private val logic_selector = Isabelle.logic_selector(Isabelle.Property("logic")) - private val auto_start = new CheckBox() - private val relative_font_size = new JSpinner() - private val tooltip_font_size = new JSpinner() - private val tooltip_margin = new JSpinner() - private val tooltip_dismiss_delay = new JSpinner() - - override def _init() - { - addComponent(Isabelle.Property("logic.title"), logic_selector.peer) - - addComponent(Isabelle.Property("auto-start.title"), auto_start.peer) - auto_start.selected = Isabelle.Boolean_Property("auto-start") - - relative_font_size.setValue(Isabelle.Int_Property("relative-font-size", 100)) - addComponent(Isabelle.Property("relative-font-size.title"), relative_font_size) - - tooltip_font_size.setValue(Isabelle.Int_Property("tooltip-font-size", 10)) - addComponent(Isabelle.Property("tooltip-font-size.title"), tooltip_font_size) - - tooltip_margin.setValue(Isabelle.Int_Property("tooltip-margin", 40)) - addComponent(Isabelle.Property("tooltip-margin.title"), tooltip_margin) - - tooltip_dismiss_delay.setValue( - Isabelle.Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)).ms.toInt) - addComponent(Isabelle.Property("tooltip-dismiss-delay.title"), tooltip_dismiss_delay) - } - - override def _save() - { - Isabelle.Property("logic") = logic_selector.selection.item.name - - Isabelle.Boolean_Property("auto-start") = auto_start.selected - - Isabelle.Int_Property("relative-font-size") = - relative_font_size.getValue().asInstanceOf[Int] - - Isabelle.Int_Property("tooltip-font-size") = - tooltip_font_size.getValue().asInstanceOf[Int] - - Isabelle.Int_Property("tooltip-margin") = - tooltip_margin.getValue().asInstanceOf[Int] - - Isabelle.Time_Property("tooltip-dismiss-delay") = - Time.seconds(tooltip_dismiss_delay.getValue().asInstanceOf[Int]) - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,176 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/isabelle_sidekick.scala - Author: Fabian Immler, TU Munich - Author: Makarius - -SideKick parsers for Isabelle proof documents. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.collection.Set -import scala.collection.immutable.TreeSet - -import javax.swing.tree.DefaultMutableTreeNode -import javax.swing.text.Position -import javax.swing.Icon - -import org.gjt.sp.jedit.{Buffer, EditPane, TextUtilities, View} -import errorlist.DefaultErrorSource -import sidekick.{SideKickParser, SideKickParsedData, SideKickCompletion, IAsset} - - -object Isabelle_Sidekick -{ - def int_to_pos(offset: Text.Offset): Position = - new Position { def getOffset = offset; override def toString = offset.toString } - - class Asset(name: String, start: Text.Offset, end: Text.Offset) extends IAsset - { - protected var _name = name - protected var _start = int_to_pos(start) - protected var _end = int_to_pos(end) - override def getIcon: Icon = null - override def getShortString: String = _name - override def getLongString: String = _name - override def getName: String = _name - override def setName(name: String) = _name = name - override def getStart: Position = _start - override def setStart(start: Position) = _start = start - override def getEnd: Position = _end - override def setEnd(end: Position) = _end = end - override def toString = _name - } -} - - -abstract class Isabelle_Sidekick(name: String) extends SideKickParser(name) -{ - /* parsing */ - - @volatile protected var stopped = false - override def stop() = { stopped = true } - - def parser(data: SideKickParsedData, model: Document_Model): Unit - - def parse(buffer: Buffer, error_source: DefaultErrorSource): SideKickParsedData = - { - stopped = false - - // FIXME lock buffer (!??) - val data = new SideKickParsedData(buffer.getName) - val root = data.root - data.getAsset(root).setEnd(Isabelle_Sidekick.int_to_pos(buffer.getLength)) - - Swing_Thread.now { Document_Model(buffer) } match { - case Some(model) => - parser(data, model) - if (stopped) root.add(new DefaultMutableTreeNode("")) - case None => root.add(new DefaultMutableTreeNode("")) - } - data - } - - - /* completion */ - - override def supportsCompletion = true - override def canCompleteAnywhere = true - - override def complete(pane: EditPane, caret: Text.Offset): SideKickCompletion = - { - val buffer = pane.getBuffer - Isabelle.swing_buffer_lock(buffer) { - Document_Model(buffer) match { - case None => null - case Some(model) => - val line = buffer.getLineOfOffset(caret) - val start = buffer.getLineStartOffset(line) - val text = buffer.getSegment(start, caret - start) - - val completion = model.session.current_syntax().completion - completion.complete(text) match { - case None => null - case Some((word, cs)) => - val ds = - (if (Isabelle_Encoding.is_active(buffer)) - cs.map(Isabelle.system.symbols.decode(_)).sortWith(_ < _) - else cs).filter(_ != word) - if (ds.isEmpty) null - else new SideKickCompletion( - pane.getView, word, ds.toArray.asInstanceOf[Array[Object]]) { } - } - } - } - } -} - - -class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle") -{ - import Thy_Syntax.Structure - - def parser(data: SideKickParsedData, model: Document_Model) - { - val syntax = model.session.current_syntax() - - def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] = - entry match { - case Structure.Block(name, body) => - val node = - new DefaultMutableTreeNode( - new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) - (offset /: body)((i, e) => - { - make_tree(i, e) foreach (nd => node.add(nd)) - i + e.length - }) - List(node) - case Structure.Atom(command) - if command.is_command && syntax.heading_level(command).isEmpty => - val node = - new DefaultMutableTreeNode( - new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) - List(node) - case _ => Nil - } - - val text = Isabelle.buffer_text(model.buffer) - val structure = Structure.parse(syntax, "theory " + model.thy_name, text) - - make_tree(0, structure) foreach (node => data.root.add(node)) - } -} - - -class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw") -{ - def parser(data: SideKickParsedData, model: Document_Model) - { - val root = data.root - val snapshot = Swing_Thread.now { model.snapshot() } // FIXME cover all nodes (!??) - for ((command, command_start) <- snapshot.node.command_range() if !stopped) { - snapshot.state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) => - { - val range = info.range + command_start - val content = command.source(info.range).replace('\n', ' ') - val info_text = - info.info match { - case elem @ XML.Elem(_, _) => - Pretty.formatted(List(elem), margin = 40).mkString("\n") - case x => x.toString - } - - new DefaultMutableTreeNode( - new Isabelle_Sidekick.Asset(command.toString, range.start, range.stop) { - override def getShortString: String = content - override def getLongString: String = info_text - override def toString = "\"" + content + "\" " + range.toString - }) - }) - } - } -} - diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/output_dockable.scala --- a/src/Tools/jEdit/src/jedit/output_dockable.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,163 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/output_dockable.scala - Author: Makarius - -Dockable window with result message output. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ - -import scala.swing.{FlowPanel, Button, CheckBox} -import scala.swing.event.ButtonClicked - -import java.awt.BorderLayout -import java.awt.event.{ComponentEvent, ComponentAdapter} - -import org.gjt.sp.jedit.View - - -class Output_Dockable(view: View, position: String) extends Dockable(view, position) -{ - Swing_Thread.require() - - private val html_panel = - new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) - { - override val handler: PartialFunction[HTML_Panel.Event, Unit] = { - case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" => - val text = elem.getFirstChild().getNodeValue() - - Document_View(view.getTextArea) match { - case Some(doc_view) => - val cmd = current_command.get - val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get - val buffer = view.getBuffer - buffer.beginCompoundEdit() - buffer.remove(start_ofs, cmd.length) - buffer.insert(start_ofs, text) - buffer.endCompoundEdit() - case None => - } - } - } - - set_content(html_panel) - - - /* component state -- owned by Swing thread */ - - private var zoom_factor = 100 - private var show_tracing = false - private var follow_caret = true - private var current_command: Option[Command] = None - - - private def handle_resize() - { - Swing_Thread.now { - html_panel.resize(Isabelle.font_family(), - scala.math.round(Isabelle.font_size() * zoom_factor / 100)) - } - } - - private def handle_perspective(): Boolean = - Swing_Thread.now { - Document_View(view.getTextArea) match { - case Some(doc_view) => - val cmd = doc_view.selected_command() - if (current_command == cmd) false - else { current_command = cmd; true } - case None => false - } - } - - private def handle_update(restriction: Option[Set[Command]] = None) - { - Swing_Thread.now { - if (follow_caret) handle_perspective() - Document_View(view.getTextArea) match { - case Some(doc_view) => - current_command match { - case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => - val snapshot = doc_view.model.snapshot() - val filtered_results = - snapshot.state(cmd).results.iterator.map(_._2) filter { - case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable - case _ => true - } - html_panel.render(filtered_results.toList) - case _ => - } - case None => - } - } - } - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case Session.Global_Settings => handle_resize() - case Session.Commands_Changed(changed) => handle_update(Some(changed)) - case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() - case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() - { - Isabelle.session.global_settings += main_actor - Isabelle.session.commands_changed += main_actor - Isabelle.session.perspective += main_actor - } - - override def exit() - { - Isabelle.session.global_settings -= main_actor - Isabelle.session.commands_changed -= main_actor - Isabelle.session.perspective -= main_actor - } - - - /* resize */ - - addComponentListener(new ComponentAdapter { - val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() } - override def componentResized(e: ComponentEvent) { delay() } - }) - - - /* controls */ - - private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) - zoom.tooltip = "Zoom factor for basic font size" - - private val tracing = new CheckBox("Tracing") { - reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } - } - tracing.selected = show_tracing - tracing.tooltip = "Indicate output of tracing messages" - - private val auto_update = new CheckBox("Auto update") { - reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } - } - auto_update.selected = follow_caret - auto_update.tooltip = "Indicate automatic update following cursor movement" - - private val update = new Button("Update") { - reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } - } - update.tooltip = "Update display according to the command at cursor position" - - private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) - add(controls.peer, BorderLayout.NORTH) - - handle_update() -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/plugin.scala --- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,401 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/plugin.scala - Author: Makarius - -Main Isabelle/jEdit plugin setup. -*/ - -package isabelle.jedit - - -import isabelle._ - -import java.io.{FileInputStream, IOException} -import java.awt.Font - -import scala.collection.mutable -import scala.swing.ComboBox - -import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, - Buffer, EditPane, ServiceManager, View} -import org.gjt.sp.jedit.buffer.JEditBuffer -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} -import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} -import org.gjt.sp.jedit.gui.DockableWindowManager - -import org.gjt.sp.util.Log - -import scala.actors.Actor -import Actor._ - - -object Isabelle -{ - /* plugin instance */ - - var system: Isabelle_System = null - var session: Session = null - - - /* properties */ - - val OPTION_PREFIX = "options.isabelle." - - object Property - { - def apply(name: String): String = - jEdit.getProperty(OPTION_PREFIX + name) - def apply(name: String, default: String): String = - jEdit.getProperty(OPTION_PREFIX + name, default) - def update(name: String, value: String) = - jEdit.setProperty(OPTION_PREFIX + name, value) - } - - object Boolean_Property - { - def apply(name: String): Boolean = - jEdit.getBooleanProperty(OPTION_PREFIX + name) - def apply(name: String, default: Boolean): Boolean = - jEdit.getBooleanProperty(OPTION_PREFIX + name, default) - def update(name: String, value: Boolean) = - jEdit.setBooleanProperty(OPTION_PREFIX + name, value) - } - - object Int_Property - { - def apply(name: String): Int = - jEdit.getIntegerProperty(OPTION_PREFIX + name) - def apply(name: String, default: Int): Int = - jEdit.getIntegerProperty(OPTION_PREFIX + name, default) - def update(name: String, value: Int) = - jEdit.setIntegerProperty(OPTION_PREFIX + name, value) - } - - object Double_Property - { - def apply(name: String): Double = - jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0) - def apply(name: String, default: Double): Double = - jEdit.getDoubleProperty(OPTION_PREFIX + name, default) - def update(name: String, value: Double) = - jEdit.setDoubleProperty(OPTION_PREFIX + name, value) - } - - object Time_Property - { - def apply(name: String): Time = - Time.seconds(Double_Property(name)) - def apply(name: String, default: Time): Time = - Time.seconds(Double_Property(name, default.seconds)) - def update(name: String, value: Time) = - Double_Property.update(name, value.seconds) - } - - - /* font */ - - def font_family(): String = jEdit.getProperty("view.font") - - def font_size(): Float = - (jEdit.getIntegerProperty("view.fontsize", 16) * - Int_Property("relative-font-size", 100)).toFloat / 100 - - - /* text area ranges */ - - case class Gfx_Range(val x: Int, val y: Int, val length: Int) - - def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = - { - val p = text_area.offsetToXY(range.start) - val q = text_area.offsetToXY(range.stop) - if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) - else None - } - - - /* tooltip markup */ - - def tooltip(text: String): String = - "
" +  // FIXME proper scaling (!?)
-      HTML.encode(text) + "
" - - def tooltip_dismiss_delay(): Time = - Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5) - - def setup_tooltips() - { - Swing_Thread.now { - val manager = javax.swing.ToolTipManager.sharedInstance - manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt) - } - } - - - /* icons */ - - def load_icon(name: String): javax.swing.Icon = - { - val icon = GUIUtilities.loadIcon(name) - if (icon.getIconWidth < 0 || icon.getIconHeight < 0) - Log.log(Log.ERROR, icon, "Bad icon: " + name) - icon - } - - - /* check JVM */ - - def check_jvm() - { - if (!Platform.is_hotspot) { - Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine", - "This is " + Platform.jvm_name, - "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!") - } - } - - - /* main jEdit components */ - - def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator - - def jedit_views(): Iterator[View] = jEdit.getViews().iterator - - def jedit_text_areas(view: View): Iterator[JEditTextArea] = - view.getEditPanes().iterator.map(_.getTextArea) - - def jedit_text_areas(): Iterator[JEditTextArea] = - jedit_views().flatMap(jedit_text_areas(_)) - - def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = - jedit_text_areas().filter(_.getBuffer == buffer) - - def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = - { - try { buffer.readLock(); body } - finally { buffer.readUnlock() } - } - - def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = - Swing_Thread.now { buffer_lock(buffer) { body } } - - def buffer_text(buffer: JEditBuffer): String = - buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } - - - /* dockable windows */ - - private def wm(view: View): DockableWindowManager = view.getDockableWindowManager - - def docked_session(view: View): Option[Session_Dockable] = - wm(view).getDockableWindow("isabelle-session") match { - case dockable: Session_Dockable => Some(dockable) - case _ => None - } - - def docked_output(view: View): Option[Output_Dockable] = - wm(view).getDockableWindow("isabelle-output") match { - case dockable: Output_Dockable => Some(dockable) - case _ => None - } - - def docked_raw_output(view: View): Option[Raw_Output_Dockable] = - wm(view).getDockableWindow("isabelle-raw-output") match { - case dockable: Raw_Output_Dockable => Some(dockable) - case _ => None - } - - def docked_protocol(view: View): Option[Protocol_Dockable] = - wm(view).getDockableWindow("isabelle-protocol") match { - case dockable: Protocol_Dockable => Some(dockable) - case _ => None - } - - - /* logic image */ - - def default_logic(): String = - { - val logic = system.getenv("JEDIT_LOGIC") - if (logic != "") logic - else system.getenv_strict("ISABELLE_LOGIC") - } - - class Logic_Entry(val name: String, val description: String) - { - override def toString = description - } - - def logic_selector(logic: String): ComboBox[Logic_Entry] = - { - val entries = - new Logic_Entry("", "default (" + default_logic() + ")") :: - system.find_logics().map(name => new Logic_Entry(name, name)) - val component = new ComboBox(entries) - entries.find(_.name == logic) match { - case None => - case Some(entry) => component.selection.item = entry - } - component.tooltip = "Isabelle logic image" - component - } - - def start_session() - { - val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5) - val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) - val logic = { - val logic = Property("logic") - if (logic != null && logic != "") logic - else Isabelle.default_logic() - } - session.start(timeout, modes ::: List(logic)) - } -} - - -class Plugin extends EBPlugin -{ - /* session management */ - - private def init_model(buffer: Buffer) - { - Isabelle.swing_buffer_lock(buffer) { - val opt_model = - Document_Model(buffer) match { - case Some(model) => model.refresh; Some(model) - case None => - Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { - case Some((dir, thy_name)) => - Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name)) - case None => None - } - } - if (opt_model.isDefined) { - for (text_area <- Isabelle.jedit_text_areas(buffer)) { - if (Document_View(text_area).map(_.model) != opt_model) - Document_View.init(opt_model.get, text_area) - } - } - } - } - - private def exit_model(buffer: Buffer) - { - Isabelle.swing_buffer_lock(buffer) { - Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) - Document_Model.exit(buffer) - } - } - - private case class Init_Model(buffer: Buffer) - private case class Exit_Model(buffer: Buffer) - private case class Init_View(buffer: Buffer, text_area: JEditTextArea) - private case class Exit_View(buffer: Buffer, text_area: JEditTextArea) - - private val session_manager = actor { - var ready = false - loop { - react { - case phase: Session.Phase => - ready = phase == Session.Ready - phase match { - case Session.Failed => - Swing_Thread.now { - val text = new scala.swing.TextArea(Isabelle.session.syslog()) - text.editable = false - Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) - } - - case Session.Ready => Isabelle.jedit_buffers.foreach(init_model) - case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model) - case _ => - } - - case Init_Model(buffer) => - if (ready) init_model(buffer) - - case Exit_Model(buffer) => - exit_model(buffer) - - case Init_View(buffer, text_area) => - if (ready) { - Isabelle.swing_buffer_lock(buffer) { - Document_Model(buffer) match { - case Some(model) => Document_View.init(model, text_area) - case None => - } - } - } - - case Exit_View(buffer, text_area) => - Isabelle.swing_buffer_lock(buffer) { - Document_View.exit(text_area) - } - - case bad => System.err.println("session_manager: ignoring bad message " + bad) - } - } - } - - - /* main plugin plumbing */ - - override def handleMessage(message: EBMessage) - { - message match { - case msg: EditorStarted => - Isabelle.check_jvm() - if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session() - - case msg: BufferUpdate - if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => - - val buffer = msg.getBuffer - if (buffer != null) session_manager ! Init_Model(buffer) - - case msg: EditPaneUpdate - if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || - msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || - msg.getWhat == EditPaneUpdate.CREATED || - msg.getWhat == EditPaneUpdate.DESTROYED) => - - val edit_pane = msg.getEditPane - val buffer = edit_pane.getBuffer - val text_area = edit_pane.getTextArea - - if (buffer != null && text_area != null) { - if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || - msg.getWhat == EditPaneUpdate.CREATED) - session_manager ! Init_View(buffer, text_area) - else - session_manager ! Exit_View(buffer, text_area) - } - - case msg: PropertiesChanged => - Swing_Thread.now { - Isabelle.setup_tooltips() - for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) - Document_View(text_area).get.extend_styles() - } - Isabelle.session.global_settings.event(Session.Global_Settings) - - case _ => - } - } - - override def start() - { - Isabelle.setup_tooltips() - Isabelle.system = new Isabelle_System - Isabelle.system.install_fonts() - Isabelle.session = new Session(Isabelle.system) - Isabelle.session.phase_changed += session_manager - } - - override def stop() - { - Isabelle.session.stop() - Isabelle.session.phase_changed -= session_manager - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/protocol_dockable.scala --- a/src/Tools/jEdit/src/jedit/protocol_dockable.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,39 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/protocol_dockable.scala - Author: Makarius - -Dockable window for protocol messages. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ -import scala.swing.{TextArea, ScrollPane} - -import org.gjt.sp.jedit.View - - -class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) -{ - private val text_area = new TextArea - set_content(new ScrollPane(text_area)) - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case result: Isabelle_Process.Result => - Swing_Thread.now { text_area.append(result.message.toString + "\n") } - - case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() { Isabelle.session.raw_messages += main_actor } - override def exit() { Isabelle.session.raw_messages -= main_actor } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/raw_output_dockable.scala --- a/src/Tools/jEdit/src/jedit/raw_output_dockable.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,42 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/raw_output_dockable.scala - Author: Makarius - -Dockable window for raw process output (stdout). -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ -import scala.swing.{TextArea, ScrollPane} - -import org.gjt.sp.jedit.View - - -class Raw_Output_Dockable(view: View, position: String) - extends Dockable(view: View, position: String) -{ - private val text_area = new TextArea - text_area.editable = false - set_content(new ScrollPane(text_area)) - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case result: Isabelle_Process.Result => - if (result.is_stdout) - Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } - - case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() { Isabelle.session.raw_messages += main_actor } - override def exit() { Isabelle.session.raw_messages -= main_actor } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/scala_console.scala --- a/src/Tools/jEdit/src/jedit/scala_console.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,155 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/scala_console.scala - Author: Makarius - -Scala instance of Console plugin. -*/ - -package isabelle.jedit - - -import isabelle._ - -import console.{Console, ConsolePane, Shell, Output} - -import org.gjt.sp.jedit.{jEdit, JARClassLoader} -import org.gjt.sp.jedit.MiscUtilities - -import java.io.{File, OutputStream, Writer, PrintWriter} - -import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} -import scala.collection.mutable - - -class Scala_Console extends Shell("Scala") -{ - /* reconstructed jEdit/plugin classpath */ - - private def reconstruct_classpath(): String = - { - def find_jars(start: String): List[String] = - if (start != null) - Standard_System.find_files(new File(start), - entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) - else Nil - val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) - path.mkString(File.pathSeparator) - } - - - /* global state -- owned by Swing thread */ - - private var interpreters = Map[Console, Interpreter]() - - private var global_console: Console = null - private var global_out: Output = null - private var global_err: Output = null - - private val console_stream = new OutputStream - { - val buf = new StringBuilder - override def flush() - { - val str = Standard_System.decode_permissive_utf8(buf.toString) - buf.clear - if (global_out == null) System.out.print(str) - else Swing_Thread.now { global_out.writeAttrs(null, str) } - } - override def close() { flush () } - def write(byte: Int) { buf.append(byte.toChar) } - } - - private val console_writer = new Writer - { - def flush() {} - def close() {} - - def write(cbuf: Array[Char], off: Int, len: Int) - { - if (len > 0) write(new String(cbuf.slice(off, off + len))) - } - - override def write(str: String) - { - if (global_out == null) System.out.println(str) - else global_out.print(null, str) - } - } - - private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = - { - global_console = console - global_out = out - global_err = if (err == null) out else err - val res = Exn.capture { scala.Console.withOut(console_stream)(e) } - console_stream.flush - global_console = null - global_out = null - global_err = null - Exn.release(res) - } - - private def report_error(str: String) - { - if (global_console == null || global_err == null) System.err.println(str) - else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } - } - - - /* jEdit console methods */ - - override def openConsole(console: Console) - { - val settings = new GenericRunnerSettings(report_error) - settings.classpath.value = reconstruct_classpath() - - val interp = new Interpreter(settings, new PrintWriter(console_writer, true)) - { - override def parentClassLoader = new JARClassLoader - } - interp.setContextClassLoader - interp.bind("view", "org.gjt.sp.jedit.View", console.getView) - interp.bind("console", "console.Console", console) - interp.interpret("import isabelle.jedit.Isabelle") - - interpreters += (console -> interp) - } - - override def closeConsole(console: Console) - { - interpreters -= console - } - - override def printInfoMessage(out: Output) - { - out.print(null, - "This shell evaluates Isabelle/Scala expressions.\n\n" + - "The following special toplevel bindings are provided:\n" + - " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + - " console -- jEdit Console plugin instance\n" + - " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n") - } - - override def printPrompt(console: Console, out: Output) - { - out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") - out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") - } - - override def execute(console: Console, input: String, out: Output, err: Output, command: String) - { - val interp = interpreters(console) - with_console(console, out, err) { interp.interpret(command) } - if (err != null) err.commandDone() - out.commandDone() - } - - override def stop(console: Console) - { - closeConsole(console) - console.clear - openConsole(console) - val out = console.getOutput - out.commandDone - printPrompt(console, out) - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/jedit/session_dockable.scala --- a/src/Tools/jEdit/src/jedit/session_dockable.scala Wed Jun 08 17:32:31 2011 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,104 +0,0 @@ -/* Title: Tools/jEdit/src/jedit/session_dockable.scala - Author: Makarius - -Dockable window for prover session management. -*/ - -package isabelle.jedit - - -import isabelle._ - -import scala.actors.Actor._ -import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing} -import scala.swing.event.{ButtonClicked, SelectionChanged} - -import java.awt.BorderLayout -import javax.swing.border.{BevelBorder, SoftBevelBorder} - -import org.gjt.sp.jedit.View - - -class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String) -{ - /* main tabs */ - - private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14) - readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html"))) - - private val syslog = new TextArea(Isabelle.session.syslog()) - syslog.editable = false - - private val tabs = new TabbedPane { - pages += new TabbedPane.Page("README", Component.wrap(readme)) - pages += new TabbedPane.Page("System log", new ScrollPane(syslog)) - - selection.index = - { - val index = Isabelle.Int_Property("session-panel.selection", 0) - if (index >= pages.length) 0 else index - } - listenTo(selection) - reactions += { - case SelectionChanged(_) => - Isabelle.Int_Property("session-panel.selection") = selection.index - } - } - - set_content(tabs) - - - /* controls */ - - val session_phase = new Label(Isabelle.session.phase.toString) - session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) - session_phase.tooltip = "Prover status" - - private val interrupt = new Button("Interrupt") { - reactions += { case ButtonClicked(_) => Isabelle.session.interrupt } - } - interrupt.tooltip = "Broadcast interrupt to all prover tasks" - - private val logic = Isabelle.logic_selector(Isabelle.Property("logic")) - logic.listenTo(logic.selection) - logic.reactions += { - case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name - } - - private val controls = - new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic) - add(controls.peer, BorderLayout.NORTH) - - - /* main actor */ - - private val main_actor = actor { - loop { - react { - case result: Isabelle_Process.Result => - if (result.is_syslog) - Swing_Thread.now { - val text = Isabelle.session.syslog() - if (text != syslog.text) { - syslog.text = text - } - } - - case phase: Session.Phase => - Swing_Thread.now { session_phase.text = " " + phase.toString + " " } - - case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) - } - } - } - - override def init() { - Isabelle.session.raw_messages += main_actor - Isabelle.session.phase_changed += main_actor - } - - override def exit() { - Isabelle.session.raw_messages -= main_actor - Isabelle.session.phase_changed -= main_actor - } -} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/output_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/output_dockable.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,163 @@ +/* Title: Tools/jEdit/src/output_dockable.scala + Author: Makarius + +Dockable window with result message output. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ + +import scala.swing.{FlowPanel, Button, CheckBox} +import scala.swing.event.ButtonClicked + +import java.awt.BorderLayout +import java.awt.event.{ComponentEvent, ComponentAdapter} + +import org.gjt.sp.jedit.View + + +class Output_Dockable(view: View, position: String) extends Dockable(view, position) +{ + Swing_Thread.require() + + private val html_panel = + new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size())) + { + override val handler: PartialFunction[HTML_Panel.Event, Unit] = { + case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" => + val text = elem.getFirstChild().getNodeValue() + + Document_View(view.getTextArea) match { + case Some(doc_view) => + val cmd = current_command.get + val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get + val buffer = view.getBuffer + buffer.beginCompoundEdit() + buffer.remove(start_ofs, cmd.length) + buffer.insert(start_ofs, text) + buffer.endCompoundEdit() + case None => + } + } + } + + set_content(html_panel) + + + /* component state -- owned by Swing thread */ + + private var zoom_factor = 100 + private var show_tracing = false + private var follow_caret = true + private var current_command: Option[Command] = None + + + private def handle_resize() + { + Swing_Thread.now { + html_panel.resize(Isabelle.font_family(), + scala.math.round(Isabelle.font_size() * zoom_factor / 100)) + } + } + + private def handle_perspective(): Boolean = + Swing_Thread.now { + Document_View(view.getTextArea) match { + case Some(doc_view) => + val cmd = doc_view.selected_command() + if (current_command == cmd) false + else { current_command = cmd; true } + case None => false + } + } + + private def handle_update(restriction: Option[Set[Command]] = None) + { + Swing_Thread.now { + if (follow_caret) handle_perspective() + Document_View(view.getTextArea) match { + case Some(doc_view) => + current_command match { + case Some(cmd) if !restriction.isDefined || restriction.get.contains(cmd) => + val snapshot = doc_view.model.snapshot() + val filtered_results = + snapshot.state(cmd).results.iterator.map(_._2) filter { + case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing // FIXME not scalable + case _ => true + } + html_panel.render(filtered_results.toList) + case _ => + } + case None => + } + } + } + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case Session.Global_Settings => handle_resize() + case Session.Commands_Changed(changed) => handle_update(Some(changed)) + case Session.Perspective => if (follow_caret && handle_perspective()) handle_update() + case bad => System.err.println("Output_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() + { + Isabelle.session.global_settings += main_actor + Isabelle.session.commands_changed += main_actor + Isabelle.session.perspective += main_actor + } + + override def exit() + { + Isabelle.session.global_settings -= main_actor + Isabelle.session.commands_changed -= main_actor + Isabelle.session.perspective -= main_actor + } + + + /* resize */ + + addComponentListener(new ComponentAdapter { + val delay = Swing_Thread.delay_last(Isabelle.session.update_delay) { handle_resize() } + override def componentResized(e: ComponentEvent) { delay() } + }) + + + /* controls */ + + private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) + zoom.tooltip = "Zoom factor for basic font size" + + private val tracing = new CheckBox("Tracing") { + reactions += { case ButtonClicked(_) => show_tracing = this.selected; handle_update() } + } + tracing.selected = show_tracing + tracing.tooltip = "Indicate output of tracing messages" + + private val auto_update = new CheckBox("Auto update") { + reactions += { case ButtonClicked(_) => follow_caret = this.selected; handle_update() } + } + auto_update.selected = follow_caret + auto_update.tooltip = "Indicate automatic update following cursor movement" + + private val update = new Button("Update") { + reactions += { case ButtonClicked(_) => handle_perspective(); handle_update() } + } + update.tooltip = "Update display according to the command at cursor position" + + private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update) + add(controls.peer, BorderLayout.NORTH) + + handle_update() +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/plugin.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/plugin.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,401 @@ +/* Title: Tools/jEdit/src/plugin.scala + Author: Makarius + +Main Isabelle/jEdit plugin setup. +*/ + +package isabelle.jedit + + +import isabelle._ + +import java.io.{FileInputStream, IOException} +import java.awt.Font + +import scala.collection.mutable +import scala.swing.ComboBox + +import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, + Buffer, EditPane, ServiceManager, View} +import org.gjt.sp.jedit.buffer.JEditBuffer +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} +import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} +import org.gjt.sp.jedit.gui.DockableWindowManager + +import org.gjt.sp.util.Log + +import scala.actors.Actor +import Actor._ + + +object Isabelle +{ + /* plugin instance */ + + var system: Isabelle_System = null + var session: Session = null + + + /* properties */ + + val OPTION_PREFIX = "options.isabelle." + + object Property + { + def apply(name: String): String = + jEdit.getProperty(OPTION_PREFIX + name) + def apply(name: String, default: String): String = + jEdit.getProperty(OPTION_PREFIX + name, default) + def update(name: String, value: String) = + jEdit.setProperty(OPTION_PREFIX + name, value) + } + + object Boolean_Property + { + def apply(name: String): Boolean = + jEdit.getBooleanProperty(OPTION_PREFIX + name) + def apply(name: String, default: Boolean): Boolean = + jEdit.getBooleanProperty(OPTION_PREFIX + name, default) + def update(name: String, value: Boolean) = + jEdit.setBooleanProperty(OPTION_PREFIX + name, value) + } + + object Int_Property + { + def apply(name: String): Int = + jEdit.getIntegerProperty(OPTION_PREFIX + name) + def apply(name: String, default: Int): Int = + jEdit.getIntegerProperty(OPTION_PREFIX + name, default) + def update(name: String, value: Int) = + jEdit.setIntegerProperty(OPTION_PREFIX + name, value) + } + + object Double_Property + { + def apply(name: String): Double = + jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0) + def apply(name: String, default: Double): Double = + jEdit.getDoubleProperty(OPTION_PREFIX + name, default) + def update(name: String, value: Double) = + jEdit.setDoubleProperty(OPTION_PREFIX + name, value) + } + + object Time_Property + { + def apply(name: String): Time = + Time.seconds(Double_Property(name)) + def apply(name: String, default: Time): Time = + Time.seconds(Double_Property(name, default.seconds)) + def update(name: String, value: Time) = + Double_Property.update(name, value.seconds) + } + + + /* font */ + + def font_family(): String = jEdit.getProperty("view.font") + + def font_size(): Float = + (jEdit.getIntegerProperty("view.fontsize", 16) * + Int_Property("relative-font-size", 100)).toFloat / 100 + + + /* text area ranges */ + + case class Gfx_Range(val x: Int, val y: Int, val length: Int) + + def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = + { + val p = text_area.offsetToXY(range.start) + val q = text_area.offsetToXY(range.stop) + if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) + else None + } + + + /* tooltip markup */ + + def tooltip(text: String): String = + "
" +  // FIXME proper scaling (!?)
+      HTML.encode(text) + "
" + + def tooltip_dismiss_delay(): Time = + Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5) + + def setup_tooltips() + { + Swing_Thread.now { + val manager = javax.swing.ToolTipManager.sharedInstance + manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt) + } + } + + + /* icons */ + + def load_icon(name: String): javax.swing.Icon = + { + val icon = GUIUtilities.loadIcon(name) + if (icon.getIconWidth < 0 || icon.getIconHeight < 0) + Log.log(Log.ERROR, icon, "Bad icon: " + name) + icon + } + + + /* check JVM */ + + def check_jvm() + { + if (!Platform.is_hotspot) { + Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine", + "This is " + Platform.jvm_name, + "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!") + } + } + + + /* main jEdit components */ + + def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator + + def jedit_views(): Iterator[View] = jEdit.getViews().iterator + + def jedit_text_areas(view: View): Iterator[JEditTextArea] = + view.getEditPanes().iterator.map(_.getTextArea) + + def jedit_text_areas(): Iterator[JEditTextArea] = + jedit_views().flatMap(jedit_text_areas(_)) + + def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = + jedit_text_areas().filter(_.getBuffer == buffer) + + def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = + { + try { buffer.readLock(); body } + finally { buffer.readUnlock() } + } + + def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = + Swing_Thread.now { buffer_lock(buffer) { body } } + + def buffer_text(buffer: JEditBuffer): String = + buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } + + + /* dockable windows */ + + private def wm(view: View): DockableWindowManager = view.getDockableWindowManager + + def docked_session(view: View): Option[Session_Dockable] = + wm(view).getDockableWindow("isabelle-session") match { + case dockable: Session_Dockable => Some(dockable) + case _ => None + } + + def docked_output(view: View): Option[Output_Dockable] = + wm(view).getDockableWindow("isabelle-output") match { + case dockable: Output_Dockable => Some(dockable) + case _ => None + } + + def docked_raw_output(view: View): Option[Raw_Output_Dockable] = + wm(view).getDockableWindow("isabelle-raw-output") match { + case dockable: Raw_Output_Dockable => Some(dockable) + case _ => None + } + + def docked_protocol(view: View): Option[Protocol_Dockable] = + wm(view).getDockableWindow("isabelle-protocol") match { + case dockable: Protocol_Dockable => Some(dockable) + case _ => None + } + + + /* logic image */ + + def default_logic(): String = + { + val logic = system.getenv("JEDIT_LOGIC") + if (logic != "") logic + else system.getenv_strict("ISABELLE_LOGIC") + } + + class Logic_Entry(val name: String, val description: String) + { + override def toString = description + } + + def logic_selector(logic: String): ComboBox[Logic_Entry] = + { + val entries = + new Logic_Entry("", "default (" + default_logic() + ")") :: + system.find_logics().map(name => new Logic_Entry(name, name)) + val component = new ComboBox(entries) + entries.find(_.name == logic) match { + case None => + case Some(entry) => component.selection.item = entry + } + component.tooltip = "Isabelle logic image" + component + } + + def start_session() + { + val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5) + val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) + val logic = { + val logic = Property("logic") + if (logic != null && logic != "") logic + else Isabelle.default_logic() + } + session.start(timeout, modes ::: List(logic)) + } +} + + +class Plugin extends EBPlugin +{ + /* session management */ + + private def init_model(buffer: Buffer) + { + Isabelle.swing_buffer_lock(buffer) { + val opt_model = + Document_Model(buffer) match { + case Some(model) => model.refresh; Some(model) + case None => + Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { + case Some((dir, thy_name)) => + Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name)) + case None => None + } + } + if (opt_model.isDefined) { + for (text_area <- Isabelle.jedit_text_areas(buffer)) { + if (Document_View(text_area).map(_.model) != opt_model) + Document_View.init(opt_model.get, text_area) + } + } + } + } + + private def exit_model(buffer: Buffer) + { + Isabelle.swing_buffer_lock(buffer) { + Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) + Document_Model.exit(buffer) + } + } + + private case class Init_Model(buffer: Buffer) + private case class Exit_Model(buffer: Buffer) + private case class Init_View(buffer: Buffer, text_area: JEditTextArea) + private case class Exit_View(buffer: Buffer, text_area: JEditTextArea) + + private val session_manager = actor { + var ready = false + loop { + react { + case phase: Session.Phase => + ready = phase == Session.Ready + phase match { + case Session.Failed => + Swing_Thread.now { + val text = new scala.swing.TextArea(Isabelle.session.syslog()) + text.editable = false + Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) + } + + case Session.Ready => Isabelle.jedit_buffers.foreach(init_model) + case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model) + case _ => + } + + case Init_Model(buffer) => + if (ready) init_model(buffer) + + case Exit_Model(buffer) => + exit_model(buffer) + + case Init_View(buffer, text_area) => + if (ready) { + Isabelle.swing_buffer_lock(buffer) { + Document_Model(buffer) match { + case Some(model) => Document_View.init(model, text_area) + case None => + } + } + } + + case Exit_View(buffer, text_area) => + Isabelle.swing_buffer_lock(buffer) { + Document_View.exit(text_area) + } + + case bad => System.err.println("session_manager: ignoring bad message " + bad) + } + } + } + + + /* main plugin plumbing */ + + override def handleMessage(message: EBMessage) + { + message match { + case msg: EditorStarted => + Isabelle.check_jvm() + if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session() + + case msg: BufferUpdate + if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => + + val buffer = msg.getBuffer + if (buffer != null) session_manager ! Init_Model(buffer) + + case msg: EditPaneUpdate + if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || + msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || + msg.getWhat == EditPaneUpdate.CREATED || + msg.getWhat == EditPaneUpdate.DESTROYED) => + + val edit_pane = msg.getEditPane + val buffer = edit_pane.getBuffer + val text_area = edit_pane.getTextArea + + if (buffer != null && text_area != null) { + if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || + msg.getWhat == EditPaneUpdate.CREATED) + session_manager ! Init_View(buffer, text_area) + else + session_manager ! Exit_View(buffer, text_area) + } + + case msg: PropertiesChanged => + Swing_Thread.now { + Isabelle.setup_tooltips() + for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) + Document_View(text_area).get.extend_styles() + } + Isabelle.session.global_settings.event(Session.Global_Settings) + + case _ => + } + } + + override def start() + { + Isabelle.setup_tooltips() + Isabelle.system = new Isabelle_System + Isabelle.system.install_fonts() + Isabelle.session = new Session(Isabelle.system) + Isabelle.session.phase_changed += session_manager + } + + override def stop() + { + Isabelle.session.stop() + Isabelle.session.phase_changed -= session_manager + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/protocol_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/protocol_dockable.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,39 @@ +/* Title: Tools/jEdit/src/protocol_dockable.scala + Author: Makarius + +Dockable window for protocol messages. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ +import scala.swing.{TextArea, ScrollPane} + +import org.gjt.sp.jedit.View + + +class Protocol_Dockable(view: View, position: String) extends Dockable(view, position) +{ + private val text_area = new TextArea + set_content(new ScrollPane(text_area)) + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case result: Isabelle_Process.Result => + Swing_Thread.now { text_area.append(result.message.toString + "\n") } + + case bad => System.err.println("Protocol_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() { Isabelle.session.raw_messages += main_actor } + override def exit() { Isabelle.session.raw_messages -= main_actor } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/raw_output_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,42 @@ +/* Title: Tools/jEdit/src/raw_output_dockable.scala + Author: Makarius + +Dockable window for raw process output (stdout). +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ +import scala.swing.{TextArea, ScrollPane} + +import org.gjt.sp.jedit.View + + +class Raw_Output_Dockable(view: View, position: String) + extends Dockable(view: View, position: String) +{ + private val text_area = new TextArea + text_area.editable = false + set_content(new ScrollPane(text_area)) + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case result: Isabelle_Process.Result => + if (result.is_stdout) + Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } + + case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() { Isabelle.session.raw_messages += main_actor } + override def exit() { Isabelle.session.raw_messages -= main_actor } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/scala_console.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/scala_console.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,155 @@ +/* Title: Tools/jEdit/src/scala_console.scala + Author: Makarius + +Scala instance of Console plugin. +*/ + +package isabelle.jedit + + +import isabelle._ + +import console.{Console, ConsolePane, Shell, Output} + +import org.gjt.sp.jedit.{jEdit, JARClassLoader} +import org.gjt.sp.jedit.MiscUtilities + +import java.io.{File, OutputStream, Writer, PrintWriter} + +import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} +import scala.collection.mutable + + +class Scala_Console extends Shell("Scala") +{ + /* reconstructed jEdit/plugin classpath */ + + private def reconstruct_classpath(): String = + { + def find_jars(start: String): List[String] = + if (start != null) + Standard_System.find_files(new File(start), + entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) + else Nil + val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) + path.mkString(File.pathSeparator) + } + + + /* global state -- owned by Swing thread */ + + private var interpreters = Map[Console, Interpreter]() + + private var global_console: Console = null + private var global_out: Output = null + private var global_err: Output = null + + private val console_stream = new OutputStream + { + val buf = new StringBuilder + override def flush() + { + val str = Standard_System.decode_permissive_utf8(buf.toString) + buf.clear + if (global_out == null) System.out.print(str) + else Swing_Thread.now { global_out.writeAttrs(null, str) } + } + override def close() { flush () } + def write(byte: Int) { buf.append(byte.toChar) } + } + + private val console_writer = new Writer + { + def flush() {} + def close() {} + + def write(cbuf: Array[Char], off: Int, len: Int) + { + if (len > 0) write(new String(cbuf.slice(off, off + len))) + } + + override def write(str: String) + { + if (global_out == null) System.out.println(str) + else global_out.print(null, str) + } + } + + private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = + { + global_console = console + global_out = out + global_err = if (err == null) out else err + val res = Exn.capture { scala.Console.withOut(console_stream)(e) } + console_stream.flush + global_console = null + global_out = null + global_err = null + Exn.release(res) + } + + private def report_error(str: String) + { + if (global_console == null || global_err == null) System.err.println(str) + else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } + } + + + /* jEdit console methods */ + + override def openConsole(console: Console) + { + val settings = new GenericRunnerSettings(report_error) + settings.classpath.value = reconstruct_classpath() + + val interp = new Interpreter(settings, new PrintWriter(console_writer, true)) + { + override def parentClassLoader = new JARClassLoader + } + interp.setContextClassLoader + interp.bind("view", "org.gjt.sp.jedit.View", console.getView) + interp.bind("console", "console.Console", console) + interp.interpret("import isabelle.jedit.Isabelle") + + interpreters += (console -> interp) + } + + override def closeConsole(console: Console) + { + interpreters -= console + } + + override def printInfoMessage(out: Output) + { + out.print(null, + "This shell evaluates Isabelle/Scala expressions.\n\n" + + "The following special toplevel bindings are provided:\n" + + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + + " console -- jEdit Console plugin instance\n" + + " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n") + } + + override def printPrompt(console: Console, out: Output) + { + out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") + out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") + } + + override def execute(console: Console, input: String, out: Output, err: Output, command: String) + { + val interp = interpreters(console) + with_console(console, out, err) { interp.interpret(command) } + if (err != null) err.commandDone() + out.commandDone() + } + + override def stop(console: Console) + { + closeConsole(console) + console.clear + openConsole(console) + val out = console.getOutput + out.commandDone + printPrompt(console, out) + } +} diff -r 8d8b6ed0588c -r 5d294220ca43 src/Tools/jEdit/src/session_dockable.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/session_dockable.scala Wed Jun 08 17:42:07 2011 +0200 @@ -0,0 +1,104 @@ +/* Title: Tools/jEdit/src/session_dockable.scala + Author: Makarius + +Dockable window for prover session management. +*/ + +package isabelle.jedit + + +import isabelle._ + +import scala.actors.Actor._ +import scala.swing.{FlowPanel, Button, TextArea, Label, ScrollPane, TabbedPane, Component, Swing} +import scala.swing.event.{ButtonClicked, SelectionChanged} + +import java.awt.BorderLayout +import javax.swing.border.{BevelBorder, SoftBevelBorder} + +import org.gjt.sp.jedit.View + + +class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String) +{ + /* main tabs */ + + private val readme = new HTML_Panel(Isabelle.system, "SansSerif", 14) + readme.render_document(Isabelle.system.try_read(List("$JEDIT_HOME/README.html"))) + + private val syslog = new TextArea(Isabelle.session.syslog()) + syslog.editable = false + + private val tabs = new TabbedPane { + pages += new TabbedPane.Page("README", Component.wrap(readme)) + pages += new TabbedPane.Page("System log", new ScrollPane(syslog)) + + selection.index = + { + val index = Isabelle.Int_Property("session-panel.selection", 0) + if (index >= pages.length) 0 else index + } + listenTo(selection) + reactions += { + case SelectionChanged(_) => + Isabelle.Int_Property("session-panel.selection") = selection.index + } + } + + set_content(tabs) + + + /* controls */ + + val session_phase = new Label(Isabelle.session.phase.toString) + session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED) + session_phase.tooltip = "Prover status" + + private val interrupt = new Button("Interrupt") { + reactions += { case ButtonClicked(_) => Isabelle.session.interrupt } + } + interrupt.tooltip = "Broadcast interrupt to all prover tasks" + + private val logic = Isabelle.logic_selector(Isabelle.Property("logic")) + logic.listenTo(logic.selection) + logic.reactions += { + case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name + } + + private val controls = + new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic) + add(controls.peer, BorderLayout.NORTH) + + + /* main actor */ + + private val main_actor = actor { + loop { + react { + case result: Isabelle_Process.Result => + if (result.is_syslog) + Swing_Thread.now { + val text = Isabelle.session.syslog() + if (text != syslog.text) { + syslog.text = text + } + } + + case phase: Session.Phase => + Swing_Thread.now { session_phase.text = " " + phase.toString + " " } + + case bad => System.err.println("Session_Dockable: ignoring bad message " + bad) + } + } + } + + override def init() { + Isabelle.session.raw_messages += main_actor + Isabelle.session.phase_changed += main_actor + } + + override def exit() { + Isabelle.session.raw_messages -= main_actor + Isabelle.session.phase_changed -= main_actor + } +}