# HG changeset patch # User wenzelm # Date 1672076487 -3600 # Node ID d9f48960bf23ff57edbcaa5d18edf17b506171f4 # Parent 563939d757703e6f8b02995d641fc25f43eb9ae8 clarified signature: more position information via node_name; diff -r 563939d75770 -r d9f48960bf23 src/Tools/VSCode/src/vscode_model.scala --- a/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 17:36:56 2022 +0100 +++ b/src/Tools/VSCode/src/vscode_model.scala Mon Dec 26 18:41:27 2022 +0100 @@ -26,11 +26,7 @@ /* content */ - object Content { - val empty: Content = Content(Line.Document.empty) - } - - sealed case class Content(doc: Line.Document) { + sealed case class Content(node_name: Document.Node.Name, doc: Line.Document) { override def toString: String = doc.toString def text_length: Text.Offset = doc.text_length def text_range: Text.Range = doc.text_range @@ -38,7 +34,7 @@ lazy val bytes: Bytes = Bytes(Symbol.encode(text)) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) - lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text) + lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node) def recode_symbols: List[LSP.TextEdit] = (for { @@ -56,15 +52,15 @@ editor: Language_Server.Editor, node_name: Document.Node.Name ): VSCode_Model = { - VSCode_Model(session, editor, node_name, Content.empty, - node_required = File_Format.registry.is_theory(node_name)) + val content = Content(node_name, Line.Document.empty) + val is_theory = File_Format.registry.is_theory(node_name) + VSCode_Model(session, editor, content, node_required = is_theory) } } sealed case class VSCode_Model( session: Session, editor: Language_Server.Editor, - node_name: Document.Node.Name, content: VSCode_Model.Content, version: Option[Long] = None, external_file: Boolean = false, @@ -79,6 +75,8 @@ /* content */ + def node_name: Document.Node.Name = content.node_name + def get_text(range: Text.Range): Option[String] = content.doc.get_text(range) def set_version(new_version: Long): VSCode_Model = copy(version = Some(new_version)) @@ -163,7 +161,7 @@ Text.Edit.replace(0, content.text, insert) match { case Nil => None case edits => - val content1 = VSCode_Model.Content(Line.Document(insert)) + val content1 = VSCode_Model.Content(node_name, Line.Document(insert)) Some(copy(content = content1, pending_edits = pending_edits ::: edits)) } case Some(remove) => @@ -171,7 +169,7 @@ case None => error("Failed to apply document change: " + remove) case Some((Nil, _)) => None case Some((edits, doc1)) => - val content1 = VSCode_Model.Content(doc1) + val content1 = VSCode_Model.Content(node_name, doc1) Some(copy(content = content1, pending_edits = pending_edits ::: edits)) } } diff -r 563939d75770 -r d9f48960bf23 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Mon Dec 26 17:36:56 2022 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Mon Dec 26 18:41:27 2022 +0100 @@ -132,7 +132,7 @@ text <- PIDE.resources.read_file_content(node_name) if model.content.text != text } yield { - val content = Document_Model.File_Content(text) + val content = Document_Model.File_Content(node_name, text) val edits = Text.Edit.replace(0, model.content.text, text) (node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits)) }).toList @@ -288,10 +288,18 @@ /* file content */ - sealed case class File_Content(text: String) { + object File_Content { + val empty: File_Content = apply(Document.Node.Name.empty, "") + + def apply(node_name: Document.Node.Name, text: String): File_Content = + new File_Content(node_name, text) + } + + final class File_Content private(val node_name: Document.Node.Name, val text: String) { + override def toString: String = "Document_Model.File_Content(" + node_name.node + ")" lazy val bytes: Bytes = Bytes(Symbol.encode(text)) lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) - lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text) + lazy val bibtex_entries: Bibtex.Entries = Bibtex.Entries.parse(text, file_pos = node_name.node) } @@ -384,7 +392,7 @@ object File_Model { def empty(session: Session): File_Model = - File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""), + File_Model(session, None, Document_Model.File_Content.empty, false, Document.Node.Perspective_Text.empty, Nil) def init(session: Session, @@ -397,32 +405,33 @@ val file = JEdit_Lib.check_file(node_name.node) file.foreach(PIDE.plugin.file_watcher.register_parent(_)) - val content = Document_Model.File_Content(text) + val content = Document_Model.File_Content(node_name, text) val node_required1 = node_required || File_Format.registry.is_theory(node_name) - File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits) + File_Model(session, file, content, node_required1, last_perspective, pending_edits) } } case class File_Model( session: Session, - node_name: Document.Node.Name, file: Option[JFile], content: Document_Model.File_Content, node_required: Boolean, last_perspective: Document.Node.Perspective_Text.T, pending_edits: List[Text.Edit] ) extends Document_Model { + /* content */ + + def node_name: Document.Node.Name = content.node_name + + def get_text(range: Text.Range): Option[String] = + range.try_substring(content.text) + + /* required */ def set_node_required(b: Boolean): File_Model = copy(node_required = b) - /* text */ - - def get_text(range: Text.Range): Option[String] = - range.try_substring(content.text) - - /* header */ def node_header: Document.Node.Header = @@ -450,7 +459,7 @@ Text.Edit.replace(0, content.text, text) match { case Nil => None case edits => - val content1 = Document_Model.File_Content(text) + val content1 = Document_Model.File_Content(node_name, text) val pending_edits1 = pending_edits ::: edits Some(copy(content = content1, pending_edits = pending_edits1)) } @@ -595,7 +604,7 @@ if (File.is_bib(node_name.node)) { bibtex_entries getOrElse { val text = JEdit_Lib.buffer_text(buffer) - val entries = Bibtex.Entries.parse(text) + val entries = Bibtex.Entries.parse(text, file_pos = node_name.node) if (entries.errors.nonEmpty) Output.warning(cat_lines(entries.errors)) bibtex_entries = Some(entries) entries