tuned;
authorwenzelm
Tue Mar 05 18:44:02 2019 +0100 (3 months ago ago)
changeset 700483fd9298dd200
parent 70047 01732226987a
child 70049 ab993a273def
tuned;
src/Pure/General/pretty.scala
src/Pure/General/rdf.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/xml.scala
     1.1 --- a/src/Pure/General/pretty.scala	Tue Mar 05 16:40:12 2019 +0100
     1.2 +++ b/src/Pure/General/pretty.scala	Tue Mar 05 18:44:02 2019 +0100
     1.3 @@ -25,7 +25,7 @@
     1.4    def brk(width: Int, indent: Int = 0): XML.Tree =
     1.5      XML.Elem(Markup.Break(width, indent), spaces(width))
     1.6  
     1.7 -  val fbrk: XML.Tree = XML.Text("\n")
     1.8 +  val fbrk: XML.Tree = XML.newline
     1.9    def fbreaks(ts: List[XML.Tree]): XML.Body = Library.separate(fbrk, ts)
    1.10  
    1.11    val Separator: XML.Body = List(XML.elem(Markup.SEPARATOR, space), fbrk)
     2.1 --- a/src/Pure/General/rdf.scala	Tue Mar 05 16:40:12 2019 +0100
     2.2 +++ b/src/Pure/General/rdf.scala	Tue Mar 05 18:44:02 2019 +0100
     2.3 @@ -39,8 +39,7 @@
     2.4    def triples(args: List[Triple]): XML.Body =
     2.5      args.groupBy(_.subject).toList.map(
     2.6        { case (subject, ts) =>
     2.7 -          val nl = XML.Text("\n")
     2.8 -          val body = nl :: ts.flatMap(t => List(t.property, nl))
     2.9 +          val body = XML.newline :: ts.flatMap(t => List(t.property, XML.newline))
    2.10            description(subject, body)
    2.11        })
    2.12  
     3.1 --- a/src/Pure/PIDE/prover.scala	Tue Mar 05 16:40:12 2019 +0100
     3.2 +++ b/src/Pure/PIDE/prover.scala	Tue Mar 05 18:44:02 2019 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4      override def toString: String =
     3.5        XML.Elem(Markup(Markup.PROVER_COMMAND, List((Markup.NAME, name))),
     3.6          args.map(s =>
     3.7 -          List(XML.Text("\n"), XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
     3.8 +          List(XML.newline, XML.elem(Markup.PROVER_ARG, YXML.parse_body(s)))).flatten).toString
     3.9    }
    3.10  
    3.11    class Output(val message: XML.Elem) extends Message
     4.1 --- a/src/Pure/PIDE/xml.scala	Tue Mar 05 16:40:12 2019 +0100
     4.2 +++ b/src/Pure/PIDE/xml.scala	Tue Mar 05 18:44:02 2019 +0100
     4.3 @@ -34,6 +34,8 @@
     4.4    def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
     4.5    def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
     4.6  
     4.7 +  val newline: Text = Text("\n")
     4.8 +
     4.9  
    4.10    /* name space */
    4.11