diff -r 2bf8cfc98c4d -r 9c1173a7e4cb src/Tools/VSCode/src/document_model.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/VSCode/src/document_model.scala Mon Dec 19 20:27:49 2016 +0100 @@ -0,0 +1,58 @@ +/* Title: Tools/VSCode/src/document_model.scala + Author: Makarius + +Document model for line-oriented text. +*/ + +package isabelle.vscode + + +import isabelle._ + +import scala.util.parsing.input.CharSequenceReader + + +case class Document_Model( + session: Session, doc: Line.Document, node_name: Document.Node.Name, + changed: Boolean = true) +{ + /* header */ + + def is_theory: Boolean = node_name.is_theory + + lazy val node_header: Document.Node.Header = + if (is_theory) { + val toks = Token.explode(Thy_Header.bootstrap_syntax.keywords, doc.text) + val toks1 = toks.dropWhile(tok => !tok.is_command(Thy_Header.THEORY)) + toks1.iterator.zipWithIndex.collectFirst({ case (tok, i) if tok.is_begin => i }) match { + case Some(i) => + session.resources.check_thy_reader("", node_name, + new CharSequenceReader(toks1.take(i + 1).map(_.source).mkString), Token.Pos.command) + case None => Document.Node.no_header + } + } + else Document.Node.no_header + + + /* edits */ + + def text_edits: List[Text.Edit] = + if (changed) List(Text.Edit.insert(0, doc.text)) else Nil + + def node_edits: List[Document.Edit_Text] = + if (changed) { + List(session.header_edit(node_name, node_header), + node_name -> Document.Node.Clear(), + node_name -> Document.Node.Edits(text_edits), + node_name -> + Document.Node.Perspective(true, Text.Perspective.full, Document.Node.Overlays.empty)) + } + else Nil + + def unchanged: Document_Model = if (changed) copy(changed = false) else this + + + /* snapshot */ + + def snapshot(): Document.Snapshot = session.snapshot(node_name, text_edits) +}