Removing useless cruft from settings menus.

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 )

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()

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

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 ) )
         }
     } )