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/src/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 23 kB

Quelle lsp.scala Sprache: Scala

/*  Title:      Tools/VSCode/src/lsp.scala
    Author:     Makarius
    Author:     Thomas Lindae, TU Muenchen
    Author:     Diana Korchmar, LMU Muenchen

Message formats for Language Server Protocol, with adhoc PIDE extensions.
See https://github.com/Microsoft/language-server-protocol/blob/master/protocol.md
*/

package isabelle.vscode

import isabelle._

import java.io.{File => JFile}

object LSP {
  /* abstract message */

  object Message {
    val empty: JSON.Object.T = JSON.Object("jsonrpc" -> "2.0")

    def log(prefix: String, json: JSON.T, logger: Logger, verbose: Boolean): Unit = {
      val header =
        json match {
          case JSON.Object(obj) => obj -- (obj.keySet - "method" - "id")
          case _ => JSON.Object.empty
        }
      if (verbose || header.isEmpty) logger(prefix + "\n" + JSON.Format(json))
      else logger(prefix + " " + JSON.Format(header))
    }
  }

  /* notification */

  object Notification {
    def apply(method: String, params: JSON.T): JSON.T =
      Message.empty + ("method" -> method) + ("params" -> params)

    def unapply(json: JSON.T): Option[(String, Option[JSON.T])] =
      for {
        method <- JSON.string(json, "method")
        params = JSON.value(json, "params")
      } yield (method, params)
  }

  class Notification0(name: String) {
    def unapply(json: JSON.T): Boolean =
      json match {
        case Notification(method, _) => method == name
        case _ => false
      }
  }

  /* request message */

  object Id {
    def empty: Id = Id("")
  }

  sealed case class Id(id: Any) {
    require(
      id.isInstanceOf[Int] ||
      id.isInstanceOf[Long] ||
      id.isInstanceOf[Double] ||
      id.isInstanceOf[String], "bad id type")

    override def toString: String = id.toString
  }

  object RequestMessage {
    def apply(id: Id, method: String, params: JSON.T): JSON.T =
      Message.empty + ("id" -> id.id) + ("method" -> method) + ("params" -> params)

    def unapply(json: JSON.T): Option[(Id, String, Option[JSON.T])] =
      for {
        id <- JSON.long(json, "id") orElse JSON.double(json, "id") orElse JSON.string(json, "id")
        method <- JSON.string(json, "method")
        params = JSON.value(json, "params")
      } yield (Id(id), method, params)
  }

  class Request0(name: String) {
    def unapply(json: JSON.T): Option[Id] =
      json match {
        case RequestMessage(id, method, _) if method == name => Some(id)
        case _ => None
      }
  }

  class RequestTextDocumentPosition(name: String) {
    def unapply(json: JSON.T): Option[(Id, Line.Node_Position)] =
      json match {
        case RequestMessage(id, method, Some(TextDocumentPosition(node_pos))) if method == name =>
          Some((id, node_pos))
        case _ => None
      }
  }

  /* response message */

  object ResponseMessage {
    def apply(id: Id, result: Option[JSON.T] = None, error: Option[ResponseError] = None): JSON.T =
      Message.empty + ("id" -> id.id) ++
        JSON.optional("result" -> result) ++
        JSON.optional("error" -> error.map(_.json))

    def strict(id: Id, result: Option[JSON.T] = None, error: String = ""): JSON.T =
      if (error == "") apply(id, result = result)
      else {
        apply(id, error =
          Some(ResponseError(code = ErrorCodes.jsonrpcReservedErrorRangeEnd, message = error)))
      }

    def is_empty(json: JSON.T): Boolean =
      JSON.string(json, "id") == Some("") && JSON.value(json, "result").isDefined
  }

  sealed case class ResponseError(code: Int, message: String, data: Option[JSON.T] = None) {
    def json: JSON.T =
      JSON.Object("code" -> code, "message" -> message) ++ JSON.optional("data" -> data)
  }

  object ErrorCodes {
    val ParseError = -32700
    val InvalidRequest = -32600
    val MethodNotFound = -32601
    val InvalidParams = -32602
    val InternalError = -32603

    val jsonrpcReservedErrorRangeStart = -32099
    val ServerNotInitialized = -32002
    val UnknownErrorCode = -32001
    val jsonrpcReservedErrorRangeEnd = -32000

    val lspReservedErrorRangeStart = -32899
    val RequestFailed = -32803
    val ServerCancelled = -32802
    val ContentModified = -32801
    val RequestCancelled = -32800
    val lspReservedErrorRangeEnd = -32800
  }

  /* init and exit */

  object Initialize extends Request0("initialize") {
    def reply(id: Id, error: String): JSON.T =
      ResponseMessage.strict(
        id, Some(JSON.Object("capabilities" -> ServerCapabilities.json)), error)
  }

  object ServerCapabilities {
    val json: JSON.T =
      JSON.Object(
        "textDocumentSync" -> 2,
        "completionProvider" -> JSON.Object(
          "resolveProvider" -> false,
          "triggerCharacters" ->
            (Symbol.symbols.entries.flatMap(_.abbrevs).flatMap(_.toList).map(_.toString)
            ++ Symbol.symbols.entries.map(_.name).flatMap(_.toList).map(_.toString)).distinct
        ),
        "hoverProvider" -> true,
        "definitionProvider" -> true,
        "documentHighlightProvider" -> true,
        "codeActionProvider" -> true)
  }

  object Initialized extends Notification0("initialized")

  object Shutdown extends Request0("shutdown") {
    def reply(id: Id, error: String): JSON.T =
      ResponseMessage.strict(id, Some("OK"), error)
  }

  object Exit extends Notification0("exit")

  /* document positions */

  object Position {
    def apply(pos: Line.Position): JSON.T =
      JSON.Object("line" -> pos.line, "character" -> pos.column)

    def unapply(json: JSON.T): Option[Line.Position] =
      for {
        line <- JSON.int(json, "line")
        column <- JSON.int(json, "character")
      } yield Line.Position(line, column)
  }

  object Range {
    def compact(range: Line.Range): List[Int] =
      List(range.start.line, range.start.column, range.stop.line, range.stop.column)

    def apply(range: Line.Range): JSON.T =
      JSON.Object("start" -> Position(range.start), "end" -> Position(range.stop))

    def unapply(json: JSON.T): Option[Line.Range] =
      for {
        case Position(start) <- JSON.value(json, "start")
        case Position(stop) <- JSON.value(json, "end")
      } yield Line.Range(start, stop)
  }

  object Location {
    def apply(loc: Line.Node_Range): JSON.T =
      JSON.Object("uri" -> Url.print_file_name(loc.name), "range" -> Range(loc.range))

    def unapply(json: JSON.T): Option[Line.Node_Range] =
      for {
        uri <- JSON.string(json, "uri") if Url.is_wellformed_file(uri)
        case Range(range) <- JSON.value(json, "range")
      } yield Line.Node_Range(Url.absolute_file_name(uri), range)
  }

  object TextDocumentPosition {
    def unapply(json: JSON.T): Option[Line.Node_Position] =
      for {
        doc <- JSON.value(json, "textDocument")
        uri <- JSON.string(doc, "uri") if Url.is_wellformed_file(uri)
        pos_json <- JSON.value(json, "position")
        pos <- Position.unapply(pos_json)
      } yield Line.Node_Position(Url.absolute_file_name(uri), pos)
  }

  /* marked strings */

  sealed case class MarkedString(text: String, language: String = "plaintext") {
    def json: JSON.T = JSON.Object("language" -> language, "value" -> text)
  }

  object MarkedStrings {
    def json(msgs: List[MarkedString]): Option[JSON.T] =
      msgs match {
        case Nil => None
        case List(msg) => Some(msg.json)
        case _ => Some(msgs.map(_.json))
      }
  }

  /* diagnostic messages */

  object MessageType {
    val Error = 1
    val Warning = 2
    val Info = 3
    val Log = 4
  }

  object DisplayMessage {
    def apply(message_type: Int, message: String, show: Boolean): JSON.T =
      Notification(if (show) "window/showMessage" else "window/logMessage",
        JSON.Object("type" -> message_type, "message" -> message))
  }

  /* commands */

  sealed case class Command(title: String, command: String, arguments: List[JSON.T] = Nil) {
    def json: JSON.T =
      JSON.Object("title" -> title, "command" -> command, "arguments" -> arguments)
  }

  /* document edits */

  object DidOpenTextDocument {
    def unapply(json: JSON.T): Option[(JFile, String, Long, String)] =
      json match {
        case Notification("textDocument/didOpen", Some(params)) =>
          for {
            doc <- JSON.value(params, "textDocument")
            uri <- JSON.string(doc, "uri") if Url.is_wellformed_file(uri)
            lang <- JSON.string(doc, "languageId")
            version <- JSON.long(doc, "version")
            text <- JSON.string(doc, "text")
          } yield (Url.absolute_file(uri), lang, version, text)
        case _ => None
      }
  }

  sealed case class TextDocumentChange(range: Option[Line.Range], text: String)

  object DidChangeTextDocument {
    def unapply_change(json: JSON.T): Option[TextDocumentChange] =
      for (text <- JSON.string(json, "text"))
      yield TextDocumentChange(JSON.value(json, "range", Range.unapply), text)

    def unapply(json: JSON.T): Option[(JFile, Long, List[TextDocumentChange])] =
      json match {
        case Notification("textDocument/didChange", Some(params)) =>
          for {
            doc <- JSON.value(params, "textDocument")
            uri <- JSON.string(doc, "uri") if Url.is_wellformed_file(uri)
            version <- JSON.long(doc, "version")
            changes <- JSON.list(params, "contentChanges", unapply_change)
          } yield (Url.absolute_file(uri), version, changes)
        case _ => None
      }
  }

  class TextDocumentNotification(name: String) {
    def unapply(json: JSON.T): Option[JFile] =
      json match {
        case Notification(method, Some(params)) if method == name =>
          for {
            doc <- JSON.value(params, "textDocument")
            uri <- JSON.string(doc, "uri") if Url.is_wellformed_file(uri)
          } yield Url.absolute_file(uri)
        case _ => None
      }
  }

  object DidCloseTextDocument extends TextDocumentNotification("textDocument/didClose")
  object DidSaveTextDocument extends TextDocumentNotification("textDocument/didSave")

  /* workspace edits */

  sealed case class TextEdit(range: Line.Range, new_text: String) {
    def json: JSON.T = JSON.Object("range" -> Range(range), "newText" -> new_text)
  }

  sealed case class TextDocumentEdit(file: JFile, version: Option[Long], edits: List[TextEdit]) {
    def json: JSON.T =
      JSON.Object(
        "textDocument" -> (
          JSON.Object("uri" -> Url.print_file(file)) ++
          JSON.optional("version" -> version)
        ),
        "edits" -> edits.map(_.json)
      )
  }

  object WorkspaceEdit {
    def apply(edits: List[TextDocumentEdit]): JSON.T =
      JSON.Object("documentChanges" -> edits.map(_.json))
  }

  object ApplyWorkspaceEdit {
    def apply(edits: List[TextDocumentEdit]): JSON.T =
      RequestMessage(Id.empty, "workspace/applyEdit",
        JSON.Object("edit" -> WorkspaceEdit(edits))
      )
  }

  /* completion */

  object CompletionItemKind {
    val Text = 1;
    val Method = 2;
    val Function = 3;
    val Constructor = 4;
    val Field = 5;
    val Variable = 6;
    val Class = 7;
    val Interface = 8;
    val Module = 9;
    val Property = 10;
    val Unit = 11;
    val Value = 12;
    val Enum = 13;
    val Keyword = 14;
    val Snippet = 15;
    val Color = 16;
    val File = 17;
    val Reference = 18;
    val Folder = 19;
    val EnumMember = 20;
    val Constant = 21;
    val Struct = 22;
    val Event = 23;
    val Operator = 24;
    val TypeParameter = 25;
  }

  sealed case class CompletionItem(
    label: String,
    kind: Option[Int] = None,
    detail: Option[String] = None,
    documentation: Option[String] = None,
    filter_text: Option[String] = None,
    commit_characters: Option[List[String]] = None,
    text: Option[String] = None,
    range: Option[Line.Range] = None,
    command: Option[Command] = None
  ) {
    def json: JSON.T =
      JSON.Object("label" -> label) ++
      JSON.optional("kind" -> kind) ++
      JSON.optional("detail" -> detail) ++
      JSON.optional("documentation" -> documentation) ++
      JSON.optional("filterText" -> filter_text) ++
      JSON.optional("textEdit" -> range.map(TextEdit(_, text.getOrElse(label)).json)) ++
      JSON.optional("commitCharacters" -> commit_characters) ++
      JSON.optional("command" -> command.map(_.json))
  }

  object Completion extends RequestTextDocumentPosition("textDocument/completion") {
    def reply(id: Id, result: List[CompletionItem]): JSON.T =
      ResponseMessage(id, Some(result.map(_.json)))
  }

  /* spell checker */

  object Include_Word extends Notification0("PIDE/include_word") {
    val command = Command("Include word", "isabelle.include-word")
  }

  object Include_Word_Permanently extends Notification0("PIDE/include_word_permanently") {
    val command = Command("Include word permanently", "isabelle.include-word-permanently")
  }

  object Exclude_Word extends Notification0("PIDE/exclude_word") {
    val command = Command("Exclude word", "isabelle.exclude-word")
  }

  object Exclude_Word_Permanently extends Notification0("PIDE/exclude_word_permanently") {
    val command = Command("Exclude word permanently", "isabelle.exclude-word-permanently")
  }

  object Reset_Words extends Notification0("PIDE/reset_words") {
    val command = Command("Reset non-permanent words", "isabelle.reset-words")
  }

  /* hover request */

  object Hover extends RequestTextDocumentPosition("textDocument/hover") {
    def reply(id: Id, result: Option[(Line.Range, List[MarkedString])]): JSON.T = {
      val res =
        result match {
          case Some((range, contents)) =>
            JSON.Object(
              "contents" -> MarkedStrings.json(contents).getOrElse(Nil),
              "range" -> Range(range))
          case None => JSON.Object("contents" -> Nil)
        }
      ResponseMessage(id, Some(res))
    }
  }

  /* goto definition request */

  object GotoDefinition extends RequestTextDocumentPosition("textDocument/definition") {
    def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
      ResponseMessage(id, Some(result.map(Location.apply)))
  }

  /* document highlights request */

  object DocumentHighlight {
    def text(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(1))
    def read(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(2))
    def write(range: Line.Range): DocumentHighlight = DocumentHighlight(range, Some(3))
  }

  sealed case class DocumentHighlight(range: Line.Range, kind: Option[Int] = None) {
    def json: JSON.T =
      kind match {
        case None => JSON.Object("range" -> Range(range))
        case Some(k) => JSON.Object("range" -> Range(range), "kind" -> k)
      }
  }

  object DocumentHighlights extends RequestTextDocumentPosition("textDocument/documentHighlight") {
    def reply(id: Id, result: List[DocumentHighlight]): JSON.T =
      ResponseMessage(id, Some(result.map(_.json)))
  }

  /* diagnostics */

  sealed case class Diagnostic(
    range: Line.Range,
    message: String,
    severity: Option[Int] = None,
    code: Option[Int] = None,
    source: Option[String] = None
  ) {
    def json: JSON.T =
      Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
      JSON.optional("severity" -> severity) ++
      JSON.optional("code" -> code) ++
      JSON.optional("source" -> source)
  }

  object DiagnosticSeverity {
    val Error = 1
    val Warning = 2
    val Information = 3
    val Hint = 4
  }

  object PublishDiagnostics {
    def apply(file: JFile, diagnostics: List[Diagnostic]): JSON.T =
      Notification("textDocument/publishDiagnostics",
        JSON.Object("uri" -> Url.print_file(file), "diagnostics" -> diagnostics.map(_.json)))
  }

  /* code actions */

  sealed case class CodeAction(title: String, edits: List[TextDocumentEdit]) {
    def json: JSON.T =
      JSON.Object("title" -> title, "edit" -> WorkspaceEdit(edits))
  }

  object CodeActionRequest {
    def unapply(json: JSON.T): Option[(Id, JFile, Line.Range)] =
      json match {
        case RequestMessage(id, "textDocument/codeAction", Some(params)) =>
          for {
            doc <- JSON.value(params, "textDocument")
            uri <- JSON.string(doc, "uri") if Url.is_wellformed_file(uri)
            case Range(range) <- JSON.value(params, "range")
          } yield (id, Url.absolute_file(uri), range)
        case _ => None
      }

    def reply(id: Id, actions: List[CodeAction]): JSON.T =
      ResponseMessage(id, Some(actions.map(_.json)))
  }

  /* decorations */

  sealed case class Decoration_Range(range: Line.Range, hover_message: List[MarkedString] = Nil) {
    def json: JSON.T =
      JSON.Object("range" -> Range.compact(range)) ++
      JSON.optional("hover_message" -> MarkedStrings.json(hover_message))
  }

  object Decoration_Entry {
    def text_color(color: Rendering.Color.Value, content: List[Decoration_Range]): Decoration_Entry =
      Decoration_Entry("text_" + color.toString, content)
  }
  sealed case class Decoration_Entry(typ: String, content: List[Decoration_Range]) {
    def json: JSON.T = JSON.Object("type" -> typ, "content" -> content.map(_.json))
  }

  sealed case class Decoration(entries: List[Decoration_Entry]) {
    def json(file: JFile): JSON.T =
      Notification("PIDE/decoration",
        JSON.Object("uri" -> Url.print_file(file), "entries" -> entries.map(_.json)))
  }

  object Decoration_Request {
    def unapply(json: JSON.T): Option[JFile] =
      json match {
        case Notification("PIDE/decoration_request", Some(params)) =>
          for (uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri))
            yield Url.absolute_file(uri)
        case _ => None
      }
  }

  /* caret update: bidirectional */

  object Caret_Update {
    def apply(node_pos: Line.Node_Position, focus: Boolean): JSON.T =
      Notification("PIDE/caret_update",
        JSON.Object(
          "uri" -> Url.print_file_name(node_pos.name),
          "line" -> node_pos.pos.line,
          "character" -> node_pos.pos.column,
          "focus" -> focus))

    def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
      json match {
        case Notification("PIDE/caret_update", Some(params)) =>
          val caret =
            for {
              uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri)
              pos <- Position.unapply(params)
            } yield (Url.absolute_file(uri), pos)
          Some(caret)
        case _ => None
      }
  }

  /* dynamic output */

  object Dynamic_Output {
    def apply(content: String, decorations: Option[Decoration] = None): JSON.T =
      Notification("PIDE/dynamic_output",
        JSON.Object("content" -> content) ++
        JSON.optional("decorations" -> decorations.map(_.json)))
  }

  object Output_Set_Margin {
    def unapply(json: JSON.T): Option[Double] =
      json match {
        case Notification("PIDE/output_set_margin", Some(params)) =>
          JSON.double(params, "margin")
        case _ => None
      }
  }

  /* state output */

  object State_Output {
    def apply(
       id: Counter.ID,
       content: String,
       auto_update: Boolean,
       decorations: Option[Decoration] = None
    ): JSON.T =
      Notification("PIDE/state_output",
        JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++
        JSON.optional("decorations" -> decorations.map(_.json)))
  }

  class State_Id_Notification(name: String) {
    def unapply(json: JSON.T): Option[Counter.ID] =
      json match {
        case Notification(method, Some(params)) if method == name => JSON.long(params, "id")
        case _ => None
      }
  }

  object State_Init extends Request0("PIDE/state_init") {
    def reply(id: Id, state_id: Counter.ID): JSON.T =
      ResponseMessage(id, Some(JSON.Object("state_id" -> state_id)))
  }

  object State_Exit extends State_Id_Notification("PIDE/state_exit")
  object State_Locate extends State_Id_Notification("PIDE/state_locate")
  object State_Update extends State_Id_Notification("PIDE/state_update")

  object State_Auto_Update {
    def unapply(json: JSON.T): Option[(Counter.ID, Boolean)] =
      json match {
        case Notification("PIDE/state_auto_update", Some(params)) =>
          for {
            id <- JSON.long(params, "id")
            enabled <- JSON.bool(params, "enabled")
          } yield (id, enabled)
        case _ => None
      }
  }

  object State_Set_Margin {
    def unapply(json: JSON.T): Option[(Counter.ID, Double)] =
      json match {
        case Notification("PIDE/state_set_margin", Some(params)) =>
          for {
            id <- JSON.long(params, "id")
            margin <- JSON.double(params, "margin")
          } yield (id, margin)
        case _ => None
      }
  }

  /* preview */

  object Preview_Request {
    def unapply(json: JSON.T): Option[(JFile, Int)] =
      json match {
        case Notification("PIDE/preview_request", Some(params)) =>
          for {
            uri <- JSON.string(params, "uri") if Url.is_wellformed_file(uri)
            column <- JSON.int(params, "column")
          } yield (Url.absolute_file(uri), column)
        case _ => None
      }

    def reply(file: JFile, column: Int, label: String, content: String): JSON.T =
      Notification("PIDE/preview_response",
        JSON.Object(
          "uri" -> Url.print_file(file),
          "column" -> column,
          "label" -> label,
          "content" -> content))
  }

  /* abbrevs */

  object Abbrevs_Request extends Notification0("PIDE/abbrevs_request") {
    def reply(abbrevs: List[(String, String)]): JSON.T =
      Notification("PIDE/abbrevs_response",
        JSON.Object("abbrevs" -> (for ((a, b) <- abbrevs) yield List(a, b))))
  }

  /* documentation */

  object Documentation_Request
    extends Notification0("PIDE/documentation_request")

  object Doc_Entry {
    def apply(entry: Doc.Entry): JSON.T =
      JSON.Object(
        "print_html" -> entry.print_html,
        "platform_path" -> File.platform_path(entry.path))
  }

  object Doc_Section {
    def apply(section: Doc.Section): JSON.T =
      JSON.Object(
        "title" -> section.title,
        "important" -> section.important,
        "entries" -> section.entries.map(Doc_Entry.apply))
  }

  object Documentation_Response {
    def apply(ml_settings: ML_Settings): JSON.T = {
      val doc_contents = Doc.contents(ml_settings)
      Notification("PIDE/documentation_response",
        JSON.Object("sections" -> doc_contents.sections.map(Doc_Section.apply)))
    }
  }

  /* sledgehammer */

  object Sledgehammer_Provers_Request
    extends Notification0("PIDE/sledgehammer_provers_request")

  object Sledgehammer_Provers_Response {
    def apply(provers: String): JSON.T =
      Notification("PIDE/sledgehammer_provers_response", JSON.Object("provers" -> provers))
  }

  object Sledgehammer_Request {
    def unapply(json: JSON.T): Option[List[String]] =
      json match {
        case Notification("PIDE/sledgehammer_request", Some(params)) =>
          for {
            provers <- JSON.string(params, "provers")
            isar <- JSON.bool(params, "isar")
            try0 <- JSON.bool(params, "try0")
          } yield List(provers, isar.toString, try0.toString)
        case _ => None
      }
  }

  object Sledgehammer_Status {
    def apply(message: String): JSON.T =
      Notification("PIDE/sledgehammer_status", JSON.Object("message" -> message))
  }

  object Sledgehammer_Output {
    def apply(content: String): JSON.T =
      Notification("PIDE/sledgehammer_output", JSON.Object("content" -> content))
  }

  object Sledgehammer_Cancel extends Notification0("PIDE/sledgehammer_cancel")

  object Sledgehammer_Locate extends Notification0("PIDE/sledgehammer_locate")

  object Sledgehammer_Sendback {
    def unapply(json: JSON.T): Option[String] =
      json match {
        case Notification("PIDE/sledgehammer_sendback", Some(params)) =>
          JSON.string(params, "text")
        case _ => None
      }
  }

  object Sledgehammer_Insert {
    def apply(node_pos: Line.Node_Position, text: String): JSON.T =
      Notification("PIDE/sledgehammer_insert",
        JSON.Object(
          "uri" -> Url.print_file_name(node_pos.name),
          "line" -> node_pos.pos.line,
          "character" -> node_pos.pos.column,
          "text" -> text))
  }
}

quality92%

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.