# HG changeset patch # User wenzelm # Date 1348220836 -7200 # Node ID f59475e6589f47982ceacb22dfa223dda8ffce60 # Parent 02eb071529986df6594d1fe3735d6c07c8a7e943# Parent 8ae5804c4ba81cc0366c90206229b9f73ff55fd3 merged diff -r 02eb07152998 -r f59475e6589f src/Pure/Concurrent/simple_thread.scala --- 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 = diff -r 02eb07152998 -r f59475e6589f src/Pure/General/pretty.scala --- 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)) diff -r 02eb07152998 -r f59475e6589f src/Pure/PIDE/command.scala --- 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) } diff -r 02eb07152998 -r f59475e6589f src/Pure/PIDE/isabelle_markup.scala --- 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 */ diff -r 02eb07152998 -r f59475e6589f src/Pure/PIDE/markup_tree.scala --- 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) } } } diff -r 02eb07152998 -r f59475e6589f src/Pure/PIDE/protocol.ML --- 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; diff -r 02eb07152998 -r f59475e6589f src/Pure/PIDE/xml.scala --- 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)) diff -r 02eb07152998 -r f59475e6589f src/Pure/System/invoke_scala.ML --- 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 diff -r 02eb07152998 -r f59475e6589f src/Pure/System/invoke_scala.scala --- 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)) diff -r 02eb07152998 -r f59475e6589f src/Pure/System/session.scala --- 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) } diff -r 02eb07152998 -r f59475e6589f src/Pure/library.scala --- 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 } diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/etc/options diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/src/isabelle_rendering.scala --- 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, diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/src/isabelle_sidekick.scala --- 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', ' ') diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/src/output2_dockable.scala --- 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 diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/src/pretty_text_area.scala --- 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() } diff -r 02eb07152998 -r f59475e6589f src/Tools/jEdit/src/rich_text_area.scala --- 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)