| changeset 66043 | f704c063e95d |
| parent 66041 | c49bd8bb4839 |
| child 66044 | bd7516709051 |
| 66042:98aaeff47795 | 66043:f704c063e95d |
|---|---|
121 XML.Text(Symbol.decode(text)) |
121 XML.Text(Symbol.decode(text)) |
122 } |
122 } |
123 |
123 |
124 def theory_document(snapshot: Document.Snapshot): XML.Body = |
124 def theory_document(snapshot: Document.Snapshot): XML.Body = |
125 { |
125 { |
126 make_html(snapshot.markup_to_XML(None, document_span_elements)) |
126 make_html(snapshot.markup_to_XML(Text.Range.full, document_span_elements)) |
127 } |
127 } |
128 } |
128 } |