src/Tools/VSCode/src/vscode_resources.scala
author wenzelm
Sat, 31 Dec 2016 14:29:16 +0100
changeset 64722 6df73de0d3c7
parent 64721 4b9c96c3850b
child 64726 c534a2ac537d
permissions -rw-r--r--
tuned signature;
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],
64718
3197b68f4314 tuned signature;
wenzelm
parents: 64716
diff changeset
    41
    base_syntax: Outer_Syntax,
3197b68f4314 tuned signature;
wenzelm
parents: 64716
diff changeset
    42
    log: Logger = No_Logger)
3197b68f4314 tuned signature;
wenzelm
parents: 64716
diff changeset
    43
  extends Resources(loaded_theories, known_theories, base_syntax, log)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    44
{
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    45
  private val state = Synchronized(VSCode_Resources.State())
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
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    48
  /* document node name */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    49
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    50
  def node_name(uri: String): Document.Node.Name =
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    51
  {
64640
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    52
    val theory = Thy_Header.thy_name(uri).getOrElse("")
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    53
    val master_dir =
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    54
      if (!VSCode_Resources.is_wellformed(uri) || theory == "") ""
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    55
      else VSCode_Resources.canonical_file(uri).getParent
f9470490e682 clarified node_name: preserve original uri;
wenzelm
parents: 64623
diff changeset
    56
    Document.Node.Name(uri, master_dir, theory)
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
    57
  }
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    58
64716
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    59
  override def import_name(qualifier: String, master: Document.Node.Name, s: String)
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    60
    : Document.Node.Name =
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    61
  {
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    62
    val name = super.import_name(qualifier, master, s)
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    63
    if (name.node.startsWith("file://") || name.node.forall(c => c != '/' && c != '\\')) name
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    64
    else name.copy(node = "file://" + name.node)
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    65
  }
473793d52d97 proper import_name;
wenzelm
parents: 64710
diff changeset
    66
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    67
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    68
  /* document models */
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
  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
    71
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
    72
  def update_model(session: Session, uri: String, text: String)
64703
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
    state.change(st =>
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
    75
      {
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    76
        val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    77
        val model1 = (model.update_text(text) getOrElse model).copy(external = false)
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
    78
        st.copy(
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    79
          models = st.models + (uri -> model1),
64709
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
    80
          pending_input = st.pending_input + uri)
5e6566ab78bf more explicit edits -- eliminated Clear;
wenzelm
parents: 64708
diff changeset
    81
      })
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    82
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
    83
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    84
  def close_model(uri: String): Option[Document_Model] =
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    85
    state.change_result(st =>
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    86
      st.models.get(uri) match {
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    87
        case None => (None, st)
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    88
        case Some(model) =>
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    89
          (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    90
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    91
64722
6df73de0d3c7 tuned signature;
wenzelm
parents: 64721
diff changeset
    92
  def sync_models(changed_files: Set[JFile]): Boolean =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    93
    state.change_result(st =>
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    94
      {
64719
wenzelm
parents: 64718
diff changeset
    95
        val changed_models =
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    96
          (for {
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    97
            (uri, model) <- st.models.iterator
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    98
            if changed_files(model.file)
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
    99
            model1 <- model.update_file
64721
4b9c96c3850b proper state update;
wenzelm
parents: 64719
diff changeset
   100
          } yield (uri, model1)).toList
64719
wenzelm
parents: 64718
diff changeset
   101
        if (changed_models.isEmpty) (false, st)
64721
4b9c96c3850b proper state update;
wenzelm
parents: 64719
diff changeset
   102
        else (true,
4b9c96c3850b proper state update;
wenzelm
parents: 64719
diff changeset
   103
          st.copy(
4b9c96c3850b proper state update;
wenzelm
parents: 64719
diff changeset
   104
            models = (st.models /: changed_models)(_ + _),
4b9c96c3850b proper state update;
wenzelm
parents: 64719
diff changeset
   105
            pending_input = (st.pending_input /: changed_models.iterator.map(_._1))(_ + _)))
64710
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   106
      })
72ca4e5f976e manage changes of external files;
wenzelm
parents: 64709
diff changeset
   107
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   108
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   109
  /* pending input */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   110
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   111
  def flush_input(session: Session)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   112
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   113
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   114
      {
64719
wenzelm
parents: 64718
diff changeset
   115
        val changed_models =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   116
          (for {
64708
wenzelm
parents: 64707
diff changeset
   117
            uri <- st.pending_input.iterator
wenzelm
parents: 64707
diff changeset
   118
            model <- st.models.get(uri)
64707
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   119
            res <- model.flush_edits
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   120
          } yield res).toList
7157685b71e3 clarified Document_Model perspective and edits;
wenzelm
parents: 64706
diff changeset
   121
64719
wenzelm
parents: 64718
diff changeset
   122
        session.update(Document.Blobs.empty, changed_models.flatMap(_._1))
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   123
        st.copy(
64719
wenzelm
parents: 64718
diff changeset
   124
          models = (st.models /: changed_models) { case (ms, (_, m)) => ms + (m.uri -> m) },
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   125
          pending_input = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   126
      })
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   127
  }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   128
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   129
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   130
  /* pending output */
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   131
64708
wenzelm
parents: 64707
diff changeset
   132
  def update_output(changed_nodes: List[String]): Unit =
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   133
    state.change(st => st.copy(pending_output = st.pending_output ++ changed_nodes))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   134
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   135
  def flush_output(channel: Channel)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   136
  {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   137
    state.change(st =>
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   138
      {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   139
        val changed_iterator =
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   140
          for {
64708
wenzelm
parents: 64707
diff changeset
   141
            uri <- st.pending_output.iterator
wenzelm
parents: 64707
diff changeset
   142
            model <- st.models.get(uri)
64704
08c2d80428ff re-use options from resources;
wenzelm
parents: 64703
diff changeset
   143
            rendering = model.rendering()
64703
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   144
            (diagnostics, model1) <- model.publish_diagnostics(rendering)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   145
          } yield {
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   146
            channel.diagnostics(model1.uri, rendering.diagnostics_output(diagnostics))
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   147
            model1
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   148
          }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   149
        st.copy(
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   150
          models = (st.models /: changed_iterator) { case (ms, m) => ms + (m.uri -> m) },
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   151
          pending_output = Set.empty)
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   152
      }
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   153
    )
a115391494ed moved main state to VSCode_Resources;
wenzelm
parents: 64640
diff changeset
   154
  }
64605
9c1173a7e4cb basic support for VSCode Language Server protocol;
wenzelm
parents:
diff changeset
   155
}