recode Unicode text on the spot, e.g. from copy-paste of output;
authorwenzelm
Mon Sep 18 18:19:06 2017 +0200 (21 months ago)
changeset 6667639db5bb7eb0a
parent 66675 6f4613dbfef6
child 66677 fa70edfcb6fa
recode Unicode text on the spot, e.g. from copy-paste of output;
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/vscode_resources.scala
     1.1 --- a/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 18:11:21 2017 +0200
     1.2 +++ b/src/Tools/VSCode/src/document_model.scala	Mon Sep 18 18:19:06 2017 +0200
     1.3 @@ -45,6 +45,16 @@
     1.4      lazy val bibtex_entries: List[Text.Info[String]] =
     1.5        try { Bibtex.entries(text) }
     1.6        catch { case ERROR(_) => Nil }
     1.7 +
     1.8 +    def recode_symbols: List[Protocol.TextEdit] =
     1.9 +      (for {
    1.10 +        (line, l) <- doc.lines.iterator.zipWithIndex
    1.11 +        text1 = Symbol.encode(line.text)
    1.12 +        if (line.text != text1)
    1.13 +      } yield {
    1.14 +        val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
    1.15 +        Protocol.TextEdit(range, text1)
    1.16 +      }).toList
    1.17    }
    1.18  
    1.19    def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
    1.20 @@ -166,12 +176,27 @@
    1.21      }
    1.22    }
    1.23  
    1.24 -  def flush_edits(doc_blobs: Document.Blobs, caret: Option[Line.Position])
    1.25 -    : Option[(List[Document.Edit_Text], Document_Model)] =
    1.26 +  def flush_edits(
    1.27 +      unicode_symbols: Boolean,
    1.28 +      doc_blobs: Document.Blobs,
    1.29 +      file: JFile,
    1.30 +      caret: Option[Line.Position])
    1.31 +    : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] =
    1.32    {
    1.33 +    val workspace_edits =
    1.34 +      if (unicode_symbols && version.isDefined) {
    1.35 +        val edits = content.recode_symbols
    1.36 +        if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits))
    1.37 +        else Nil
    1.38 +      }
    1.39 +      else Nil
    1.40 +
    1.41      val (reparse, perspective) = node_perspective(doc_blobs, caret)
    1.42 -    if (reparse || pending_edits.nonEmpty || last_perspective != perspective) {
    1.43 -      val edits = node_edits(node_header, pending_edits, perspective)
    1.44 +    if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
    1.45 +        workspace_edits.nonEmpty)
    1.46 +    {
    1.47 +      val prover_edits = node_edits(node_header, pending_edits, perspective)
    1.48 +      val edits = (workspace_edits, prover_edits)
    1.49        Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
    1.50      }
    1.51      else None
     2.1 --- a/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:11:21 2017 +0200
     2.2 +++ b/src/Tools/VSCode/src/server.scala	Mon Sep 18 18:19:06 2017 +0200
     2.3 @@ -123,7 +123,7 @@
     2.4  
     2.5    private val delay_input: Standard_Thread.Delay =
     2.6      Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
     2.7 -    { resources.flush_input(session) }
     2.8 +    { resources.flush_input(session, channel) }
     2.9  
    2.10    private val delay_load: Standard_Thread.Delay =
    2.11      Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
    2.12 @@ -487,7 +487,7 @@
    2.13      /* session */
    2.14  
    2.15      override def session: Session = server.session
    2.16 -    override def flush(): Unit = resources.flush_input(session)
    2.17 +    override def flush(): Unit = resources.flush_input(session, channel)
    2.18      override def invoke(): Unit = delay_input.invoke()
    2.19  
    2.20  
     3.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:11:21 2017 +0200
     3.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Sep 18 18:19:06 2017 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4  
     3.5    /* pending input */
     3.6  
     3.7 -  def flush_input(session: Session)
     3.8 +  def flush_input(session: Session, channel: Channel)
     3.9    {
    3.10      state.change(st =>
    3.11        {
    3.12 @@ -266,10 +266,15 @@
    3.13            (for {
    3.14              file <- st.pending_input.iterator
    3.15              model <- st.models.get(file)
    3.16 -            (edits, model1) <- model.flush_edits(st.document_blobs, st.get_caret(file))
    3.17 +            (edits, model1) <-
    3.18 +              model.flush_edits(unicode_symbols, st.document_blobs, file, st.get_caret(file))
    3.19            } yield (edits, (file, model1))).toList
    3.20  
    3.21 -        session.update(st.document_blobs, changed_models.flatMap(_._1))
    3.22 +        for { ((workspace_edits, _), _) <- changed_models if workspace_edits.nonEmpty }
    3.23 +          channel.write(Protocol.WorkspaceEdit(workspace_edits))
    3.24 +
    3.25 +        session.update(st.document_blobs, changed_models.flatMap(res => res._1._2))
    3.26 +
    3.27          st.copy(
    3.28            models = st.models ++ changed_models.iterator.map(_._2),
    3.29            pending_input = Set.empty)