src/Tools/VSCode/src/document_model.scala
changeset 64605 9c1173a7e4cb
child 64622 529bbb8977c7
equal deleted inserted replaced
64604:2bf8cfc98c4d 64605:9c1173a7e4cb
       
     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 scala.util.parsing.input.CharSequenceReader
       
    13 
       
    14 
       
    15 case class Document_Model(
       
    16   session: Session, doc: Line.Document, node_name: Document.Node.Name,
       
    17   changed: Boolean = true)
       
    18 {
       
    19   /* header */
       
    20 
       
    21   def is_theory: Boolean = node_name.is_theory
       
    22 
       
    23   lazy val node_header: Document.Node.Header =
       
    24     if (is_theory) {
       
    25       val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text)
       
    26       val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY))
       
    27       toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match {
       
    28         case Some(i) =>
       
    29           session.resources.check_thy_reader("", node_name,
       
    30             new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command)
       
    31         case None => Document.Node.no_header
       
    32       }
       
    33     }
       
    34     else Document.Node.no_header
       
    35 
       
    36 
       
    37   /* edits */
       
    38 
       
    39   def text_edits: List[Text.Edit] =
       
    40     if (changed) List(Text.Edit.insert(0, doc.text)) else Nil
       
    41 
       
    42   def node_edits: List[Document.Edit_Text] =
       
    43     if (changed) {
       
    44       List(session.header_edit(node_name, node_header),
       
    45         node_name -> Document.Node.Clear(),
       
    46         node_name -> Document.Node.Edits(text_edits),
       
    47         node_name ->
       
    48           Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty))
       
    49     }
       
    50     else Nil
       
    51 
       
    52   def unchanged: Document_Model = if (changed) copy(changed = false) else this
       
    53 
       
    54 
       
    55   /* snapshot */
       
    56 
       
    57   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
       
    58 }