# HG changeset patch
# User wenzelm
# Date 1364481405 -3600
# Node ID 3633828d80fccd45b3eb8c38ed2adcc13fdeeeb9
# Parent  4e084727faaedf6f6665bc8c9c4d2d1b209942af
basic support for Pretty.item, which is considered as logical markup and interpreted in Isabelle/Scala, but ignored elsewhere (TTY, latex etc.);

diff -r 4e084727faae -r 3633828d80fc src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Mar 28 15:00:27 2013 +0100
+++ b/src/Pure/General/pretty.ML	Thu Mar 28 15:36:45 2013 +0100
@@ -38,6 +38,7 @@
   val mark: Markup.T -> T -> T
   val mark_str: Markup.T * string -> T
   val marks_str: Markup.T list * string -> T
+  val item: T list -> T
   val command: string -> T
   val keyword: string -> T
   val text: string -> T list
@@ -157,6 +158,8 @@
 fun mark_str (m, s) = mark m (str s);
 fun marks_str (ms, s) = fold_rev mark ms (str s);
 
+val item = markup Markup.item;
+
 fun command name = mark_str (Markup.keyword1, name);
 fun keyword name = mark_str (Markup.keyword2, name);
 
diff -r 4e084727faae -r 3633828d80fc src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 28 15:00:27 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 28 15:36:45 2013 +0100
@@ -73,20 +73,28 @@
 
   val FBreak = XML.Text("\n")
 
+  def item(body: XML.Body): XML.Tree =
+    Block(2, XML.Text(Symbol.decode("\\<bullet>") + " ") :: body)
+
   val Separator = List(XML.elem(Markup.SEPARATOR, List(XML.Text(space))), FBreak)
   def separate(ts: List[XML.Tree]): XML.Body = Library.separate(Separator, ts.map(List(_))).flatten
 
 
-  /* formatted output */
+  /* standard form */
 
-  def standard_format(body: XML.Body): XML.Body =
+  def standard_form(body: XML.Body): XML.Body =
     body flatMap {
       case XML.Wrapped_Elem(markup, body1, body2) =>
-        List(XML.Wrapped_Elem(markup, body1, standard_format(body2)))
-      case XML.Elem(markup, body) => List(XML.Elem(markup, standard_format(body)))
+        List(XML.Wrapped_Elem(markup, body1, standard_form(body2)))
+      case XML.Elem(markup, body) =>
+        if (markup.name == Markup.ITEM) List(item(standard_form(body)))
+        else List(XML.Elem(markup, standard_form(body)))
       case XML.Text(text) => Library.separate(FBreak, split_lines(text).map(XML.Text))
     }
 
+
+  /* formatted output */
+
   private val margin_default = 76.0
 
   def formatted(input: XML.Body, margin: Double = margin_default,
@@ -157,7 +165,7 @@
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
       }
 
-    format(standard_format(input), 0, 0.0, Text()).content
+    format(standard_form(input), 0, 0.0, Text()).content
   }
 
   def string_of(input: XML.Body, margin: Double = margin_default,
@@ -179,7 +187,7 @@
         case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
-    standard_format(input).flatMap(fmt)
+    standard_form(input).flatMap(fmt)
   }
 
   def str_of(input: XML.Body): String = XML.content(unformatted(input))
diff -r 4e084727faae -r 3633828d80fc src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Mar 28 15:00:27 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Mar 28 15:36:45 2013 +0100
@@ -34,6 +34,7 @@
   val widthN: string
   val breakN: string val break: int -> T
   val fbreakN: string val fbreak: T
+  val itemN: string val item: T
   val hiddenN: string val hidden: T
   val theoryN: string
   val classN: string
@@ -241,6 +242,8 @@
 
 val (fbreakN, fbreak) = markup_elem "fbreak";
 
+val (itemN, item) = markup_elem "item";
+
 
 (* hidden text *)
 
diff -r 4e084727faae -r 3633828d80fc src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Mar 28 15:00:27 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 15:36:45 2013 +0100
@@ -82,9 +82,12 @@
 
   val Indent = new Properties.Int("indent")
   val BLOCK = "block"
+
   val Width = new Properties.Int("width")
   val BREAK = "break"
 
+  val ITEM = "item"
+
   val SEPARATOR = "separator"