# HG changeset patch # User wenzelm # Date 1483873237 -3600 # Node ID 9bc44bef99e65721fd6357fbdd1aa37195072a18 # Parent 07f209e957bc4e42a5ef09316a1b88b6eb765983 more explocit Document_Model.Content; diff -r 07f209e957bc -r 9bc44bef99e6 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Sun Jan 08 11:41:18 2017 +0100 +++ b/src/Pure/PIDE/line.scala Sun Jan 08 12:00:37 2017 +0100 @@ -103,8 +103,6 @@ Text.Range(0, length) } lazy val text: String = lines.mkString("", "\n", "") - lazy val bytes: Bytes = Bytes(text) - lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) override def toString: String = text diff -r 07f209e957bc -r 9bc44bef99e6 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sun Jan 08 11:41:18 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sun Jan 08 12:00:37 2017 +0100 @@ -14,18 +14,26 @@ object Document_Model { + sealed case class Content(doc: Line.Document) + { + def text_range: Text.Range = doc.text_range + def text: String = doc.text + lazy val bytes: Bytes = Bytes(text) + lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) + } + def init(session: Session, node_name: Document.Node.Name): Document_Model = { val resources = session.resources.asInstanceOf[VSCode_Resources] - val doc = Line.Document("", resources.text_length) - Document_Model(session, node_name, doc) + val content = Content(Line.Document("", resources.text_length)) + Document_Model(session, node_name, content) } } sealed case class Document_Model( session: Session, node_name: Document.Node.Name, - doc: Line.Document, + content: Document_Model.Content, external_file: Boolean = false, node_required: Boolean = false, last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, @@ -43,7 +51,7 @@ def node_header: Document.Node.Header = resources.special_header(node_name) getOrElse - resources.check_thy_reader("", node_name, Scan.char_reader(doc.text)) + resources.check_thy_reader("", node_name, Scan.char_reader(content.text)) /* perspective */ @@ -69,21 +77,21 @@ def get_blob: Option[Document.Blob] = if (is_theory) None - else Some((Document.Blob(doc.bytes, doc.chunk, pending_edits.nonEmpty))) + else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))) /* edits */ def update_text(text: String): Option[Document_Model] = { - val old_text = doc.text + val old_text = content.text val new_text = Line.normalize(text) Text.Edit.replace(0, old_text, new_text) match { case Nil => None case edits => - val doc1 = Line.Document(new_text, doc.text_length) + val content1 = Document_Model.Content(Line.Document(new_text, content.doc.text_length)) val pending_edits1 = pending_edits ::: edits - Some(copy(doc = doc1, pending_edits = pending_edits1)) + Some(copy(content = content1, pending_edits = pending_edits1)) } } diff -r 07f209e957bc -r 9bc44bef99e6 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sun Jan 08 11:41:18 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sun Jan 08 12:00:37 2017 +0100 @@ -104,7 +104,7 @@ for { model <- resources.get_model(new JFile(node_pos.name)) rendering = model.rendering() - offset <- model.doc.offset(node_pos.pos) + offset <- model.content.doc.offset(node_pos.pos) } yield (rendering, offset) @@ -286,7 +286,7 @@ (rendering, offset) <- rendering_offset(node_pos) info <- rendering.tooltips(Text.Range(offset, offset + 1)) } yield { - val doc = rendering.model.doc + val doc = rendering.model.content.doc val range = doc.range(info.range) val contents = info.info.map(tree => Pretty.string_of(List(tree), margin = rendering.tooltip_margin)) @@ -314,7 +314,7 @@ val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield { - val doc = rendering.model.doc + val doc = rendering.model.content.doc rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.text_range) .map(r => Protocol.DocumentHighlight.text(doc.range(r))) }) getOrElse Nil diff -r 07f209e957bc -r 9bc44bef99e6 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sun Jan 08 11:41:18 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Jan 08 12:00:37 2017 +0100 @@ -47,7 +47,7 @@ def diagnostics: List[Text.Info[Command.Results]] = snapshot.cumulate[Command.Results]( - model.doc.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => + model.content.text_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => { case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body))) if body.nonEmpty => Some(res + (i -> msg)) @@ -61,7 +61,7 @@ { (for { Text.Info(text_range, res) <- results.iterator - range = model.doc.range(text_range) + range = model.content.doc.range(text_range) (_, XML.Elem(Markup(name, _), body)) <- res.iterator } yield { val message = Pretty.string_of(body, margin = diagnostics_margin) diff -r 07f209e957bc -r 9bc44bef99e6 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 11:41:18 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 12:00:37 2017 +0100 @@ -71,7 +71,7 @@ { val file = node_file(name) get_model(file) match { - case Some(model) => f(Scan.char_reader(model.doc.text)) + case Some(model) => f(Scan.char_reader(model.content.text)) case None if file.isFile => val reader = Scan.byte_reader(file) try { f(reader) } finally { reader.close } @@ -138,7 +138,7 @@ def get_file_content(file: JFile): Option[String] = get_model(file) match { - case Some(model) => Some(model.doc.text) + case Some(model) => Some(model.content.text) case None => read_file_content(file) }