# HG changeset patch # User Fabian Huch # Date 1727858372 -7200 # Node ID 96eb20106a34f6e273ff207a54f6da448971be58 # Parent aa77be3e83296090c7444788e55727044d50d748 minor tuning; diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/etc/options --- 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)" diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/extension/src/output_view.ts --- 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 ` diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/extension/src/state_panel.ts --- 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 diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/component_vscode_extension.scala --- 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) diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/dynamic_output.scala --- 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) } diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/language_server.scala --- 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") } diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/lsp.scala --- 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)))) } diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/pretty_text_panel.scala --- 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, diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/state_panel.scala --- 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", _ => (), diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/vscode_model.scala --- 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 } diff -r aa77be3e8329 -r 96eb20106a34 src/Tools/VSCode/src/vscode_resources.scala --- 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