--- a/src/Pure/Concurrent/simple_thread.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/Concurrent/simple_thread.scala Fri Sep 21 11:47:16 2012 +0200
@@ -15,6 +15,12 @@
object Simple_Thread
{
+ /* prending interrupts */
+
+ def interrupted_exception(): Unit =
+ if (Thread.interrupted()) throw new InterruptedException
+
+
/* plain thread */
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread =
--- a/src/Pure/General/pretty.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/General/pretty.scala Fri Sep 21 11:47:16 2012 +0200
@@ -59,12 +59,14 @@
val FBreak = XML.Text("\n")
+ val Separator = XML.elem(Isabelle_Markup.SEPARATOR, List(FBreak))
+
/* formatted output */
- private def standard_format(tree: XML.Tree): XML.Body =
- tree match {
- case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
+ def standard_format(body: XML.Body): XML.Body =
+ body flatMap {
+ case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
}
@@ -141,7 +143,7 @@
format(ts1, blockin, after, btext1)
case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
}
- format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
+ format(standard_format(input), 0.0, 0.0, Text()).content
}
def string_of(input: XML.Body, margin: Int = margin_default,
@@ -161,7 +163,7 @@
case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
case XML.Text(_) => List(tree)
}
- input.flatMap(standard_format).flatMap(fmt)
+ standard_format(input).flatMap(fmt)
}
def str_of(input: XML.Body): String = XML.content(unformatted(input))
--- a/src/Pure/PIDE/command.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/PIDE/command.scala Fri Sep 21 11:47:16 2012 +0200
@@ -112,7 +112,8 @@
def rich_text(id: Document.Command_ID, body: XML.Body): Command =
{
- val (text, markup) = XML.content_markup(body)
+ val text = XML.content(body)
+ val markup = Markup_Tree.from_XML(body)
unparsed(id, text, markup)
}
--- a/src/Pure/PIDE/isabelle_markup.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala Fri Sep 21 11:47:16 2012 +0200
@@ -69,6 +69,8 @@
val Width = new Properties.Int("width")
val BREAK = "break"
+ val SEPARATOR = "separator"
+
/* hidden text */
--- a/src/Pure/PIDE/markup_tree.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Fri Sep 21 11:47:16 2012 +0200
@@ -12,16 +12,35 @@
import javax.swing.tree.DefaultMutableTreeNode
import scala.collection.immutable.SortedMap
+import scala.annotation.tailrec
object Markup_Tree
{
val empty: Markup_Tree = new Markup_Tree(Branches.empty)
+ def merge_disjoint(trees: List[Markup_Tree]): Markup_Tree =
+ trees match {
+ case Nil => empty
+ case head :: tail =>
+ new Markup_Tree(
+ (head.branches /: tail) {
+ case (branches, tree) =>
+ (branches /: tree.branches) {
+ case (bs, (r, entry)) =>
+ require(!bs.isDefinedAt(r))
+ bs + (r -> entry)
+ }
+ })
+ }
+
object Entry
{
def apply(markup: Text.Markup, subtree: Markup_Tree): Entry =
Entry(markup.range, List(markup.info), Set(markup.info.markup.name), subtree)
+
+ def apply(range: Text.Range, rev_markups: List[XML.Elem], subtree: Markup_Tree): Entry =
+ Entry(range, rev_markups, Set.empty ++ rev_markups.iterator.map(_.markup.name), subtree)
}
sealed case class Entry(
@@ -35,31 +54,51 @@
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) }
- }
+
+ /* XML representation */
+
+ @tailrec private def strip_elems(markups: List[Markup], body: XML.Body): (List[Markup], XML.Body) =
+ body match {
+ case List(XML.Elem(markup1, body1)) => strip_elems(markup1 :: markups, body1)
+ case _ => (markups, body)
+ }
+
+ private def make_trees(acc: (Int, List[Markup_Tree]), tree: XML.Tree): (Int, List[Markup_Tree]) =
+ {
+ val (offset, markup_trees) = acc
+
+ strip_elems(Nil, List(tree)) match {
+ case (Nil, body) =>
+ (offset + XML.text_length(body), markup_trees)
+
+ case (elems, body) =>
+ val (end_offset, subtrees) = ((offset, Nil: List[Markup_Tree]) /: body)(make_trees)
+ val range = Text.Range(offset, end_offset)
+ val entry = Entry(range, elems.map(XML.Elem(_, Nil)), merge_disjoint(subtrees))
+ (end_offset, new Markup_Tree(Branches.empty, entry) :: markup_trees)
+ }
+ }
+
+ def from_XML(body: XML.Body): Markup_Tree =
+ merge_disjoint(((0, Nil: List[Markup_Tree]) /: body)(make_trees)._2)
}
-final class Markup_Tree private(branches: Markup_Tree.Branches.T)
+final class Markup_Tree private(private val 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))
- def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
-
override def toString =
branches.toList.map(_._2) match {
case Nil => "Empty"
@@ -162,15 +201,13 @@
List((Text.Info(root_range, root_info), overlapping(root_range).toStream)))
}
- def swing_tree(parent: DefaultMutableTreeNode)
- (swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
+ def swing_tree(parent: DefaultMutableTreeNode,
+ swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode)
{
for ((_, entry) <- branches) {
- var current = parent
val node = swing_node(Text.Info(entry.range, entry.markup))
- current.add(node)
- current = node
- entry.subtree.swing_tree(current)(swing_node)
+ entry.subtree.swing_tree(node, swing_node)
+ parent.add(node)
}
}
}
--- a/src/Pure/PIDE/protocol.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/PIDE/protocol.ML Fri Sep 21 11:47:16 2012 +0200
@@ -76,7 +76,9 @@
val _ =
Isabelle_Process.protocol_command "Document.invoke_scala"
- (fn [id, tag, res] => Invoke_Scala.fulfill_method id tag res);
+ (fn [id, tag, res] =>
+ Invoke_Scala.fulfill_method id tag res
+ handle exn => if Exn.is_interrupt exn then () else reraise exn);
end;
--- a/src/Pure/PIDE/xml.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/PIDE/xml.scala Fri Sep 21 11:47:16 2012 +0200
@@ -69,32 +69,31 @@
def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
- /* 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
+ /* traverse text */
- 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 traverse_text[A](body: Body)(a: A)(op: (A, String) => A): A =
+ {
+ def traverse(x: A, t: Tree): A =
+ t match {
+ case Elem(_, ts) => (x /: ts)(traverse)
+ case Text(s) => op(x, s)
}
-
- body.foreach(traverse)
- (text.toString, markup_tree.reverse_markup)
+ (a /: body)(traverse)
}
- 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
+ def text_length(body: Body): Int = traverse_text(body)(0) { case (n, s) => n + s.length }
+
+
+ /* text content */
+
+ def content(body: Body): String =
+ {
+ val text = new StringBuilder(text_length(body))
+ traverse_text(body)(()) { case (_, s) => text.append(s) }
+ text.toString
+ }
+
+ def content(tree: Tree): String = content(List(tree))
--- a/src/Pure/System/invoke_scala.ML Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/System/invoke_scala.ML Fri Sep 21 11:47:16 2012 +0200
@@ -52,6 +52,7 @@
| "1" => Exn.Res res
| "2" => Exn.Exn (ERROR res)
| "3" => Exn.Exn (Fail res)
+ | "4" => Exn.Exn Exn.Interrupt
| _ => raise Fail "Bad tag");
val promise =
Synchronized.change_result promises
--- a/src/Pure/System/invoke_scala.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/System/invoke_scala.scala Fri Sep 21 11:47:16 2012 +0200
@@ -49,6 +49,7 @@
val OK = Value("1")
val ERROR = Value("2")
val FAIL = Value("3")
+ val INTERRUPT = Value("4")
}
def method(name: String, arg: String): (Tag.Value, String) =
@@ -57,6 +58,7 @@
Exn.capture { f(arg) } match {
case Exn.Res(null) => (Tag.NULL, "")
case Exn.Res(res) => (Tag.OK, res)
+ case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
}
case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
--- a/src/Pure/System/session.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/System/session.scala Fri Sep 21 11:47:16 2012 +0200
@@ -172,6 +172,7 @@
previous: Document.Version,
version: Document.Version)
private case class Messages(msgs: List[Isabelle_Process.Message])
+ private case class Finished_Scala(id: String, tag: Invoke_Scala.Tag.Value, result: String)
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
@@ -179,6 +180,8 @@
var prune_next = System.currentTimeMillis() + prune_delay.ms
+ var futures = Map.empty[String, java.util.concurrent.Future[Unit]]
+
/* buffered prover messages */
@@ -338,14 +341,21 @@
}
case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
- Future.fork {
- val arg = XML.content(output.body)
- val (tag, res) = Invoke_Scala.method(name, arg)
- prover.get.invoke_scala(id, tag, res)
- }
+ futures += (id ->
+ default_thread_pool.submit(() =>
+ {
+ val arg = XML.content(output.body)
+ val (tag, result) = Invoke_Scala.method(name, arg)
+ this_actor ! Finished_Scala(id, tag, result)
+ }))
case Isabelle_Markup.Cancel_Scala(id) if output.is_protocol =>
- System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
+ futures.get(id) match {
+ case Some(future) =>
+ future.cancel(true)
+ this_actor ! Finished_Scala(id, Invoke_Scala.Tag.INTERRUPT, "")
+ case None =>
+ }
case _ if output.is_init =>
phase = Session.Ready
@@ -416,6 +426,12 @@
if prover.isDefined && global_state().is_assigned(change.previous) =>
handle_change(change)
+ case Finished_Scala(id, tag, result) if prover.isDefined =>
+ if (futures.isDefinedAt(id)) {
+ prover.get.invoke_scala(id, tag, result)
+ futures -= id
+ }
+
case bad if !bad.isInstanceOf[Change] =>
System.err.println("session_actor: ignoring bad message " + bad)
}
--- a/src/Pure/library.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Pure/library.scala Fri Sep 21 11:47:16 2012 +0200
@@ -199,4 +199,13 @@
val quote = Library.quote _
val commas = Library.commas _
val commas_quote = Library.commas_quote _
+
+
+ /* parallel tasks */
+
+ implicit def function_as_callable[A](f: () => A) =
+ new java.util.concurrent.Callable[A] { def call = f() }
+
+ val default_thread_pool =
+ scala.collection.parallel.ThreadPoolTasks.defaultThreadPool
}
--- a/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Fri Sep 21 11:47:16 2012 +0200
@@ -29,9 +29,16 @@
/* message priorities */
private val writeln_pri = 1
- private val warning_pri = 2
- private val legacy_pri = 3
- private val error_pri = 4
+ private val tracing_pri = 2
+ private val warning_pri = 3
+ private val legacy_pri = 4
+ private val error_pri = 5
+
+ private val message_pri = Map(
+ Isabelle_Markup.WRITELN -> writeln_pri, Isabelle_Markup.WRITELN_MESSAGE -> writeln_pri,
+ Isabelle_Markup.TRACING -> tracing_pri, Isabelle_Markup.TRACING_MESSAGE -> tracing_pri,
+ Isabelle_Markup.WARNING -> warning_pri, Isabelle_Markup.WARNING_MESSAGE -> warning_pri,
+ Isabelle_Markup.ERROR -> error_pri, Isabelle_Markup.ERROR_MESSAGE -> error_pri)
/* icons */
@@ -146,10 +153,8 @@
Some(Protocol.command_status_markup + Isabelle_Markup.WARNING + Isabelle_Markup.ERROR),
{
case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
- if (markup.name == Isabelle_Markup.WARNING)
- (status, pri max Isabelle_Rendering.warning_pri)
- else if (markup.name == Isabelle_Markup.ERROR)
- (status, pri max Isabelle_Rendering.error_pri)
+ if (markup.name == Isabelle_Markup.WARNING || markup.name == Isabelle_Markup.ERROR)
+ (status, pri max Isabelle_Rendering.message_pri(markup.name))
else (Protocol.command_status(status, markup), pri)
})
if (results.isEmpty) None
@@ -340,13 +345,10 @@
snapshot.cumulate_markup[Int](range, 0,
Some(Set(Isabelle_Markup.WRITELN, Isabelle_Markup.WARNING, Isabelle_Markup.ERROR)),
{
- case (pri, Text.Info(_, XML.Elem(Markup(name, _), _))) =>
- name match {
- case Isabelle_Markup.WRITELN => pri max Isabelle_Rendering.writeln_pri
- case Isabelle_Markup.WARNING => pri max Isabelle_Rendering.warning_pri
- case Isabelle_Markup.ERROR => pri max Isabelle_Rendering.error_pri
- case _ => pri
- }
+ case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+ if name == Isabelle_Markup.WRITELN ||
+ name == Isabelle_Markup.WARNING ||
+ name == Isabelle_Markup.ERROR => pri max Isabelle_Rendering.message_pri(name)
})
for {
Text.Info(r, pri) <- results
@@ -355,6 +357,37 @@
}
+ private val message_colors = Map(
+ Isabelle_Rendering.writeln_pri -> writeln_message_color,
+ Isabelle_Rendering.tracing_pri -> tracing_message_color,
+ Isabelle_Rendering.warning_pri -> warning_message_color,
+ Isabelle_Rendering.error_pri -> error_message_color)
+
+ def line_background(range: Text.Range): Option[(Color, Boolean)] =
+ {
+ val messages =
+ Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
+ Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
+ val results =
+ snapshot.cumulate_markup[Int](range, 0, Some(messages),
+ {
+ case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
+ if name == Isabelle_Markup.WRITELN_MESSAGE ||
+ name == Isabelle_Markup.TRACING_MESSAGE ||
+ name == Isabelle_Markup.WARNING_MESSAGE ||
+ name == Isabelle_Markup.ERROR_MESSAGE => pri max Isabelle_Rendering.message_pri(name)
+ })
+ val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
+
+ val is_separator = pri > 0 &&
+ snapshot.cumulate_markup[Boolean](range, false, Some(Set(Isabelle_Markup.SEPARATOR)),
+ {
+ case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.SEPARATOR, _), _))) => true
+ }).exists(_.info)
+
+ message_colors.get(pri).map((_, is_separator))
+ }
+
def background1(range: Text.Range): Stream[Text.Info[Color]] =
{
if (snapshot.is_outdated) Stream(Text.Info(range, outdated_color))
@@ -370,14 +403,6 @@
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, _), _))) =>
@@ -414,7 +439,6 @@
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 Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Fri Sep 21 11:47:16 2012 +0200
@@ -198,7 +198,7 @@
val root = data.root
for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
snapshot.state.command_state(snapshot.version, command).markup
- .swing_tree(root)((info: Text.Info[List[XML.Elem]]) =>
+ .swing_tree(root, (info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
--- a/src/Tools/jEdit/src/output2_dockable.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala Fri Sep 21 11:47:16 2012 +0200
@@ -77,7 +77,7 @@
else current_output
if (new_output != current_output)
- pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
+ pretty_text_area.update(new_snapshot, Library.separate(Pretty.Separator, new_output))
current_snapshot = new_snapshot
current_state = new_state
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Sep 21 11:47:16 2012 +0200
@@ -20,7 +20,15 @@
object Pretty_Text_Area
{
- def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
+ private def text_rendering(base_snapshot: Document.Snapshot, formatted_body: XML.Body):
+ (String, Isabelle_Rendering) =
+ {
+ val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
+ val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
+ (text, rendering)
+ }
+
+ private def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
: (String, Document.State) =
{
val command = Command.rich_text(Document.new_id(), formatted_body)
@@ -51,54 +59,52 @@
Swing_Thread.require()
- 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 var current_rendering: Isabelle_Rendering =
+ Pretty_Text_Area.text_rendering(current_base_snapshot, Nil)._2
+ private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
- 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()
{
Swing_Thread.require()
val font = new Font(current_font_family, Font.PLAIN, current_font_size)
-
getPainter.setFont(font)
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
- current_font_metrics = painter.getFontMetrics(font)
- current_margin = (getWidth / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
+ val font_metrics = getPainter.getFontMetrics(font)
+ val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
+
+ val base_snapshot = current_base_snapshot
+ val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
- val (text, rendering) = text_rendering()
- current_rendering = rendering
+ future_rendering.map(_.cancel(true))
+ future_rendering = Some(default_thread_pool.submit(() =>
+ {
+ val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+ Simple_Thread.interrupted_exception()
- try {
- getBuffer.beginCompoundEdit
- getBuffer.setReadOnly(false)
- setText(text)
- setCaretPosition(0)
- getBuffer.setReadOnly(true)
- }
- finally {
- getBuffer.endCompoundEdit
- }
+ Swing_Thread.later {
+ current_rendering = rendering
+
+ try {
+ getBuffer.beginCompoundEdit
+ getBuffer.setReadOnly(false)
+ setText(text)
+ setCaretPosition(0)
+ getBuffer.setReadOnly(true)
+ }
+ finally {
+ getBuffer.endCompoundEdit
+ }
+ }
+ }))
}
def resize(font_family: String, font_size: Int)
@@ -141,8 +147,14 @@
/* init */
+ override def isCaretVisible: Boolean = false
+
+ getPainter.setStructureHighlightEnabled(false)
+ getPainter.setLineHighlightEnabled(false)
+
getBuffer.setTokenMarker(new Token_Markup.Marker(true, None))
getBuffer.setReadOnly(true)
+
rich_text_area.activate()
}
--- a/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 11:44:55 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Fri Sep 21 11:47:16 2012 +0200
@@ -86,7 +86,7 @@
}
}
- private def robust_rendering(body: Isabelle_Rendering => Unit)
+ def robust_rendering(body: Isabelle_Rendering => Unit)
{
robust_body(()) { body(painter_rendering) }
}
@@ -198,6 +198,14 @@
if (physical_lines(i) != -1) {
val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+ // line background color
+ for { (color, separator) <- rendering.line_background(line_range) }
+ {
+ gfx.setColor(color)
+ val sep = if (separator) (2 min (line_height / 2)) else 0
+ gfx.fillRect(0, y + i * line_height, text_area.getWidth, line_height - sep)
+ }
+
// background color (1)
for {
Text.Info(range, color) <- rendering.background1(line_range)