--- a/src/Tools/VSCode/etc/options Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/etc/options Wed Oct 02 10:39:32 2024 +0200
@@ -22,10 +22,10 @@
-- "use PIDE extensions for Language Server Protocol"
option vscode_unicode_symbols_output : bool = false for vscode
- -- "output Isabelle symbols via Unicode in Output (e.g. tooltips and panels) (according to etc/symbols)"
+ -- "output Isabelle symbols via Unicode in Output (according to etc/symbols)"
option vscode_unicode_symbols_edits : bool = false for vscode
- -- "output Isabelle symbols via Unicode in Edits (e.g. completions and code actions) (according to etc/symbols)"
+ -- "output Isabelle symbols via Unicode in Edits (according to etc/symbols)"
option vscode_caret_perspective : int = 50 for vscode
-- "number of visible lines above and below the caret (0: unrestricted)"
--- a/src/Tools/VSCode/extension/src/output_view.ts Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/extension/src/output_view.ts Wed Oct 02 10:39:32 2024 +0200
@@ -22,7 +22,10 @@
private _view?: WebviewView
private content: string = ''
- constructor(private readonly _extension_uri: Uri, private readonly _language_client: LanguageClient) { }
+ constructor(
+ private readonly _extension_uri: Uri,
+ private readonly _language_client: LanguageClient
+ ) { }
public resolveWebviewView(
view: WebviewView,
@@ -48,7 +51,8 @@
open_webview_link(message.link)
break
case "resize":
- this._language_client.sendNotification(lsp.output_set_margin_type, { margin: message.margin })
+ this._language_client.sendNotification(
+ lsp.output_set_margin_type, { margin: message.margin })
break
}
})
@@ -85,7 +89,8 @@
{
const script_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'main.js')))
const css_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'media', 'vscode.css')))
- const font_uri = webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
+ const font_uri =
+ webview.asWebviewUri(Uri.file(path.join(extension_path, 'fonts', 'IsabelleDejaVuSansMono.ttf')))
return `<!DOCTYPE html>
<html lang='en'>
--- a/src/Tools/VSCode/extension/src/state_panel.ts Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/extension/src/state_panel.ts Wed Oct 02 10:39:32 2024 +0200
@@ -62,7 +62,8 @@
open_webview_link(message.link)
break
case "resize":
- language_client.sendNotification(lsp.state_set_margin_type, { id: this.state_id, margin: message.margin })
+ language_client.sendNotification(
+ lsp.state_set_margin_type, { id: this.state_id, margin: message.margin })
break
default:
break
--- a/src/Tools/VSCode/src/component_vscode_extension.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/component_vscode_extension.scala Wed Oct 02 10:39:32 2024 +0200
@@ -135,27 +135,27 @@
private def options_json(options: Options): String = {
- val relevant_options = Set(
- "editor_output_state",
- "auto_time_start",
- "auto_time_limit",
- "auto_nitpick",
- "auto_sledgehammer",
- "auto_methods",
- "auto_quickcheck",
- "auto_solve_direct",
- "sledgehammer_provers",
- "sledgehammer_timeout",
- )
-
- options.iterator.filter(
- opt => opt.for_tag(Options.TAG_VSCODE) || opt.for_content || relevant_options.contains(opt.name)
- ).map(opt => {
+ val relevant_options =
+ Set(
+ "editor_output_state",
+ "auto_time_start",
+ "auto_time_limit",
+ "auto_nitpick",
+ "auto_sledgehammer",
+ "auto_methods",
+ "auto_quickcheck",
+ "auto_solve_direct",
+ "sledgehammer_provers",
+ "sledgehammer_timeout")
+
+ (for {
+ opt <- options.iterator
+ if opt.for_tag(Options.TAG_VSCODE) || opt.for_content || relevant_options.contains(opt.name)
+ } yield {
val (enum_values, enum_descriptions) = opt.typ match {
case Options.Bool => (
Some(List("", "true", "false")),
- Some(List("Use System Preference.", "Enable.", "Disable."))
- )
+ Some(List("Use System Preference.", "Enable.", "Disable.")))
case _ => (None, None)
}
@@ -167,13 +167,14 @@
case _ => ""
}
- quote("isabelle.options." + opt.name) + ": " + JSON.Format(
- JSON.Object(
- "type" -> "string",
- "default" -> default,
- "description" -> opt.description,
- ) ++ JSON.optional("enum" -> enum_values) ++ JSON.optional("enumDescriptions" -> enum_descriptions)
- ) + ","
+ quote("isabelle.options." + opt.name) + ": " +
+ JSON.Format(
+ JSON.Object(
+ "type" -> "string",
+ "default" -> default,
+ "description" -> opt.description) ++
+ JSON.optional("enum" -> enum_values) ++
+ JSON.optional("enumDescriptions" -> enum_descriptions)) + ","
}).mkString
}
@@ -210,9 +211,8 @@
Isabelle_System.make_directory(build_dir + path.dir))
}
- for (entry <- Isabelle_Fonts.fonts()) {
- Isabelle_System.copy_file(entry.path, Isabelle_System.make_directory(build_dir + Path.basic("fonts")))
- }
+ val fonts_dir = Isabelle_System.make_directory(build_dir + Path.basic("fonts"))
+ for (entry <- Isabelle_Fonts.fonts()) { Isabelle_System.copy_file(entry.path, fonts_dir) }
val manifest_text2 =
manifest_text + cat_lines(Isabelle_Fonts.fonts().map(e => "fonts/" + e.path.file_name))
val manifest_entries2 = split_lines(manifest_text2).filter(_.nonEmpty)
--- a/src/Tools/VSCode/src/dynamic_output.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala Wed Oct 02 10:39:32 2024 +0200
@@ -16,7 +16,8 @@
class Dynamic_Output private(server: Language_Server) {
private val pretty_panel_ = Synchronized(None: Option[Pretty_Text_Panel])
- def pretty_panel: Pretty_Text_Panel = pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
+ def pretty_panel: Pretty_Text_Panel =
+ pretty_panel_.value.getOrElse(error("No Pretty Panel for Dynamic Output"))
private def handle_update(restriction: Option[Set[Command]], force: Boolean = false): Unit = {
val output =
@@ -55,11 +56,11 @@
def init(): Unit = {
server.session.commands_changed += main
server.session.caret_focus += main
- pretty_panel_.change(p => Some(Pretty_Text_Panel(
- server.resources,
- server.channel,
- LSP.Dynamic_Output.apply,
- )))
+ pretty_panel_.change(_ =>
+ Some(Pretty_Text_Panel(
+ server.resources,
+ server.channel,
+ LSP.Dynamic_Output.apply)))
handle_update(None)
}
--- a/src/Tools/VSCode/src/language_server.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/language_server.scala Wed Oct 02 10:39:32 2024 +0200
@@ -424,9 +424,10 @@
def code_action_request(id: LSP.Id, file: JFile, range: Line.Range): Unit = {
def extract_sendbacks(body: XML.Body): List[(String, Properties.T)] = {
body match {
- case (XML.Elem(Markup(Markup.SENDBACK, p), b) :: rest) => (XML.content(b), p) :: extract_sendbacks(rest)
- case (XML.Elem(m, b) :: rest) => extract_sendbacks(b ++ rest)
- case (e :: rest) => extract_sendbacks(rest)
+ case XML.Elem(Markup(Markup.SENDBACK, p), b) :: rest =>
+ (XML.content(b), p) :: extract_sendbacks(rest)
+ case XML.Elem(m, b) :: rest => extract_sendbacks(b ++ rest)
+ case e :: rest => extract_sendbacks(rest)
case Nil => Nil
}
}
@@ -443,8 +444,7 @@
.select(
text_range2,
Markup.Elements.full,
- command_states => _ => Some(command_states.flatMap(_.results.iterator.map(_._2).toList))
- )
+ command_states => _ => Some(command_states.flatMap(_.results.iterator.map(_._2).toList)))
.flatMap(info => extract_sendbacks(info.info).flatMap {
(s, p) =>
for {
@@ -452,7 +452,7 @@
(node, command) <- snapshot.find_command(id)
start <- node.command_start(command)
range = command.core_range + start
- current_text <- doc.get_text(range)
+ current_text <- model.get_text(range)
line_range = doc.range(range)
whole_line = doc.lines(line_range.start.line)
@@ -528,10 +528,12 @@
case LSP.State_Exit(state_id) => State_Panel.exit(state_id)
case LSP.State_Locate(state_id) => State_Panel.locate(state_id)
case LSP.State_Update(state_id) => State_Panel.update(state_id)
- case LSP.State_Auto_Update(state_id, enabled) => State_Panel.auto_update(state_id, enabled)
+ case LSP.State_Auto_Update(state_id, enabled) =>
+ State_Panel.auto_update(state_id, enabled)
case LSP.State_Set_Margin(state_id, margin) => State_Panel.set_margin(state_id, margin)
case LSP.Symbols_Request(id) => symbols_request(id)
- case LSP.Symbols_Convert_Request(id, text, boolean) => symbols_convert_request(id, text, boolean)
+ case LSP.Symbols_Convert_Request(id, text, boolean) =>
+ symbols_convert_request(id, text, boolean)
case LSP.Preview_Request(file, column) => preview_request(file, column)
case _ => if (!LSP.ResponseMessage.is_empty(json)) log("### IGNORED")
}
--- a/src/Tools/VSCode/src/lsp.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/lsp.scala Wed Oct 02 10:39:32 2024 +0200
@@ -109,7 +109,10 @@
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)))
+ 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
@@ -401,7 +404,7 @@
JSON.optional("detail" -> detail) ++
JSON.optional("documentation" -> documentation) ++
JSON.optional("filterText" -> filter_text) ++
- JSON.optional("textEdit" -> range.map(r => TextEdit(range = r, new_text = text.getOrElse(label)).json)) ++
+ JSON.optional("textEdit" -> range.map(TextEdit(_, text.getOrElse(label)).json)) ++
JSON.optional("commitCharacters" -> commit_characters) ++
JSON.optional("command" -> command.map(_.json))
}
@@ -552,16 +555,13 @@
def json_entries: JSON.T =
decorations.map(decoration => JSON.Object(
"type" -> decoration._1,
- "content" -> decoration._2.map(_.json))
- )
+ "content" -> decoration._2.map(_.json)))
def json(file: JFile): JSON.T =
Notification("PIDE/decoration",
JSON.Object(
"uri" -> Url.print_file(file),
- "entries" -> json_entries
- )
- )
+ "entries" -> json_entries))
}
object Decoration_Request {
@@ -609,8 +609,7 @@
def apply(content: String, decoration: Option[Decoration] = None): JSON.T =
Notification("PIDE/dynamic_output",
JSON.Object("content" -> content) ++
- JSON.optional("decorations" -> decoration.map(_.json_entries))
- )
+ JSON.optional("decorations" -> decoration.map(_.json_entries)))
}
object Output_Set_Margin {
@@ -634,8 +633,7 @@
): JSON.T =
Notification("PIDE/state_output",
JSON.Object("id" -> id, "content" -> content, "auto_update" -> auto_update) ++
- JSON.optional("decorations" -> decorations.map(_.json_entries))
- )
+ JSON.optional("decorations" -> decorations.map(_.json_entries)))
}
class State_Id_Notification(name: String) {
@@ -688,14 +686,12 @@
JSON.Object(
"symbol" -> symbol.symbol,
"name" -> symbol.name,
- "argument" -> symbol.argument.toString,
- ) ++
- JSON.optional("code", symbol.code) ++
- JSON.optional("font", symbol.font) ++
- JSON.Object(
- "groups" -> symbol.groups,
- "abbrevs" -> symbol.abbrevs,
- )
+ "argument" -> symbol.argument.toString) ++
+ JSON.optional("code", symbol.code) ++
+ JSON.optional("font", symbol.font) ++
+ JSON.Object(
+ "groups" -> symbol.groups,
+ "abbrevs" -> symbol.abbrevs)
ResponseMessage(id, Some(symbols.entries.map(s => json(s))))
}
--- a/src/Tools/VSCode/src/pretty_text_panel.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/pretty_text_panel.scala Wed Oct 02 10:39:32 2024 +0200
@@ -6,8 +6,10 @@
package isabelle.vscode
+
import isabelle._
+
object Pretty_Text_Panel {
def apply(
resources: VSCode_Resources,
--- a/src/Tools/VSCode/src/state_panel.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/state_panel.scala Wed Oct 02 10:39:32 2024 +0200
@@ -60,11 +60,13 @@
/* query operation */
private val output_active = Synchronized(true)
- private val pretty_panel = Synchronized(Pretty_Text_Panel(
- server.resources,
- server.channel,
- (content, decorations) => LSP.State_Output(id, content, auto_update_enabled.value, decorations)
- ))
+ private val pretty_panel =
+ Synchronized(Pretty_Text_Panel(
+ server.resources,
+ server.channel,
+ (content, decorations) =>
+ LSP.State_Output(id, content, auto_update_enabled.value, decorations)
+ ))
private val print_state =
new Query_Operation(server.editor, (), "print_state", _ => (),
--- a/src/Tools/VSCode/src/vscode_model.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_model.scala Wed Oct 02 10:39:32 2024 +0200
@@ -183,8 +183,7 @@
val (reparse, perspective) = node_perspective(doc_blobs, caret)
if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
val prover_edits = node_edits(node_header, pending_edits, perspective)
- val edits = (prover_edits)
- Some(edits, copy(pending_edits = Nil, last_perspective = perspective))
+ Some(prover_edits, copy(pending_edits = Nil, last_perspective = perspective))
}
else None
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Fri Jul 19 17:08:20 2024 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Oct 02 10:39:32 2024 +0200
@@ -279,7 +279,7 @@
model.flush_edits(st.document_blobs, file, st.get_caret(file))
} yield (edits, (file, model1))).toList
- session.update(st.document_blobs, changed_models.flatMap(res => res._1))
+ session.update(st.document_blobs, changed_models.flatMap(_._1))
st.copy(
models = st.models ++ changed_models.iterator.map(_._2),
@@ -331,13 +331,10 @@
/* output text */
- def output_text(content: String): String =
- Symbol.output(unicode_symbols_output, content)
- def output_edit(content: String): String =
- Symbol.output(unicode_symbols_edits, content)
+ def output_text(content: String): String = Symbol.output(unicode_symbols_output, content)
+ def output_edit(content: String): String = Symbol.output(unicode_symbols_edits, content)
- def output_xml_text(body: XML.Tree): String =
- output_text(XML.content(body))
+ def output_xml_text(body: XML.Tree): String = output_text(XML.content(body))
def output_pretty(body: XML.Body, margin: Double): String =
output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric))
@@ -373,7 +370,6 @@
}
-
/* spell checker */
val spell_checker = new Spell_Checker_Variable