basic support for symbolic pretty printing;
authorwenzelm
Thu May 06 16:27:47 2010 +0200 (2010-05-06)
changeset 3668341a1210519fd
parent 36682 3f989067f87d
child 36684 943f1ca7b375
basic support for symbolic pretty printing;
tuned;
src/Pure/General/markup.scala
src/Pure/General/position.scala
src/Pure/General/pretty.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/General/markup.scala	Thu May 06 15:04:37 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Thu May 06 16:27:47 2010 +0200
     1.3 @@ -9,6 +9,24 @@
     1.4  
     1.5  object Markup
     1.6  {
     1.7 +  /* property values */
     1.8 +
     1.9 +  def get_string(name: String, props: List[(String, String)]): Option[String] =
    1.10 +    props.find(p => p._1 == name).map(_._2)
    1.11 +
    1.12 +  def parse_int(s: String): Option[Int] =
    1.13 +    try { Some(Integer.parseInt(s)) }
    1.14 +    catch { case _: NumberFormatException => None }
    1.15 +
    1.16 +  def get_int(name: String, props: List[(String, String)]): Option[Int] =
    1.17 +  {
    1.18 +    get_string(name, props) match {
    1.19 +      case None => None
    1.20 +      case Some(value) => parse_int(value)
    1.21 +    }
    1.22 +  }
    1.23 +
    1.24 +
    1.25    /* name */
    1.26  
    1.27    val NAME = "name"
    1.28 @@ -40,6 +58,15 @@
    1.29    val LOCATION = "location"
    1.30  
    1.31  
    1.32 +  /* pretty printing */
    1.33 +
    1.34 +  val INDENT = "indent"
    1.35 +  val BLOCK = "block"
    1.36 +  val WIDTH = "width"
    1.37 +  val BREAK = "break"
    1.38 +  val FBREAK = "fbreak"
    1.39 +
    1.40 +
    1.41    /* hidden text */
    1.42  
    1.43    val HIDDEN = "hidden"
     2.1 --- a/src/Pure/General/position.scala	Thu May 06 15:04:37 2010 +0200
     2.2 +++ b/src/Pure/General/position.scala	Thu May 06 16:27:47 2010 +0200
     2.3 @@ -11,27 +11,14 @@
     2.4  {
     2.5    type T = List[(String, String)]
     2.6  
     2.7 -  private def get_string(name: String, pos: T): Option[String] =
     2.8 -    pos.find(p => p._1 == name).map(_._2)
     2.9 -
    2.10 -  private def get_int(name: String, pos: T): Option[Int] =
    2.11 -  {
    2.12 -    get_string(name, pos) match {
    2.13 -      case None => None
    2.14 -      case Some(value) =>
    2.15 -        try { Some(Integer.parseInt(value)) }
    2.16 -        catch { case _: NumberFormatException => None }
    2.17 -    }
    2.18 -  }
    2.19 -
    2.20 -  def get_line(pos: T): Option[Int] = get_int(Markup.LINE, pos)
    2.21 -  def get_column(pos: T): Option[Int] = get_int(Markup.COLUMN, pos)
    2.22 -  def get_offset(pos: T): Option[Int] = get_int(Markup.OFFSET, pos)
    2.23 -  def get_end_line(pos: T): Option[Int] = get_int(Markup.END_LINE, pos)
    2.24 -  def get_end_column(pos: T): Option[Int] = get_int(Markup.END_COLUMN, pos)
    2.25 -  def get_end_offset(pos: T): Option[Int] = get_int(Markup.END_OFFSET, pos)
    2.26 -  def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos)
    2.27 -  def get_id(pos: T): Option[String] = get_string(Markup.ID, pos)
    2.28 +  def get_line(pos: T): Option[Int] = Markup.get_int(Markup.LINE, pos)
    2.29 +  def get_column(pos: T): Option[Int] = Markup.get_int(Markup.COLUMN, pos)
    2.30 +  def get_offset(pos: T): Option[Int] = Markup.get_int(Markup.OFFSET, pos)
    2.31 +  def get_end_line(pos: T): Option[Int] = Markup.get_int(Markup.END_LINE, pos)
    2.32 +  def get_end_column(pos: T): Option[Int] = Markup.get_int(Markup.END_COLUMN, pos)
    2.33 +  def get_end_offset(pos: T): Option[Int] = Markup.get_int(Markup.END_OFFSET, pos)
    2.34 +  def get_file(pos: T): Option[String] = Markup.get_string(Markup.FILE, pos)
    2.35 +  def get_id(pos: T): Option[String] = Markup.get_string(Markup.ID, pos)
    2.36  
    2.37    def get_range(pos: T): Option[(Int, Int)] =
    2.38      (get_offset(pos), get_end_offset(pos)) match {
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/pretty.scala	Thu May 06 16:27:47 2010 +0200
     3.3 @@ -0,0 +1,50 @@
     3.4 +/*  Title:      Pure/General/pretty.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Symbolic pretty printing.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +
    3.13 +object Pretty
    3.14 +{
    3.15 +  object Block
    3.16 +  {
    3.17 +    def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
    3.18 +      XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
    3.19 +
    3.20 +    def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
    3.21 +      tree match {
    3.22 +        case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
    3.23 +          Markup.parse_int(indent) match {
    3.24 +            case Some(i) => Some((i, body))
    3.25 +            case None => None
    3.26 +          }
    3.27 +        case _ => None
    3.28 +      }
    3.29 +  }
    3.30 +
    3.31 +  object Break
    3.32 +  {
    3.33 +    def apply(width: Int): XML.Tree =
    3.34 +      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width)))
    3.35 +
    3.36 +    def unapply(tree: XML.Tree): Option[Int] =
    3.37 +      tree match {
    3.38 +        case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
    3.39 +        case _ => None
    3.40 +      }
    3.41 +  }
    3.42 +
    3.43 +  object FBreak
    3.44 +  {
    3.45 +    def apply(): XML.Tree = XML.Elem(Markup.FBREAK, Nil, List(XML.Text(" ")))
    3.46 +
    3.47 +    def unapply(tree: XML.Tree): Boolean =
    3.48 +      tree match {
    3.49 +        case XML.Elem(Markup.FBREAK, Nil, _) => true
    3.50 +        case _ => false
    3.51 +      }
    3.52 +  }
    3.53 +}
     4.1 --- a/src/Pure/build-jars	Thu May 06 15:04:37 2010 +0200
     4.2 +++ b/src/Pure/build-jars	Thu May 06 16:27:47 2010 +0200
     4.3 @@ -27,6 +27,7 @@
     4.4    General/linear_set.scala
     4.5    General/markup.scala
     4.6    General/position.scala
     4.7 +  General/pretty.scala
     4.8    General/scan.scala
     4.9    General/symbol.scala
    4.10    General/xml.scala