1.1 --- a/src/Pure/General/markup.scala	Thu May 06 23:32:29 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Thu May 06 23:52:20 2010 +0200
     1.3 @@ -64,7 +64,6 @@
     1.4    val BLOCK = "block"
     1.5    val WIDTH = "width"
     1.6    val BREAK = "break"
     1.7 -  val FBREAK = "fbreak"
     1.8  
     1.9  
    1.10    /* hidden text */

     2.1 --- a/src/Pure/General/pretty.ML	Thu May 06 23:32:29 2010 +0200
     2.2 +++ b/src/Pure/General/pretty.ML	Thu May 06 23:52:20 2010 +0200
     2.3 @@ -309,7 +309,7 @@
     2.4            Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
     2.5        | out (String (s, _)) = Buffer.add s
     2.6        | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
     2.7 -      | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
     2.8 +      | out (Break (true, _)) = Buffer.add (Output.output "\n");
     2.9    in out prt Buffer.empty end;
    2.10  
    2.11  (*unformatted output*)

     3.1 --- a/src/Pure/General/pretty.scala	Thu May 06 23:32:29 2010 +0200
     3.2 +++ b/src/Pure/General/pretty.scala	Thu May 06 23:52:20 2010 +0200
     3.3 @@ -39,16 +39,7 @@
     3.4        }
     3.5    }
     3.6  
     3.7 -  object FBreak
     3.8 -  {
     3.9 -    def apply(): XML.Tree = XML.Elem(Markup.FBREAK, Nil, List(XML.Text(" ")))
    3.10 -
    3.11 -    def unapply(tree: XML.Tree): Boolean =
    3.12 -      tree match {
    3.13 -        case XML.Elem(Markup.FBREAK, Nil, _) => true
    3.14 -        case _ => false
    3.15 -      }
    3.16 -  }
    3.17 +  val FBreak = XML.Text("\n")
    3.18  
    3.19  
    3.20    /* formatted output */
    3.21 @@ -64,7 +55,7 @@
    3.22    private def breakdist(trees: List[XML.Tree], after: Int): Int =
    3.23      trees match {
    3.24        case Break(_) :: _ => 0
    3.25 -      case FBreak() :: _ => 0
    3.26 +      case FBreak :: _ => 0
    3.27        case XML.Elem(_, _, body) :: ts =>
    3.28          (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
    3.29        case XML.Text(s) :: ts => s.length + breakdist(ts, after)
    3.30 @@ -74,11 +65,19 @@
    3.31    private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
    3.32      trees match {
    3.33        case Nil => Nil
    3.34 -      case FBreak() :: _ => trees
    3.35 -      case Break(_) :: ts => FBreak() :: ts
    3.36 +      case FBreak :: _ => trees
    3.37 +      case Break(_) :: ts => FBreak :: ts
    3.38        case t :: ts => t :: forcenext(ts)
    3.39      }
    3.40  
    3.41 +  private def standard(tree: XML.Tree): List[XML.Tree] =
    3.42 +    tree match {
    3.43 +      case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard)))
    3.44 +      case XML.Text(text) =>
    3.45 +        Library.separate(FBreak,
    3.46 +          Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
    3.47 +    }
    3.48 +
    3.49    def string_of(input: List[XML.Tree], margin: Int = 76): String =
    3.50    {
    3.51      val breakgain = margin / 20
    3.52 @@ -102,11 +101,11 @@
    3.53            if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
    3.54              format(ts, blockin, after, text.blanks(wd))
    3.55            else format(ts, blockin, after, text.newline.blanks(blockin))
    3.56 -        case FBreak() :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
    3.57 +        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
    3.58  
    3.59          case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text)
    3.60          case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
    3.61        }
    3.62 -    format(input, 0, 0, Text()).content
    3.63 +    format(input.flatMap(standard), 0, 0, Text()).content
    3.64    }
    3.65  }

     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 06 23:32:29 2010 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 06 23:52:20 2010 +0200
     4.3 @@ -115,8 +115,6 @@
     4.4              [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
     4.5            else if name = Markup.breakN then
     4.6              [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
     4.7 -          else if name = Markup.fbreakN then
     4.8 -            [Pgml.Break {mandatory = SOME true, indent = NONE}]
     4.9            else content
    4.10          end
    4.11    | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);