--- a/src/Pure/General/pretty.scala Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/General/pretty.scala Tue Sep 18 14:51:12 2012 +0200
@@ -146,7 +146,7 @@
def string_of(input: XML.Body, margin: Int = margin_default,
metric: String => Double = metric_default): String =
- XML.content(formatted(input, margin, metric)).mkString
+ XML.content(formatted(input, margin, metric))
/* unformatted output */
@@ -164,5 +164,5 @@
input.flatMap(standard_format).flatMap(fmt)
}
- def str_of(input: XML.Body): String = XML.content(unformatted(input)).mkString
+ def str_of(input: XML.Body): String = XML.content(unformatted(input))
}
--- a/src/Pure/PIDE/command.scala Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/PIDE/command.scala Tue Sep 18 14:51:12 2012 +0200
@@ -109,8 +109,7 @@
def rich_text(id: Document.Command_ID, body: XML.Body): Command =
{
- val text = XML.content(body).mkString
- val markup = Markup_Tree.empty // FIXME
+ val (text, markup) = XML.content_markup(body)
unparsed(id, text, markup)
}
--- a/src/Pure/PIDE/xml.scala Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/PIDE/xml.scala Tue Sep 18 14:51:12 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,33 @@
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
+ // FIXME proper order!?
+ 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)
+ }
+
+ 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 Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Pure/System/session.scala Tue Sep 18 14:51:12 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/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Tue Sep 18 14:51:12 2012 +0200
@@ -20,7 +20,7 @@
object Pretty_Text_Area
{
- def document_state(formatted_body: XML.Body): Document.State =
+ def document_state(formatted_body: XML.Body): (String, Document.State) =
{
val command = Command.rich_text(Document.new_id(), formatted_body)
val node_name = command.node_name
@@ -39,7 +39,7 @@
.define_version(version1, state0.the_assignment(version0))
.assign(version1.id, List(command.id -> Some(Document.new_id())))._2
- state1
+ (command.source, state1)
}
}
@@ -52,19 +52,22 @@
private var current_font_size: Int = 12
private var current_margin: Int = 0
private var current_body: XML.Body = Nil
- private var current_rendering: Isabelle_Rendering = make_rendering()
+ private var current_rendering: Isabelle_Rendering = text_rendering()._2
- private def make_rendering(): Isabelle_Rendering =
+ val text_area = new JEditEmbeddedTextArea
+ 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))
- Isabelle_Rendering(Pretty_Text_Area.document_state(body).snapshot(), Isabelle.options.value)
- }
+ val (text, state) = Pretty_Text_Area.document_state(body)
+ val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
- val text_area = new JEditEmbeddedTextArea
- val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
+ (text, rendering)
+ }
def refresh()
{
@@ -80,8 +83,8 @@
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 {
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Tue Sep 18 13:36:28 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Tue Sep 18 14:51:12 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)
}