From 83fb32336bec9fe5addc5837ebd4241e8377b217 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Maxime=20D=C3=A9n=C3=A8s?= Date: Mon, 7 Aug 2023 07:33:31 +0200 Subject: [PATCH] Syntax highlighting in proofview Fixes #549. --- .../src/components/atoms/Goal.module.css | 47 ++++++++++++++++++- .../src/components/atoms/Goal.tsx | 6 ++- .../components/atoms/Hypothesis.module.css | 45 ++++++++++++++++++ .../src/components/atoms/Hypothesis.tsx | 8 ++-- .../molecules/CollapsibleGoalBlock.tsx | 5 +- .../src/components/molecules/GoalBlock.tsx | 5 +- .../components/molecules/HypothesesBlock.tsx | 3 +- .../src/components/organisms/GoalTabs.tsx | 5 +- client/goal-view-ui/src/types.ts | 24 +++++++++- client/goal-view-ui/src/utilities/pp.tsx | 23 +++++++++ client/src/protocol/types.ts | 24 ++++++++-- language-server/lsp/printing.ml | 43 +++++++++++++++++ language-server/lsp/printing.mli | 17 +++++++ language-server/lsp/proofState.ml | 15 +++--- 14 files changed, 246 insertions(+), 24 deletions(-) create mode 100644 client/goal-view-ui/src/utilities/pp.tsx create mode 100644 language-server/lsp/printing.ml create mode 100644 language-server/lsp/printing.mli diff --git a/client/goal-view-ui/src/components/atoms/Goal.module.css b/client/goal-view-ui/src/components/atoms/Goal.module.css index 04551247c..02ded75ca 100644 --- a/client/goal-view-ui/src/components/atoms/Goal.module.css +++ b/client/goal-view-ui/src/components/atoms/Goal.module.css @@ -4,4 +4,49 @@ white-space: pre-wrap; width: 100%; margin-top: 6px; -} \ No newline at end of file +} + +.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); +} diff --git a/client/goal-view-ui/src/components/atoms/Goal.tsx b/client/goal-view-ui/src/components/atoms/Goal.tsx index 6a18e95f7..96b358fc1 100644 --- a/client/goal-view-ui/src/components/atoms/Goal.tsx +++ b/client/goal-view-ui/src/components/atoms/Goal.tsx @@ -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 = (props) => { @@ -12,7 +14,7 @@ const goal : FunctionComponent = (props) => { return (
- {goal} + {fragmentOfPpString(goal, classes)}
); }; diff --git a/client/goal-view-ui/src/components/atoms/Hypothesis.module.css b/client/goal-view-ui/src/components/atoms/Hypothesis.module.css index a043ab7dd..cfa96cca7 100644 --- a/client/goal-view-ui/src/components/atoms/Hypothesis.module.css +++ b/client/goal-view-ui/src/components/atoms/Hypothesis.module.css @@ -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); +} \ No newline at end of file diff --git a/client/goal-view-ui/src/components/atoms/Hypothesis.tsx b/client/goal-view-ui/src/components/atoms/Hypothesis.tsx index 7d3939f7d..b2264a4fe 100644 --- a/client/goal-view-ui/src/components/atoms/Hypothesis.tsx +++ b/client/goal-view-ui/src/components/atoms/Hypothesis.tsx @@ -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 = (props) => { @@ -21,10 +23,10 @@ const hypothesis: FunctionComponent = (props) => { {idString} : - {type} + {fragmentOfPpString(type, classes)}
); }; -export default hypothesis; \ No newline at end of file +export default hypothesis; diff --git a/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx b/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx index e2909644e..55f6b2931 100644 --- a/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx +++ b/client/goal-view-ui/src/components/molecules/CollapsibleGoalBlock.tsx @@ -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, diff --git a/client/goal-view-ui/src/components/molecules/GoalBlock.tsx b/client/goal-view-ui/src/components/molecules/GoalBlock.tsx index 6e04fa739..e8654a030 100644 --- a/client/goal-view-ui/src/components/molecules/GoalBlock.tsx +++ b/client/goal-view-ui/src/components/molecules/GoalBlock.tsx @@ -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, }[] } }; diff --git a/client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx b/client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx index 0f32fe39b..844524987 100644 --- a/client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx +++ b/client/goal-view-ui/src/components/molecules/HypothesesBlock.tsx @@ -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, }[]; }; diff --git a/client/goal-view-ui/src/components/organisms/GoalTabs.tsx b/client/goal-view-ui/src/components/organisms/GoalTabs.tsx index e45accb01..bf03556ce 100644 --- a/client/goal-view-ui/src/components/organisms/GoalTabs.tsx +++ b/client/goal-view-ui/src/components/organisms/GoalTabs.tsx @@ -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 }[] }[]; }; diff --git a/client/goal-view-ui/src/types.ts b/client/goal-view-ui/src/types.ts index 4b1e4cb68..dec02702a 100644 --- a/client/goal-view-ui/src/types.ts +++ b/client/goal-view-ui/src/types.ts @@ -1,11 +1,31 @@ +import { integer } from "vscode-languageclient"; type Nullable = 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 diff --git a/client/goal-view-ui/src/utilities/pp.tsx b/client/goal-view-ui/src/utilities/pp.tsx new file mode 100644 index 000000000..872221d2f --- /dev/null +++ b/client/goal-view-ui/src/utilities/pp.tsx @@ -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 {fragmentOfPpString(pp[2], classes)}; + case "Ppcmd_print_break": + return " ".repeat(pp[1]); + case "Ppcmd_force_newline": + return
; + case "Ppcmd_comment": + return pp[1]; + } +}; diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts index 097d44e50..83da7e746 100644 --- a/client/src/protocol/types.ts +++ b/client/src/protocol/types.ts @@ -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; @@ -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 { diff --git a/language-server/lsp/printing.ml b/language-server/lsp/printing.ml new file mode 100644 index 000000000..ccb19cfa3 --- /dev/null +++ b/language-server/lsp/printing.ml @@ -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 \ No newline at end of file diff --git a/language-server/lsp/printing.mli b/language-server/lsp/printing.mli new file mode 100644 index 000000000..a1370a7fc --- /dev/null +++ b/language-server/lsp/printing.mli @@ -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 diff --git a/language-server/lsp/proofState.ml b/language-server/lsp/proofState.ml index 9e4b35405..559d32066 100644 --- a/language-server/lsp/proofState.ml +++ b/language-server/lsp/proofState.ml @@ -11,17 +11,20 @@ (* See LICENSE file. *) (* *) (**************************************************************************) + +open Printing + type hyp = { identifiers: string list; - type_ : string; [@key "type"] + type_ : pp; [@key "type"] diff: string; - body: string option; [@yojson.option] + body: pp option; [@yojson.option] } [@@deriving yojson] type goal = { id: int; hypotheses: hyp list; - goal: string; + goal: pp; } [@@deriving yojson] type t = { @@ -58,9 +61,9 @@ let mk_goal env sigma g = let typ = pr_letype_env env sigma typ in let hyp = { identifiers = ids; - type_ = Pp.string_of_ppcmds typ; + type_ = pp_of_coqpp typ; diff = "None"; - body = Option.map (fun body -> Pp.string_of_ppcmds @@ pr_leconstr_env ~inctx:true env sigma body) body; + body = Option.map (fun body -> pp_of_coqpp @@ pr_leconstr_env ~inctx:true env sigma body) body; } in (env', hyp :: l) in @@ -70,7 +73,7 @@ let mk_goal env sigma g = { id; hypotheses = List.rev hyps; - goal = Pp.string_of_ppcmds ccl; + goal = pp_of_coqpp ccl; } let get_proof st =