--- 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) + ")")
--- 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)
--- 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 */
--- 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())
--- 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<Preview_Response, void>("PIDE/preview_response")
+
+
+/* Isabelle symbols */
+
+export interface Symbols
+{
+ entries: [symbol.Entry]
+}
+
+export const symbols_type =
+ new NotificationType<Symbols, void>("PIDE/symbols")
+
+export const symbols_request_type =
+ new NotificationType<void, void>("PIDE/symbols_request")
--- /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<Symbol, string>()
+const codes = new Map<Symbol, number>()
+
+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
--- 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
}
--- 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))
+ }
+ }
}
--- 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")
}
}
--- 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 */
--- 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)
}
}
--- 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)] =