src/Tools/VSCode/src/document_model.scala
changeset 66676 39db5bb7eb0a
parent 66674 30d5195299e2
child 66984 a1d3e5df0c95
     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