# HG changeset patch # User wenzelm # Date 1326398297 -3600 # Node ID 805de058722bbb49bc762fc35eb55f638a89ca9d # Parent d4558296bdc3dff2eb9ce03d0306d370dc023896 added cat_lines convenience; diff -r d4558296bdc3 -r 805de058722b src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Jan 12 20:57:37 2012 +0100 +++ b/src/Pure/System/session.scala Thu Jan 12 20:58:17 2012 +0100 @@ -120,7 +120,7 @@ def current_syntax(): Outer_Syntax = syntax @volatile private var reverse_syslog = List[XML.Elem]() - def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n") + def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString)) @volatile private var _phase: Session.Phase = Session.Inactive private def phase_=(new_phase: Session.Phase) diff -r d4558296bdc3 -r 805de058722b src/Pure/library.scala --- a/src/Pure/library.scala Thu Jan 12 20:57:37 2012 +0100 +++ b/src/Pure/library.scala Thu Jan 12 20:58:17 2012 +0100 @@ -98,6 +98,8 @@ /* strings */ + def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n") + def quote(s: String): String = "\"" + s + "\"" def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ") def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"") @@ -208,7 +210,7 @@ val space_explode = Library.space_explode _ val split_lines = Library.split_lines _ - + val cat_lines = Library.cat_lines _ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ diff -r d4558296bdc3 -r 805de058722b src/Tools/jEdit/src/isabelle_rendering.scala --- a/src/Tools/jEdit/src/isabelle_rendering.scala Thu Jan 12 20:57:37 2012 +0100 +++ b/src/Tools/jEdit/src/isabelle_rendering.scala Thu Jan 12 20:58:17 2012 +0100 @@ -102,7 +102,7 @@ Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))) }) match { case Text.Info(_, msgs) #:: _ if !msgs.isEmpty => - Some(msgs.iterator.map(_._2).mkString("\n")) + Some(cat_lines(msgs.iterator.map(_._2))) case _ => None } @@ -256,7 +256,7 @@ (tip1 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) ::: (tip2 match { case Text.Info(_, Some(text)) #:: _ => List(text) case _ => Nil }) - if (tips.isEmpty) None else Some(tips.mkString("\n")) + if (tips.isEmpty) None else Some(cat_lines(tips)) } private val subexp_include =