# HG changeset patch
# User wenzelm
# Date 1282477944 -7200
# Node ID d163f0f28e8cd985f9bddd133b43f72fe3c881c6
# Parent  0fe2c01ef7da40763cd8e876e94b99f20c687c70
tuned signatures;

diff -r 0fe2c01ef7da -r d163f0f28e8c src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sun Aug 22 12:54:12 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sun Aug 22 13:52:24 2010 +0200
@@ -14,12 +14,14 @@
 {
   /* markup trees with physical blocks and breaks */
 
+  def block(body: XML.Body): XML.Tree = Block(2, body)
+
   object Block
   {
-    def apply(i: Int, body: List[XML.Tree]): XML.Tree =
+    def apply(i: Int, body: XML.Body): XML.Tree =
       XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body)
 
-    def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
+    def unapply(tree: XML.Tree): Option[(Int, XML.Body)] =
       tree match {
         case XML.Elem(
           Markup(Markup.BLOCK, List((Markup.INDENT, Markup.Int(i)))), body) => Some((i, body))
@@ -45,7 +47,7 @@
 
   /* formatted output */
 
-  private def standard_format(tree: XML.Tree): List[XML.Tree] =
+  private def standard_format(tree: XML.Tree): XML.Body =
     tree match {
       case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
       case XML.Text(text) =>
@@ -53,12 +55,12 @@
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
     }
 
-  case class Text(tx: List[XML.Tree] = Nil, val pos: Double = 0.0, val nl: Int = 0)
+  case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
   {
     def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
     def string(s: String, len: Double): Text = copy(tx = XML.Text(s) :: tx, pos = pos + len)
     def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
-    def content: List[XML.Tree] = tx.reverse
+    def content: XML.Body = tx.reverse
   }
 
   private val margin_default = 76
@@ -71,8 +73,8 @@
       ((s: String) => if (s == "\n") 1.0 else metrics.stringWidth(s) / unit)
     }
 
-  def formatted(input: List[XML.Tree], margin: Int = margin_default,
-    metric: String => Double = metric_default): List[XML.Tree] =
+  def formatted(input: XML.Body, margin: Int = margin_default,
+    metric: String => Double = metric_default): XML.Body =
   {
     val breakgain = margin / 20
     val emergencypos = margin / 2
@@ -83,7 +85,7 @@
         case XML.Text(s) => metric(s)
       }
 
-    def breakdist(trees: List[XML.Tree], after: Double): Double =
+    def breakdist(trees: XML.Body, after: Double): Double =
       trees match {
         case Break(_) :: _ => 0.0
         case FBreak :: _ => 0.0
@@ -91,7 +93,7 @@
         case Nil => after
       }
 
-    def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
+    def forcenext(trees: XML.Body): XML.Body =
       trees match {
         case Nil => Nil
         case FBreak :: _ => trees
@@ -99,7 +101,7 @@
         case t :: ts => t :: forcenext(ts)
       }
 
-    def format(trees: List[XML.Tree], blockin: Double, after: Double, text: Text): Text =
+    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
@@ -129,16 +131,16 @@
     format(input.flatMap(standard_format), 0.0, 0.0, Text()).content
   }
 
-  def string_of(input: List[XML.Tree], margin: Int = margin_default,
+  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
 
 
   /* unformatted output */
 
-  def unformatted(input: List[XML.Tree]): List[XML.Tree] =
+  def unformatted(input: XML.Body): XML.Body =
   {
-    def fmt(tree: XML.Tree): List[XML.Tree] =
+    def fmt(tree: XML.Tree): XML.Body =
       tree match {
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
@@ -149,6 +151,6 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: List[XML.Tree]): String =
+  def str_of(input: XML.Body): String =
     unformatted(input).iterator.flatMap(XML.content).mkString
 }
diff -r 0fe2c01ef7da -r d163f0f28e8c src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Aug 22 12:54:12 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sun Aug 22 13:52:24 2010 +0200
@@ -95,7 +95,7 @@
 
   private val xml_cache = new XML.Cache(131071)
 
-  private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
+  private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {
     if (pid.isEmpty && kind == Markup.INIT)
       pid = props.find(_._1 == Markup.PID).map(_._1)
@@ -257,7 +257,7 @@
       val default_buffer = new Array[Byte](65536)
       var c = -1
 
-      def read_chunk(): List[XML.Tree] =
+      def read_chunk(): XML.Body =
       {
         //{{{
         // chunk size
diff -r 0fe2c01ef7da -r d163f0f28e8c src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Aug 22 12:54:12 2010 +0200
+++ b/src/Pure/Thy/html.scala	Sun Aug 22 13:52:24 2010 +0200
@@ -41,7 +41,7 @@
 
   // document markup
 
-  def span(cls: String, body: List[XML.Tree]): XML.Elem =
+  def span(cls: String, body: XML.Body): XML.Elem =
     XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
 
   def hidden(txt: String): XML.Elem =
@@ -50,9 +50,9 @@
   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
 
-  def spans(input: XML.Tree, original_data: Boolean = false): List[XML.Tree] =
+  def spans(input: XML.Tree, original_data: Boolean = false): XML.Body =
   {
-    def html_spans(tree: XML.Tree): List[XML.Tree] =
+    def html_spans(tree: XML.Tree): XML.Body =
       tree match {
         case XML.Elem(Markup(name, _), ts) =>
           if (original_data)
diff -r 0fe2c01ef7da -r d163f0f28e8c src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Sun Aug 22 12:54:12 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Sun Aug 22 13:52:24 2010 +0200
@@ -116,7 +116,7 @@
   /* internal messages */
 
   private case class Resize(font_family: String, font_size: Int)
-  private case class Render(body: List[XML.Tree])
+  private case class Render(body: XML.Body)
   private case object Refresh
 
   private val main_actor = actor {
@@ -127,7 +127,7 @@
     var current_font_family = ""
     var current_font_size: Int = 0
     var current_margin: Int = 0
-    var current_body: List[XML.Tree] = Nil
+    var current_body: XML.Body = Nil
 
     def resize(font_family: String, font_size: Int)
     {
@@ -152,7 +152,7 @@
 
     def refresh() { render(current_body) }
 
-    def render(body: List[XML.Tree])
+    def render(body: XML.Body)
     {
       current_body = body
       val html_body =
@@ -190,5 +190,5 @@
 
   def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   def refresh() { main_actor ! Refresh }
-  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+  def render(body: XML.Body) { main_actor ! Render(body) }
 }