--- 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=(
--- /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()
+ }
+}
--- /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)
+ }
+}
--- /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()
+ }
+}
--- /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 =
+ """<?xml version="1.0" encoding="utf-8"?>
+<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
+ "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
+<html xmlns="http://www.w3.org/1999/xhtml">
+<head>
+<style media="all" type="text/css">
+""" +
+ system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
+
+ private val template_tail =
+"""
+</style>
+</head>
+<body/>
+</html>
+"""
+
+ 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) }
+}
--- /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())
+ }
+}
--- /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
+ }
+ }
+ }
+}
--- /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)
+ }
+}
--- /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])
+ }
+}
--- /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("<parser stopped>"))
+ case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
+ }
+ 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
+ })
+ })
+ }
+ }
+}
+
--- 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()
- }
-}
--- 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)
- }
-}
--- 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()
- }
-}
--- 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 =
- """<?xml version="1.0" encoding="utf-8"?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN"
- "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-<head>
-<style media="all" type="text/css">
-""" +
- system.try_read(system.getenv_strict("JEDIT_STYLE_SHEETS").split(":"))
-
- private val template_tail =
-"""
-</style>
-</head>
-<body/>
-</html>
-"""
-
- 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) }
-}
--- 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())
- }
-}
--- 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
- }
- }
- }
-}
--- 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)
- }
-}
--- 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])
- }
-}
--- 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("<parser stopped>"))
- case None => root.add(new DefaultMutableTreeNode("<buffer inactive>"))
- }
- 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
- })
- })
- }
- }
-}
-
--- 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()
-}
--- 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 =
- "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
- Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
- HTML.encode(text) + "</pre></html>"
-
- 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
- }
-}
--- 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 }
-}
--- 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 }
-}
--- 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)
- }
-}
--- 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
- }
-}
--- /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()
+}
--- /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 =
+ "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
+ Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
+ HTML.encode(text) + "</pre></html>"
+
+ 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
+ }
+}
--- /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 }
+}
--- /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 }
+}
--- /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)
+ }
+}
--- /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
+ }
+}