src/Tools/VSCode/src/document_model.scala
author wenzelm
Thu, 29 Dec 2016 22:10:29 +0100
changeset 64704 08c2d80428ff
parent 64703 a115391494ed
child 64707 7157685b71e3
permissions -rw-r--r--
re-use options from resources;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/VSCode/src/document_model.scala
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     3
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     4
Document model for line-oriented text.
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     5
*/
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     6
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     7
package isabelle.vscode
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     8
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
     9
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    10
import isabelle._
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    11
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    12
import scala.util.parsing.input.CharSequenceReader
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    14
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    15
case class Document_Model(
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64702
diff changeset
    16
  session: Session, node_name: Document.Node.Name, doc: Line.Document,
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    17
  changed: Boolean = true,
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    18
  published_diagnostics: List[Text.Info[Command.Results]] = Nil)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    19
{
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    20
  /* name */
64680
wenzelm
parents: 64679
diff changeset
    21
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    22
  override def toString: String = node_name.toString
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    23
64690
599873de8b01 more uniform pending_input / pending_output;
wenzelm
parents: 64683
diff changeset
    24
  def uri: String = node_name.node
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    25
  def is_theory: Boolean = node_name.is_theory
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
64690
599873de8b01 more uniform pending_input / pending_output;
wenzelm
parents: 64683
diff changeset
    27
599873de8b01 more uniform pending_input / pending_output;
wenzelm
parents: 64683
diff changeset
    28
  /* header */
599873de8b01 more uniform pending_input / pending_output;
wenzelm
parents: 64683
diff changeset
    29
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    30
  def node_header: Document.Node.Header =
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    31
    resources.special_header(node_name) getOrElse
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    32
    {
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    33
      if (is_theory)
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    34
        resources.check_thy_reader(
64673
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    35
          "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    36
      else Document.Node.no_header
b5965890e54d more uniform treatment of file name vs. theory name and special header;
wenzelm
parents: 64672
diff changeset
    37
    }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    38
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
  /* edits */
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    41
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
  def text_edits: List[Text.Edit] =
64672
d8e0619abb60 clarified document: no stored text;
wenzelm
parents: 64671
diff changeset
    43
    if (changed) List(Text.Edit.insert(0, doc.make_text)) else Nil
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    44
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    45
  def node_edits: List[Document.Edit_Text] =
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    46
    if (changed) {
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    47
      List(session.header_edit(node_name, node_header),
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    48
        node_name -> Document.Node.Clear(),
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
        node_name -> Document.Node.Edits(text_edits),
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
        node_name ->
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    51
          Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    52
    }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    53
    else Nil
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    54
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    55
  def unchanged: Document_Model = if (changed) copy(changed = false) else this
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    56
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
64679
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    58
  /* diagnostics */
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    59
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    60
  def publish_diagnostics(rendering: VSCode_Rendering)
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    61
    : Option[(List[Text.Info[Command.Results]], Document_Model)] =
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    62
  {
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    63
    val diagnostics = rendering.diagnostics
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    64
    if (diagnostics == published_diagnostics) None
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    65
    else Some(diagnostics, copy(published_diagnostics = diagnostics))
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    66
  }
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    67
b2bf280b7e13 more uniform treatment of input/output wrt. client;
wenzelm
parents: 64673
diff changeset
    68
64702
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    69
  /* session */
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    70
d95b9117cb5b re-use resources from session;
wenzelm
parents: 64690
diff changeset
    71
  def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    72
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    73
  def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
64622
529bbb8977c7 more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents: 64605
diff changeset
    74
64704
08c2d80428ff re-use options from resources;
wenzelm
parents: 64703
diff changeset
    75
  def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    76
}