--- a/Admin/isatest/settings/mac-poly-M2 Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M2 Wed Sep 19 12:11:09 2012 +0200
@@ -6,7 +6,7 @@
ML_SYSTEM="polyml-5.5.0"
ML_PLATFORM="x86-darwin"
-ML_HOME="/home/polyml/polyml-svn/$ML_PLATFORM"
+ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/Admin/isatest/settings/mac-poly-M4 Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M4 Wed Sep 19 12:11:09 2012 +0200
@@ -2,7 +2,7 @@
init_components /home/isabelle/contrib "$HOME/admin/components/main"
- POLYML_HOME="/home/polyml/polyml-svn"
+ POLYML_HOME="/home/polyml/polyml-5.5.0"
ML_SYSTEM="polyml-5.5.0"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
--- a/Admin/isatest/settings/mac-poly-M8 Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M8 Wed Sep 19 12:11:09 2012 +0200
@@ -2,7 +2,7 @@
init_components /home/isabelle/contrib "$HOME/admin/components/main"
- POLYML_HOME="/home/polyml/polyml-svn"
+ POLYML_HOME="/home/polyml/polyml-5.5.0"
ML_SYSTEM="polyml-5.5.0"
ML_PLATFORM="x86-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
--- a/src/Pure/General/position.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/General/position.scala Wed Sep 19 12:11:09 2012 +0200
@@ -20,6 +20,12 @@
val File = new Properties.String(Isabelle_Markup.FILE)
val Id = new Properties.Long(Isabelle_Markup.ID)
+ val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
+ val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
+ val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
+ val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
+ val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
+
object Line_File
{
def unapply(pos: T): Option[(Int, String)] =
@@ -30,6 +36,16 @@
}
}
+ object Def_Line_File
+ {
+ def unapply(pos: T): Option[(Int, String)] =
+ (pos, pos) match {
+ case (Def_Line(i), Def_File(name)) => Some((i, name))
+ case (_, Def_File(name)) => Some((1, name))
+ case _ => None
+ }
+ }
+
object Range
{
def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
@@ -50,6 +66,15 @@
}
}
+ object Def_Id_Offset
+ {
+ def unapply(pos: T): Option[(Long, Text.Offset)] =
+ (pos, pos) match {
+ case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
+ case _ => None
+ }
+ }
+
object Id_Range
{
def unapply(pos: T): Option[(Long, Text.Range)] =
@@ -59,16 +84,7 @@
}
}
- private val purge_pos = Map(
- Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
- Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
- Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
- Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
- Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
-
- def purge(props: T): T =
- for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
- yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
+ def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
/* here: inlined formal markup */
--- a/src/Pure/General/pretty.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/General/pretty.scala Wed Sep 19 12:11:09 2012 +0200
@@ -146,7 +146,7 @@
def string_of(input: XML.Body, margin: Int = margin_default,
metric: String => Double = metric_default): String =
- formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
+ XML.content(formatted(input, margin, metric))
/* unformatted output */
@@ -164,6 +164,5 @@
input.flatMap(standard_format).flatMap(fmt)
}
- def str_of(input: XML.Body): String =
- unformatted(input).iterator.flatMap(XML.content).mkString
+ def str_of(input: XML.Body): String = XML.content(unformatted(input))
}
--- a/src/Pure/PIDE/blob.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/blob.scala Wed Sep 19 12:11:09 2012 +0200
@@ -24,5 +24,5 @@
def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
- val empty_state: Blob.State = Blob.State(this)
+ val init_state: Blob.State = Blob.State(this)
}
--- a/src/Pure/PIDE/command.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 19 12:11:09 2012 +0200
@@ -60,10 +60,13 @@
case XML.Elem(Markup(name, atts), body) =>
atts match {
case Isabelle_Markup.Serial(i) =>
- val result = XML.Elem(Markup(name, Position.purge(atts)), body)
- val st0 = copy(results = results + (i -> result))
+ val props = Position.purge(atts)
+ val result = XML.Elem(Markup(name, props), body)
+ val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+
+ val st0 = copy(results = results + (i -> result_message))
val st1 =
- if (Protocol.is_tracing(message)) st0
+ if (Protocol.is_tracing(result)) st0
else
(st0 /: Protocol.message_positions(command, message))(
(st, range) => st.add_markup(Text.Info(range, result)))
@@ -79,7 +82,8 @@
type Span = List[Token]
- def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span): Command =
+ def apply(id: Document.Command_ID, node_name: Document.Node.Name,
+ span: Span, markup: Markup_Tree): Command =
{
val source: String =
span match {
@@ -96,13 +100,21 @@
i += n
}
- new Command(id, node_name, span1.toList, source)
+ new Command(id, node_name, span1.toList, source, markup)
}
- def unparsed(source: String): Command =
- Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
+ val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+
+ def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
+ Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
- val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+ def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
+
+ def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+ {
+ val (text, markup) = XML.content_markup(body)
+ unparsed(id, text, markup)
+ }
/* perspective */
@@ -131,7 +143,8 @@
val id: Document.Command_ID,
val node_name: Document.Node.Name,
val span: Command.Span,
- val source: String)
+ val source: String,
+ val init_markup: Markup_Tree)
{
/* classification */
@@ -167,5 +180,5 @@
/* accumulated results */
- val empty_state: Command.State = Command.State(this)
+ val init_state: Command.State = Command.State(this, markup = init_markup)
}
--- a/src/Pure/PIDE/document.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/document.scala Wed Sep 19 12:11:09 2012 +0200
@@ -350,7 +350,7 @@
def define_command(command: Command): State =
{
val id = command.id
- copy(commands = commands + (id -> command.empty_state))
+ copy(commands = commands + (id -> command.init_state))
}
def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
@@ -474,7 +474,7 @@
catch {
case _: State.Fail =>
try { the_command_state(command.id) }
- catch { case _: State.Fail => command.empty_state }
+ catch { case _: State.Fail => command.init_state }
}
}
--- a/src/Pure/PIDE/isabelle_markup.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Wed Sep 19 12:11:09 2012 +0200
@@ -231,6 +231,16 @@
val STDERR = "stderr"
val EXIT = "exit"
+ val WRITELN_MESSAGE = "writeln_message"
+ val TRACING_MESSAGE = "tracing_message"
+ val WARNING_MESSAGE = "warning_message"
+ val ERROR_MESSAGE = "error_message"
+
+ val message: String => String =
+ Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
+ WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+ .withDefault((name: String) => name + "_message")
+
val Return_Code = new Properties.Int("return_code")
val LEGACY = "legacy"
--- a/src/Pure/PIDE/markup_tree.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Wed Sep 19 12:11:09 2012 +0200
@@ -35,23 +35,30 @@
else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
def markup: List[XML.Elem] = rev_markup.reverse
+
+ def reverse_markup: Entry =
+ copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
}
object Branches
{
type T = SortedMap[Text.Range, Entry]
val empty: T = SortedMap.empty(Text.Range.Ordering)
+
+ def reverse_markup(branches: T): T =
+ (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
}
}
final class Markup_Tree private(branches: Markup_Tree.Branches.T)
{
+ import Markup_Tree._
+
private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
this(branches + (entry.range -> entry))
-
- import Markup_Tree._
+ def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
override def toString =
branches.toList.map(_._2) match {
--- a/src/Pure/PIDE/protocol.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Sep 19 12:11:09 2012 +0200
@@ -135,18 +135,21 @@
def is_tracing(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
case _ => false
}
def is_warning(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
case _ => false
}
def is_error(msg: XML.Tree): Boolean =
msg match {
case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
+ case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
case _ => false
}
@@ -154,6 +157,8 @@
msg match {
case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+ case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
+ List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
case _ => false
}
--- a/src/Pure/PIDE/xml.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/xml.scala Wed Sep 19 12:11:09 2012 +0200
@@ -12,8 +12,6 @@
import java.lang.ref.WeakReference
import javax.xml.parsers.DocumentBuilderFactory
-import scala.collection.mutable
-
object XML
{
@@ -71,18 +69,32 @@
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
- /* text content */
+ /* content -- text and markup */
+
+ private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
+ {
+ var text = new StringBuilder
+ var markup_tree = Markup_Tree.empty
- def content_stream(tree: Tree): Stream[String] =
- tree match {
- case Elem(_, body) => content_stream(body)
- case Text(content) => Stream(content)
- }
- def content_stream(body: Body): Stream[String] =
- body.toStream.flatten(content_stream(_))
+ def traverse(tree: Tree): Unit =
+ tree match {
+ case Elem(markup, trees) =>
+ val offset = text.length
+ trees.foreach(traverse)
+ val end_offset = text.length
+ if (record_markup)
+ markup_tree +=
+ isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
+ case Text(s) => text.append(s)
+ }
- def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
- def content(body: Body): Iterator[String] = content_stream(body).iterator
+ body.foreach(traverse)
+ (text.toString, markup_tree.reverse_markup)
+ }
+
+ def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)
+ def content(body: Body): String = make_content(body, false)._1
+ def content(tree: Tree): String = make_content(List(tree), false)._1
--- a/src/Pure/System/session.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/System/session.scala Wed Sep 19 12:11:09 2012 +0200
@@ -125,7 +125,7 @@
/* global state */
private val syslog = Volatile(Queue.empty[XML.Elem])
- def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
+ def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
@volatile private var _phase: Session.Phase = Session.Inactive
private def phase_=(new_phase: Session.Phase)
@@ -311,7 +311,7 @@
}
case Isabelle_Markup.Assign_Execs if output.is_protocol =>
- XML.content(output.body).mkString match {
+ XML.content(output.body) match {
case Protocol.Assign(id, assign) =>
try {
val cmds = global_state >>> (_.assign(id, assign))
@@ -328,7 +328,7 @@
}
case Isabelle_Markup.Removed_Versions if output.is_protocol =>
- XML.content(output.body).mkString match {
+ XML.content(output.body) match {
case Protocol.Removed(removed) =>
try {
global_state >> (_.removed_versions(removed))
@@ -339,7 +339,7 @@
case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
Future.fork {
- val arg = XML.content(output.body).mkString
+ val arg = XML.content(output.body)
val (tag, res) = Invoke_Scala.method(name, arg)
prover.get.invoke_scala(id, tag, res)
}
--- a/src/Pure/Thy/thy_syntax.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Sep 19 12:11:09 2012 +0200
@@ -68,7 +68,7 @@
/* result structure */
val spans = parse_spans(syntax.scan(text))
- spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+ spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
result()
}
}
@@ -226,7 +226,7 @@
commands
case cmd :: _ =>
val hook = commands.prev(cmd)
- val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+ val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
(commands /: cmds2)(_ - _).append_after(hook, inserted)
}
}
--- a/src/Tools/jEdit/etc/isabelle-jedit.css Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css Wed Sep 19 12:11:09 2012 +0200
@@ -2,10 +2,10 @@
.message { margin-top: 0.3ex; background-color: #F0F0F0; }
-.writeln { }
-.tracing { background-color: #F0F8FF; }
-.warning { background-color: #EEE8AA; }
-.error { background-color: #FFC1C1; }
+.writeln_message { }
+.tracing_message { background-color: #F0F8FF; }
+.warning_message { background-color: #EEE8AA; }
+.error_message { background-color: #FFC1C1; }
.report { display: none; }
--- a/src/Tools/jEdit/etc/options Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/etc/options Wed Sep 19 12:11:09 2012 +0200
@@ -31,6 +31,10 @@
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
+option writeln_message_color : string = "F0F0F0FF"
+option tracing_message_color : string = "F0F8FFFF"
+option warning_message_color : string = "EEE8AAFF"
+option error_message_color : string = "FFC1C1FF"
option bad_color : string = "FF6A6A64"
option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
--- a/src/Tools/jEdit/lib/Tools/jedit Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Wed Sep 19 12:11:09 2012 +0200
@@ -18,6 +18,7 @@
"src/isabelle_options.scala"
"src/isabelle_rendering.scala"
"src/isabelle_sidekick.scala"
+ "src/jedit_lib.scala"
"src/jedit_thy_load.scala"
"src/jedit_options.scala"
"src/output_dockable.scala"
@@ -27,10 +28,10 @@
"src/protocol_dockable.scala"
"src/raw_output_dockable.scala"
"src/readme_dockable.scala"
+ "src/rich_text_area.scala"
"src/scala_console.scala"
"src/session_dockable.scala"
"src/syslog_dockable.scala"
- "src/text_area_painter.scala"
"src/text_overview.scala"
"src/token_markup.scala"
)
--- a/src/Tools/jEdit/src/document_model.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Wed Sep 19 12:11:09 2012 +0200
@@ -66,7 +66,7 @@
def node_header(): Document.Node.Header =
{
Swing_Thread.require()
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
} match {
@@ -92,24 +92,6 @@
}
-
- /* point range */
-
- def point_range(offset: Text.Offset): Text.Range =
- Isabelle.buffer_lock(buffer) {
- def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
- try {
- val c = text(offset)
- if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
- Text.Range(offset, offset + 2)
- else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
- Text.Range(offset - 1, offset + 1)
- else Text.Range(offset, offset + 1)
- }
- catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
- }
-
-
/* pending text edits */
private object pending_edits // owned by Swing thread
@@ -151,7 +133,7 @@
def init()
{
flush()
- session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+ session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer))
}
def exit()
--- a/src/Tools/jEdit/src/document_view.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Wed Sep 19 12:11:09 2012 +0200
@@ -17,13 +17,9 @@
import java.lang.System
import java.text.BreakIterator
import java.awt.{Color, Graphics2D, Point}
-import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
- FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
import javax.swing.event.{CaretListener, CaretEvent}
-import org.gjt.sp.util.Log
-
-import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
+import org.gjt.sp.jedit.{jEdit, 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}
@@ -71,46 +67,10 @@
{
private val session = model.session
-
- /* robust extension body */
-
- def robust_body[A](default: A)(body: => A): A =
- {
- try {
- Swing_Thread.require()
- if (model.buffer == text_area.getBuffer) body
- else {
- Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
- default
- }
- }
- catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
- }
-
-
- /* visible text range */
+ def get_rendering(): Isabelle_Rendering =
+ Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
- def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
- Text.Range(start, end min model.buffer.getLength)
-
- def visible_range(): Option[Text.Range] =
- {
- val n = text_area.getVisibleLines
- if (n > 0) {
- val start = text_area.getScreenLineStartOffset(0)
- val raw_end = text_area.getScreenLineEndOffset(n - 1)
- Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength))
- }
- else None
- }
-
- def invalidate_range(range: Text.Range)
- {
- text_area.invalidateLineRange(
- model.buffer.getLineOfOffset(range.start),
- model.buffer.getLineOfOffset(range.stop))
- }
+ val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _)
/* perspective */
@@ -137,101 +97,13 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
+ // no robust_body
model.update_perspective()
}
}
- /* active areas within the text */
-
- private class Active_Area[A](
- rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
- {
- private var the_info: Option[Text.Info[A]] = None
-
- def info: Option[Text.Info[A]] = the_info
-
- def update(new_info: Option[Text.Info[A]])
- {
- val old_info = the_info
- if (new_info != old_info) {
- for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
- invalidate_range(range)
- the_info = new_info
- }
- }
-
- def update_rendering(r: Isabelle_Rendering, range: Text.Range)
- { update(rendering(r)(range)) }
-
- def reset { update(None) }
- }
-
- // owned by Swing thread
-
- private var control: Boolean = false
-
- private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
- def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
-
- private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
- def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
-
- private val active_areas = List(highlight_area, hyperlink_area)
- private def active_reset(): Unit = active_areas.foreach(_.reset)
-
- private val focus_listener = new FocusAdapter {
- override def focusLost(e: FocusEvent) { active_reset() }
- }
-
- private val window_listener = new WindowAdapter {
- override def windowIconified(e: WindowEvent) { active_reset() }
- override def windowDeactivated(e: WindowEvent) { active_reset() }
- }
-
- private val mouse_listener = new MouseAdapter {
- override def mouseClicked(e: MouseEvent) {
- hyperlink_area.info match {
- case Some(Text.Info(range, link)) => link.follow(text_area.getView)
- case None =>
- }
- }
- }
-
- private val mouse_motion_listener = new MouseMotionAdapter {
- override def mouseMoved(e: MouseEvent) {
- control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
- if (control && model.buffer.isLoaded) {
- Isabelle.buffer_lock(model.buffer) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
- active_areas.foreach(_.update_rendering(rendering, mouse_range))
- }
- }
- else active_reset()
- }
- }
-
-
- /* text area painting */
-
- private val text_area_painter = new Text_Area_Painter(this)
-
- private val tooltip_painter = new TextAreaExtension
- {
- override def getToolTipText(x: Int, y: Int): String =
- {
- robust_body(null: String) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- val offset = text_area.xyToOffset(x, y)
- val range = Text.Range(offset, offset + 1)
- val tip =
- if (control) rendering.tooltip(range)
- else rendering.tooltip_message(range)
- tip.map(Isabelle.tooltip(_)) getOrElse null
- }
- }
- }
+ /* gutter */
private val gutter_painter = new TextAreaExtension
{
@@ -239,7 +111,7 @@
first_line: Int, last_line: Int, physical_lines: Array[Int],
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
- robust_body(()) {
+ rich_text_area.robust_body(()) {
Swing_Thread.assert()
val gutter = text_area.getGutter
@@ -248,12 +120,13 @@
val FOLD_MARKER_SIZE = 12
if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
- Isabelle.buffer_lock(model.buffer) {
- val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
+ val buffer = model.buffer
+ JEdit_Lib.buffer_lock(buffer) {
+ val rendering = get_rendering()
for (i <- 0 until physical_lines.length) {
if (physical_lines(i) != -1) {
- val line_range = proper_line_range(start(i), end(i))
+ val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
// gutter icons
rendering.gutter_message(line_range) match {
@@ -308,7 +181,7 @@
case changed: Session.Commands_Changed =>
val buffer = model.buffer
Swing_Thread.later {
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
if (model.buffer == text_area.getBuffer) {
val snapshot = model.snapshot()
@@ -317,9 +190,9 @@
changed.commands.exists(snapshot.node.commands.contains)))
Swing_Thread.later { overview.delay_repaint.invoke() }
- visible_range() match {
+ JEdit_Lib.visible_range(text_area) match {
case Some(visible) =>
- if (changed.assignment) invalidate_range(visible)
+ if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
else {
val visible_cmds =
snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
@@ -328,7 +201,7 @@
line <- 0 until text_area.getVisibleLines
start = text_area.getScreenLineStartOffset(line) if start >= 0
end = text_area.getScreenLineEndOffset(line) if end >= 0
- range = proper_line_range(start, end)
+ range = JEdit_Lib.proper_line_range(buffer, start, end)
line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
if line_cmds.exists(changed.commands)
} text_area.invalidateScreenLineRange(line, line)
@@ -351,14 +224,10 @@
private def activate()
{
val painter = text_area.getPainter
+
painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
- text_area_painter.activate()
+ rich_text_area.activate()
text_area.getGutter.addExtension(gutter_painter)
- text_area.addFocusListener(focus_listener)
- text_area.getView.addWindowListener(window_listener)
- painter.addMouseListener(mouse_listener)
- painter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
text_area.addLeftOfScrollBar(overview)
session.raw_edits += main_actor
@@ -368,17 +237,13 @@
private def deactivate()
{
val painter = text_area.getPainter
+
session.raw_edits -= main_actor
session.commands_changed -= main_actor
- text_area.removeFocusListener(focus_listener)
- text_area.getView.removeWindowListener(window_listener)
- painter.removeMouseMotionListener(mouse_motion_listener)
- painter.removeMouseListener(mouse_listener)
text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
text_area.getGutter.removeExtension(gutter_painter)
- text_area_painter.deactivate()
- painter.removeExtension(tooltip_painter)
+ rich_text_area.deactivate()
painter.removeExtension(update_perspective)
}
}
--- a/src/Tools/jEdit/src/hyperlink.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/hyperlink.scala Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
{
Swing_Thread.require()
- Isabelle.jedit_buffer(jedit_file) match {
+ JEdit_Lib.jedit_buffer(jedit_file) match {
case Some(buffer) =>
view.goToBuffer(buffer)
val text_area = view.getTextArea
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Wed Sep 19 12:11:09 2012 +0200
@@ -14,6 +14,8 @@
import java.io.{File => JFile}
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.util.Log
import scala.collection.immutable.SortedMap
@@ -24,17 +26,28 @@
new Isabelle_Rendering(snapshot, options)
- /* physical rendering */
+ /* message priorities */
private val writeln_pri = 1
private val warning_pri = 2
private val legacy_pri = 3
private val error_pri = 4
+
+ /* icons */
+
+ private def load_icon(name: String): Icon =
+ {
+ val icon = GUIUtilities.loadIcon(name)
+ if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+ Log.log(Log.ERROR, icon, "Bad icon: " + name)
+ icon
+ }
+
private val gutter_icons = Map(
- warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
- legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
- error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
+ warning_pri -> load_icon("16x16/status/dialog-information.png"),
+ legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
+ error_pri -> load_icon("16x16/status/dialog-error.png"))
/* token markup -- text styles */
@@ -96,6 +109,10 @@
val warning_color = color_value("warning_color")
val error_color = color_value("error_color")
val error1_color = color_value("error1_color")
+ val writeln_message_color = color_value("writeln_message_color")
+ val tracing_message_color = color_value("tracing_message_color")
+ val warning_message_color = color_value("warning_message_color")
+ val error_message_color = color_value("error_message_color")
val bad_color = color_value("bad_color")
val intensify_color = color_value("intensify_color")
val quoted_color = color_value("quoted_color")
@@ -189,7 +206,7 @@
case _ => false }).isEmpty) =>
props match {
- case Position.Line_File(line, name) if Path.is_ok(name) =>
+ case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
Isabelle_System.source_file(Path.explode(name)) match {
case Some(path) =>
val jedit_file = Isabelle_System.platform_path(path)
@@ -197,7 +214,7 @@
case None => links
}
- case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
+ case Position.Def_Id_Offset(id, offset) =>
snapshot.state.find_command(snapshot.version, id) match {
case Some((node, command)) =>
val sources =
@@ -346,11 +363,21 @@
Text.Info(r, result) <-
snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
range, (Some(Protocol.Status.init), None),
- Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
+ Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
+ Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
+ Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
{
case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
if (Protocol.command_status_markup(markup.name)) =>
(Some(Protocol.command_status(status, markup)), color)
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _), _))) =>
+ (None, Some(writeln_message_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _))) =>
+ (None, Some(tracing_message_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _))) =>
+ (None, Some(warning_message_color))
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _))) =>
+ (None, Some(error_message_color))
case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
(None, Some(bad_color))
case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
@@ -387,6 +414,7 @@
private val text_colors: Map[String, Color] = Map(
+ Isabelle_Markup.COMMAND -> keyword1_color,
Isabelle_Markup.STRING -> Color.BLACK,
Isabelle_Markup.ALTSTRING -> Color.BLACK,
Isabelle_Markup.VERBATIM -> Color.BLACK,
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Wed Sep 19 12:11:09 2012 +0200
@@ -91,7 +91,7 @@
Swing_Thread.assert()
val buffer = pane.getBuffer
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
get_syntax match {
case None => null
case Some(syntax) =>
@@ -166,7 +166,7 @@
node_name(buffer) match {
case Some(name) =>
- val text = Isabelle.buffer_text(buffer)
+ val text = JEdit_Lib.buffer_text(buffer)
val structure = Structure.parse(syntax, name, text)
make_tree(0, structure) foreach (node => data.root.add(node))
true
@@ -177,15 +177,15 @@
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
- "isabelle", Isabelle.get_recent_syntax, Isabelle.buffer_node_name)
+ "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
- "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
+ "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
- "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
+ "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
class Isabelle_Sidekick_Raw
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala Wed Sep 19 12:11:09 2012 +0200
@@ -0,0 +1,148 @@
+/* Title: Tools/jEdit/src/jedit_lib.scala
+ Author: Makarius
+
+Misc library functions for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.{jEdit, Buffer, View}
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+
+
+object JEdit_Lib
+{
+ /* buffers */
+
+ 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) }
+
+ def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+ def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+ Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+ def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+ {
+ val name = buffer_name(buffer)
+ Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+ }
+
+
+ /* main jEdit components */
+
+ def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
+
+ def jedit_buffer(name: String): Option[Buffer] =
+ jedit_buffers().find(buffer => buffer_name(buffer) == name)
+
+ 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() }
+ }
+
+
+ /* point range */
+
+ def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
+ buffer_lock(buffer) {
+ def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
+ try {
+ val c = text(offset)
+ if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
+ Text.Range(offset, offset + 2)
+ else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
+ Text.Range(offset - 1, offset + 1)
+ else Text.Range(offset, offset + 1)
+ }
+ catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
+ }
+
+
+ /* proper line range */
+
+ // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
+ def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
+ Text.Range(start, end min buffer.getLength)
+
+
+ /* visible text range */
+
+ def visible_range(text_area: TextArea): Option[Text.Range] =
+ {
+ val buffer = text_area.getBuffer
+ val n = text_area.getVisibleLines
+ if (n > 0) {
+ val start = text_area.getScreenLineStartOffset(0)
+ val raw_end = text_area.getScreenLineEndOffset(n - 1)
+ Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
+ }
+ else None
+ }
+
+ def invalidate_range(text_area: TextArea, range: Text.Range)
+ {
+ val buffer = text_area.getBuffer
+ text_area.invalidateLineRange(
+ buffer.getLineOfOffset(range.start),
+ buffer.getLineOfOffset(range.stop))
+ }
+
+
+ /* char width */
+
+ def char_width(text_area: TextArea): Int =
+ {
+ val painter = text_area.getPainter
+ val font = painter.getFont
+ val font_context = painter.getFontRenderContext
+ font.getStringBounds(" ", font_context).getWidth.round.toInt
+ }
+
+
+ /* graphics range */
+
+ class Gfx_Range(val x: Int, val y: Int, val length: Int)
+
+ // NB: jEdit already normalizes \r\n and \r to \n
+ // NB: last line lacks \n
+ def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
+ {
+ val buffer = text_area.getBuffer
+
+ val p = text_area.offsetToXY(range.start)
+
+ val end = buffer.getLength
+ val stop = range.stop
+ val (q, r) =
+ if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
+ else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+ (text_area.offsetToXY(stop - 1), char_width(text_area))
+ else (text_area.offsetToXY(stop), 0)
+
+ if (p != null && q != null && p.x < q.x + r && p.y == q.y)
+ Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
+ else None
+ }
+}
+
--- a/src/Tools/jEdit/src/jedit_thy_load.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala Wed Sep 19 12:11:09 2012 +0200
@@ -36,9 +36,9 @@
override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
{
Swing_Thread.now {
- Isabelle.jedit_buffer(name.node) match {
+ JEdit_Lib.jedit_buffer(name.node) match {
case Some(buffer) =>
- Isabelle.buffer_lock(buffer) {
+ JEdit_Lib.buffer_lock(buffer) {
Some(f(buffer.getSegment(0, buffer.getLength)))
}
case None => None
--- a/src/Tools/jEdit/src/output2_dockable.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala Wed Sep 19 12:11:09 2012 +0200
@@ -31,13 +31,14 @@
private var zoom_factor = 100
private var show_tracing = false
private var do_update = true
- private var current_state = Command.empty.empty_state
- private var current_body: XML.Body = Nil
+ private var current_snapshot = Document.State.init.snapshot()
+ private var current_state = Command.empty.init_state
+ private var current_output: List[XML.Tree] = Nil
/* pretty text panel */
- private val pretty_text_area = new Pretty_Text_Area
+ private val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
@@ -53,33 +54,34 @@
{
Swing_Thread.require()
- val new_state =
- if (follow) {
- Document_View(view.getTextArea) match {
- case Some(doc_view) =>
- val snapshot = doc_view.model.snapshot()
+ val (new_snapshot, new_state) =
+ Document_View(view.getTextArea) match {
+ case Some(doc_view) =>
+ val snapshot = doc_view.model.snapshot()
+ if (follow && !snapshot.is_outdated) {
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
- case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
- case None => Command.empty.empty_state
+ case Some(cmd) =>
+ (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+ case None =>
+ (Document.State.init.snapshot(), Command.empty.init_state)
}
- case None => Command.empty.empty_state
- }
+ }
+ else (current_snapshot, current_state)
+ case None => (current_snapshot, current_state)
}
- else current_state
- val new_body =
+ val new_output =
if (!restriction.isDefined || restriction.get.contains(new_state.command))
- new_state.results.iterator.map(_._2).filter(
- { // FIXME not scalable
- case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
- case _ => true
- }).toList
- else current_body
+ new_state.results.iterator.map(_._2)
+ .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable
+ else current_output
- if (new_body != current_body) pretty_text_area.update(new_body)
+ if (new_output != current_output)
+ pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
+ current_snapshot = new_snapshot
current_state = new_state
- current_body = new_body
+ current_output = new_output
}
--- a/src/Tools/jEdit/src/output_dockable.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
private var zoom_factor = 100
private var show_tracing = false
private var do_update = true
- private var current_state = Command.empty.empty_state
+ private var current_state = Command.empty.init_state
private var current_body: XML.Body = Nil
@@ -47,7 +47,7 @@
val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
Document_View(view.getTextArea) match {
case Some(doc_view) =>
- doc_view.robust_body() {
+ doc_view.rich_text_area.robust_body() {
val cmd = current_state.command
val model = doc_view.model
val buffer = model.buffer
@@ -91,20 +91,17 @@
val snapshot = doc_view.model.snapshot()
snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
- case None => Command.empty.empty_state
+ case None => Command.empty.init_state
}
- case None => Command.empty.empty_state
+ case None => Command.empty.init_state
}
}
else current_state
val new_body =
if (!restriction.isDefined || restriction.get.contains(new_state.command))
- new_state.results.iterator.map(_._2).filter(
- { // FIXME not scalable
- case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
- case _ => true
- }).toList
+ new_state.results.iterator.map(_._2)
+ .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList // FIXME not scalable
else current_body
if (new_body != current_body) html_panel.render(new_body)
--- a/src/Tools/jEdit/src/plugin.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Wed Sep 19 12:11:09 2012 +0200
@@ -9,23 +9,17 @@
import isabelle._
-import java.lang.System
-import java.awt.Font
import javax.swing.JOptionPane
-import scala.collection.mutable
import scala.swing.{ListView, ScrollPane}
-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.{jEdit, EBMessage, EBPlugin, Buffer, View}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.util.Log
import scala.actors.Actor._
@@ -82,62 +76,6 @@
}
- /* 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
- }
-
-
- /* buffers */
-
- 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) }
-
- def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
- def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
- Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
-
- def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
- {
- val name = buffer_name(buffer)
- Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
- }
-
-
- /* main jEdit components */
-
- def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
-
- def jedit_buffer(name: String): Option[Buffer] =
- jedit_buffers().find(buffer => buffer_name(buffer) == name)
-
- 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() }
- }
-
-
/* document model and view */
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -145,24 +83,24 @@
def document_views(buffer: Buffer): List[Document_View] =
for {
- text_area <- jedit_text_areas(buffer).toList
+ text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
doc_view = document_view(text_area)
if doc_view.isDefined
} yield doc_view.get
def exit_model(buffer: Buffer)
{
- swing_buffer_lock(buffer) {
- jedit_text_areas(buffer).foreach(Document_View.exit)
+ JEdit_Lib.swing_buffer_lock(buffer) {
+ JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
Document_Model.exit(buffer)
}
}
def init_model(buffer: Buffer)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
val opt_model =
- buffer_node_name(buffer) match {
+ JEdit_Lib.buffer_node_name(buffer) match {
case Some(node_name) =>
document_model(buffer) match {
case Some(model) if model.name == node_name => Some(model)
@@ -171,7 +109,7 @@
case None => None
}
if (opt_model.isDefined) {
- for (text_area <- jedit_text_areas(buffer)) {
+ for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
if (document_view(text_area).map(_.model) != opt_model)
Document_View.init(opt_model.get, text_area)
}
@@ -181,7 +119,7 @@
def init_view(buffer: Buffer, text_area: JEditTextArea)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
document_model(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
@@ -191,7 +129,7 @@
def exit_view(buffer: Buffer, text_area: JEditTextArea)
{
- swing_buffer_lock(buffer) {
+ JEdit_Lib.swing_buffer_lock(buffer) {
Document_View.exit(text_area)
}
}
@@ -264,10 +202,10 @@
{
val view = jEdit.getActiveView()
- val buffers = Isabelle.jedit_buffers().toList
+ val buffers = JEdit_Lib.jedit_buffers().toList
if (buffers.forall(_.isLoaded)) {
def loaded_buffer(name: String): Boolean =
- buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+ buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
val thys =
for (buffer <- buffers; model <- Isabelle.document_model(buffer))
@@ -314,16 +252,16 @@
}
case Session.Ready =>
- Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
Swing_Thread.later { delay_load.invoke() }
case Session.Shutdown =>
- Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
Swing_Thread.later { delay_load.revoke() }
case _ =>
}
- case bad => System.err.println("session_manager: ignoring bad message " + bad)
+ case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
}
}
}
@@ -426,7 +364,7 @@
Isabelle.options.value.save_prefs()
Isabelle.session.phase_changed -= session_manager
- Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+ JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
Isabelle.session.stop()
}
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Wed Sep 19 12:11:09 2012 +0200
@@ -9,24 +9,71 @@
import isabelle._
-import java.awt.{Font, FontMetrics}
+import java.awt.{Font, FontMetrics, Toolkit}
+import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
+import javax.swing.{KeyStroke, JComponent}
+
+import org.gjt.sp.jedit.{jEdit, View, Registers}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
-import org.gjt.sp.jedit.jEdit
import org.gjt.sp.util.SyntaxUtilities
+
import scala.swing.{BorderPanel, Component}
-class Pretty_Text_Area extends BorderPanel
+object Pretty_Text_Area
+{
+ def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
+ : (String, Document.State) =
+ {
+ val command = Command.rich_text(Document.new_id(), formatted_body)
+ val node_name = command.node_name
+ val edits: List[Document.Edit_Text] =
+ List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
+
+ val state0 = base_snapshot.state.define_command(command)
+ val version0 = base_snapshot.version
+ val nodes0 = version0.nodes
+
+ assert(nodes0(node_name).commands.isEmpty)
+
+ val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+ val version1 = Document.Version.make(version0.syntax, nodes1)
+ val state1 =
+ state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
+ .define_version(version1, state0.the_assignment(version0))
+ .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
+
+ (command.source, state1)
+ }
+}
+
+class Pretty_Text_Area(view: View) extends BorderPanel
{
Swing_Thread.require()
- val text_area = new JEditEmbeddedTextArea
-
private var current_font_metrics: FontMetrics = null
private var current_font_family = "Dialog"
private var current_font_size: Int = 12
private var current_margin: Int = 0
private var current_body: XML.Body = Nil
+ private var current_base_snapshot = Document.State.init.snapshot()
+ private var current_rendering: Isabelle_Rendering = text_rendering()._2
+
+ private val text_area = new JEditEmbeddedTextArea
+ private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
+ private val buffer = text_area.getBuffer
+
+ private def text_rendering(): (String, Isabelle_Rendering) =
+ {
+ Swing_Thread.require()
+
+ val body =
+ Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
+ val (text, state) = Pretty_Text_Area.document_state(current_base_snapshot, body)
+ val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
+
+ (text, rendering)
+ }
def refresh()
{
@@ -42,14 +89,15 @@
current_font_metrics = painter.getFontMetrics(font)
current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
- val text =
- Pretty.string_of(current_body, current_margin, Pretty.font_metric(current_font_metrics))
+ val (text, rendering) = text_rendering()
+ current_rendering = rendering
- val buffer = text_area.getBuffer
try {
buffer.beginCompoundEdit
+ buffer.setReadOnly(false)
text_area.setText(text)
text_area.setCaretPosition(0)
+ buffer.setReadOnly(true)
}
finally {
buffer.endCompoundEdit
@@ -65,14 +113,40 @@
refresh()
}
- def update(body: XML.Body)
+ def update(base_snapshot: Document.Snapshot, body: XML.Body)
{
Swing_Thread.require()
+ require(!base_snapshot.is_outdated)
+ current_base_snapshot = base_snapshot
current_body = body
refresh()
}
+
+ /* keyboard actions */
+
+ private val action_listener = new ActionListener {
+ def actionPerformed(e: ActionEvent) {
+ e.getActionCommand match {
+ case "copy" => Registers.copy(text_area, '$')
+ case _ =>
+ }
+ }
+ }
+
+ text_area.registerKeyboardAction(action_listener, "copy",
+ KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED)
+ text_area.registerKeyboardAction(action_listener, "copy",
+ KeyStroke.getKeyStroke(KeyEvent.VK_C,
+ Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
+
+
+ /* init */
+
+ buffer.setTokenMarker(new Token_Markup.Marker(true, None))
+ buffer.setReadOnly(true)
layout(Component.wrap(text_area)) = BorderPanel.Position.Center
+ rich_text_area.activate()
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
react {
case output: Isabelle_Process.Output =>
if (output.is_stdout || output.is_stderr)
- Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
+ Swing_Thread.later { text_area.append(XML.content(output.message)) }
case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/rich_text_area.scala Wed Sep 19 12:11:09 2012 +0200
@@ -0,0 +1,489 @@
+/* Title: Tools/jEdit/src/rich_text_area.scala
+ Author: Makarius
+
+Enhanced version of jEdit text area, with rich text rendering,
+tooltips, hyperlinks etc.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Graphics2D, Shape, Window, Color}
+import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
+ FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
+import java.awt.font.TextAttribute
+import java.text.AttributedString
+import java.util.ArrayList
+
+import org.gjt.sp.util.Log
+import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
+import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
+
+
+class Rich_Text_Area(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering)
+{
+ private val buffer = text_area.getBuffer
+
+
+ /* robust extension body */
+
+ def robust_body[A](default: A)(body: => A): A =
+ {
+ try {
+ Swing_Thread.require()
+ if (buffer == text_area.getBuffer) body
+ else {
+ Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
+ default
+ }
+ }
+ catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+ }
+
+
+ /* original painters */
+
+ private def pick_extension(name: String): TextAreaExtension =
+ {
+ text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
+ match {
+ case List(x) => x
+ case _ => error("Expected exactly one " + name)
+ }
+ }
+
+ private val orig_text_painter =
+ pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
+
+
+ /* common painter state */
+
+ @volatile private var painter_rendering: Isabelle_Rendering = null
+ @volatile private var painter_clip: Shape = null
+
+ private val set_state = 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)
+ {
+ painter_rendering = get_rendering()
+ painter_clip = gfx.getClip
+ }
+ }
+
+ private val reset_state = 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)
+ {
+ painter_rendering = null
+ painter_clip = null
+ }
+ }
+
+ private def robust_rendering(body: Isabelle_Rendering => Unit)
+ {
+ robust_body(()) { body(painter_rendering) }
+ }
+
+
+ /* active areas within the text */
+
+ private class Active_Area[A](
+ rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
+ {
+ private var the_info: Option[Text.Info[A]] = None
+
+ def info: Option[Text.Info[A]] = the_info
+
+ def update(new_info: Option[Text.Info[A]])
+ {
+ val old_info = the_info
+ if (new_info != old_info) {
+ for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
+ JEdit_Lib.invalidate_range(text_area, range)
+ the_info = new_info
+ }
+ }
+
+ def update_rendering(r: Isabelle_Rendering, range: Text.Range)
+ { update(rendering(r)(range)) }
+
+ def reset { update(None) }
+ }
+
+ // owned by Swing thread
+
+ private var control: Boolean = false
+
+ private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
+ private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
+ private val active_areas = List(highlight_area, hyperlink_area)
+ private def active_reset(): Unit = active_areas.foreach(_.reset)
+
+ private val focus_listener = new FocusAdapter {
+ override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
+ }
+
+ private val window_listener = new WindowAdapter {
+ override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
+ override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
+ }
+
+ private val mouse_listener = new MouseAdapter {
+ override def mouseClicked(e: MouseEvent) {
+ robust_body(()) {
+ hyperlink_area.info match {
+ case Some(Text.Info(range, link)) => link.follow(view)
+ case None =>
+ }
+ }
+ }
+ }
+
+ private val mouse_motion_listener = new MouseMotionAdapter {
+ override def mouseMoved(e: MouseEvent) {
+ robust_body(()) {
+ control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+ if (control && !buffer.isLoading) {
+ JEdit_Lib.buffer_lock(buffer) {
+ val rendering = get_rendering()
+ val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
+ val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
+ active_areas.foreach(_.update_rendering(rendering, mouse_range))
+ }
+ }
+ else active_reset()
+ }
+ }
+ }
+
+
+ /* tooltips */
+
+ private val tooltip_painter = new TextAreaExtension
+ {
+ override def getToolTipText(x: Int, y: Int): String =
+ {
+ robust_body(null: String) {
+ val rendering = get_rendering()
+ val offset = text_area.xyToOffset(x, y)
+ val range = Text.Range(offset, offset + 1)
+ val tip =
+ if (control) rendering.tooltip(range)
+ else rendering.tooltip_message(range)
+ tip.map(Isabelle.tooltip(_)) getOrElse null
+ }
+ }
+ }
+
+
+ /* text background */
+
+ 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)
+ {
+ robust_rendering { rendering =>
+ val ascent = text_area.getPainter.getFontMetrics.getAscent
+
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+
+ // background color (1)
+ for {
+ Text.Info(range, color) <- rendering.background1(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color (2)
+ for {
+ Text.Info(range, color) <- rendering.background2(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+ }
+
+ // squiggly underline
+ for {
+ Text.Info(range, color) <- rendering.squiggly_underline(line_range)
+ r <- JEdit_Lib.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)
+ }
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ /* text */
+
+ private def paint_chunk_list(rendering: Isabelle_Rendering,
+ gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+ {
+ val clip_rect = gfx.getClipBounds
+ val painter = text_area.getPainter
+ val font_context = painter.getFontRenderContext
+
+ var w = 0.0f
+ var chunk = head
+ while (chunk != null) {
+ val chunk_offset = line_start + chunk.offset
+ if (x + w + chunk.width > clip_rect.x &&
+ x + w < clip_rect.x + clip_rect.width && chunk.accessable)
+ {
+ val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
+ val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
+ val chunk_font = chunk.style.getFont
+ val chunk_color = chunk.style.getForegroundColor
+
+ def string_width(s: String): Float =
+ if (s.isEmpty) 0.0f
+ else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+
+ val caret_range =
+ if (text_area.isCaretVisible)
+ JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+ else Text.Range(-1)
+
+ val markup =
+ for {
+ r1 <- rendering.text_color(chunk_range, chunk_color)
+ r2 <- r1.try_restrict(chunk_range)
+ } yield r2
+
+ val padded_markup =
+ if (markup.isEmpty)
+ Iterator(Text.Info(chunk_range, chunk_color))
+ else
+ Iterator(
+ Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
+ markup.iterator ++
+ Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
+
+ var x1 = x + w
+ gfx.setFont(chunk_font)
+ for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
+ val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+ gfx.setColor(color)
+
+ range.try_restrict(caret_range) match {
+ case Some(r) if !r.is_singularity =>
+ val i = r.start - range.start
+ val j = r.stop - range.start
+ val s1 = str.substring(0, i)
+ val s2 = str.substring(i, j)
+ val s3 = str.substring(j)
+
+ if (!s1.isEmpty) gfx.drawString(s1, x1, y)
+
+ val astr = new AttributedString(s2)
+ astr.addAttribute(TextAttribute.FONT, chunk_font)
+ astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+ astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+ gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+
+ if (!s3.isEmpty)
+ gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+
+ case _ =>
+ gfx.drawString(str, x1, y)
+ }
+ x1 += string_width(str)
+ }
+ }
+ w += chunk.width
+ chunk = chunk.next.asInstanceOf[Chunk]
+ }
+ w
+ }
+
+ 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)
+ {
+ robust_rendering { rendering =>
+ val clip = gfx.getClip
+ val x0 = text_area.getHorizontalOffset
+ val fm = text_area.getPainter.getFontMetrics
+ var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+
+ for (i <- 0 until physical_lines.length) {
+ val line = physical_lines(i)
+ if (line != -1) {
+ val screen_line = first_line + i
+ val chunks = text_area.getChunksOfScreenLine(screen_line)
+ if (chunks != null) {
+ val line_start = buffer.getLineStartOffset(line)
+ gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+ val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
+ gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+ orig_text_painter.paintValidLine(gfx,
+ screen_line, line, start(i), end(i), y + line_height * i)
+ gfx.setClip(clip)
+ }
+ }
+ y0 += line_height
+ }
+ }
+ }
+ }
+
+
+ /* foreground */
+
+ private val foreground_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)
+ {
+ robust_rendering { rendering =>
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+
+ // foreground color
+ for {
+ Text.Info(range, color) <- rendering.foreground(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // highlight range -- potentially from other snapshot
+ for {
+ info <- highlight_area.info
+ Text.Info(range, color) <- info.try_restrict(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // hyperlink range -- potentially from other snapshot
+ for {
+ info <- hyperlink_area.info
+ Text.Info(range, _) <- info.try_restrict(line_range)
+ r <- JEdit_Lib.gfx_range(text_area, range)
+ } {
+ gfx.setColor(rendering.hyperlink_color)
+ gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+ }
+ }
+ }
+ }
+ }
+ }
+
+
+ /* caret -- outside of text range */
+
+ private class Caret_Painter(before: Boolean) extends TextAreaExtension
+ {
+ override def paintValidLine(gfx: Graphics2D,
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ {
+ robust_rendering { _ =>
+ if (before) gfx.clipRect(0, 0, 0, 0)
+ else gfx.setClip(painter_clip)
+ }
+ }
+ }
+
+ private val before_caret_painter1 = new Caret_Painter(true)
+ private val after_caret_painter1 = new Caret_Painter(false)
+ private val before_caret_painter2 = new Caret_Painter(true)
+ private val after_caret_painter2 = new Caret_Painter(false)
+
+ private val caret_painter = new TextAreaExtension
+ {
+ override def paintValidLine(gfx: Graphics2D,
+ screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+ {
+ robust_rendering { _ =>
+ if (text_area.isCaretVisible) {
+ val caret = text_area.getCaretPosition
+ if (start <= caret && caret == end - 1) {
+ val painter = text_area.getPainter
+ val fm = painter.getFontMetrics
+
+ val offset = caret - text_area.getLineStartOffset(physical_line)
+ val x = text_area.offsetToXY(physical_line, offset).x
+ gfx.setColor(painter.getCaretColor)
+ gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
+ }
+ }
+ }
+ }
+ }
+
+
+ /* activation */
+
+ def activate()
+ {
+ val painter = text_area.getPainter
+ painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
+ painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
+ painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
+ painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
+ painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
+ painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
+ painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
+ painter.addExtension(500, foreground_painter)
+ painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
+ painter.removeExtension(orig_text_painter)
+ painter.addMouseListener(mouse_listener)
+ painter.addMouseMotionListener(mouse_motion_listener)
+ text_area.addFocusListener(focus_listener)
+ view.addWindowListener(window_listener)
+ }
+
+ def deactivate()
+ {
+ val painter = text_area.getPainter
+ view.removeWindowListener(window_listener)
+ text_area.removeFocusListener(focus_listener)
+ painter.removeMouseMotionListener(mouse_motion_listener)
+ painter.removeMouseListener(mouse_listener)
+ painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
+ painter.removeExtension(reset_state)
+ painter.removeExtension(foreground_painter)
+ painter.removeExtension(caret_painter)
+ painter.removeExtension(after_caret_painter2)
+ painter.removeExtension(before_caret_painter2)
+ painter.removeExtension(after_caret_painter1)
+ painter.removeExtension(before_caret_painter1)
+ painter.removeExtension(text_painter)
+ painter.removeExtension(background_painter)
+ painter.removeExtension(tooltip_painter)
+ painter.removeExtension(set_state)
+ }
+}
+
--- a/src/Tools/jEdit/src/text_area_painter.scala Wed Sep 19 10:57:44 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,401 +0,0 @@
-/* Title: Tools/jEdit/src/text_area_painter.scala
- Author: Makarius
-
-Painter setup for main jEdit text area, depending on common snapshot.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Graphics2D, Shape}
-import java.awt.font.TextAttribute
-import java.text.AttributedString
-import java.util.ArrayList
-
-import org.gjt.sp.jedit.Debug
-import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
-
-
-class Text_Area_Painter(doc_view: Document_View)
-{
- private val model = doc_view.model
- private val buffer = model.buffer
- private val text_area = doc_view.text_area
-
-
- /* graphics range */
-
- private def char_width(): Int =
- {
- val painter = text_area.getPainter
- val font = painter.getFont
- val font_context = painter.getFontRenderContext
- font.getStringBounds(" ", font_context).getWidth.round.toInt
- }
-
- private class Gfx_Range(val x: Int, val y: Int, val length: Int)
-
- // NB: jEdit already normalizes \r\n and \r to \n
- // NB: last line lacks \n
- private def gfx_range(range: Text.Range): Option[Gfx_Range] =
- {
- val p = text_area.offsetToXY(range.start)
-
- val end = buffer.getLength
- val stop = range.stop
- val (q, r) =
- if (stop >= end) (text_area.offsetToXY(end), char_width())
- else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
- (text_area.offsetToXY(stop - 1), char_width())
- else (text_area.offsetToXY(stop), 0)
-
- if (p != null && q != null && p.x < q.x + r && p.y == q.y)
- Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
- else None
- }
-
-
- /* original painters */
-
- private def pick_extension(name: String): TextAreaExtension =
- {
- text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
- match {
- case List(x) => x
- case _ => error("Expected exactly one " + name)
- }
- }
-
- private val orig_text_painter =
- pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
-
-
- /* common painter state */
-
- @volatile private var painter_rendering: Isabelle_Rendering = null
- @volatile private var painter_clip: Shape = null
-
- private val set_state = 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)
- {
- painter_rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
- painter_clip = gfx.getClip
- }
- }
-
- private val reset_state = 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)
- {
- painter_rendering = null
- painter_clip = null
- }
- }
-
- private def robust_rendering(body: Isabelle_Rendering => Unit)
- {
- doc_view.robust_body(()) { body(painter_rendering) }
- }
-
-
- /* text background */
-
- 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)
- {
- robust_rendering { rendering =>
- val ascent = text_area.getPainter.getFontMetrics.getAscent
-
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = doc_view.proper_line_range(start(i), end(i))
-
- // background color (1)
- for {
- Text.Info(range, color) <- rendering.background1(line_range)
- r <- gfx_range(range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // background color (2)
- for {
- Text.Info(range, color) <- rendering.background2(line_range)
- r <- gfx_range(range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
- }
-
- // squiggly underline
- for {
- Text.Info(range, color) <- rendering.squiggly_underline(line_range)
- r <- gfx_range(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)
- }
- }
- }
- }
- }
- }
- }
-
-
- /* text */
-
- private def paint_chunk_list(rendering: Isabelle_Rendering,
- gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
- {
- val clip_rect = gfx.getClipBounds
- val painter = text_area.getPainter
- val font_context = painter.getFontRenderContext
-
- var w = 0.0f
- var chunk = head
- while (chunk != null) {
- val chunk_offset = line_start + chunk.offset
- if (x + w + chunk.width > clip_rect.x &&
- x + w < clip_rect.x + clip_rect.width && chunk.accessable)
- {
- val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
- val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
- val chunk_font = chunk.style.getFont
- val chunk_color = chunk.style.getForegroundColor
-
- def string_width(s: String): Float =
- if (s.isEmpty) 0.0f
- else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
-
- val caret_range =
- if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition)
- else Text.Range(-1)
-
- val markup =
- for {
- r1 <- rendering.text_color(chunk_range, chunk_color)
- r2 <- r1.try_restrict(chunk_range)
- } yield r2
-
- val padded_markup =
- if (markup.isEmpty)
- Iterator(Text.Info(chunk_range, chunk_color))
- else
- Iterator(
- Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
- markup.iterator ++
- Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
-
- var x1 = x + w
- gfx.setFont(chunk_font)
- for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
- val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
- gfx.setColor(color)
-
- range.try_restrict(caret_range) match {
- case Some(r) if !r.is_singularity =>
- val i = r.start - range.start
- val j = r.stop - range.start
- val s1 = str.substring(0, i)
- val s2 = str.substring(i, j)
- val s3 = str.substring(j)
-
- if (!s1.isEmpty) gfx.drawString(s1, x1, y)
-
- val astr = new AttributedString(s2)
- astr.addAttribute(TextAttribute.FONT, chunk_font)
- astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
- astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
- gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
-
- if (!s3.isEmpty)
- gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
-
- case _ =>
- gfx.drawString(str, x1, y)
- }
- x1 += string_width(str)
- }
- }
- w += chunk.width
- chunk = chunk.next.asInstanceOf[Chunk]
- }
- w
- }
-
- 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)
- {
- robust_rendering { rendering =>
- val clip = gfx.getClip
- val x0 = text_area.getHorizontalOffset
- val fm = text_area.getPainter.getFontMetrics
- var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
-
- for (i <- 0 until physical_lines.length) {
- val line = physical_lines(i)
- if (line != -1) {
- val screen_line = first_line + i
- val chunks = text_area.getChunksOfScreenLine(screen_line)
- if (chunks != null) {
- val line_start = text_area.getBuffer.getLineStartOffset(line)
- gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
- val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
- gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
- orig_text_painter.paintValidLine(gfx,
- screen_line, line, start(i), end(i), y + line_height * i)
- gfx.setClip(clip)
- }
- }
- y0 += line_height
- }
- }
- }
- }
-
-
- /* foreground */
-
- private val foreground_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)
- {
- robust_rendering { rendering =>
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = doc_view.proper_line_range(start(i), end(i))
-
- // foreground color
- for {
- Text.Info(range, color) <- rendering.foreground(line_range)
- r <- gfx_range(range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // highlight range -- potentially from other snapshot
- for {
- info <- doc_view.highlight_info()
- Text.Info(range, color) <- info.try_restrict(line_range)
- r <- gfx_range(range)
- } {
- gfx.setColor(color)
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
-
- // hyperlink range -- potentially from other snapshot
- for {
- info <- doc_view.hyperlink_info()
- Text.Info(range, _) <- info.try_restrict(line_range)
- r <- gfx_range(range)
- } {
- gfx.setColor(rendering.hyperlink_color)
- gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
- }
- }
- }
- }
- }
- }
-
-
- /* caret -- outside of text range */
-
- private class Caret_Painter(before: Boolean) extends TextAreaExtension
- {
- override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
- {
- robust_rendering { _ =>
- if (before) gfx.clipRect(0, 0, 0, 0)
- else gfx.setClip(painter_clip)
- }
- }
- }
-
- private val before_caret_painter1 = new Caret_Painter(true)
- private val after_caret_painter1 = new Caret_Painter(false)
- private val before_caret_painter2 = new Caret_Painter(true)
- private val after_caret_painter2 = new Caret_Painter(false)
-
- private val caret_painter = new TextAreaExtension
- {
- override def paintValidLine(gfx: Graphics2D,
- screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
- {
- robust_rendering { _ =>
- if (text_area.isCaretVisible) {
- val caret = text_area.getCaretPosition
- if (start <= caret && caret == end - 1) {
- val painter = text_area.getPainter
- val fm = painter.getFontMetrics
-
- val offset = caret - text_area.getLineStartOffset(physical_line)
- val x = text_area.offsetToXY(physical_line, offset).x
- gfx.setColor(painter.getCaretColor)
- gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
- }
- }
- }
- }
- }
-
-
- /* activation */
-
- def activate()
- {
- val painter = text_area.getPainter
- painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
- painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
- painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
- painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
- painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
- painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
- painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
- painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
- painter.addExtension(500, foreground_painter)
- painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
- painter.removeExtension(orig_text_painter)
- }
-
- def deactivate()
- {
- val painter = text_area.getPainter
- painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
- painter.removeExtension(reset_state)
- painter.removeExtension(foreground_painter)
- painter.removeExtension(caret_painter)
- painter.removeExtension(after_caret_painter2)
- painter.removeExtension(before_caret_painter2)
- painter.removeExtension(after_caret_painter1)
- painter.removeExtension(before_caret_painter1)
- painter.removeExtension(text_painter)
- painter.removeExtension(background_painter)
- painter.removeExtension(set_state)
- }
-}
-
--- a/src/Tools/jEdit/src/text_overview.scala Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala Wed Sep 19 12:11:09 2012 +0200
@@ -65,8 +65,8 @@
super.paintComponent(gfx)
Swing_Thread.assert()
- doc_view.robust_body(()) {
- Isabelle.buffer_lock(buffer) {
+ doc_view.rich_text_area.robust_body(()) {
+ JEdit_Lib.buffer_lock(buffer) {
val snapshot = doc_view.model.snapshot()
if (snapshot.is_outdated) {