# HG changeset patch # User wenzelm # Date 1482939900 -3600 # Node ID b2bf280b7e1312cda7fbf022406a06f2287246fd # Parent 914dffe59cc5d237e63ce64f72cf037ab20d12e5 more uniform treatment of input/output wrt. client; support for diagnistic messages; misc tuning; diff -r 914dffe59cc5 -r b2bf280b7e13 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Wed Dec 28 11:28:31 2016 +0100 +++ b/src/Pure/PIDE/line.scala Wed Dec 28 16:45:00 2016 +0100 @@ -123,6 +123,11 @@ move(offset, 0, lines) } + def range(text_range: Text.Range, length: Length = Length): Range = + Range( + position(text_range.start, length), + position(text_range.stop, length)) + def offset(pos: Position, length: Length = Length): Option[Text.Offset] = { val l = pos.line diff -r 914dffe59cc5 -r b2bf280b7e13 src/Tools/VSCode/etc/options --- a/src/Tools/VSCode/etc/options Wed Dec 28 11:28:31 2016 +0100 +++ b/src/Tools/VSCode/etc/options Wed Dec 28 16:45:00 2016 +0100 @@ -1,7 +1,10 @@ (* :mode=isabelle-options: *) 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)" diff -r 914dffe59cc5 -r b2bf280b7e13 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Wed Dec 28 11:28:31 2016 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Wed Dec 28 16:45:00 2016 +0100 @@ -13,8 +13,9 @@ case class Document_Model( - session: Session, doc: Line.Document, node_name: Document.Node.Name, - changed: Boolean = true) + session: Session, doc: Line.Document, node_name: Document.Node.Name, text_length: Length, + changed: Boolean = true, + published_diagnostics: List[Text.Info[Command.Results]] = Nil) { /* header */ @@ -48,10 +49,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) } diff -r 914dffe59cc5 -r b2bf280b7e13 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Wed Dec 28 11:28:31 2016 +0100 +++ b/src/Tools/VSCode/src/server.scala Wed Dec 28 16:45:00 2016 +0100 @@ -88,7 +88,8 @@ sealed case class State( session: Option[Session] = None, - models: Map[String, Document_Model] = Map.empty) + models: Map[String, Document_Model] = Map.empty, + pending_output: Set[Document.Node.Name] = Set.empty) } class Server( @@ -109,11 +110,68 @@ 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) + rendering = model.rendering(options) offset <- model.doc.offset(node_pos.pos, text_length) } yield (rendering, offset) + /* input from client */ + + private val delay_input = + Standard_Thread.delay_last(options.seconds("editor_input_delay")) { + state.change(st => + { + val changed = (for { entry <- st.models.iterator if entry._2.changed } yield entry).toList + val edits = for { (_, model) <- changed; edit <- model.node_edits(resources) } yield edit + session.update(Document.Blobs.empty, edits) + st.copy( + models = (st.models /: changed)({ case (ms, (uri, m)) => ms + (uri -> m.unchanged) })) + }) + } + + 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, text_length) + st.copy(models = st.models + (uri -> model)) + }) + 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_last(options.seconds("editor_update_delay")) { + state.change(st => + { + val changed_iterator = + for { + node_name <- st.pending_output.iterator + uri = node_name.node + model <- st.models.get(uri) + rendering = model.rendering(options) + (diagnostics, model1) <- model.publish_diagnostics(rendering) + } yield { + channel.diagnostics(uri, rendering.diagnostics_output(diagnostics)) + (uri, model1) + } + st.copy( + models = (st.models /: changed_iterator) { case (ms, (uri, m)) => ms + (uri -> m) }, + pending_output = Set.empty) + }) + } + + /* init and exit */ def init(id: Protocol.Id) @@ -156,6 +214,8 @@ } session.phase_changed += session_phase + session.commands_changed += commands_changed + session.start(receiver => Isabelle_Process(options = options, logic = session_name, dirs = session_dirs, modes = modes, receiver = receiver)) @@ -181,7 +241,10 @@ case _ => } session.phase_changed += session_phase + session.commands_changed -= commands_changed session.stop() + delay_input.revoke() + delay_output.revoke() st.copy(session = None) }) } @@ -192,35 +255,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 +265,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, text_length) 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)) } diff -r 914dffe59cc5 -r b2bf280b7e13 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 11:28:31 2016 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Dec 28 16:45:00 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]( + Text.Range.full, 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, model.text_length) + (_, 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") @@ -45,7 +90,8 @@ 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) + def position(offset: Symbol.Offset) = + doc.position(chunk.decode(offset), model.text_length) Line.Range(position(range.start), position(range.stop)) case _ => Line.Range(Line.Position((line1 - 1) max 0))