class VSCode_Sledgehammer(server: Language_Server) { privateval query_operation = new Query_Operation(server.editor, (), "sledgehammer", consume_status, consume_output)
privatedef consume_status(status: Query_Operation.Status): Unit = { val message =
status match { case Query_Operation.Status.waiting => "Waiting for evaluation of context ..." case Query_Operation.Status.running => "Sledgehammering ..." case Query_Operation.Status.finished => "Finished"
}
server.channel.write(LSP.Sledgehammer_Status(message))
}
privatedef consume_output(output: Editor.Output): Unit = { val content = XML.string_of_body(Pretty.unbreakable(output.messages))
server.channel.write(LSP.Sledgehammer_Output(content))
}
def provers(): Unit =
server.channel.write(
LSP.Sledgehammer_Provers_Response(server.options.string("sledgehammer_provers")))
def request(args: List[String]): Unit =
server.editor.send_dispatcher { query_operation.apply_query(args) }
def sendback(text: String): Unit =
server.editor.send_dispatcher { for {
(snapshot, command) <- query_operation.query_command()
node_pos <- snapshot.find_command_position(command.id, 0)
} { val node_pos1 = node_pos.advance(command.source(command.core_range))
server.channel.write(LSP.Sledgehammer_Insert(node_pos1, text))
}
}
def cancel(): Unit = server.editor.send_dispatcher { query_operation.cancel_query() } def locate(): Unit = server.editor.send_dispatcher { query_operation.locate_query() }
def init(): Unit = query_operation.activate() def exit(): Unit = query_operation.deactivate()
}
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
