# HG changeset patch # User wenzelm # Date 1497041718 -7200 # Node ID 637b26fd3349f5760ba2b5dd150625172701f905 # Parent 3804a9640088520c0e781dc1a1f1aae016a640c0# Parent b8555ca0af07824f875ed337197bafed833b8d9a merged diff -r 3804a9640088 -r 637b26fd3349 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Pure/General/completion.scala Fri Jun 09 22:55:18 2017 +0200 @@ -189,10 +189,10 @@ def complete( range: Text.Range, history: Completion.History, - do_decode: Boolean, + unicode: Boolean, original: String): Option[Completion.Result] = { - def decode(s: String): String = if (do_decode) Symbol.decode(s) else s + def decode(s: String): String = if (unicode) Symbol.decode(s) else s val items = for { (xname, (kind, name)) <- names @@ -408,14 +408,13 @@ def complete( history: Completion.History, - do_decode: Boolean, + unicode: Boolean, explicit: Boolean, start: Text.Offset, text: CharSequence, caret: Int, language_context: Completion.Language_Context): Option[Completion.Result] = { - def decode(s: String): String = if (do_decode) Symbol.decode(s) else s val length = text.length val abbrevs_result = @@ -477,17 +476,21 @@ Character.codePointCount(original, 0, original.length) > 1) val unique = completions.length == 1 + def decode1(s: String): String = if (unicode) Symbol.decode(s) else s + def decode2(s: String): String = if (unicode) s else Symbol.decode(s) + val items = for { (complete_word, name0) <- completions - name1 = decode(name0) + name1 = decode1(name0) + name2 = decode2(name0) if name1 != original (s1, s2) = Completion.split_template(name1) move = - s2.length description = if (is_symbol(name0)) { - if (name0 == name1) List(name0) - else List(name1, "(symbol " + quote(name0) + ")") + if (name1 == name2) List(name1) + else List(name1, "(symbol " + quote(name2) + ")") } else if (is_keyword_template(complete_word, true)) List(name1, "(template " + quote(complete_word) + ")") diff -r 3804a9640088 -r 637b26fd3349 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Pure/General/symbol.scala Fri Jun 09 22:55:18 2017 +0200 @@ -369,7 +369,7 @@ ("abbrev", a) <- props.reverse } yield sym -> a): _*) - val codes: List[(String, Int)] = + val codes: List[(Symbol, Int)] = { val Code = new Properties.String("code") for { @@ -500,7 +500,7 @@ def names: Map[Symbol, String] = symbols.names def groups: List[(String, List[Symbol])] = symbols.groups def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs - def codes: List[(String, Int)] = symbols.codes + def codes: List[(Symbol, Int)] = symbols.codes def decode(text: String): String = symbols.decode(text) def encode(text: String): String = symbols.encode(text) diff -r 3804a9640088 -r 637b26fd3349 src/Pure/PIDE/rendering.scala --- a/src/Pure/PIDE/rendering.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Pure/PIDE/rendering.scala Fri Jun 09 22:55:18 2017 +0200 @@ -153,6 +153,18 @@ /* markup elements */ + val semantic_completion_elements = + Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) + + val language_context_elements = + Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, + Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, + Markup.ML_STRING, Markup.ML_COMMENT) + + val language_elements = Markup.Elements(Markup.LANGUAGE) + + val citation_elements = Markup.Elements(Markup.CITATION) + val active_elements = Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW, Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL) @@ -169,9 +181,6 @@ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, Markup.CARTOUCHE, Markup.ANTIQUOTED) - val semantic_completion_elements = - Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION) - val tooltip_elements = Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING, @@ -197,11 +206,11 @@ /* completion */ - def semantic_completion(completed_range: Option[Text.Range], range: Text.Range) + def semantic_completion(completed_range: Option[Text.Range], caret_range: Text.Range) : Option[Text.Info[Completion.Semantic]] = if (snapshot.is_outdated) None else { - snapshot.select(range, Rendering.semantic_completion_elements, _ => + snapshot.select(caret_range, Rendering.semantic_completion_elements, _ => { case Completion.Semantic.Info(info) => completed_range match { @@ -212,6 +221,53 @@ }).headOption.map(_.info) } + def semantic_completion_result( + history: Completion.History, + unicode: Boolean, + completed_range: Option[Text.Range], + caret_range: Text.Range, + try_get_text: Text.Range => Option[String]): (Boolean, Option[Completion.Result]) = + { + semantic_completion(completed_range, caret_range) match { + case Some(Text.Info(_, Completion.No_Completion)) => (true, None) + case Some(Text.Info(range, names: Completion.Names)) => + try_get_text(range) match { + case Some(original) => (false, names.complete(range, history, unicode, original)) + case None => (false, None) + } + case None => (false, None) + } + } + + def language_context(range: Text.Range): Option[Completion.Language_Context] = + snapshot.select(range, Rendering.language_context_elements, _ => + { + case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => + if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) + else None + case Text.Info(_, elem) + if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => + Some(Completion.Language_Context.ML_inner) + case Text.Info(_, _) => + Some(Completion.Language_Context.inner) + }).headOption.map(_.info) + + def language_path(range: Text.Range): Option[Text.Range] = + snapshot.select(range, Rendering.language_elements, _ => + { + case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) => + Some(snapshot.convert(info_range)) + case _ => None + }).headOption.map(_.info) + + def citation(range: Text.Range): Option[Text.Info[String]] = + snapshot.select(range, Rendering.citation_elements, _ => + { + case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => + Some(Text.Info(snapshot.convert(info_range), name)) + case _ => None + }).headOption.map(_.info) + /* spell checker */ diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/extension/src/extension.ts Fri Jun 09 22:55:18 2017 +0200 @@ -6,6 +6,7 @@ import * as decorations from './decorations'; import * as preview from './preview'; import * as protocol from './protocol'; +import * as symbol from './symbol'; import { ExtensionContext, workspace, window, commands } from 'vscode'; import { LanguageClient, LanguageClientOptions, SettingMonitor, ServerOptions, TransportKind, NotificationType } from 'vscode-languageclient'; @@ -110,6 +111,16 @@ language_client.onReady().then(() => preview.init(context, language_client)) + /* Isabelle symbols */ + + language_client.onReady().then(() => + { + language_client.onNotification(protocol.symbols_type, + params => symbol.update(params.entries)) + language_client.sendNotification(protocol.symbols_request_type) + }) + + /* start server */ context.subscriptions.push(language_client.start()) diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/extension/src/protocol.ts --- a/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/extension/src/protocol.ts Fri Jun 09 22:55:18 2017 +0200 @@ -2,6 +2,7 @@ import { Position, Range, MarkedString, DecorationOptions, DecorationRenderOptions } from 'vscode' import { NotificationType } from 'vscode-languageclient'; +import * as symbol from './symbol' /* decorations */ @@ -67,3 +68,17 @@ export const preview_response_type = new NotificationType("PIDE/preview_response") + + +/* Isabelle symbols */ + +export interface Symbols +{ + entries: [symbol.Entry] +} + +export const symbols_type = + new NotificationType("PIDE/symbols") + +export const symbols_request_type = + new NotificationType("PIDE/symbols_request") diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/extension/src/symbol.ts --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/extension/src/symbol.ts Fri Jun 09 22:55:18 2017 +0200 @@ -0,0 +1,41 @@ +'use strict'; + +export type Symbol = string + +export interface Entry +{ + symbol: Symbol, + name: string, + code: number +} + +let symbol_entries: [Entry] +const names = new Map() +const codes = new Map() + +export function get_name(sym: Symbol): string | undefined +{ + return names.get(sym) +} + +export function get_code(sym: Symbol): number | undefined +{ + return codes.get(sym) +} + +export function get_unicode(sym: Symbol): string +{ + const code = get_code(sym) + return code ? String.fromCharCode(code) : "" +} + +export function update(entries: [Entry]) +{ + symbol_entries = entries + names.clear + codes.clear + for (const entry of entries) { + names.set(entry.symbol, entry.name) + codes.set(entry.symbol, entry.code) + } +} \ No newline at end of file diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/src/document_model.scala Fri Jun 09 22:55:18 2017 +0200 @@ -191,4 +191,12 @@ def rendering(snapshot: Document.Snapshot): VSCode_Rendering = new VSCode_Rendering(this, snapshot) def rendering(): VSCode_Rendering = rendering(snapshot()) + + + /* syntax */ + + lazy private val syntax0 = Outer_Syntax.init() + + def syntax(): Outer_Syntax = + if (is_theory) session.recent_syntax(node_name) else syntax0 } diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/src/protocol.scala --- a/src/Tools/VSCode/src/protocol.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/src/protocol.scala Fri Jun 09 22:55:18 2017 +0200 @@ -491,4 +491,20 @@ "label" -> label, "content" -> content)) } + + + /* Isabelle symbols */ + + object Symbols_Request extends Notification0("PIDE/symbols_request") + + object Symbols + { + def apply(): JSON.T = + { + val entries = + for ((sym, code) <- Symbol.codes) + yield Map("symbol" -> sym, "name" -> Symbol.names(sym), "code" -> code) + Notification("PIDE/symbols", Map("entries" -> entries)) + } + } } diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/src/server.scala Fri Jun 09 22:55:18 2017 +0200 @@ -325,7 +325,7 @@ { val result = (for ((rendering, offset) <- rendering_offset(node_pos)) - yield rendering.completion(Text.Range(offset - 1, offset))) getOrElse Nil + yield rendering.completion(node_pos.pos, offset)) getOrElse Nil channel.write(Protocol.Completion.reply(id, result)) } @@ -398,6 +398,7 @@ case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos) case Protocol.Caret_Update(caret) => update_caret(caret) case Protocol.Preview_Request(file, column) => request_preview(file, column) + case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols()) case _ => log("### IGNORED") } } diff -r 3804a9640088 -r 637b26fd3349 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Fri Jun 09 22:55:18 2017 +0200 @@ -68,27 +68,51 @@ class VSCode_Rendering(val model: Document_Model, snapshot: Document.Snapshot) extends Rendering(snapshot, model.resources.options, model.session) { + rendering => + + /* completion */ - def completion(range: Text.Range): List[Protocol.CompletionItem] = - semantic_completion(None, range) match { - case Some(Text.Info(complete_range, names: Completion.Names)) => - model.content.try_get_text(complete_range) match { - case Some(original) => - names.complete(complete_range, Completion.History.empty, - model.resources.unicode_symbols, original) match { - case Some(result) => - result.items.map(item => - Protocol.CompletionItem( - label = item.replacement, - detail = Some(item.description.mkString(" ")), - range = Some(model.content.doc.range(item.range)))) - case None => Nil - } - case None => Nil + def before_caret_range(caret: Text.Offset): Text.Range = + { + val former_caret = snapshot.revert(caret) + snapshot.convert(Text.Range(former_caret - 1, former_caret)) + } + + def completion(caret_pos: Line.Position, caret: Text.Offset): List[Protocol.CompletionItem] = + { + val doc = model.content.doc + val line = caret_pos.line + doc.offset(Line.Position(line)) match { + case None => Nil + case Some(line_start) => + val history = Completion.History.empty + val caret_range = before_caret_range(caret) + + val syntax = model.syntax() + val syntax_completion = + syntax.completion.complete(history, unicode = false, explicit = true, + line_start, doc.lines(line).text, caret - line_start, + language_context(caret_range) getOrElse syntax.language_context) + + val (no_completion, semantic_completion) = + rendering.semantic_completion_result( + history, false, syntax_completion.map(_.range), caret_range, doc.try_get_text(_)) + + if (no_completion) Nil + else { + Completion.Result.merge(history, semantic_completion, syntax_completion) match { + case None => Nil + case Some(result) => + result.items.map(item => + Protocol.CompletionItem( + label = item.replacement, + detail = Some(item.description.mkString(" ")), + range = Some(doc.range(item.range)))) + } } - case _ => Nil } + } /* diagnostics */ diff -r 3804a9640088 -r 637b26fd3349 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Fri Jun 09 22:55:18 2017 +0200 @@ -156,7 +156,7 @@ opt_rendering: Option[JEdit_Rendering]): Option[Completion.Result] = { val buffer = text_area.getBuffer - val decode = Isabelle_Encoding.is_active(buffer) + val unicode = Isabelle_Encoding.is_active(buffer) Isabelle.buffer_syntax(buffer) match { case Some(syntax) => @@ -164,8 +164,8 @@ (for { rendering <- opt_rendering if PIDE.options.bool("jedit_completion_context") - range = JEdit_Lib.before_caret_range(text_area, rendering) - context <- rendering.language_context(range) + caret_range = JEdit_Lib.before_caret_range(text_area, rendering) + context <- rendering.language_context(caret_range) } yield context) getOrElse syntax.language_context val caret = text_area.getCaretPosition @@ -175,7 +175,7 @@ line_text <- JEdit_Lib.try_get_text(buffer, line_range) result <- syntax.completion.complete( - history, decode, explicit, line_start, line_text, caret - line_start, context) + history, unicode, explicit, line_start, line_text, caret - line_start, context) } yield result case None => None @@ -294,7 +294,7 @@ val painter = text_area.getPainter val history = PIDE.plugin.completion_history.value - val decode = Isabelle_Encoding.is_active(buffer) + val unicode = Isabelle_Encoding.is_active(buffer) def open_popup(result: Completion.Result) { @@ -355,16 +355,9 @@ { opt_rendering match { case Some(rendering) => - val caret_range = JEdit_Lib.before_caret_range(text_area, rendering) - rendering.semantic_completion(result0.map(_.range), caret_range) match { - case Some(Text.Info(_, Completion.No_Completion)) => (true, None) - case Some(Text.Info(range, names: Completion.Names)) => - JEdit_Lib.try_get_text(buffer, range) match { - case Some(original) => (false, names.complete(range, history, decode, original)) - case None => (false, None) - } - case None => (false, None) - } + rendering.semantic_completion_result(history, unicode, result0.map(_.range), + JEdit_Lib.before_caret_range(text_area, rendering), + JEdit_Lib.try_get_text(buffer, _)) case None => (false, None) } } diff -r 3804a9640088 -r 637b26fd3349 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Jun 09 18:36:25 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Jun 09 22:55:18 2017 +0200 @@ -113,15 +113,6 @@ private val indentation_elements = Markup.Elements(Markup.Command_Indent.name) - private val language_context_elements = - Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM, - Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE, - Markup.ML_STRING, Markup.ML_COMMENT) - - private val language_elements = Markup.Elements(Markup.LANGUAGE) - - private val citation_elements = Markup.Elements(Markup.CITATION) - private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT) private val highlight_elements = @@ -199,38 +190,6 @@ }).headOption.map(_.info).getOrElse(0) - /* completion */ - - def language_context(range: Text.Range): Option[Completion.Language_Context] = - snapshot.select(range, JEdit_Rendering.language_context_elements, _ => - { - case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) => - if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes)) - else None - case Text.Info(_, elem) - if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT => - Some(Completion.Language_Context.ML_inner) - case Text.Info(_, _) => - Some(Completion.Language_Context.inner) - }).headOption.map(_.info) - - def language_path(range: Text.Range): Option[Text.Range] = - snapshot.select(range, JEdit_Rendering.language_elements, _ => - { - case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) => - Some(snapshot.convert(info_range)) - case _ => None - }).headOption.map(_.info) - - def citation(range: Text.Range): Option[Text.Info[String]] = - snapshot.select(range, JEdit_Rendering.citation_elements, _ => - { - case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) => - Some(Text.Info(snapshot.convert(info_range), name)) - case _ => None - }).headOption.map(_.info) - - /* breakpoints */ def breakpoint(range: Text.Range): Option[(Command, Long)] =