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

Better highlights #744

Merged
merged 5 commits into from
May 31, 2024
Merged

Better highlights #744

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7fb3301
Process highlights as execution happens.
rtetley Feb 21, 2024
66dc43c
Allow for getting overview until specific range.
rtetley Feb 22, 2024
adfa409
Change exec_overview handling. Handle processing ranges.
rtetley Feb 22, 2024
7d9d3b8
Add prepared range.
rtetley Mar 28, 2024
1870fac
Add support for delegated proofs.
rtetley Mar 28, 2024
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
6 changes: 3 additions & 3 deletions client/src/Decorations.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ import * as vscode from 'vscode';
import { DidChangeConfigurationParams } from 'vscode-languageclient';

interface Decorations {
parsed: vscode.TextEditorDecorationType;
prepared: vscode.TextEditorDecorationType;
processing: vscode.TextEditorDecorationType;
processed: vscode.TextEditorDecorationType
}
Expand All @@ -20,7 +20,7 @@ export function initializeDecorations(context: vscode.ExtensionContext) {
}

decorationsContinuous = {
parsed: create({
prepared: create({
overviewRulerColor: 'cyan',
overviewRulerLane: vscode.OverviewRulerLane.Right,
}),
Expand All @@ -35,7 +35,7 @@ export function initializeDecorations(context: vscode.ExtensionContext) {
};

decorationsManual = {
parsed: create({
prepared: create({
outlineWidth: '1px',
outlineStyle: 'solid',
overviewRulerColor: 'cyan',
Expand Down
46 changes: 38 additions & 8 deletions client/src/client.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,9 @@ import {decorationsManual, decorationsContinuous} from './Decorations';
export default class Client extends LanguageClient {

private static _channel: any = vscode.window.createOutputChannel('VsCoq');
private _decorations: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
private _decorationsPrepared: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
private _decorationsProcessed: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();
private _decorationsProcessing: Map<String, vscode.Range[]> = new Map<String, vscode.Range[]>();

constructor(
serverOptions: ServerOptions,
Expand All @@ -32,18 +34,26 @@ export default class Client extends LanguageClient {
Client._channel.appendLine(message);
}

public saveHighlights(uri: String, processingRange: vscode.Range[], processedRange: vscode.Range[]) {
this._decorations.set(uri, processedRange);
public saveHighlights(uri: String, preparedRange: vscode.Range[], processingRange: vscode.Range[], processedRange: vscode.Range[]) {
this._decorationsPrepared.set(uri, preparedRange);
this._decorationsProcessing.set(uri, processingRange);
this._decorationsProcessed.set(uri, processedRange);
}

public updateHightlights() {
for(let entry of this._decorations.entries()) {
for(let entry of this._decorationsPrepared.entries()) {
this.updateDocumentEditors(entry[0], entry[1], "prepared");
}
for(let entry of this._decorationsProcessing.entries()) {
this.updateDocumentEditors(entry[0], entry[1], "processing");
}
for(let entry of this._decorationsProcessed.entries()) {
this.updateDocumentEditors(entry[0], entry[1]);
}
};

public resetHighlights() {
for(let entry of this._decorations.entries()) {
for(let entry of this._decorationsProcessed.entries()) {
this.resetDocumentEditors(entry[0]);
}
}
Expand All @@ -57,19 +67,39 @@ export default class Client extends LanguageClient {
private resetDocumentEditors(uri: String) {
const editors = this.getDocumentEditors(uri);
editors.map(editor => {
editor.setDecorations(decorationsManual.prepared, []);
editor.setDecorations(decorationsContinuous.prepared, []);
editor.setDecorations(decorationsManual.processing, []);
editor.setDecorations(decorationsContinuous.processing, []);
editor.setDecorations(decorationsManual.processed, []);
editor.setDecorations(decorationsContinuous.processed, []);
});
}

private updateDocumentEditors(uri: String, ranges: vscode.Range[]) {
private updateDocumentEditors(uri: String, ranges: vscode.Range[], type: String = "processed") {
const config = vscode.workspace.getConfiguration('vscoq.proof');
const editors = this.getDocumentEditors(uri);
editors.map(editor => {
if(config.mode === 0) {
editor.setDecorations(decorationsManual.processed, ranges);
if(type === "prepared") {
editor.setDecorations(decorationsManual.prepared, ranges);
}
if(type === "processing") {
editor.setDecorations(decorationsManual.processing, ranges);
}
if (type === "processed") {
editor.setDecorations(decorationsManual.processed, ranges);
}
} else {
editor.setDecorations(decorationsContinuous.processed, ranges);
if(type === "prepared") {
editor.setDecorations(decorationsContinuous.prepared, ranges);
}
if(type === "processing") {
editor.setDecorations(decorationsContinuous.processing, ranges);
}
if (type === "processed") {
editor.setDecorations(decorationsContinuous.processed, ranges);
}
}
});
}
Expand Down
1 change: 1 addition & 0 deletions client/src/extension.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -216,6 +216,7 @@ export function activate(context: ExtensionContext) {

client.saveHighlights(
notification.uri,
notification.preparedRange,
notification.processingRange,
notification.processedRange
);
Expand Down
3 changes: 2 additions & 1 deletion client/src/protocol/types.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,8 @@ export interface ProofViewNotification {
}

export interface UpdateHighlightsNotification {
uri: Uri;
uri: Uri;
preparedRange: Range[];
processingRange: Range[];
processedRange: Range[];
}
Expand Down
137 changes: 90 additions & 47 deletions language-server/dm/documentManager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,6 +37,7 @@ type state = {
document : Document.document;
execution_state : ExecutionManager.state;
observe_id : observe_id option;
overview: exec_overview;
}

type event =
Expand All @@ -61,48 +62,76 @@ let inject_em_events events = List.map inject_em_event events

type events = event Sel.Event.t list

type exec_overview = {
processing : Range.t list;
processed : Range.t list;
}

let merge_adjacent_ranges (r1,l) r2 =
if Position.compare r1.Range.end_ r2.Range.start == 0 then
Range.{ start = r1.Range.start; end_ = r2.Range.end_ }, l
else
r2, r1 :: l

let compress_sorted_ranges = function
| [] -> []
| range :: tl ->
let r, l = List.fold_left merge_adjacent_ranges (range,[]) tl in
r :: l

let compress_ranges ranges =
let ranges = List.sort (fun { Range.start = s1 } { Range.start = s2 } -> Position.compare s1 s2) ranges in
compress_sorted_ranges ranges

let executed_ranges doc execution_state loc =
let ranges_of l =
compress_ranges @@ List.map (Document.range_of_id_with_blank_space doc) l
in
let ids_before_loc = List.map (fun s -> s.Document.id) @@ Document.sentences_before doc loc in
let processed_ids = List.filter (fun x -> ExecutionManager.is_executed execution_state x || ExecutionManager.is_remotely_executed execution_state x) ids_before_loc in
log @@ Printf.sprintf "highlight: processed: %s" (String.concat " " (List.map Stateid.to_string processed_ids));
{
processing = [];
processed = ranges_of processed_ids;
}
let print_exec_overview st =
let {processing; processed; prepared} = st.overview in
log @@ "--------- Prepared ranges ---------";
List.iter (fun r -> log @@ Range.to_string r) prepared;
log @@ "-------------------------------------";
log @@ "--------- Processing ranges ---------";
List.iter (fun r -> log @@ Range.to_string r) processing;
log @@ "-------------------------------------";
log @@ "--------- Processed ranges ---------";
List.iter (fun r -> log @@ Range.to_string r) processed;
log @@ "-------------------------------------"

let overview_until_range st range =
let find_final_range l = List.find_opt (fun (r: Range.t) -> Range.included ~in_:r range) l in
let {processed; processing; prepared} = st.overview in
let final_range = find_final_range processed in
match final_range with
| None ->
let final_range = find_final_range processing in
begin match final_range with
| None -> { processed; processing; prepared }
| Some { start } ->
let processing = (List.filter (fun (r: Range.t) -> not @@ Range.included ~in_:r range) processing) in
let processing = List.append processing [Range.create ~start:start ~end_:range.end_] in
{processing; processed; prepared}
end
| Some { start } ->
let processed = (List.filter (fun (r: Range.t) -> not @@ Range.included ~in_:r range) processed) in
let processed = List.append processed [Range.create ~start:start ~end_:range.end_] in
{ processing; processed; prepared }

let prepare_overview st id =
match Document.get_sentence st.document id with
| None -> st (*Can't find the sentence, just return the state as is*)
| Some { id } ->
(* Sentence already executed, no need to prepare*)
if ExecutionManager.is_executed st.execution_state id then
st
else
(* Create the correct prepared range *)
begin match st.observe_id with
| None -> st (* No observe_id means continuous mode, no need to do anything*)
| Some Top ->
(* Create range from first sentence to id *)
let range = Document.range_of_id_with_blank_space st.document id in
let start = Position.create ~character:0 ~line:0 in
let range = Range.create ~end_: range.end_ ~start: start in
let prepared = [range] in
let overview = {st.overview with prepared} in
{st with overview}
| Some (Id o_id) ->
(* Create range from o_id to id*)
let o_range = Document.range_of_id_with_blank_space st.document o_id in
let range = Document.range_of_id_with_blank_space st.document id in
if Position.compare o_range.end_ range.end_ < 0 then
let range = Range.create ~end_: range.end_ ~start: o_range.end_ in
let prepared = [range] in
let overview = {st.overview with prepared} in
{st with overview}
else
st
end

let executed_ranges st =
let loc = match st.observe_id with
| None -> max_int
| Some Top -> 0
| Some (Id id) -> match Document.get_sentence st.document id with
| None -> failwith "observe_id does not exist"
| Some { stop } -> stop
in
executed_ranges st.document st.execution_state loc
match st.observe_id with
| None -> st.overview
| Some Top -> { processing = []; processed = []; prepared = []; }
| Some (Id id) ->
let range = Document.range_of_id st.document id in
overview_until_range st range

let observe_id_range st =
let doc = Document.raw_document st.document in
Expand Down Expand Up @@ -177,13 +206,13 @@ let observe ~background state id : (state * event Sel.Event.t list) =
match Document.get_sentence state.document id with
| None -> (state, []) (* TODO error? *)
| Some {id } ->
let vst_for_next_todo, todo = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
let vst_for_next_todo, todo, _ = ExecutionManager.build_tasks_for (Document.schedule state.document) state.execution_state id in
if CList.is_empty todo then
(state, [])
else
let priority = if background then None else Some PriorityManager.execution in
let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started = Unix.gettimeofday (); background }) in
(state, [ event ])
(state, [ event ] )

let clear_observe_id st =
{ st with observe_id = None }
Expand All @@ -192,6 +221,7 @@ let reset_to_top st =
{ st with observe_id = Some Top }

let interpret_to st id =
let st = prepare_overview st id in
let observe_id = if st.observe_id = None then None else (Some (Id id)) in
let st = { st with observe_id} in
observe ~background:false st id
Expand Down Expand Up @@ -291,7 +321,8 @@ let init init_vs ~opts uri ~text observe_id =
let init_vs = Vernacstate.freeze_full_state () in
let document = Document.create_document init_vs.Vernacstate.synterp text in
let execution_state, feedback = ExecutionManager.init init_vs in
let st = { uri; opts; init_vs; document; execution_state; observe_id } in
let overview = { processing = []; processed = []; prepared = []} in
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

nitpick: define an empty_overview since you do this twice

let st = { uri; opts; init_vs; document; execution_state; observe_id; overview } in
validate_document st, [inject_em_event feedback]

let reset { uri; opts; init_vs; document; execution_state; observe_id } =
Expand All @@ -301,7 +332,8 @@ let reset { uri; opts; init_vs; document; execution_state; observe_id } =
ExecutionManager.destroy execution_state;
let execution_state, feedback = ExecutionManager.init init_vs in
let observe_id = if observe_id = None then None else (Some Top) in
let st = { uri; opts; init_vs; document; execution_state; observe_id} in
let overview = { processing = []; processed = []; prepared = []} in
let st = { uri; opts; init_vs; document; execution_state; observe_id; overview } in
validate_document st, [inject_em_event feedback]

let apply_text_edits state edits =
Expand All @@ -318,7 +350,7 @@ let apply_text_edits state edits =
let handle_event ev st =
match ev with
| Execute { id; todo = []; started } -> (* the vst_for_next_todo is also in st.execution_state *)
let time = Unix.gettimeofday () -. started in
let time = Unix.gettimeofday () -. started in
log (Printf.sprintf "ExecuteToLoc %d ends after %2.3f" (Stateid.to_int id) time);
(* We update the state to trigger a publication of diagnostics *)
(Some st, [])
Expand All @@ -330,9 +362,20 @@ let handle_event ev st =
executing *)
let priority = if background then None else Some PriorityManager.execution in
let event = Sel.now ?priority (Execute {id; vst_for_next_todo; todo; started; background }) in
(Some {st with execution_state}, inject_em_events events @ [event])
let overview = ExecutionManager.update_overview task todo execution_state st.document st.overview in
(Some {st with execution_state; overview}, inject_em_events events @ [event])
| ExecutionManagerEvent ev ->
let execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
let id, execution_state_update, events = ExecutionManager.handle_event ev st.execution_state in
let st =
match (id, execution_state_update) with
| Some id, Some exec_st ->
let overview = ExecutionManager.update_processed id exec_st st.document st.overview in
{st with overview}
| Some id, None ->
let overview = ExecutionManager.update_processed id st.execution_state st.document st.overview in
{st with overview}
| _, _ -> st
in
(Option.map (fun execution_state -> {st with execution_state}) execution_state_update, inject_em_events events)

let get_proof st diff_mode pos =
Expand Down
7 changes: 2 additions & 5 deletions language-server/dm/documentManager.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,8 @@ val pp_event : Format.formatter -> event -> unit

type events = event Sel.Event.t list

val print_exec_overview : state -> unit

val init : Vernacstate.t -> opts:Coqargs.injection_command list -> DocumentUri.t -> text:string -> observe_id option -> state * events
(** [init st opts uri text] initializes the document manager with initial vernac state
[st] on which command line opts will be set. *)
Expand Down Expand Up @@ -78,11 +80,6 @@ val interpret_in_background : state -> (state * events)
val reset : state -> state * events
(** resets Coq *)

type exec_overview = {
processing : Range.t list;
processed : Range.t list;
}

val executed_ranges : state -> exec_overview
(** returns the ranges corresponding to the sentences
that have been executed and remotely executes *)
Expand Down
Loading
Loading