Skip to content

Commit

Permalink
Merge pull request #559 from coq-community/goal-pp
Browse files Browse the repository at this point in the history 
Syntax highlighting in proofview
  • Loading branch information
@maximedenes
maximedenes authored Aug 7, 2023
2 parents 7f19d3f + 83fb323 commit 60230e0
Show file tree
Hide file tree
Showing 14 changed files with 246 additions and 24 deletions.
47 changes: 46 additions & 1 deletion client/goal-view-ui/src/components/atoms/Goal.module.css
View file
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
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
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
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
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
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
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
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
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
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
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
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
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

0 comments on commit 60230e0

Please sign in to comment.