# HG changeset patch
# User wenzelm
# Date 1459514334 -7200
# Node ID 70b9c7d4ed7fd5034e4c74802122fa79a38e6159
# Parent  0371c369ab1de7206d1a14fddf55c190bc21769c
more robust pretty printing: permissive treatment of bad values;

diff -r 0371c369ab1d -r 70b9c7d4ed7f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Apr 01 11:45:04 2016 +0200
+++ b/src/Pure/General/pretty.ML	Fri Apr 01 14:38:54 2016 +0200
@@ -110,6 +110,8 @@
 
 (** printing items: compound phrases, strings, and breaks **)
 
+val force_nat = Integer.max 0;
+
 abstype T =
     Block of (Output.output * Output.output) * bool * int * T list * int
       (*markup output, consistent, indentation, body, length*)
@@ -123,6 +125,7 @@
 
 fun make_block {markup, consistent, indent} body =
   let
+    val indent' = force_nat indent;
     fun body_length prts len =
       let
         val (line, rest) = take_prefix (fn Break (true, _, _) => false | _ => true) prts;
@@ -130,10 +133,10 @@
       in
         (case rest of
           Break (true, _, ind) :: rest' =>
-            body_length (Break (false, indent + ind, 0) :: rest') len'
+            body_length (Break (false, indent' + ind, 0) :: rest') len'
         | [] => len')
       end;
-  in Block (markup, consistent, indent, body, body_length body 0) end;
+  in Block (markup, consistent, indent', body, body_length body 0) end;
 
 fun markup_block {markup, consistent, indent} es =
   make_block {markup = Markup.output markup, consistent = consistent, indent = indent} es;
@@ -142,10 +145,10 @@
 
 (** derived operations to create formatting expressions **)
 
-val str = Str o Output.output_width;
+val str = Output.output_width ##> force_nat #> Str;
 
-fun brk wd = Break (false, wd, 0);
-fun brk_indent wd ind = Break (false, wd, ind);
+fun brk wd = Break (false, force_nat wd, 0);
+fun brk_indent wd ind = Break (false, force_nat wd, ind);
 val fbrk = Break (true, 1, 0);
 
 fun breaks prts = Library.separate (brk 1) prts;
@@ -392,7 +395,7 @@
         (map from_ML prts)
   | from_ML (ML_Pretty.Break (force, wd, ind)) =
       Break (force, FixedInt.toInt wd, FixedInt.toInt ind)
-  | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt len);
+  | from_ML (ML_Pretty.String (s, len)) = Str (s, FixedInt.toInt (force_nat len));
 
 val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
 val from_polyml = ML_Pretty.from_polyml #> from_ML;
diff -r 0371c369ab1d -r 70b9c7d4ed7f src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Fri Apr 01 11:45:04 2016 +0200
+++ b/src/Pure/General/pretty.scala	Fri Apr 01 14:38:54 2016 +0200
@@ -64,6 +64,8 @@
       indent: Int,
       body: List[Tree]): Tree =
   {
+    val indent1 = force_nat(indent)
+
     def body_length(prts: List[Tree], len: Double): Double =
     {
       val (line, rest) =
@@ -71,16 +73,18 @@
       val len1 = ((0.0 /: line) { case (l, t) => l + t.length }) max len
       rest match {
         case Break(true, _, ind) :: rest1 =>
-          body_length(Break(false, indent + ind, 0) :: rest1, len1)
+          body_length(Break(false, indent1 + ind, 0) :: rest1, len1)
         case Nil => len1
       }
     }
-    Block(markup, consistent, indent, body, body_length(body, 0.0))
+    Block(markup, consistent, indent1, body, body_length(body, 0.0))
   }
 
 
   /* formatted output */
 
+  private def force_nat(i: Int): Int = i max 0
+
   private sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
   {
     def newline: Text = copy(tx = fbrk :: tx, pos = 0.0, nl = nl + 1)
@@ -125,7 +129,7 @@
             case Markup.Block(consistent, indent) =>
               List(make_block(None, consistent, indent, make_tree(body)))
             case Markup.Break(width, indent) =>
-              List(Break(false, width, indent))
+              List(Break(false, force_nat(width), force_nat(indent)))
             case Markup(Markup.ITEM, _) =>
               List(make_block(None, false, 2,
                 make_tree(XML.elem(Markup.BULLET, space) :: space ::: body)))