1.1 --- a/src/Pure/General/pretty.ML Wed Mar 27 22:36:03 2013 +0100
1.2 +++ b/src/Pure/General/pretty.ML Thu Mar 28 15:37:39 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 Wed Mar 27 22:36:03 2013 +0100
2.2 +++ b/src/Pure/General/pretty.scala Thu Mar 28 15:37:39 2013 +0100
2.3 @@ -73,26 +73,34 @@
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 metric: Metric = Metric_Default): XML.Body =
2.37 {
2.38 - sealed case class Text(tx: XML.Body = Nil, val pos: Double = 0.0, val nl: Int = 0)
2.39 + sealed case class Text(tx: XML.Body = Nil, pos: Double = 0.0, nl: Int = 0)
2.40 {
2.41 def newline: Text = copy(tx = FBreak :: tx, pos = 0.0, nl = nl + 1)
2.42 def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + metric(s))
2.43 @@ -101,7 +109,7 @@
2.44 }
2.45
2.46 val breakgain = margin / 20
2.47 - val emergencypos = margin / 2
2.48 + val emergencypos = (margin / 2).round.toInt
2.49
2.50 def content_length(tree: XML.Tree): Double =
2.51 XML.traverse_text(List(tree))(0.0)(_ + metric(_))
2.52 @@ -122,12 +130,12 @@
2.53 case t :: ts => t :: forcenext(ts)
2.54 }
2.55
2.56 - def format(trees: XML.Body, blockin: Double, after: Double, text: Text): Text =
2.57 + def format(trees: XML.Body, blockin: Int, after: Double, text: Text): Text =
2.58 trees match {
2.59 case Nil => text
2.60
2.61 case Block(indent, body) :: ts =>
2.62 - val pos1 = text.pos + indent
2.63 + val pos1 = (text.pos + indent).ceil.toInt
2.64 val pos2 = pos1 % emergencypos
2.65 val blockin1 =
2.66 if (pos1 < emergencypos) pos1
2.67 @@ -137,10 +145,10 @@
2.68 format(ts1, blockin, after, btext)
2.69
2.70 case Break(wd) :: ts =>
2.71 - if (text.pos + wd <= (margin - breakdist(ts, after)).max(blockin + breakgain))
2.72 + if (text.pos + wd <= ((margin - breakdist(ts, after)) max (blockin + breakgain)))
2.73 format(ts, blockin, after, text.blanks(wd))
2.74 - else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
2.75 - case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
2.76 + else format(ts, blockin, after, text.newline.blanks(blockin))
2.77 + case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin))
2.78
2.79 case XML.Wrapped_Elem(markup, body1, body2) :: ts =>
2.80 val btext = format(body2, blockin, breakdist(ts, after), text.copy(tx = Nil))
2.81 @@ -157,7 +165,7 @@
2.82 case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s))
2.83 }
2.84
2.85 - format(standard_format(input), 0.0, 0.0, Text()).content
2.86 + format(standard_form(input), 0, 0.0, Text()).content
2.87 }
2.88
2.89 def string_of(input: XML.Body, margin: Double = margin_default,
2.90 @@ -179,7 +187,7 @@
2.91 case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
2.92 case XML.Text(_) => List(tree)
2.93 }
2.94 - standard_format(input).flatMap(fmt)
2.95 + standard_form(input).flatMap(fmt)
2.96 }
2.97
2.98 def str_of(input: XML.Body): String = XML.content(unformatted(input))
3.1 --- a/src/Pure/PIDE/markup.ML Wed Mar 27 22:36:03 2013 +0100
3.2 +++ b/src/Pure/PIDE/markup.ML Thu Mar 28 15:37:39 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 Wed Mar 27 22:36:03 2013 +0100
4.2 +++ b/src/Pure/PIDE/markup.scala Thu Mar 28 15:37:39 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
5.1 --- a/src/Pure/Thy/present.ML Wed Mar 27 22:36:03 2013 +0100
5.2 +++ b/src/Pure/Thy/present.ML Thu Mar 28 15:37:39 2013 +0100
5.3 @@ -52,11 +52,14 @@
5.4 structure Browser_Info = Theory_Data
5.5 (
5.6 type T = {chapter: string, name: string};
5.7 - val empty = {chapter = Context.PureN, name = Context.PureN}: T;
5.8 + val empty = {chapter = "Unsorted", name = "Unknown"}: T;
5.9 fun extend _ = empty;
5.10 fun merge _ = empty;
5.11 );
5.12
5.13 +val _ = Context.>> (Context.map_theory
5.14 + (Browser_Info.put {chapter = Context.PureN, name = Context.PureN}));
5.15 +
5.16 val session_name = #name o Browser_Info.get;
5.17 val session_chapter_name = (fn {chapter, name} => [chapter, name]) o Browser_Info.get;
5.18