src/Tools/VSCode/src/document_model.scala
author wenzelm
Tue Jan 03 14:17:03 2017 +0100 (2017-01-03)
changeset 64759 100941134718
parent 64729 4eccd9bc5fd9
child 64775 dd3797f1e0d6
permissions -rw-r--r--
clarified master_dir: file-URL;
     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 import scala.util.parsing.input.CharSequenceReader
    15 
    16 
    17 object Document_Model
    18 {
    19   def init(session: Session, uri: String): Document_Model =
    20   {
    21     val resources = session.resources.asInstanceOf[VSCode_Resources]
    22     val node_name = resources.node_name(uri)
    23     val doc = Line.Document("", resources.text_length)
    24     Document_Model(session, node_name, doc)
    25   }
    26 }
    27 
    28 sealed case class Document_Model(
    29   session: Session,
    30   node_name: Document.Node.Name,
    31   doc: Line.Document,
    32   external_file: Boolean = false,
    33   node_required: Boolean = false,
    34   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    35   pending_edits: Vector[Text.Edit] = Vector.empty,
    36   published_diagnostics: List[Text.Info[Command.Results]] = Nil)
    37 {
    38   /* name */
    39 
    40   override def toString: String = node_name.toString
    41 
    42   def uri: String = node_name.node
    43   def is_theory: Boolean = node_name.is_theory
    44 
    45 
    46   /* external file */
    47 
    48   val file: JFile = Url.file(uri).getCanonicalFile
    49 
    50   def external(b: Boolean): Document_Model = copy(external_file = b)
    51 
    52   def register(watcher: File_Watcher)
    53   {
    54     val dir = file.getParentFile
    55     if (dir != null && dir.isDirectory) watcher.register(dir)
    56   }
    57 
    58 
    59   /* header */
    60 
    61   def node_header: Document.Node.Header =
    62     resources.special_header(node_name) getOrElse
    63     {
    64       if (is_theory)
    65         resources.check_thy_reader(
    66           "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command)
    67       else Document.Node.no_header
    68     }
    69 
    70 
    71   /* perspective */
    72 
    73   def node_visible: Boolean = !external_file
    74 
    75   def text_perspective: Text.Perspective =
    76     if (node_visible) Text.Perspective.full else Text.Perspective.empty
    77 
    78   def node_perspective: Document.Node.Perspective_Text =
    79     Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty)
    80 
    81 
    82   /* edits */
    83 
    84   def update_text(new_text: String): Option[Document_Model] =
    85   {
    86     val old_text = doc.make_text
    87     if (new_text == old_text) None
    88     else {
    89       val doc1 = Line.Document(new_text, doc.text_length)
    90       val pending_edits1 =
    91         if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits
    92       val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text)
    93       Some(copy(doc = doc1, pending_edits = pending_edits2))
    94     }
    95   }
    96 
    97   def update_file: Option[Document_Model] =
    98     if (external_file) {
    99       try { update_text(File.read(file)) }
   100       catch { case ERROR(_) => None }
   101     }
   102     else None
   103 
   104   def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
   105   {
   106     val perspective = node_perspective
   107     if (pending_edits.nonEmpty || last_perspective != perspective) {
   108       val text_edits = pending_edits.toList
   109       val edits =
   110         session.header_edit(node_name, node_header) ::
   111         (if (text_edits.isEmpty) Nil
   112          else List[Document.Edit_Text](node_name -> Document.Node.Edits(text_edits))) :::
   113         (if (last_perspective == perspective) Nil
   114          else List[Document.Edit_Text](node_name -> perspective))
   115       Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective)))
   116     }
   117     else None
   118   }
   119 
   120 
   121   /* diagnostics */
   122 
   123   def publish_diagnostics(rendering: VSCode_Rendering)
   124     : Option[(List[Text.Info[Command.Results]], Document_Model)] =
   125   {
   126     val diagnostics = rendering.diagnostics
   127     if (diagnostics == published_diagnostics) None
   128     else Some(diagnostics, copy(published_diagnostics = diagnostics))
   129   }
   130 
   131 
   132   /* prover session */
   133 
   134   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
   135 
   136   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList)
   137 
   138   def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
   139 }