src/Tools/VSCode/src/document_model.scala
author wenzelm
Tue Dec 20 22:24:16 2016 +0100 (2016-12-20)
changeset 64622 529bbb8977c7
parent 64605 9c1173a7e4cb
child 64649 d67c3094a0c2
permissions -rw-r--r--
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
     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 and rendering */
    56 
    57   def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits)
    58 
    59   def rendering(options: Options): VSCode_Rendering =
    60     new VSCode_Rendering(snapshot(), options, session.resources)
    61 }