Skip to content

Commit

Permalink
move monaco setup back to editor
Browse files Browse the repository at this point in the history
  • Loading branch information
abentkamp committed Dec 6, 2023
1 parent 5117455 commit 3ed4ed4
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 3 deletions.
3 changes: 0 additions & 3 deletions client/src/App.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -15,10 +15,7 @@ import Tools from './Tools'
import Examples from './Examples'
import LoadingMenu from './LoadingMenu'
import { config } from './config/config'
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { monacoSetup } from './monacoSetup'

monacoSetup()

const App: React.FC = () => {
const [restart, setRestart] = useState()
Expand Down
3 changes: 3 additions & 0 deletions client/src/Editor.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,12 @@ import { config } from './config/config'
import { IConnectionProvider } from 'monaco-languageclient'
import { toSocket, WebSocketMessageWriter } from 'vscode-ws-jsonrpc'
import { DisposingWebSocketMessageReader } from './reader'
import { monacoSetup } from './monacoSetup'

const socketUrl = ((window.location.protocol === "https:") ? "wss://" : "ws://") + window.location.host + "/websocket"

monacoSetup()

const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme: string}> =
({setRestart, onDidChangeContent, value, theme}) => {
const uri = monaco.Uri.parse('file:///LeanProject/LeanProject.lean')
Expand Down

0 comments on commit 3ed4ed4

Please sign in to comment.