basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
authorwenzelm
Thu Mar 28 15:36:45 2013 +0100 (2013-03-28 ago)
changeset 515703633828d80fc
parent 51569 4e084727faae
child 51571 1eb3316d6d93
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);
src/Pure/General/pretty.ML
src/Pure/General/pretty.scala
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/General/pretty.ML	Thu Mar 28 15:00:27 2013 +0100
     1.2 +++ b/src/Pure/General/pretty.ML	Thu Mar 28 15:36:45 2013 +0100
     1.3 @@ -38,6 +38,7 @@
     1.4    val mark: Markup.T -> T -> T
     1.5    val mark_str: Markup.T * string -> T
     1.6    val marks_str: Markup.T list * string -> T
     1.7 +  val item: T list -> T
     1.8    val command: string -> T
     1.9    val keyword: string -> T
    1.10    val text: string -> T list
    1.11 @@ -157,6 +158,8 @@
    1.12  fun mark_str (m, s) = mark m (str s);
    1.13  fun marks_str (ms, s) = fold_rev mark ms (str s);
    1.14  
    1.15 +val item = markup Markup.item;
    1.16 +
    1.17  fun command name = mark_str (Markup.keyword1, name);
    1.18  fun keyword name = mark_str (Markup.keyword2, name);
    1.19  
     2.1 --- a/src/Pure/General/pretty.scala	Thu Mar 28 15:00:27 2013 +0100
     2.2 +++ b/src/Pure/General/pretty.scala	Thu Mar 28 15:36:45 2013 +0100
     2.3 @@ -73,20 +73,28 @@
     2.4  
     2.5    val FBreak = XML.Text("\n")
     2.6  
     2.7 +  def item(body: XML.Body): XML.Tree =
     2.8 +    Block(2, XML.Text(Symbol.decode("\\<bullet>") + " ") :: body)
     2.9 +
    2.10    val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
    2.11    def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
    2.12  
    2.13  
    2.14 -  /* formatted output */
    2.15 +  /* standard form */
    2.16  
    2.17 -  def standard_format(body: XML.Body): XML.Body =
    2.18 +  def standard_form(body: XML.Body): XML.Body =
    2.19      body flatMap {
    2.20        case XML.Wrapped_Elem(markup, body1, body2) =>
    2.21 -        List(XML.Wrapped_Elem(markup, body1, standard_format(body2)))
    2.22 -      case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
    2.23 +        List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
    2.24 +      case XML.Elem(markup, body) =>
    2.25 +        if (markup.name == Markup.ITEM) List(item(standard_form(body)))
    2.26 +        else List(XML.Elem(markup, standard_form(body)))
    2.27        case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
    2.28      }
    2.29  
    2.30 +
    2.31 +  /* formatted output */
    2.32 +
    2.33    private val margin_default = 76.0
    2.34  
    2.35    def formatted(input: XML.Body, margin: Double = margin_default,
    2.36 @@ -157,7 +165,7 @@
    2.37          case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
    2.38        }
    2.39  
    2.40 -    format(standard_format(input), 0, 0.0, Text()).content
    2.41 +    format(standard_form(input), 0, 0.0, Text()).content
    2.42    }
    2.43  
    2.44    def string_of(input: XML.Body, margin: Double = margin_default,
    2.45 @@ -179,7 +187,7 @@
    2.46          case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
    2.47          case XML.Text(_) => List(tree)
    2.48        }
    2.49 -    standard_format(input).flatMap(fmt)
    2.50 +    standard_form(input).flatMap(fmt)
    2.51    }
    2.52  
    2.53    def str_of(input: XML.Body): String = XML.content(unformatted(input))
     3.1 --- a/src/Pure/PIDE/markup.ML	Thu Mar 28 15:00:27 2013 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Thu Mar 28 15:36:45 2013 +0100
     3.3 @@ -34,6 +34,7 @@
     3.4    val widthN: string
     3.5    val breakN: string val break: int -> T
     3.6    val fbreakN: string val fbreak: T
     3.7 +  val itemN: string val item: T
     3.8    val hiddenN: string val hidden: T
     3.9    val theoryN: string
    3.10    val classN: string
    3.11 @@ -241,6 +242,8 @@
    3.12  
    3.13  val (fbreakN, fbreak) = markup_elem "fbreak";
    3.14  
    3.15 +val (itemN, item) = markup_elem "item";
    3.16 +
    3.17  
    3.18  (* hidden text *)
    3.19  
     4.1 --- a/src/Pure/PIDE/markup.scala	Thu Mar 28 15:00:27 2013 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 15:36:45 2013 +0100
     4.3 @@ -82,9 +82,12 @@
     4.4  
     4.5    val Indent = new Properties.Int("indent")
     4.6    val BLOCK = "block"
     4.7 +
     4.8    val Width = new Properties.Int("width")
     4.9    val BREAK = "break"
    4.10  
    4.11 +  val ITEM = "item"
    4.12 +
    4.13    val SEPARATOR = "separator"
    4.14  
    4.15