--- a/src/Pure/General/codepoint.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/General/codepoint.scala Wed Dec 28 20:42:28 2016 +0100
@@ -25,7 +25,7 @@
def length(s: String): Int = iterator(s).length
- trait Length extends isabelle.Length
+ trait Length extends Text.Length
{
protected def codepoint_length(c: Int): Int = 1
@@ -34,7 +34,7 @@
def offset(s: String, i: Int): Option[Text.Offset] =
{
- if (i <= 0 || s.forall(_ < 0x80)) isabelle.Length.offset(s, i)
+ if (i <= 0 || s.forall(_ < 0x80)) Text.Length.offset(s, i)
else {
val length = s.length
var offset = 0
--- a/src/Pure/General/length.scala Wed Dec 28 17:22:16 2016 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,33 +0,0 @@
-/* Title: Pure/General/length.scala
- Author: Makarius
-
-Text length wrt. encoding.
-*/
-
-package isabelle
-
-
-trait Length
-{
- def apply(text: String): Int
- def offset(text: String, i: Int): Option[Text.Offset]
-}
-
-object Length extends Length
-{
- def apply(text: String): Int = text.length
- def offset(text: String, i: Int): Option[Text.Offset] =
- if (0 <= i && i <= text.length) Some(i) else None
-
- val encodings: List[(String, Length)] =
- List(
- "UTF-16" -> Length,
- "UTF-8" -> UTF8.Length,
- "codepoints" -> Codepoint.Length,
- "symbols" -> Symbol.Length)
-
- def encoding(name: String): Length =
- encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
- error("Bad text length encoding: " + quote(name) +
- " (expected " + commas_quote(encodings.map(_._1)) + ")")
-}
--- a/src/Pure/General/symbol.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/General/symbol.scala Wed Dec 28 20:42:28 2016 +0100
@@ -130,11 +130,11 @@
def length(text: CharSequence): Int = iterator(text).length
- object Length extends isabelle.Length
+ object Length extends Text.Length
{
def apply(text: String): Int = length(text)
def offset(text: String, i: Int): Option[Text.Offset] =
- if (i <= 0 || iterator(text).forall(s => s.length == 1)) isabelle.Length.offset(text, i)
+ if (i <= 0 || iterator(text).forall(s => s.length == 1)) Text.Length.offset(text, i)
else if (i <= length(text)) Some(iterator(text).take(i).mkString.length)
else None
}
--- a/src/Pure/Isar/token.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Isar/token.ML Wed Dec 28 20:42:28 2016 +0100
@@ -275,7 +275,7 @@
| Verbatim => (Markup.verbatim, "")
| Cartouche => (Markup.cartouche, "")
| Comment => (Markup.comment, "")
- | Error msg => (Markup.bad, msg)
+ | Error msg => (Markup.bad (), msg)
| _ => (Markup.empty, "");
fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));
--- a/src/Pure/ML/ml_lex.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/ML/ml_lex.ML Wed Dec 28 20:42:28 2016 +0100
@@ -147,7 +147,7 @@
| Char => (Markup.ML_char, "")
| String => (if SML then Markup.SML_string else Markup.ML_string, "")
| Comment => (if SML then Markup.SML_comment else Markup.ML_comment, "")
- | Error msg => (Markup.bad, msg)
+ | Error msg => (Markup.bad (), msg)
| _ => (Markup.empty, "");
in
--- a/src/Pure/PIDE/command.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/command.ML Wed Dec 28 20:42:28 2016 +0100
@@ -116,7 +116,7 @@
Input.source_explode (Token.input_of tok)
|> map_filter (fn (sym, pos) =>
if Symbol.is_malformed sym
- then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
+ then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE);
val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols;
in (is_malformed, reports) end;
@@ -242,7 +242,7 @@
let
val _ = status tr Markup.failed;
val _ = status tr Markup.finished;
- val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
+ val _ = if null errs then (report tr (Markup.bad ()); Exn.interrupt ()) else ();
in {failed = true, command = tr, state = st} end
| SOME st' =>
let
--- a/src/Pure/PIDE/document.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/document.scala Wed Dec 28 20:42:28 2016 +0100
@@ -808,7 +808,7 @@
node.commands.iterator.takeWhile(_ != command).map(_.source) ++
(if (offset == 0) Iterator.empty
else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset)))))
- val pos = (Line.Position.zero /: sources_iterator)(_.advance(_))
+ val pos = (Line.Position.zero /: sources_iterator)(_.advance(_, Text.Length))
Line.Node_Position(name, pos)
}
--- a/src/Pure/PIDE/execution.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/execution.ML Wed Dec 28 20:42:28 2016 +0100
@@ -116,7 +116,7 @@
Exn.Exn exn =>
(status task [Markup.failed];
status task [Markup.finished];
- Output.report [Markup.markup_only Markup.bad];
+ Output.report [Markup.markup_only (Markup.bad ())];
if exec_id = 0 then ()
else List.app (Future.error_message pos) (Runtime.exn_messages_ids exn))
| Exn.Res _ =>
--- a/src/Pure/PIDE/line.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/line.scala Wed Dec 28 20:42:28 2016 +0100
@@ -31,12 +31,12 @@
case i => i
}
- def advance(text: String, length: Length = Length): Position =
+ def advance(text: String, text_length: Text.Length): Position =
if (text.isEmpty) this
else {
val lines = Library.split_lines(text)
val l = line + lines.length - 1
- val c = (if (l == line) column else 0) + length(Library.trim_line(lines.last))
+ val c = (if (l == line) column else 0) + text_length(Library.trim_line(lines.last))
Position(l, c)
}
}
@@ -80,21 +80,14 @@
object Document
{
- val empty: Document = new Document(Nil)
-
- def apply(lines: List[Line]): Document =
- if (lines.isEmpty) empty
- else new Document(lines)
-
- def apply(text: String): Document =
- if (text == "") empty
- else if (text.contains('\r'))
- new Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))))
+ def apply(text: String, text_length: Text.Length): Document =
+ if (text.contains('\r'))
+ Document(Library.split_lines(text).map(s => Line(Library.trim_line(s))), text_length)
else
- new Document(Library.split_lines(text).map(s => Line(s)))
+ Document(Library.split_lines(text).map(s => Line(s)), text_length)
}
- final class Document private(val lines: List[Line])
+ sealed case class Document(lines: List[Line], text_length: Text.Length)
{
def make_text: String = lines.mkString("", "\n", "")
@@ -107,7 +100,7 @@
}
override def hashCode(): Int = lines.hashCode
- def position(offset: Text.Offset, length: Length = Length): Position =
+ def position(text_offset: Text.Offset): Position =
{
@tailrec def move(i: Text.Offset, lines_count: Int, lines_rest: List[Line]): Position =
{
@@ -116,25 +109,34 @@
case line :: ls =>
val n = line.text.length
if (ls.isEmpty || i <= n)
- Position(lines_count).advance(line.text.substring(n - i), length)
+ Position(lines_count).advance(line.text.substring(n - i), text_length)
else move(i - (n + 1), lines_count + 1, ls)
}
}
- move(offset, 0, lines)
+ move(text_offset, 0, lines)
}
- def offset(pos: Position, length: Length = Length): Option[Text.Offset] =
+ def range(text_range: Text.Range): Range =
+ Range(position(text_range.start), position(text_range.stop))
+
+ def offset(pos: Position): Option[Text.Offset] =
{
val l = pos.line
val c = pos.column
if (0 <= l && l < lines.length) {
val line_offset =
if (l == 0) 0
- else (0 /: lines.iterator.take(l - 1))({ case (n, line) => n + length(line.text) + 1 })
- length.offset(lines(l).text, c).map(line_offset + _)
+ else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
+ text_length.offset(lines(l).text, c).map(line_offset + _)
}
else None
}
+
+ lazy val end_offset: Text.Offset =
+ if (lines.isEmpty) 0
+ else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
+
+ def full_range: Text.Range = Text.Range(0, end_offset)
}
@@ -148,8 +150,6 @@
{
require(text.forall(c => c != '\r' && c != '\n'))
- lazy val length_codepoints: Int = Codepoint.iterator(text).length
-
override def equals(that: Any): Boolean =
that match {
case other: Line => text == other.text
--- a/src/Pure/PIDE/markup.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/markup.ML Wed Dec 28 20:42:28 2016 +0100
@@ -173,7 +173,7 @@
val protocolN: string
val reportN: string val report: T
val no_reportN: string val no_report: T
- val badN: string val bad: T
+ val badN: string val bad: unit -> T
val intensifyN: string val intensify: T
val browserN: string
val graphviewN: string
@@ -573,7 +573,8 @@
val (reportN, report) = markup_elem "report";
val (no_reportN, no_report) = markup_elem "no_report";
-val (badN, bad) = markup_elem "bad";
+val badN = "bad";
+fun bad () = (badN, serial_properties (serial ()));
val (intensifyN, intensify) = markup_elem "intensify";
--- a/src/Pure/PIDE/rendering.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/rendering.scala Wed Dec 28 20:42:28 2016 +0100
@@ -10,6 +10,35 @@
object Rendering
{
+ /* message priorities */
+
+ val state_pri = 1
+ val writeln_pri = 2
+ val information_pri = 3
+ val tracing_pri = 4
+ val warning_pri = 5
+ val legacy_pri = 6
+ val error_pri = 7
+
+ val message_pri = Map(
+ Markup.STATE -> state_pri,
+ Markup.STATE_MESSAGE -> state_pri,
+ Markup.WRITELN -> writeln_pri,
+ Markup.WRITELN_MESSAGE -> writeln_pri,
+ Markup.INFORMATION -> information_pri,
+ Markup.INFORMATION_MESSAGE -> information_pri,
+ Markup.TRACING -> tracing_pri,
+ Markup.TRACING_MESSAGE -> tracing_pri,
+ Markup.WARNING -> warning_pri,
+ Markup.WARNING_MESSAGE -> warning_pri,
+ Markup.LEGACY -> legacy_pri,
+ Markup.LEGACY_MESSAGE -> legacy_pri,
+ Markup.ERROR -> error_pri,
+ Markup.ERROR_MESSAGE -> error_pri)
+
+
+ /* markup elements */
+
private val tooltip_descriptions =
Map(
Markup.CITATION -> "citation",
--- a/src/Pure/PIDE/text.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/PIDE/text.scala Wed Dec 28 20:42:28 2016 +0100
@@ -25,6 +25,7 @@
{
def apply(start: Offset): Range = Range(start, start)
+ val full: Range = apply(0, Integer.MAX_VALUE / 2)
val offside: Range = apply(-1)
object Ordering extends scala.math.Ordering[Text.Range]
@@ -79,7 +80,7 @@
{
val empty: Perspective = Perspective(Nil)
- def full: Perspective = Perspective(List(Range(0, Integer.MAX_VALUE / 2)))
+ def full: Perspective = Perspective(List(Range.full))
def apply(ranges: Seq[Range]): Perspective =
{
@@ -180,4 +181,32 @@
(rest, remove(i, count, string))
}
}
+
+
+ /* text length wrt. encoding */
+
+ trait Length
+ {
+ def apply(text: String): Int
+ def offset(text: String, i: Int): Option[Text.Offset]
+ }
+
+ object Length extends Length
+ {
+ def apply(text: String): Int = text.length
+ def offset(text: String, i: Int): Option[Text.Offset] =
+ if (0 <= i && i <= text.length) Some(i) else None
+
+ val encodings: List[(String, Length)] =
+ List(
+ "UTF-16" -> Length,
+ "UTF-8" -> UTF8.Length,
+ "codepoints" -> Codepoint.Length,
+ "symbols" -> Symbol.Length)
+
+ def encoding(name: String): Length =
+ encodings.collectFirst({ case (a, length) if name == a => length }) getOrElse
+ error("Bad text length encoding: " + quote(name) +
+ " (expected " + commas_quote(encodings.map(_._1)) + ")")
+ }
}
--- a/src/Pure/Pure.thy Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Pure.thy Wed Dec 28 20:42:28 2016 +0100
@@ -991,7 +991,7 @@
local
fun report_back () =
- Output.report [Markup.markup Markup.bad "Explicit backtracking"];
+ Output.report [Markup.markup (Markup.bad ()) "Explicit backtracking"];
val _ =
Outer_Syntax.command @{command_keyword back} "explicit backtracking of proof command"
--- a/src/Pure/Syntax/syntax_ext.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML Wed Dec 28 20:42:28 2016 +0100
@@ -217,7 +217,7 @@
(case xsym of
Delim s =>
if Position.is_reported pos andalso exists Symbol.is_utf8 (Symbol.explode s) then
- [((pos, Markup.bad),
+ [((pos, Markup.bad ()),
"Mixfix delimiter contains raw Unicode -- this is non-portable and unreliable")]
else []
| _ => []);
--- a/src/Pure/Syntax/syntax_phases.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Wed Dec 28 20:42:28 2016 +0100
@@ -375,7 +375,7 @@
fun parse_failed ctxt pos msg kind =
cat_error msg ("Failed to parse " ^ kind ^
- Markup.markup_report (Context_Position.reported_text ctxt pos Markup.bad ""));
+ Markup.markup_report (Context_Position.reported_text ctxt pos (Markup.bad ()) ""));
fun parse_sort ctxt =
Syntax.parse_input ctxt Term_XML.Decode.sort Markup.language_sort
@@ -746,7 +746,7 @@
| token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
| token_trans "_free" x = SOME (Pretty.marks_str (free_or_skolem ctxt x))
| token_trans "_bound" x = SOME (Pretty.mark_str (Markup.bound, x))
- | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad, x))
+ | token_trans "_loose" x = SOME (Pretty.mark_str (Markup.bad (), x))
| token_trans "_var" x = SOME (Pretty.mark_str (var_or_skolem x))
| token_trans "_numeral" x = SOME (Pretty.mark_str (Markup.numeral, x))
| token_trans "_inner_string" x = SOME (Pretty.mark_str (Markup.inner_string, x))
--- a/src/Pure/Tools/print_operation.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/Tools/print_operation.ML Wed Dec 28 20:42:28 2016 +0100
@@ -49,7 +49,7 @@
(fn {state, args, writeln_result, ...} =>
let
val _ = Toplevel.context_of state handle Toplevel.UNDEF => error "Unknown context";
- fun err s = Pretty.mark_str (Markup.bad, s);
+ fun err s = Pretty.mark_str (Markup.bad (), s);
fun print name =
(case AList.lookup (op =) (Synchronized.value print_operations) name of
SOME (_, pr) => (pr state handle Toplevel.UNDEF => [err "Unknown context"])
--- a/src/Pure/build-jars Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/build-jars Wed Dec 28 20:42:28 2016 +0100
@@ -49,7 +49,6 @@
General/graphics_file.scala
General/http_server.scala
General/json.scala
- General/length.scala
General/linear_set.scala
General/logger.scala
General/long_name.scala
--- a/src/Pure/skip_proof.ML Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Pure/skip_proof.ML Wed Dec 28 20:42:28 2016 +0100
@@ -19,7 +19,7 @@
fun report ctxt =
if Context_Position.is_visible ctxt then
- Output.report [Markup.markup Markup.bad "Skipped proof"]
+ Output.report [Markup.markup (Markup.bad ()) "Skipped proof"]
else ();
--- a/src/Tools/VSCode/etc/options Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/etc/options Wed Dec 28 20:42:28 2016 +0100
@@ -1,7 +1,16 @@
(* :mode=isabelle-options: *)
+option vscode_input_delay : real = 0.3
+ -- "delay for client input (edits)"
+
+option vscode_output_delay : real = 0.5
+ -- "delay for client output (rendering)"
+
option vscode_tooltip_margin : int = 60
- -- "margin for tooltip pretty-printing"
+ -- "margin for pretty-printing of tooltips"
+
+option vscode_diagnostics_margin : int = 80
+ -- "margin for pretty-printing of diagnostic messages"
option vscode_timing_threshold : real = 0.1
-- "default threshold for timing display (seconds)"
--- a/src/Tools/VSCode/src/channel.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/channel.scala Wed Dec 28 20:42:28 2016 +0100
@@ -90,13 +90,20 @@
/* display message */
- def display_message(message_type: Int, message: String, show: Boolean = true): Unit =
- write(Protocol.DisplayMessage(message_type, Output.clean_yxml(message), show))
+ def display_message(message_type: Int, msg: String, show: Boolean = true): Unit =
+ write(Protocol.DisplayMessage(message_type, Output.clean_yxml(msg), show))
+
+ def error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, true) }
+ def warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, true) }
+ def writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, true) }
- def error_message(message: String, show: Boolean = true): Unit =
- display_message(Protocol.MessageType.Error, message, show)
- def warning(message: String, show: Boolean = true): Unit =
- display_message(Protocol.MessageType.Warning, message, show)
- def writeln(message: String, show: Boolean = true): Unit =
- display_message(Protocol.MessageType.Info, message, show)
+ def log_error_message(msg: String) { display_message(Protocol.MessageType.Error, msg, false) }
+ def log_warning(msg: String) { display_message(Protocol.MessageType.Warning, msg, false) }
+ def log_writeln(msg: String) { display_message(Protocol.MessageType.Info, msg, false) }
+
+
+ /* diagnostics */
+
+ def diagnostics(uri: String, diagnostics: List[Protocol.Diagnostic]): Unit =
+ write(Protocol.PublishDiagnostics(uri, diagnostics))
}
--- a/src/Tools/VSCode/src/document_model.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala Wed Dec 28 20:42:28 2016 +0100
@@ -14,12 +14,20 @@
case class Document_Model(
session: Session, doc: Line.Document, node_name: Document.Node.Name,
- changed: Boolean = true)
+ changed: Boolean = true,
+ published_diagnostics: List[Text.Info[Command.Results]] = Nil)
{
+ override def toString: String = node_name.toString
+
+
+ /* name */
+
+ def uri: String = node_name.node
+ def is_theory: Boolean = node_name.is_theory
+
+
/* header */
- def is_theory: Boolean = node_name.is_theory
-
def node_header(resources: VSCode_Resources): Document.Node.Header =
resources.special_header(node_name) getOrElse
{
@@ -48,10 +56,21 @@
def unchanged: Document_Model = if (changed) copy(changed = false) else this
+ /* diagnostics */
+
+ def publish_diagnostics(rendering: VSCode_Rendering)
+ : Option[(List[Text.Info[Command.Results]], Document_Model)] =
+ {
+ val diagnostics = rendering.diagnostics
+ if (diagnostics == published_diagnostics) None
+ else Some(diagnostics, copy(published_diagnostics = diagnostics))
+ }
+
+
/* snapshot and rendering */
def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
- def rendering(options: Options, text_length: Length): VSCode_Rendering =
- new VSCode_Rendering(this, snapshot(), options, text_length, session.resources)
+ def rendering(options: Options): VSCode_Rendering =
+ new VSCode_Rendering(this, snapshot(), options, session.resources)
}
--- a/src/Tools/VSCode/src/protocol.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/protocol.scala Wed Dec 28 20:42:28 2016 +0100
@@ -311,4 +311,32 @@
def reply(id: Id, result: List[Line.Node_Range]): JSON.T =
ResponseMessage(id, Some(result.map(Location.apply(_))))
}
+
+
+ /* diagnostics */
+
+ sealed case class Diagnostic(range: Line.Range, message: String,
+ severity: Option[Int] = None, code: Option[Int] = None, source: Option[String] = None)
+ {
+ def json: JSON.T =
+ Message.empty + ("range" -> Range(range)) + ("message" -> message) ++
+ (severity match { case Some(x) => Map("severity" -> x) case None => Map.empty }) ++
+ (code match { case Some(x) => Map("code" -> x) case None => Map.empty }) ++
+ (source match { case Some(x) => Map("source" -> x) case None => Map.empty })
+ }
+
+ object DiagnosticSeverity
+ {
+ val Error = 0
+ val Warning = 1
+ val Information = 2
+ val Hint = 3
+ }
+
+ object PublishDiagnostics
+ {
+ def apply(uri: String, diagnostics: List[Diagnostic]): JSON.T =
+ Notification("textDocument/publishDiagnostics",
+ Map("uri" -> uri, "diagnostics" -> diagnostics.map(_.json)))
+ }
}
--- a/src/Tools/VSCode/src/server.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala Wed Dec 28 20:42:28 2016 +0100
@@ -27,14 +27,14 @@
{
try {
var log_file: Option[Path] = None
- var text_length = Length.encoding(default_text_length)
+ var text_length = Text.Length.encoding(default_text_length)
var dirs: List[Path] = Nil
var logic = default_logic
var modes: List[String] = Nil
var options = Options.init()
def text_length_choice: String =
- commas(Length.encodings.map(
+ commas(Text.Length.encodings.map(
{ case (a, _) => if (a == default_text_length) a + " (default)" else a }))
val getopts = Getopts("""
@@ -51,7 +51,7 @@
Run the VSCode Language Server protocol (JSON RPC) over stdin/stdout.
""",
"L:" -> (arg => log_file = Some(Path.explode(arg))),
- "T:" -> (arg => Length.encoding(arg)),
+ "T:" -> (arg => Text.Length.encoding(arg)),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
"l:" -> (arg => logic = arg),
"m:" -> (arg => modes = arg :: modes),
@@ -88,13 +88,15 @@
sealed case class State(
session: Option[Session] = None,
- models: Map[String, Document_Model] = Map.empty)
+ models: Map[String, Document_Model] = Map.empty,
+ pending_input: Set[Document.Node.Name] = Set.empty,
+ pending_output: Set[Document.Node.Name] = Set.empty)
}
class Server(
channel: Channel,
options: Options,
- text_length: Length = Length.encoding(Server.default_text_length),
+ text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
session_name: String = Server.default_logic,
session_dirs: List[Path] = Nil,
modes: List[String] = Nil)
@@ -109,11 +111,88 @@
def rendering_offset(node_pos: Line.Node_Position): Option[(VSCode_Rendering, Text.Offset)] =
for {
model <- state.value.models.get(node_pos.name)
- rendering = model.rendering(options, text_length)
- offset <- model.doc.offset(node_pos.pos, text_length)
+ rendering = model.rendering(options)
+ offset <- model.doc.offset(node_pos.pos)
} yield (rendering, offset)
+ /* input from client */
+
+ private val delay_input =
+ Standard_Thread.delay_last(options.seconds("vscode_input_delay")) {
+ state.change(st =>
+ {
+ val changed =
+ (for {
+ node_name <- st.pending_input.iterator
+ model <- st.models.get(node_name.node)
+ if model.changed } yield model).toList
+ session.update(Document.Blobs.empty,
+ for { model <- changed; edit <- model.node_edits(resources) } yield edit)
+ st.copy(
+ models = (st.models /: changed) { case (ms, m) => ms + (m.uri -> m.unchanged) },
+ pending_input = Set.empty)
+ })
+ }
+
+ def update_document(uri: String, text: String)
+ {
+ state.change(st =>
+ {
+ val node_name = resources.node_name(uri)
+ val model = Document_Model(session, Line.Document(text, text_length), node_name)
+ st.copy(
+ models = st.models + (uri -> model),
+ pending_input = st.pending_input + node_name)
+ })
+ delay_input.invoke()
+ }
+
+
+ /* output to client */
+
+ private val commands_changed =
+ Session.Consumer[Session.Commands_Changed](getClass.getName) {
+ case changed =>
+ state.change(st => st.copy(pending_output = st.pending_output ++ changed.nodes))
+ delay_output.invoke()
+ }
+
+ private val delay_output: Standard_Thread.Delay =
+ Standard_Thread.delay_last(options.seconds("vscode_output_delay")) {
+ if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
+ else {
+ state.change(st =>
+ {
+ val changed_iterator =
+ for {
+ node_name <- st.pending_output.iterator
+ model <- st.models.get(node_name.node)
+ rendering = model.rendering(options)
+ (diagnostics, model1) <- model.publish_diagnostics(rendering)
+ } yield {
+ channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
+ model1
+ }
+ st.copy(
+ models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
+ pending_output = Set.empty)
+ }
+ )
+ }
+ }
+
+
+ /* syslog */
+
+ private val all_messages =
+ Session.Consumer[Prover.Message](getClass.getName) {
+ case output: Prover.Output if output.is_syslog =>
+ channel.log_writeln(XML.content(output.message))
+ case _ =>
+ }
+
+
/* init and exit */
def init(id: Protocol.Id)
@@ -156,6 +235,9 @@
}
session.phase_changed += session_phase
+ session.commands_changed += commands_changed
+ session.all_messages += all_messages
+
session.start(receiver =>
Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
modes = modes, receiver = receiver))
@@ -177,11 +259,15 @@
Session.Consumer(getClass.getName) {
case Session.Inactive =>
session.phase_changed -= session_phase
+ session.commands_changed -= commands_changed
+ session.all_messages -= all_messages
reply("")
case _ =>
}
session.phase_changed += session_phase
session.stop()
+ delay_input.revoke()
+ delay_output.revoke()
st.copy(session = None)
})
}
@@ -192,35 +278,6 @@
}
- /* document management */
-
- private val delay_flush =
- Standard_Thread.delay_last(options.seconds("editor_input_delay")) {
- state.change(st =>
- {
- val models = st.models
- val changed = (for { entry <- models.iterator if entry._2.changed } yield entry).toList
- val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit
- val models1 =
- (models /: changed)({ case (m, (uri, model)) => m + (uri -> model.unchanged) })
-
- session.update(Document.Blobs.empty, edits)
- st.copy(models = models1)
- })
- }
-
- def update_document(uri: String, text: String)
- {
- state.change(st =>
- {
- val node_name = resources.node_name(uri)
- val model = Document_Model(session, Line.Document(text), node_name)
- st.copy(models = st.models + (uri -> model))
- })
- delay_flush.invoke()
- }
-
-
/* hover */
def hover(id: Protocol.Id, node_pos: Line.Node_Position)
@@ -231,10 +288,9 @@
info <- rendering.tooltip(Text.Range(offset, offset + 1))
} yield {
val doc = rendering.model.doc
- val start = doc.position(info.range.start, text_length)
- val stop = doc.position(info.range.stop, text_length)
+ val range = doc.range(info.range)
val s = Pretty.string_of(info.info, margin = rendering.tooltip_margin)
- (Line.Range(start, stop), List("```\n" + s + "\n```")) // FIXME proper content format
+ (range, List("```\n" + s + "\n```")) // FIXME proper content format
}
channel.write(Protocol.Hover.reply(id, result))
}
@@ -275,7 +331,7 @@
case _ => channel.log("### IGNORED")
}
}
- catch { case exn: Throwable => channel.error_message(Exn.message(exn)) }
+ catch { case exn: Throwable => channel.log_error_message(Exn.message(exn)) }
}
@tailrec def loop()
--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 20:42:28 2016 +0100
@@ -12,6 +12,24 @@
object VSCode_Rendering
{
+ /* diagnostic messages */
+
+ private val message_severity =
+ Map(
+ Markup.WRITELN -> Protocol.DiagnosticSeverity.Hint,
+ Markup.INFORMATION -> Protocol.DiagnosticSeverity.Information,
+ Markup.WARNING -> Protocol.DiagnosticSeverity.Warning,
+ Markup.LEGACY -> Protocol.DiagnosticSeverity.Warning,
+ Markup.ERROR -> Protocol.DiagnosticSeverity.Error,
+ Markup.BAD -> Protocol.DiagnosticSeverity.Error)
+
+
+ /* markup elements */
+
+ private val diagnostics_elements =
+ Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR,
+ Markup.BAD)
+
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION)
}
@@ -20,10 +38,37 @@
val model: Document_Model,
snapshot: Document.Snapshot,
options: Options,
- text_length: Length,
resources: Resources)
extends Rendering(snapshot, options, resources)
{
+ /* diagnostics */
+
+ def diagnostics: List[Text.Info[Command.Results]] =
+ snapshot.cumulate[Command.Results](
+ model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ =>
+ {
+ case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body)))
+ if body.nonEmpty => Some(res + (i -> msg))
+
+ case _ => None
+ })
+
+ val diagnostics_margin = options.int("vscode_diagnostics_margin")
+
+ def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] =
+ {
+ (for {
+ Text.Info(text_range, res) <- results.iterator
+ range = model.doc.range(text_range)
+ (_, XML.Elem(Markup(name, _), body)) <- res.iterator
+ } yield {
+ val message = Pretty.string_of(body, margin = diagnostics_margin)
+ val severity = VSCode_Rendering.message_severity.get(name)
+ Protocol.Diagnostic(range, message, severity = severity)
+ }).toList
+ }
+
+
/* tooltips */
def tooltip_margin: Int = options.int("vscode_tooltip_margin")
@@ -44,9 +89,8 @@
opt_text match {
case Some(text) if range.start > 0 =>
val chunk = Symbol.Text_Chunk(text)
- val doc = Line.Document(text)
- def position(offset: Symbol.Offset) = doc.position(chunk.decode(offset), text_length)
- Line.Range(position(range.start), position(range.stop))
+ val doc = Line.Document(text, model.doc.text_length)
+ doc.range(chunk.decode(range))
case _ =>
Line.Range(Line.Position((line1 - 1) max 0))
})
--- a/src/Tools/jEdit/src/document_model.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Wed Dec 28 20:42:28 2016 +0100
@@ -69,6 +69,9 @@
class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name)
{
+ override def toString: String = node_name.toString
+
+
/* header */
def is_theory: Boolean = node_name.is_theory
--- a/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Wed Dec 28 20:42:28 2016 +0100
@@ -270,7 +270,8 @@
JEdit_Lib.buffer_lock(buffer) {
(Line.Position.zero /:
(Symbol.iterator(JEdit_Lib.buffer_text(buffer)).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))
+ zipWithIndex.takeWhile(p => p._2 < offset - 1).
+ map(_._1)))(_.advance(_, Text.Length))
}
hyperlink_file(focus, Line.Node_Position(name, pos))
case _ =>
--- a/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 28 17:22:16 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Dec 28 20:42:28 2016 +0100
@@ -25,33 +25,6 @@
new JEdit_Rendering(snapshot, options)
- /* message priorities */
-
- private val state_pri = 1
- private val writeln_pri = 2
- private val information_pri = 3
- private val tracing_pri = 4
- private val warning_pri = 5
- private val legacy_pri = 6
- private val error_pri = 7
-
- private val message_pri = Map(
- Markup.STATE -> state_pri,
- Markup.STATE_MESSAGE -> state_pri,
- Markup.WRITELN -> writeln_pri,
- Markup.WRITELN_MESSAGE -> writeln_pri,
- Markup.INFORMATION -> information_pri,
- Markup.INFORMATION_MESSAGE -> information_pri,
- Markup.TRACING -> tracing_pri,
- Markup.TRACING_MESSAGE -> tracing_pri,
- Markup.WARNING -> warning_pri,
- Markup.WARNING_MESSAGE -> warning_pri,
- Markup.LEGACY -> legacy_pri,
- Markup.LEGACY_MESSAGE -> legacy_pri,
- Markup.ERROR -> error_pri,
- Markup.ERROR_MESSAGE -> error_pri)
-
-
/* popup window bounds */
def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
@@ -529,13 +502,9 @@
snapshot.cumulate[List[Text.Info[Command.Results.Entry]]](
range, Nil, JEdit_Rendering.tooltip_message_elements, _ =>
{
- case (msgs, Text.Info(info_range, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+ case (msgs, Text.Info(info_range,
+ XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
if body.nonEmpty =>
- val entry: Command.Results.Entry = (Document_ID.make(), msg)
- Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
-
- case (msgs, Text.Info(info_range,
- XML.Elem(Markup(name, props @ Markup.Serial(serial)), body))) =>
val entry: Command.Results.Entry =
serial -> XML.Elem(Markup(Markup.message(name), props), body)
Some(Text.Info(snapshot.convert(info_range), entry) :: msgs)
@@ -563,20 +532,20 @@
/* gutter */
private def gutter_message_pri(msg: XML.Tree): Int =
- if (Protocol.is_error(msg)) JEdit_Rendering.error_pri
- else if (Protocol.is_legacy(msg)) JEdit_Rendering.legacy_pri
- else if (Protocol.is_warning(msg)) JEdit_Rendering.warning_pri
- else if (Protocol.is_information(msg)) JEdit_Rendering.information_pri
+ if (Protocol.is_error(msg)) Rendering.error_pri
+ else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
+ else if (Protocol.is_warning(msg)) Rendering.warning_pri
+ else if (Protocol.is_information(msg)) Rendering.information_pri
else 0
private lazy val gutter_message_content = Map(
- JEdit_Rendering.information_pri ->
+ Rendering.information_pri ->
(JEdit_Lib.load_icon(options.string("gutter_information_icon")), information_message_color),
- JEdit_Rendering.warning_pri ->
+ Rendering.warning_pri ->
(JEdit_Lib.load_icon(options.string("gutter_warning_icon")), warning_message_color),
- JEdit_Rendering.legacy_pri ->
+ Rendering.legacy_pri ->
(JEdit_Lib.load_icon(options.string("gutter_legacy_icon")), warning_message_color),
- JEdit_Rendering.error_pri ->
+ Rendering.error_pri ->
(JEdit_Lib.load_icon(options.string("gutter_error_icon")), error_message_color))
def gutter_content(range: Text.Range): Option[(Icon, Color)] =
@@ -596,18 +565,18 @@
/* squiggly underline */
private lazy val squiggly_colors = Map(
- JEdit_Rendering.writeln_pri -> writeln_color,
- JEdit_Rendering.information_pri -> information_color,
- JEdit_Rendering.warning_pri -> warning_color,
- JEdit_Rendering.legacy_pri -> legacy_color,
- JEdit_Rendering.error_pri -> error_color)
+ Rendering.writeln_pri -> writeln_color,
+ Rendering.information_pri -> information_color,
+ Rendering.warning_pri -> warning_color,
+ Rendering.legacy_pri -> legacy_color,
+ Rendering.error_pri -> error_color)
def squiggly_underline(range: Text.Range): List[Text.Info[Color]] =
{
val results =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.squiggly_elements, _ =>
{
- case (pri, Text.Info(_, elem)) => Some(pri max JEdit_Rendering.message_pri(elem.name))
+ case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
})
for {
Text.Info(r, pri) <- results
@@ -619,19 +588,19 @@
/* message output */
private lazy val message_colors = Map(
- JEdit_Rendering.writeln_pri -> writeln_message_color,
- JEdit_Rendering.information_pri -> information_message_color,
- JEdit_Rendering.tracing_pri -> tracing_message_color,
- JEdit_Rendering.warning_pri -> warning_message_color,
- JEdit_Rendering.legacy_pri -> legacy_message_color,
- JEdit_Rendering.error_pri -> error_message_color)
+ Rendering.writeln_pri -> writeln_message_color,
+ Rendering.information_pri -> information_message_color,
+ Rendering.tracing_pri -> tracing_message_color,
+ Rendering.warning_pri -> warning_message_color,
+ Rendering.legacy_pri -> legacy_message_color,
+ Rendering.error_pri -> error_message_color)
def line_background(range: Text.Range): Option[(Color, Boolean)] =
{
val results =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
{
- case (pri, Text.Info(_, elem)) => Some(pri max JEdit_Rendering.message_pri(elem.name))
+ case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
})
val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }