src/Tools/VSCode/src/document_model.scala
author wenzelm
Mon Sep 18 18:19:06 2017 +0200 (22 months ago)
changeset 66676 39db5bb7eb0a
parent 66674 30d5195299e2
child 66984 a1d3e5df0c95
permissions -rw-r--r--
recode Unicode text on the spot, e.g. from copy-paste of output;
     1 /*  Title:      Tools/VSCode/src/document_model.scala
     2     Author:     Makarius
     3 
     4 Document model for line-oriented text.
     5 */
     6 
     7 package isabelle.vscode
     8 
     9 
    10 import isabelle._
    11 
    12 import java.io.{File => JFile}
    13 
    14 
    15 object Document_Model
    16 {
    17   /* decorations */
    18 
    19   object Decoration
    20   {
    21     def empty(typ: String): Decoration = Decoration(typ, Nil)
    22 
    23     def ranges(typ: String, ranges: List[Text.Range]): Decoration =
    24       Decoration(typ, ranges.map(Text.Info(_, List.empty[XML.Body])))
    25   }
    26   sealed case class Decoration(typ: String, content: List[Text.Info[List[XML.Body]]])
    27 
    28 
    29   /* content */
    30 
    31   object Content
    32   {
    33     val empty: Content = Content(Line.Document.empty)
    34   }
    35 
    36   sealed case class Content(doc: Line.Document)
    37   {
    38     override def toString: String = doc.toString
    39     def text_length: Text.Offset = doc.text_length
    40     def text_range: Text.Range = doc.text_range
    41     def text: String = doc.text
    42 
    43     lazy val bytes: Bytes = Bytes(text)
    44     lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text)
    45     lazy val bibtex_entries: List[Text.Info[String]] =
    46       try { Bibtex.entries(text) }
    47       catch { case ERROR(_) => Nil }
    48 
    49     def recode_symbols: List[Protocol.TextEdit] =
    50       (for {
    51         (line, l) <- doc.lines.iterator.zipWithIndex
    52         text1 = Symbol.encode(line.text)
    53         if (line.text != text1)
    54       } yield {
    55         val range = Line.Range(Line.Position(l), Line.Position(l, line.text.length))
    56         Protocol.TextEdit(range, text1)
    57       }).toList
    58   }
    59 
    60   def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
    61     Document_Model(session, editor, node_name, Content.empty)
    62 }
    63 
    64 sealed case class Document_Model(
    65   session: Session,
    66   editor: Server.Editor,
    67   node_name: Document.Node.Name,
    68   content: Document_Model.Content,
    69   version: Option[Long] = None,
    70   external_file: Boolean = false,
    71   node_required: Boolean = false,
    72   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    73   pending_edits: List[Text.Edit] = Nil,
    74   published_diagnostics: List[Text.Info[Command.Results]] = Nil,
    75   published_decorations: List[Document_Model.Decoration] = Nil) extends Document.Model
    76 {
    77   model =>
    78 
    79 
    80   /* content */
    81 
    82   def try_get_text(range: Text.Range): Option[String] = content.doc.try_get_text(range)
    83 
    84   def set_version(new_version: Long): Document_Model = copy(version = Some(new_version))
    85 
    86 
    87   /* external file */
    88 
    89   def external(b: Boolean): Document_Model = copy(external_file = b)
    90 
    91   def node_visible: Boolean = !external_file
    92 
    93 
    94   /* header */
    95 
    96   def node_header: Document.Node.Header =
    97     resources.special_header(node_name) getOrElse
    98       resources.check_thy_reader(node_name, Scan.char_reader(content.text))
    99 
   100 
   101   /* perspective */
   102 
   103   def node_perspective(doc_blobs: Document.Blobs, caret: Option[Line.Position])
   104     : (Boolean, Document.Node.Perspective_Text) =
   105   {
   106     if (is_theory) {
   107       val snapshot = model.snapshot()
   108 
   109       val caret_perspective = resources.options.int("vscode_caret_perspective") max 0
   110       val caret_range =
   111         if (caret_perspective != 0) {
   112           caret match {
   113             case Some(pos) =>
   114               val doc = content.doc
   115               val pos1 = Line.Position((pos.line - caret_perspective) max 0)
   116               val pos2 = Line.Position((pos.line + caret_perspective + 1) min doc.lines.length)
   117               Text.Range(doc.offset(pos1).get, doc.offset(pos2).get)
   118             case None => Text.Range.offside
   119           }
   120         }
   121         else if (node_visible) content.text_range
   122         else Text.Range.offside
   123 
   124       val text_perspective =
   125         if (snapshot.commands_loading_ranges(resources.visible_node(_)).nonEmpty)
   126           Text.Perspective.full
   127         else
   128           content.text_range.try_restrict(caret_range) match {
   129             case Some(range) => Text.Perspective(List(range))
   130             case None => Text.Perspective.empty
   131           }
   132 
   133       val overlays = editor.node_overlays(node_name)
   134 
   135       (snapshot.node.load_commands_changed(doc_blobs),
   136         Document.Node.Perspective(node_required, text_perspective, overlays))
   137     }
   138     else (false, Document.Node.no_perspective_text)
   139   }
   140 
   141 
   142   /* blob */
   143 
   144   def get_blob: Option[Document.Blob] =
   145     if (is_theory) None
   146     else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)))
   147 
   148 
   149   /* bibtex entries */
   150 
   151   def bibtex_entries: List[Text.Info[String]] =
   152     model.content.bibtex_entries
   153 
   154 
   155   /* edits */
   156 
   157   def change_text(text: String, range: Option[Line.Range] = None): Option[Document_Model] =
   158   {
   159     val insert = Line.normalize(text)
   160     range match {
   161       case None =>
   162         Text.Edit.replace(0, content.text, insert) match {
   163           case Nil => None
   164           case edits =>
   165             val content1 = Document_Model.Content(Line.Document(insert))
   166             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
   167         }
   168       case Some(remove) =>
   169         content.doc.change(remove, insert) match {
   170           case None => error("Failed to apply document change: " + remove)
   171           case Some((Nil, _)) => None
   172           case Some((edits, doc1)) =>
   173             val content1 = Document_Model.Content(doc1)
   174             Some(copy(content = content1, pending_edits = pending_edits ::: edits))
   175         }
   176     }
   177   }
   178 
   179   def flush_edits(
   180       unicode_symbols: Boolean,
   181       doc_blobs: Document.Blobs,
   182       file: JFile,
   183       caret: Option[Line.Position])
   184     : Option[((List[Protocol.TextDocumentEdit], List[Document.Edit_Text]), Document_Model)] =
   185   {
   186     val workspace_edits =
   187       if (unicode_symbols && version.isDefined) {
   188         val edits = content.recode_symbols
   189         if (edits.nonEmpty) List(Protocol.TextDocumentEdit(file, version.get, edits))
   190         else Nil
   191       }
   192       else Nil
   193 
   194     val (reparse, perspective) = node_perspective(doc_blobs, caret)
   195     if (reparse || pending_edits.nonEmpty || last_perspective != perspective ||
   196         workspace_edits.nonEmpty)
   197     {
   198       val prover_edits = node_edits(node_header, pending_edits, perspective)
   199       val edits = (workspace_edits, prover_edits)
   200       Some((edits, copy(pending_edits = Nil, last_perspective = perspective)))
   201     }
   202     else None
   203   }
   204 
   205 
   206   /* publish annotations */
   207 
   208   def publish(rendering: VSCode_Rendering):
   209     (Option[List[Text.Info[Command.Results]]], Option[List[Document_Model.Decoration]], Document_Model) =
   210   {
   211     val diagnostics = rendering.diagnostics
   212     val decorations =
   213       if (node_visible) rendering.decorations
   214       else { for (deco <- published_decorations) yield Document_Model.Decoration.empty(deco.typ) }
   215 
   216     val changed_diagnostics =
   217       if (diagnostics == published_diagnostics) None else Some(diagnostics)
   218     val changed_decorations =
   219       if (decorations == published_decorations) None
   220       else if (published_decorations.isEmpty) Some(decorations)
   221       else Some(for { (a, b) <- decorations zip published_decorations if a != b } yield a)
   222 
   223     (changed_diagnostics, changed_decorations,
   224       copy(published_diagnostics = diagnostics, published_decorations = decorations))
   225   }
   226 
   227 
   228   /* prover session */
   229 
   230   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
   231 
   232   def is_stable: Boolean = pending_edits.isEmpty
   233   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
   234 
   235   def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
   236     new VSCode_Rendering(snapshot, model)
   237   def rendering(): VSCode_Rendering = rendering(snapshot())
   238 
   239 
   240   /* syntax */
   241 
   242   lazy private val syntax0 = Outer_Syntax.init()
   243 
   244   def syntax(): Outer_Syntax =
   245     if (is_theory) session.recent_syntax(node_name) else syntax0
   246 }