# HG changeset patch
# User wenzelm
# Date 1364482023 -3600
# Node ID 6d3a3ea5fc6e9fed4b8a301ddd0198464f92902e
# Parent  8e97017538ba8a157535a0709dd0f45e3c68a83a# Parent  1eb3316d6d9349bd3580595837cb86e095c19d3c
merged

diff -r 8e97017538ba -r 6d3a3ea5fc6e src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu Mar 28 15:45:08 2013 +0100
+++ b/src/Pure/General/pretty.ML	Thu Mar 28 15:47:03 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 8e97017538ba -r 6d3a3ea5fc6e src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Thu Mar 28 15:45:08 2013 +0100
+++ b/src/Pure/General/pretty.scala	Thu Mar 28 15:47:03 2013 +0100
@@ -73,26 +73,34 @@
 
   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,
     metric: Metric = Metric_Default): XML.Body =
   {
-    sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
+    sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
     {
       def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
       def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
@@ -101,7 +109,7 @@
     }
 
     val breakgain = margin / 20
-    val emergencypos = margin / 2
+    val emergencypos = (margin / 2).round.toInt
 
     def content_length(tree: XML.Tree): Double =
       XML.traverse_text(List(tree))(0.0)(_ + metric(_))
@@ -122,12 +130,12 @@
         case t :: ts => t :: forcenext(ts)
       }
 
-    def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
+    def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
       trees match {
         case Nil => text
 
         case Block(indent, body) :: ts =>
-          val pos1 = text.pos + indent
+          val pos1 = (text.pos + indent).ceil.toInt
           val pos2 = pos1 % emergencypos
           val blockin1 =
             if (pos1 < emergencypos) pos1
@@ -137,10 +145,10 @@
           format(ts1, blockin, after, btext)
 
         case Break(wd) :: ts =>
-          if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
+          if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
             format(ts, blockin, after, text.blanks(wd))
-          else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
-        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
+          else format(ts, blockin, after, text.newline.blanks(blockin))
+        case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
 
         case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
           val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
@@ -157,7 +165,7 @@
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
       }
 
-    format(standard_format(input), 0.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 8e97017538ba -r 6d3a3ea5fc6e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Mar 28 15:45:08 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Thu Mar 28 15:47:03 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 8e97017538ba -r 6d3a3ea5fc6e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Thu Mar 28 15:45:08 2013 +0100
+++ b/src/Pure/PIDE/markup.scala	Thu Mar 28 15:47:03 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"
 
 
diff -r 8e97017538ba -r 6d3a3ea5fc6e src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Thu Mar 28 15:45:08 2013 +0100
+++ b/src/Pure/Thy/present.ML	Thu Mar 28 15:47:03 2013 +0100
@@ -52,11 +52,14 @@
 structure Browser_Info = Theory_Data
 (
   type T = {chapter: string, name: string};
-  val empty = {chapter = Context.PureN, name = Context.PureN}: T;
+  val empty = {chapter = "Unsorted", name = "Unknown"}: T;
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
+val _ = Context.>> (Context.map_theory
+  (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
+
 val session_name = #name o Browser_Info.get;
 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;