Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/Tools/VSCode/extension/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 5 kB

Quelle lsp.ts Sprache: unbekannt

/*  Author:     Makarius
    Author:     Thomas Lindae, TU Muenchen
    Author:     Diana Korchmar, LMU Muenchen

Message formats for Language Server Protocol, with adhoc PIDE extensions
(see Tools/VSCode/src/lsp.scala).
*/

'use strict';

import { MarkdownString } from 'vscode'
import { NotificationType, RequestType0 } from 'vscode-languageclient'

/* decorations */

export interface Decoration_Options {
  range: number[],
  hover_message?: MarkdownString | MarkdownString[]
}

export interface Decoration
{
  "type": string
  content: Decoration_Options[]
}

export interface Document_Decorations {
  uri: string
  entries: Decoration[]
}

export const decoration_type =
  new NotificationType<Document_Decorations>("PIDE/decoration")

export interface Decoration_Request
{
  uri: string
}

export const decoration_request_type =
  new NotificationType<Decoration_Request>("PIDE/decoration_request")

/* caret handling */

export interface Caret_Update
{
  uri?: string
  line?: number
  character?: number
  focus?: boolean
}

export const caret_update_type =
  new NotificationType<Caret_Update>("PIDE/caret_update")

/* dynamic output */

export interface Dynamic_Output
{
  content: string
}

export const dynamic_output_type =
  new NotificationType<Dynamic_Output>("PIDE/dynamic_output")

export interface Output_Set_Margin
{
  margin: number
}

export const output_set_margin_type =
  new NotificationType<Output_Set_Margin>("PIDE/output_set_margin")

/* state */

export interface State_Output
{
  id: number
  content: string
  auto_update: boolean
}

export const state_output_type =
  new NotificationType<State_Output>("PIDE/state_output")

export interface State_Set_Margin
{
  id: number
  margin: number
}

export const state_set_margin_type =
  new NotificationType<State_Set_Margin>("PIDE/state_set_margin")

export interface State_Id
{
  id: number
}

export interface Auto_Update
{
  id: number
  enabled: boolean
}

export const state_init_type = new RequestType0("PIDE/state_init")
export const state_exit_type = new NotificationType<State_Id>("PIDE/state_exit")
export const state_locate_type = new NotificationType<State_Id>("PIDE/state_locate")
export const state_update_type = new NotificationType<State_Id>("PIDE/state_update")
export const state_auto_update_type = new NotificationType<Auto_Update>("PIDE/state_auto_update")

/* preview */

export interface Preview_Request
{
  uri: string
  column: number
}

export interface Preview_Response
{
  uri: string
  column: number
  label: string
  content: string
}

export const preview_request_type =
  new NotificationType<Preview_Request>("PIDE/preview_request")

export const preview_response_type =
  new NotificationType<Preview_Response>("PIDE/preview_response")

/* abbrevs */

export interface Abbrevs_Response {
  abbrevs: [string, string][];
}

export const abbrevs_request_type =
  new NotificationType<void>("PIDE/abbrevs_request")

export const abbrevs_response_type =
  new NotificationType<Abbrevs_Response>("PIDE/abbrevs_response");

/* documentation */

export const documentation_request_type =
  new NotificationType<void>("PIDE/documentation_request")

export interface Doc_Entry {
  print_html: string;
  platform_path: string;
}

export interface Doc_Section {
  title: string;
  important: boolean;
  entries: Array<Doc_Entry>;
}

export interface Documentation_Response {
  sections: Array<Doc_Section>;
}

export const documentation_response_type =
  new NotificationType<Documentation_Response>("PIDE/documentation_response");

/* Sledgehammer */

export interface Sledgehammer_Request {
  provers: string;
  isar: boolean;
  try0: boolean;
}

export interface Sledgehammer_Status {
  message: string;
}

export interface Sledgehammer_Output {
  content: string;
  position: {
    uri: string;
    line: number;
    character: number;
  };
  sendback_id: number;
  state_location: {
    uri: string;
    line: number;
    character: number;
  };
}

export interface Sledgehammer_Sendback {
  text: string;
}

export interface Sledgehammer_Insert {
  uri: string;
  line: number;
  character: number;
  text: string;
}

export interface Sledgehammer_Provers {
  provers: string;
}

export const sledgehammer_request_type =
  new NotificationType<Sledgehammer_Request>("PIDE/sledgehammer_request");

export const sledgehammer_cancel_type =
  new NotificationType<void>("PIDE/sledgehammer_cancel");

export const sledgehammer_locate_type =
  new NotificationType<void>("PIDE/sledgehammer_locate");

export const sledgehammer_sendback_type =
  new NotificationType<Sledgehammer_Sendback>("PIDE/sledgehammer_sendback");

export const sledgehammer_insert_type =
  new NotificationType<Sledgehammer_Insert>("PIDE/sledgehammer_insert");

export const sledgehammer_provers_request_type =
  new NotificationType<void>("PIDE/sledgehammer_provers_request");

export const sledgehammer_provers_response_type =
  new NotificationType<Sledgehammer_Provers>("PIDE/sledgehammer_provers_response");

export const sledgehammer_status_type =
  new NotificationType<Sledgehammer_Status>("PIDE/sledgehammer_status");

export const sledgehammer_output_type =
  new NotificationType<Sledgehammer_Output>("PIDE/sledgehammer_output");

/* spell checker */

export const include_word_type =
  new NotificationType<void>("PIDE/include_word")

export const include_word_permanently_type =
  new NotificationType<void>("PIDE/include_word_permanently")

export const exclude_word_type =
  new NotificationType<void>("PIDE/exclude_word")

export const exclude_word_permanently_type =
  new NotificationType<void>("PIDE/exclude_word_permanently")

export const reset_words_type =
  new NotificationType<void>("PIDE/reset_words")