diff --git a/lurchmath/document-settings.js b/lurchmath/document-settings.js index 4a858eaa..db619221 100644 --- a/lurchmath/document-settings.js +++ b/lurchmath/document-settings.js @@ -36,13 +36,13 @@ if ( typeof( localStorage ) !== 'undefined' ) appSettings.load() */ export const install = editor => { editor.ui.registry.addMenuItem( 'docsettings', { - text : 'Edit document settings', + text : 'Document settings', icon : 'settings', tooltip : 'Edit document settings', onAction : () => { // Create settings instance and LurchDocument instance const settings = new Settings( 'Document settings', - LurchDocument.settingsMetadata ) + LurchDocument.shortSettingsMetadata ) const LDoc = new LurchDocument( editor ) // Load document settings into it const allowedKeys = settings.keys() @@ -79,7 +79,9 @@ export const install = editor => { * @param {string} key - the name of the setting to look up */ export const lookup = ( editor, key ) => { - // Create all the objects we need to use for lookup + // Create all the objects we need to use for lookup. We usethe full + // settingsMetadata for this since the settings themselves might be needed + // elsewhere even if we don't let the user edit them. const settings = new Settings( 'Document settings', LurchDocument.settingsMetadata ) const metadata = settings.metadata.metadataFor( key ) diff --git a/lurchmath/header-editor.js b/lurchmath/header-editor.js index 92c00136..7eba13d0 100644 --- a/lurchmath/header-editor.js +++ b/lurchmath/header-editor.js @@ -227,7 +227,7 @@ export const install = editor => { // dependencies) in the header. This list of dependencies never leaves the // header, so this is the only way to edit it. editor.ui.registry.addMenuItem( 'editdependencyurls', { - text : 'Edit background material', + text : 'Add or remove context', tooltip : 'Edit the list of documents on which this one depends', icon : 'edit-block', onAction : () => { @@ -241,7 +241,7 @@ export const install = editor => { } } ) // Create the dialog, but do not populate it with dependencies yet. - const dialog = new Dialog( 'Edit background material', editor ) + const dialog = new Dialog( 'Add or remove context documents', editor ) dialog.json.size = 'medium' const listItem = new ListItem( 'dependencies' ) listItem.setSelectable() diff --git a/lurchmath/lurch-document.js b/lurchmath/lurch-document.js index 2a596679..5822029a 100644 --- a/lurchmath/lurch-document.js +++ b/lurchmath/lurch-document.js @@ -507,6 +507,28 @@ export class LurchDocument { ) ) + /** + * This is a truncated version of {@link settingsMetadata} to keep users + * away from advanced, confusing, or no longer functional settings. + */ + static shortSettingsMetadata = new SettingsMetadata( + new SettingsCategoryMetadata( + 'Document metadata', + new TextSettingMetadata( 'title', 'Title', '' ), + new TextSettingMetadata( 'author', 'Author', '' ), + new TextSettingMetadata( 'date', 'Date', '' ), + new LongTextSettingMetadata( 'abstract', 'Abstract', '' ) + ), + new SettingsCategoryMetadata( + 'Validation options', + new BoolSettingMetadata( 'instantiateEverything', 'Try harder to validate (can be much slower)', false ) + // , + // We temporarily hide the following since it doesn't work yet. + // new BoolSettingMetadata( 'hideShellNames', 'Hide marginal shell annotations in semantic view', false ) + ) + ) + + /** * This array lists those settings that should be marked as classes on the * body element of the editor's document. This exposes them to CSS rules diff --git a/lurchmath/settings-install.js b/lurchmath/settings-install.js index e0529756..80b0a614 100644 --- a/lurchmath/settings-install.js +++ b/lurchmath/settings-install.js @@ -1,4 +1,3 @@ - /** * This module exports one function that installs in a TinyMCE editor features * for editing application settings, and it also exports the settings object @@ -30,30 +29,30 @@ export const appSettings = new Settings( 'notation', 'Default notation to use for new documents', [ 'Lurch notation', 'LaTeX' ], - 'LaTeX' + 'Lurch notation' ), new CategorySettingMetadata( 'expression editor type', 'Type of expression editor to use', [ 'Beginner', 'Intermediate', 'Advanced' ], - 'Beginner' + 'Advanced' ), new CategorySettingMetadata( 'expository math editor type', 'Type of expository math editor to use', [ 'Beginner', 'Intermediate', 'Advanced' ], - 'Beginner' + 'Advanced' ), new BoolSettingMetadata( 'dollar sign shortcut', 'Use $ as a shortcut for entering expository math', - false + true ), new CategorySettingMetadata( 'default shell style', 'Default style for environments in new documents', [ 'boxed', 'minimal' ], - 'boxed' + 'minimal' ), new NoteMetadata( 'If you change the default environment style, you will need to ' @@ -66,7 +65,7 @@ export const appSettings = new Settings( 'application width in window', 'Width of application in browser window', [ 'Fixed size', 'Full width' ], - 'Full width' + 'Fixed size' ), new BoolSettingMetadata( 'developer mode on', @@ -143,7 +142,7 @@ export const appSettings = new Settings( 'preferred meaning style', 'Preferred style to use when viewing content\'s meaning', [ 'Hierarchy', 'Code' ], - 'Hierarchy' + 'Code' ), new LongTextSettingMetadata( 'declaration type templates', @@ -186,6 +185,49 @@ export const appSettings = new Settings( ) ) +/** + * This is a truncated version of {@link appSettings} use for the Preferences + * dialog to hide from advanced, confusing, or no longer functional settings. + * + * @see {@link Settings} + */ +export const shortAppSettings = new Settings( + 'Application settings', + new SettingsMetadata( + new SettingsCategoryMetadata( + 'Export to LaTeX', + new BoolSettingMetadata( + 'add LaTeX document wrapper', + 'Wrap the result in a document environment', + true + ), + new BoolSettingMetadata( + 'export LaTeX selection only', + 'Convert only the selection to LaTeX', + false + ), + new BoolSettingMetadata( + 'export LaTeX shells', + 'Export shells as LaTeX environments', + true + ), + ), + new SettingsCategoryMetadata( + 'Application warnings', + new ShowWarningSettingMetadata( + 'warn before extract header', + 'Show warning before moving the header into the document', + 'Moving the header into the document is an action that cannot be undone.' + ), + new ShowWarningSettingMetadata( + 'warn before embed header', + 'Show warning before moving document content into header', + 'Moving content into the header is an action that cannot be undone.' + ) + ) + ) +) + // Internal use only // Called when the user says OK in the app settings dialog. // Parameter is a list of what settings they changed (array of string keys), @@ -218,12 +260,12 @@ const applySettings = changes => { */ export const install = editor => { editor.ui.registry.addMenuItem( 'preferences', { - text : 'Preferences', - tooltip : 'Preferences', + text : 'Application settings', + tooltip : 'Lurch application settings', icon : 'preferences', onAction : () => { appSettings.load() - appSettings.userEdit( editor ).then( changes => + shortAppSettings.userEdit( editor ).then( changes => applySettings( changes ) ) } } )