src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Fri, 30 Dec 2016 11:54:11 +0100
changeset 64708 dd7f1a7e03f4
parent 64707 7157685b71e3
child 64709 5e6566ab78bf
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
     1
/*  Title:      Tools/VSCode/src/vscode_resources.scala
64605
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
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
     4
Resources for VSCode Language Server, based on file-system URIs.
64605
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 java.net.{URI, URISyntaxException}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    13
import java.io.{File => JFile}
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
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
    16
object VSCode_Resources
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    17
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    18
  /* file URIs */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    19
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    20
  def is_wellformed(uri: String): Boolean =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    21
    try { new JFile(new URI(uri)); true }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    22
    catch { case _: URISyntaxException | _: IllegalArgumentException => false }
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    23
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    24
  def canonical_file(uri: String): JFile =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    25
    new JFile(new URI(uri)).getCanonicalFile
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    26
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    27
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    28
  /* internal state */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    29
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    30
  sealed case class State(
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    31
    models: Map[String, Document_Model] = Map.empty,
64708
wenzelm
parents: 64707
diff changeset
    32
    pending_input: Set[String] = Set.empty,
wenzelm
parents: 64707
diff changeset
    33
    pending_output: Set[String] = Set.empty)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    34
}
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    35
64623
83f012ce2567 clarified module name;
wenzelm
parents: 64605
diff changeset
    36
class VSCode_Resources(
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    37
    val options: Options,
64706
wenzelm
parents: 64704
diff changeset
    38
    val text_length: Text.Length,
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    39
    loaded_theories: Set[String],
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    40
    known_theories: Map[String, Document.Node.Name],
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    41
    base_syntax: Outer_Syntax)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    42
  extends Resources(loaded_theories, known_theories, base_syntax)
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    43
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    44
  private val state = Synchronized(VSCode_Resources.State())
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    45
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    46
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    47
  /* document node name */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    48
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    49
  def node_name(uri: String): Document.Node.Name =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
  {
64640
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    51
    val theory = Thy_Header.thy_name(uri).getOrElse("")
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    52
    val master_dir =
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    53
      if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    54
      else VSCode_Resources.canonical_file(uri).getParent
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    55
    Document.Node.Name(uri, master_dir, theory)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    56
  }
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    57
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    58
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    59
  /* document models */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    60
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    61
  def get_model(uri: String): Option[Document_Model] = state.value.models.get(uri)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    62
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    63
  def update_model(model: Document_Model)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    64
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    65
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    66
      st.copy(
64708
wenzelm
parents: 64707
diff changeset
    67
        models = st.models + (model.uri -> model),
wenzelm
parents: 64707
diff changeset
    68
        pending_input = st.pending_input + model.uri))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    69
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    70
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    71
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    72
  /* pending input */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    73
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    74
  def flush_input(session: Session)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    75
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    76
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    77
      {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    78
        val changed =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    79
          (for {
64708
wenzelm
parents: 64707
diff changeset
    80
            uri <- st.pending_input.iterator
wenzelm
parents: 64707
diff changeset
    81
            model <- st.models.get(uri)
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
    82
            res <- model.flush_edits
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
    83
          } yield res).toList
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
    84
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
    85
        session.update(Document.Blobs.empty, changed.flatMap(_._1))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    86
        st.copy(
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
    87
          models = (st.models /: changed) { case (ms, (_, m)) => ms + (m.uri -> m) },
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    88
          pending_input = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    89
      })
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    90
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    91
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    92
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    93
  /* pending output */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    94
64708
wenzelm
parents: 64707
diff changeset
    95
  def update_output(changed_nodes: List[String]): Unit =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    96
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    97
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    98
  def flush_output(channel: Channel)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    99
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   100
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   101
      {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   102
        val changed_iterator =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   103
          for {
64708
wenzelm
parents: 64707
diff changeset
   104
            uri <- st.pending_output.iterator
wenzelm
parents: 64707
diff changeset
   105
            model <- st.models.get(uri)
64704
08c2d80428ff re-use options from resources;
wenzelm
parents: 64703
diff changeset
   106
            rendering = model.rendering()
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   107
            (diagnostics, model1) <- model.publish_diagnostics(rendering)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   108
          } yield {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   109
            channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   110
            model1
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   111
          }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   112
        st.copy(
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   113
          models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   114
          pending_output = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   115
      }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   116
    )
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   117
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   118
}