Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Syntax highlighting in proofview #559

Merged
merged 1 commit into from
Aug 7, 2023
Merged

Syntax highlighting in proofview #559

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
47 changes: 46 additions & 1 deletion client/goal-view-ui/src/components/atoms/Goal.module.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,4 +4,49 @@
white-space: pre-wrap;
width: 100%;
margin-top: 6px;
}
}

.constr-notation {
color: var(--vscode-coq-termNotation);
}
.constr-keyword {
color: var(--vscode-coq-termKeyword);
}
.constr-evar {
color: var(--vscode-coq-termEvar);
font-style: italic;
}
.constr-path {
color: var(--vscode-coq-termPath);
}
.constr-reference {
color: var(--vscode-coq-termReference);
}
.constr-type {
color: var(--vscode-coq-termType);
}
.constr-variable {
color: var(--vscode-coq-termVariable);
}
.message-debug {
color: var(--vscode-coq-debugMessage);
}
.message-error {
color: var(--vscode-coq-errorMessage);
text-decoration: underline;
}
.message-warning {
color: var(--vscode-coq-warningMessage);
}
.module-keyword {
color: var(--vscode-coq-moduleKeyword);
}
.tactic-keyword {
color: var(--vscode-coq-tacticKeyword);
}
.tactic-primitive {
color: var(--vscode-coq-tacticPrimitive);
}
.tactic-string {
color: var(--vscode-coq-tacticString);
}
6 changes: 4 additions & 2 deletions client/goal-view-ui/src/components/atoms/Goal.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,11 @@
import React, {FunctionComponent} from 'react';

import classes from './Goal.module.css';
import { PpString } from '../../types';
import { fragmentOfPpString } from '../../utilities/pp';

type GoalProps = {
goal: string,
goal: PpString,
};

const goal : FunctionComponent<GoalProps> = (props) => {
Expand All @@ -12,7 +14,7 @@ const goal : FunctionComponent<GoalProps> = (props) => {

return (
<div className={classes.Goal}>
{goal}
{fragmentOfPpString(goal, classes)}
</div>
);
};
Expand Down
45 changes: 45 additions & 0 deletions client/goal-view-ui/src/components/atoms/Hypothesis.module.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,3 +24,48 @@
.Type {
color: var(--vscode-editor-foreground);
}

.constr-notation {
color: var(--vscode-coq-termNotation);
}
.constr-keyword {
color: var(--vscode-coq-termKeyword);
}
.constr-evar {
color: var(--vscode-coq-termEvar);
font-style: italic;
}
.constr-path {
color: var(--vscode-coq-termPath);
}
.constr-reference {
color: var(--vscode-coq-termReference);
}
.constr-type {
color: var(--vscode-coq-termType);
}
.constr-variable {
color: var(--vscode-coq-termVariable);
}
.message-debug {
color: var(--vscode-coq-debugMessage);
}
.message-error {
color: var(--vscode-coq-errorMessage);
text-decoration: underline;
}
.message-warning {
color: var(--vscode-coq-warningMessage);
}
.module-keyword {
color: var(--vscode-coq-moduleKeyword);
}
.tactic-keyword {
color: var(--vscode-coq-tacticKeyword);
}
.tactic-primitive {
color: var(--vscode-coq-tacticPrimitive);
}
.tactic-string {
color: var(--vscode-coq-tacticString);
}
8 changes: 5 additions & 3 deletions client/goal-view-ui/src/components/atoms/Hypothesis.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,12 @@
import React, {FunctionComponent} from 'react';

import classes from './Hypothesis.module.css';
import { PpString } from '../../types';
import { fragmentOfPpString } from '../../utilities/pp';

type HypothesisProps = {
identifiers: string[],
type: string,
type: PpString,
};

const hypothesis: FunctionComponent<HypothesisProps> = (props) => {
Expand All @@ -21,10 +23,10 @@ const hypothesis: FunctionComponent<HypothesisProps> = (props) => {
<span className={classes.Identifier}>{idString}</span>
<span className={classes.Separator}> : </span>
</span>
<span className={classes.Type}>{type}</span>
<span className={classes.Type}>{fragmentOfPpString(type, classes)}</span>
<br/>
</li>
);
};

export default hypothesis;
export default hypothesis;
5 changes: 3 additions & 2 deletions client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,15 @@ import {VscChevronDown} from 'react-icons/vsc';
import GoalBlock from './GoalBlock';

import classes from './GoalBlock.module.css';
import { PpString } from '../../types';

type CollapsibleGoalBlockProps = {
goal: {
id: string,
goal: string,
goal: PpString,
hypotheses: {
identifiers: string[],
type: string,
type: PpString,
}[]
},
collapseHandler: (id: string) => void,
Expand Down
5 changes: 3 additions & 2 deletions client/goal-view-ui/src/components/molecules/GoalBlock.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,15 @@ import Goal from '../atoms/Goal';
import Separator from '../atoms/Separator';

import classes from './GoalBlock.module.css';
import { PpString } from '../../types';

type GoalBlockProps = {
goal: {
id: string,
goal: string,
goal: PpString,
hypotheses: {
identifiers: string[],
type: string,
type: PpString,
}[]
}
};
Expand Down
3 changes: 2 additions & 1 deletion client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,12 @@ import React, {FunctionComponent} from 'react';
import Hypothesis from '../atoms/Hypothesis';

import classes from './HypothesesBlock.module.css';
import { PpString } from '../../types';

type HypothesesBlockProps = {
hypotheses: {
identifiers: string[],
type: string,
type: PpString,
}[];
};

Expand Down
5 changes: 3 additions & 2 deletions client/goal-view-ui/src/components/organisms/GoalTabs.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,14 +8,15 @@ import { VscPass } from 'react-icons/vsc';

import GoalBlock from '../molecules/GoalBlock';
import EmptyState from '../atoms/EmptyState';
import { PpString } from '../../types';

type GoalSectionProps = {
goals: {
id: string,
goal: string,
goal: PpString,
hypotheses: {
identifiers: string[],
type: string
type: PpString
}[]
}[];
};
Expand Down
24 changes: 22 additions & 2 deletions client/goal-view-ui/src/types.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,31 @@
import { integer } from "vscode-languageclient";
type Nullable<T> = T | null;

export type PpTag = string;

export type BlockType =
| ["Pp_hbox"]
| ["Pp_vbox", integer]
| ["Pp_hvbox", integer]
| ["Pp_hovbox", integer];

export type PpString =
| ["Ppcmd_empty"]
| ["Ppcmd_string", string]
| ["Ppcmd_glue", PpString[]]
| ["Ppcmd_box", BlockType, PpString]
| ["Ppcmd_tag", PpTag, PpString]
| ["Ppcmd_print_break", integer, integer]
| ["Ppcmd_force_newline"]
| ["Ppcmd_comment", string[]];


export type Goal = {
id: string,
goal: string,
goal: PpString,
hypotheses: {
identifiers: string[],
type: string
type: PpString
}[],
isOpen: boolean,
displayId: number
Expand Down
23 changes: 23 additions & 0 deletions client/goal-view-ui/src/utilities/pp.tsx
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
import { ReactElement, ReactFragment } from 'react';
import { PpString } from '../types';

export const fragmentOfPpString = (pp:PpString, classes:CSSModuleClasses) : ReactFragment => {
switch (pp[0]) {
case "Ppcmd_empty":
return <></>;
case "Ppcmd_string":
return pp[1];
case "Ppcmd_glue":
return pp[1].map(pp => fragmentOfPpString(pp, classes));
case "Ppcmd_box":
return fragmentOfPpString(pp[2], classes);
case "Ppcmd_tag":
return <span className={classes[pp[1].replace(".", "-")]}>{fragmentOfPpString(pp[2], classes)}</span>;
case "Ppcmd_print_break":
return " ".repeat(pp[1]);
case "Ppcmd_force_newline":
return <br/>;
case "Ppcmd_comment":
return pp[1];
}
};
24 changes: 21 additions & 3 deletions client/src/protocol/types.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,25 @@ export enum FeedbackChannel {
info,
notice,
ignore
}
}

export type PpTag = string;

export type BlockType =
| ["Pp_hbox"]
| ["Pp_vbox", integer]
| ["Pp_hvbox", integer]
| ["Pp_hovbox", integer];

export type PpString =
| ["Ppcmd_empty"]
| ["Ppcmd_string", string]
| ["Ppcmd_glue", PpString[]]
| ["Ppcmd_box", BlockType, PpString]
| ["Ppcmd_tag", PpTag, PpString]
| ["Ppcmd_print_break", integer, integer]
| ["Ppcmd_force_newline"]
| ["Ppcmd_comment", string[]];

export interface CoqFeedback {
range: Range;
Expand All @@ -23,12 +41,12 @@ export interface CoqFeedbackNotification {

export interface Hypothesis {
identifiers: string[];
type: string;
type: PpString;
}

export interface Goal {
id: integer;
goal: string;
goal: PpString;
hypotheses: Hypothesis[];
}
interface ProofViewNotificationType {
Expand Down
43 changes: 43 additions & 0 deletions language-server/lsp/printing.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
(**************************************************************************)
(* *)
(* VSCoq *)
(* *)
(* Copyright INRIA and contributors *)
(* (see version control and README file for authors & dates) *)
(* *)
(**************************************************************************)
(* *)
(* This file is distributed under the terms of the MIT License. *)
(* See LICENSE file. *)
(* *)
(**************************************************************************)

type pp_tag = string [@@deriving yojson]

type block_type = Pp.block_type =
| Pp_hbox
| Pp_vbox of int
| Pp_hvbox of int
| Pp_hovbox of int
[@@deriving yojson]

type pp =
| Ppcmd_empty
| Ppcmd_string of string
| Ppcmd_glue of pp list
| Ppcmd_box of block_type * pp
| Ppcmd_tag of pp_tag * pp
| Ppcmd_print_break of int * int
| Ppcmd_force_newline
| Ppcmd_comment of string list
[@@deriving yojson]

let rec pp_of_coqpp t = match Pp.repr t with
| Pp.Ppcmd_empty -> Ppcmd_empty
| Pp.Ppcmd_string s -> Ppcmd_string s
| Pp.Ppcmd_glue l -> Ppcmd_glue (List.map pp_of_coqpp l)
| Pp.Ppcmd_box (bt, pp) -> Ppcmd_box (bt, pp_of_coqpp pp)
| Pp.Ppcmd_tag (tag, pp) -> Ppcmd_tag (tag, pp_of_coqpp pp)
| Pp.Ppcmd_print_break (m,n) -> Ppcmd_print_break (m,n)
| Pp.Ppcmd_force_newline -> Ppcmd_force_newline
| Pp.Ppcmd_comment l -> Ppcmd_comment l
17 changes: 17 additions & 0 deletions language-server/lsp/printing.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
(**************************************************************************)
(* *)
(* VSCoq *)
(* *)
(* Copyright INRIA and contributors *)
(* (see version control and README file for authors & dates) *)
(* *)
(**************************************************************************)
(* *)
(* This file is distributed under the terms of the MIT License. *)
(* See LICENSE file. *)
(* *)
(**************************************************************************)

type pp [@@deriving yojson]

val pp_of_coqpp : Pp.t -> pp
Loading