ConceptProd/ConceptPortal-public
1
0
Fork 0
mirror of https://github.com/IRBorisov/ConceptPortal.git synced 2025-06-26 13:00:39 +03:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix selection after insert

Browse Source
This commit is contained in:
IRBorisov 2023-08-13 21:57:05 +03:00
parent 1dc2a80629
commit 036046734e
1 changed files with 4 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
rsconcept/frontend/src/components/RSInput/textEditing.ts
View File

@ -68,6 +68,7 @@ export class TextWrapper {
} }
insertToken(tokenID: TokenID): boolean { insertToken(tokenID: TokenID): boolean {
const hasSelection = this.ref.view.state.selection.main.from !== this.ref.view.state.selection.main.to
switch (tokenID) { switch (tokenID) {
case TokenID.NT_DECLARATIVE_EXPR: this.envelopeWith('D{ξ∈X1 | P1[ξ]', '}'); return true; case TokenID.NT_DECLARATIVE_EXPR: this.envelopeWith('D{ξ∈X1 | P1[ξ]', '}'); return true;
case TokenID.NT_IMPERATIVE_EXPR: this.envelopeWith('I{(σ, γ) | σ:∈X1; γ:=F1[σ]; P1[σ, γ]', '}'); return true; case TokenID.NT_IMPERATIVE_EXPR: this.envelopeWith('I{(σ, γ) | σ:∈X1; γ:=F1[σ]; P1[σ, γ]', '}'); return true;
@ -84,7 +85,7 @@ export class TextWrapper {
this.envelopeWith('(', ')'); this.envelopeWith('(', ')');
this.ref.view.dispatch({ this.ref.view.dispatch({
selection: { selection: {
anchor: this.ref.view.state.selection.main.from + 1, anchor: hasSelection ? this.ref.view.state.selection.main.to: this.ref.view.state.selection.main.from + 1,
} }
}); });
return true; return true;
@ -93,15 +94,14 @@ export class TextWrapper {
this.envelopeWith('[', ']'); this.envelopeWith('[', ']');
this.ref.view.dispatch({ this.ref.view.dispatch({
selection: { selection: {
anchor: this.ref.view.state.selection.main.from + 1, anchor: hasSelection ? this.ref.view.state.selection.main.to: this.ref.view.state.selection.main.from + 1,
} }
}); });
return true; return true;
} }
case TokenID.BOOLEAN: { case TokenID.BOOLEAN: {
const selStart = this.ref.view.state.selection.main.from; const selStart = this.ref.view.state.selection.main.from;
if (selStart !== this.ref.view.state.selection.main.to && if (hasSelection && this.ref.view.state.sliceDoc(selStart, selStart + 1) === 'ℬ') {
this.ref.view.state.sliceDoc(selStart, selStart + 1) === 'ℬ') {
this.envelopeWith('ℬ', ''); this.envelopeWith('ℬ', '');
} else { } else {
this.envelopeWith('ℬ(', ')'); this.envelopeWith('ℬ(', ')');