|
@@ -84,6 +84,10 @@ export class PreambleWidget extends WidgetType {
|
|
|
return this.expanded === other.expanded
|
|
return this.expanded === other.expanded
|
|
|
}
|
|
}
|
|
|
|
|
|
|
|
|
|
+ get estimatedHeight() {
|
|
|
|
|
+ return this.expanded ? -1 : 54
|
|
|
|
|
+ }
|
|
|
|
|
+
|
|
|
getToggleText(view: EditorView) {
|
|
getToggleText(view: EditorView) {
|
|
|
if (this.expanded) {
|
|
if (this.expanded) {
|
|
|
return view.state.phrase(`hide_document_preamble`)
|
|
return view.state.phrase(`hide_document_preamble`)
|