# HG changeset patch
# User wenzelm
# Date 1273182740 -7200
# Node ID 379f5b1e7f91772e8d527c52d3331b3cbdbf5bb7
# Parent  321d392ab12e0a798143ff0f9b318ca962751dbf
replaced slightly odd fbreak markup by plain "\n", which also coincides with regular linebreaks produced outside the ML pretty engine;

diff -r 321d392ab12e -r 379f5b1e7f91 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Thu May 06 23:32:29 2010 +0200
+++ b/src/Pure/General/markup.scala	Thu May 06 23:52:20 2010 +0200
@@ -64,7 +64,6 @@
   val BLOCK = "block"
   val WIDTH = "width"
   val BREAK = "break"
-  val FBREAK = "fbreak"
 
 
   /* hidden text */
diff -r 321d392ab12e -r 379f5b1e7f91 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu May 06 23:32:29 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu May 06 23:52:20 2010 +0200
@@ -309,7 +309,7 @@
           Buffer.add bg #> Buffer.markup (Markup.block indent) (fold out prts) #> Buffer.add en
       | out (String (s, _)) = Buffer.add s
       | out (Break (false, wd)) = Buffer.markup (Markup.break wd) (Buffer.add (output_spaces wd))
-      | out (Break (true, _)) = Buffer.markup Markup.fbreak (Buffer.add (output_spaces 1));
+      | out (Break (true, _)) = Buffer.add (Output.output "\n");
   in out prt Buffer.empty end;
 
 (*unformatted output*)
diff -r 321d392ab12e -r 379f5b1e7f91 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu May 06 23:32:29 2010 +0200
+++ b/src/Pure/General/pretty.scala	Thu May 06 23:52:20 2010 +0200
@@ -39,16 +39,7 @@
       }
   }
 
-  object FBreak
-  {
-    def apply(): XML.Tree = XML.Elem(Markup.FBREAK, Nil, List(XML.Text(" ")))
-
-    def unapply(tree: XML.Tree): Boolean =
-      tree match {
-        case XML.Elem(Markup.FBREAK, Nil, _) => true
-        case _ => false
-      }
-  }
+  val FBreak = XML.Text("\n")
 
 
   /* formatted output */
@@ -64,7 +55,7 @@
   private def breakdist(trees: List[XML.Tree], after: Int): Int =
     trees match {
       case Break(_) :: _ => 0
-      case FBreak() :: _ => 0
+      case FBreak :: _ => 0
       case XML.Elem(_, _, body) :: ts =>
         (0 /: body)(_ + XML.content_length(_)) + breakdist(ts, after)
       case XML.Text(s) :: ts => s.length + breakdist(ts, after)
@@ -74,11 +65,19 @@
   private def forcenext(trees: List[XML.Tree]): List[XML.Tree] =
     trees match {
       case Nil => Nil
-      case FBreak() :: _ => trees
-      case Break(_) :: ts => FBreak() :: ts
+      case FBreak :: _ => trees
+      case Break(_) :: ts => FBreak :: ts
       case t :: ts => t :: forcenext(ts)
     }
 
+  private def standard(tree: XML.Tree): List[XML.Tree] =
+    tree match {
+      case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard)))
+      case XML.Text(text) =>
+        Library.separate(FBreak,
+          Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
+    }
+
   def string_of(input: List[XML.Tree], margin: Int = 76): String =
   {
     val breakgain = margin / 20
@@ -102,11 +101,11 @@
           if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
             format(ts, blockin, after, text.blanks(wd))
           else format(ts, blockin, after, text.newline.blanks(blockin))
-        case FBreak() :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
+        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
 
         case XML.Elem(_, _, body) :: ts => format(body ::: ts, blockin, after, text)
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
       }
-    format(input, 0, 0, Text()).content
+    format(input.flatMap(standard), 0, 0, Text()).content
   }
 }
diff -r 321d392ab12e -r 379f5b1e7f91 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 06 23:32:29 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Thu May 06 23:52:20 2010 +0200
@@ -115,8 +115,6 @@
             [Pgml.Box {orient = NONE, indent = Properties.get_int atts Markup.indentN, content = content}]
           else if name = Markup.breakN then
             [Pgml.Break {mandatory = NONE, indent = Properties.get_int atts Markup.widthN}]
-          else if name = Markup.fbreakN then
-            [Pgml.Break {mandatory = SOME true, indent = NONE}]
           else content
         end
   | pgml_terms (XML.Text text) = map (Pgml.Raw o Pgml.atom_to_xml) (pgml_syms text);