Skip to content

Commit

Permalink
setup vscode-lean4 as submodule
Browse files Browse the repository at this point in the history
  • Loading branch information
joneugster committed Jun 1, 2024
1 parent c053899 commit 40fbb28
Show file tree
Hide file tree
Showing 19 changed files with 104 additions and 1,683 deletions.
6 changes: 3 additions & 3 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
[submodule "Projects/lean4web-tools"]
path = Projects/lean4web-tools
url = https://github.com/hhu-adam/lean4web-tools.git
[submodule "client/vscode-lean4"]
path = client/vscode-lean4
url = https://github.com/leanprover/vscode-lean4.git
[submodule "client/monaco-lean4"]
path = client/monaco-lean4
url = git@github.com:hhu-adam/monaco-lean4.git
1 change: 1 addition & 0 deletions client/monaco-lean4
Submodule monaco-lean4 added at f0187e
19 changes: 10 additions & 9 deletions client/src/Editor.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,11 @@ import { useEffect, useRef, useState } from 'react'
import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js'
import { loadRenderInfoview } from '@leanprover/infoview/loader'
import { InfoviewApi } from '@leanprover/infoview-api'
import { InfoProvider } from './editor/infoview'
import { LeanClient } from './editor/leanclient'
import { AbbreviationRewriter } from './editor/abbreviation/rewriter/AbbreviationRewriter'
import { AbbreviationProvider } from './editor/abbreviation/AbbreviationProvider'
import { LeanTaskGutter } from './editor/taskgutter'
import { InfoProvider } from '../monaco-lean4/vscode-lean4/src/infoview'
import { LeanClient } from '../monaco-lean4/vscode-lean4/src/leanclient'
import { AbbreviationRewriter } from '../monaco-lean4/vscode-lean4/src/abbreviation/rewriter/AbbreviationRewriter'
import { AbbreviationProvider } from '../monaco-lean4/vscode-lean4/src/abbreviation/AbbreviationProvider'
import { LeanTaskGutter } from '../monaco-lean4/vscode-lean4/src/taskgutter'
import Split from 'react-split'
import Notification from './Notification'
import settings from './config/settings'
Expand All @@ -17,9 +17,10 @@ import { DisposingWebSocketMessageReader } from './reader'
import { monacoSetup } from './monacoSetup'

import './css/Editor.css'
import './editor/infoview.css'
import './editor/vscode.css'
import './css/infoview.css'
import './css/vscode.css'
import { render } from '@testing-library/react'
import { AbbreviationConfig } from '../monaco-lean4/vscode-lean4/src/abbreviation/config'

monacoSetup()

Expand Down Expand Up @@ -96,7 +97,8 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
wrappingStrategy: "advanced",
})
setEditor(editor)
const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(), model, editor)

const abbrevRewriter = new AbbreviationRewriter(new AbbreviationProvider(AbbreviationConfig), model, editor)
return () => {
editor.dispose();
model.dispose();
Expand Down Expand Up @@ -184,7 +186,6 @@ const Editor: React.FC<{setRestart?, onDidChangeContent?, value: string, theme:
setRestart((project?) => restart)
}, [editor, infoviewApi, infoProvider])


return (
<div className='editor-wrapper'>
<Split className={`editor ${ dragging? 'dragging':''}`}
Expand Down
66 changes: 66 additions & 0 deletions client/src/Untitled-1.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,66 @@
jeugster@razorbill:~/Lean/lean4web$ git log dev
commit e60940bb6546775ebe0ea0b7d06b8ec02cf175b4 (dev)
Author: Jon Eugster <[email protected]>
Date: Wed May 29 15:52:58 2024 +0200

add vscode-lean4 as submodule

commit c06471c81129dbad2f8a7cbd2718b2f1b79127de (origin/dev)
Author: Jon Eugster <[email protected]>
Date: Tue May 7 12:20:09 2024 +0200

many things

commit 3cc8a85d28bf42ca3254f1458b725f77251d33d0
Author: Jon Eugster <[email protected]>
Date: Thu May 2 17:18:45 2024 +0200

temp. add entire vscode-lean4 extension

commit 013dbada1fd2557ce5d25b8fd88f32aba1ce8e41
Author: Jon Eugster <[email protected]>
Date: Thu May 2 04:06:56 2024 +0200

cleanup App.tsx and config













commit 5e2ea468ab9401eb0d5d16efbde21bbe9cc6521f
Author: Jon Eugster <[email protected]>
Date: Thu May 2 02:32:02 2024 +0200

cleanup navigation. includes #12.

commit 012f97aa23a1a516171c075b6f45ad7be789e2b0
Author: Jon Eugster <[email protected]>
Date: Tue Apr 30 17:29:49 2024 +0200

cleanup App.tsx, part 2

commit 30055c00891c2caff8a8446feee78766c1807063
Author: Jon Eugster <[email protected]>
Date: Tue Apr 30 17:17:35 2024 +0200

cleanup App.tsx, part 1

commit 182ba518ea89d046914b3242e97dc4cc9974944f
Author: Jon Eugster <[email protected]>
Date: Tue Apr 30 17:17:04 2024 +0200

fix updated infoview

commit 88d83ea6b1cd0885c9fcd19223d629ddf507af44
Author: Jon Eugster <[email protected]>
Date: Mon Apr 29 20:30:14 2024 +0200

temporarily use my own npm packages instead
23 changes: 23 additions & 0 deletions client/src/config/editor.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{
"glyphMargin": true,
"lineDecorationsWidth": 5,
"folding": false,
"lineNumbers": "on",
"lineNumbersMinChars": 1,
"rulers": [100],
"lightbulb": {
"enabled": true
},
"unicodeHighlight": {
"ambiguousCharacters": false
},
"automaticLayout": true,
"minimap": {
"enabled": false
},
"tabSize": 2,
"semanticHighlighting.enabled": true,
"theme": "vs",
"fontFamily": "JuliaMono",
"wrappingStrategy": "advanced"
}
File renamed without changes.
File renamed without changes.
49 changes: 0 additions & 49 deletions client/src/editor/abbreviation/AbbreviationHoverProvider.ts

This file was deleted.

108 changes: 0 additions & 108 deletions client/src/editor/abbreviation/AbbreviationProvider.ts

This file was deleted.

Loading

0 comments on commit 40fbb28

Please sign in to comment.