equal
deleted
inserted
replaced
71 |
71 |
72 /* content -- text and markup */ |
72 /* content -- text and markup */ |
73 |
73 |
74 private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) = |
74 private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) = |
75 { |
75 { |
76 var text = new StringBuilder |
76 val text = new StringBuilder |
77 var markup_tree = Markup_Tree.empty |
77 var markup_tree = Markup_Tree.empty |
78 |
78 |
79 def traverse(tree: Tree): Unit = |
79 def traverse(tree: Tree): Unit = |
80 tree match { |
80 tree match { |
81 case Elem(markup, trees) => |
81 case Elem(markup, trees) => |