Skip to content

Commit

Permalink
cleanup and window width
Browse files Browse the repository at this point in the history
  • Loading branch information
@joneugster
joneugster committed Jul 24, 2024
1 parent 170560e commit 5fc893e
Show file tree
Hide file tree
Showing 2 changed files with 16 additions and 93 deletions.
42 changes: 13 additions & 29 deletions client/src/App.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@ import { LeanMonaco, LeanMonacoEditor } from 'lean4monaco'
import defaultSettings from './config/settings'
import Split from 'react-split'
import { Menu } from './Navigation'

import { IPreferencesContext, PreferencesContext } from './Popups/Settings'
import { useWindowDimensions } from './utils/window_width'
import './css/App.css'
import './css/Editor.css'
import { IPreferencesContext, PreferencesContext } from './Popups/Settings'

/** Expected arguments which can be provided in the URL. */
interface UrlArgs {
Expand Down Expand Up @@ -57,6 +57,7 @@ function App() {
const [project, setProject] = useState<string>('mathlib-demo')
const [url, setUrl] = useState<string|null>(null)
const [contentFromUrl, setContentFromUrl] = useState<string>('')
const {width, height} = useWindowDimensions()

Check failure on line 60 in client/src/App.tsx

View workflow job for this annotation

GitHub Actions / build 

'height' is declared but its value is never read.

function setContent (code: string) {
editor?.getModel()?.setValue(code)
Expand Down Expand Up @@ -87,37 +88,22 @@ function App() {
}
}, [])

// Use the window witdh to switch between mobile/desktop layout
useEffect(() => {
const _mobile = width < 800
if (!preferences.saveInLocalStore && _mobile !== preferences.mobile) {
setPreferences({ ...preferences, mobile: _mobile })
}
}, [width])

// Setting up the editor and infoview
useEffect(() => {
const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket" + "/" + project
console.log(`socket url: ${socketUrl}`)

// TODO: is this link still recent?
// see available options here:
// https://microsoft.github.io/monaco-editor/typedoc/variables/editor.EditorOptions.html
const editorOptions = {
// glyphMargin: true,
// lineDecorationsWidth: 5,
// folding: false,
// lineNumbers: 'on',
// lineNumbersMinChars: 1,
// "editor.rulers": [100],
// lightbulb: {
// enabled: true
// },
// unicodeHighlight: {
// ambiguousCharacters: false,
// },
// automaticLayout: true,
// minimap: {
// enabled: false
// },
// theme: 'vs',
// fontFamily: "JuliaMono",
}
// 'inputModeEnabled': true,
// 'inputModeCustomTranslations': {},
// 'eagerReplacementEnabled': true,
// 'customTheme': '',

const leanMonaco = new LeanMonaco()
const leanMonacoEditor = new LeanMonacoEditor()
Expand All @@ -129,14 +115,12 @@ function App() {
"editor.lightbulb": {enabled: true},
"editor.wordWrap": preferences.wordWrap ? "on" : "off",
"editor.wrappingStrategy": "advanced",

"editor.semanticHighlighting.enabled": true,
"editor.acceptSuggestionOnEnter": preferences.acceptSuggestionOnEnter ? "on" : "off", // nope?
"editor.theme": preferences.theme,

"editor.eagerReplacementEnabled": true,

"lean4.input.leader": preferences.abbreviationCharacter

}})
leanMonaco.setInfoviewElement(infoviewRef.current!)
await leanMonacoEditor.start(codeviewRef.current!, `/project/${project}.lean`, '')
Expand Down
67 changes: 3 additions & 64 deletions client/src/Popups/Settings.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ import lean4webConfig from '../config/config'
import { Popup } from '../Navigation';
import defaultSettings from '../config/settings'

/** This must be kept in sync with ../config/settings.ts */
export interface IPreferencesContext {
// lean4web
mobile: boolean
Expand All @@ -20,6 +21,7 @@ export interface IPreferencesContext {
abbreviationCharacter: string
}

/** The context holding the preferences */
export const PreferencesContext = React.createContext<{
preferences: IPreferencesContext,
setPreferences: React.Dispatch<React.SetStateAction<IPreferencesContext>>
Expand All @@ -35,62 +37,7 @@ const SettingsPopup: React.FC<{
project: any
setProject: any
}> = ({open, handleClose, closeNav, project, setProject}) => {

const { preferences, setPreferences } = useContext(PreferencesContext)
// const [abbreviationCharacter, setAbbreviationCharacter] = React.useState(preferences.abbreviationCharacter)

/* Vertical layout is changeable in the settings.
If screen width is below 800, default to vertical layout instead. */
// const {width, height} = useWindowDimensions()
// const [mobile, setVerticalLayout] = React.useState(width < 800)
// const [wordWrap, setWordWrap] = React.useState(true)
// const [acceptSuggestionOnEnter, setAcceptSuggestionOnEnter] = React.useState(false)

// Synchronize state with initial local store
useEffect(() => {



// let _abbreviationCharacter = window.localStorage.getItem("abbreviationCharacter")
// let _mobile = window.localStorage.getItem("mobile")
// let _wordWrap = window.localStorage.getItem("wordWrap")
// let _acceptSuggestionOnEnter = window.localStorage.getItem("acceptSuggestionOnEnter")
// let _theme = window.localStorage.getItem("theme")
// let _savingAllowed = window.localStorage.getItem("savingAllowed")
// let _customTheme = window.localStorage.getItem("customTheme")
// if (_abbreviationCharacter) {
// setAbbreviationCharacter(_abbreviationCharacter)
// setSavingAllowed(true)
// }
// if (_mobile) {
// setVerticalLayout(_mobile == 'true')
// setSavingAllowed(true)
// }
// if (_theme) {
// setTheme(_theme)
// setSavingAllowed(true)
// }
// if (_wordWrap) {
// setWordWrap(_wordWrap == "true")
// setSavingAllowed(true)
// }
// if (_acceptSuggestionOnEnter) {
// setAcceptSuggestionOnEnter(_acceptSuggestionOnEnter == "true")
// setSavingAllowed(true)
// }
// if (_customTheme) {
// setCustomTheme(_customTheme)
// setSavingAllowed(true)
// try {
// var loadedTheme = JSON.parse(_customTheme)
// monaco.editor.defineTheme('custom', loadedTheme)
// } catch (error) {
// // invalid custom theme
// setCustomTheme('')
// if (_theme == 'custom') {setTheme('lightPlus')}
// }
// }
}, [])

function modifyPreferences(key: keyof IPreferencesContext, value: any) {
let newPreferences: any = { ...preferences }
Expand All @@ -105,7 +52,7 @@ const SettingsPopup: React.FC<{
if (typeof value === 'string') {
window.localStorage.setItem(key, value)
} else if (typeof value === 'boolean') {
// Boolean values
// turn boolean values into string
window.localStorage.setItem(key, value ? 'true' : 'false')
} else {
// other values aren't implemented yet.
Expand Down Expand Up @@ -163,14 +110,6 @@ const SettingsPopup: React.FC<{
{/* <option value="Visual Studio Light">visual studio light</option> */}
{/* <option value="Visual Studio Dark">visual studio dark</option> */}
</select>

{/* <label htmlFor="theme-upload" className="file-upload-button" >Load from Disk</label>
<input id="theme-upload" type="file" onChange={uploadTheme} /> */}

{/* <Button variant="contained" component="label" className='file-upload-button' onClick={uploadTheme}>
Load from DisksetTheme
<input id="theme-upload" type="file" onChange={uploadTheme} />
</Button> */}
</p>
<p>
<Switch id="mobile" onChange={() => {
Expand Down

0 comments on commit 5fc893e

Please sign in to comment.