# HG changeset patch # User wenzelm # Date 1483900514 -3600 # Node ID 048aa6ea3d325ce6694af65bb24830a9ffbefafd # Parent 5477d6b1222f66a7a5235ade35640373ef1a91da# Parent 9c69b495c05d7cf058fb7d96dd352cbaecb8911d merged diff -r 5477d6b1222f -r 048aa6ea3d32 NEWS --- a/NEWS Sat Jan 07 09:56:33 2017 +0100 +++ b/NEWS Sun Jan 08 19:35:14 2017 +0100 @@ -13,6 +13,13 @@ entry of the specified logic session in the editor, while its parent is used for formal checking. +* The PIDE document model maintains file content independently of the +status of jEdit editor buffers. Reloading jEdit buffers no longer causes +changes of formal document content. Theory dependencies are always +resolved internally, without the need for corresponding editor buffers. +The system option "jedit_auto_load" has been discontinued: it is +effectively always enabled. + *** HOL *** diff -r 5477d6b1222f -r 048aa6ea3d32 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Doc/JEdit/JEdit.thy Sun Jan 08 19:35:14 2017 +0100 @@ -850,12 +850,16 @@ \label{fig:theories} \end{figure} - Certain events to open or update editor buffers cause Isabelle/jEdit to - resolve dependencies of theory imports. The system requests to load - additional files into editor buffers, in order to be included in the - document model for further checking. It is also possible to let the system - resolve dependencies automatically, according to the system option - @{system_option jedit_auto_load}. + Theory imports are resolved automatically by the PIDE document model: all + required files are loaded and stored internally, without the need to open + corresponding jEdit buffers. Opening or closing editor buffers later on has + no impact on the formal document content: it only affects visibility. + + In contrast, auxiliary files (e.g.\ from \<^verbatim>\ML_file\ commands) are \<^emph>\not\ + resolved within the editor by default, but the prover process takes care of + that. This may be changed by enabling the system option @{system_option + jedit_auto_resolve}: it ensures that all files are uniformly provided by the + editor. \<^medskip> The visible \<^emph>\perspective\ of Isabelle/jEdit is defined by the collective diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/General/antiquote.scala --- a/src/Pure/General/antiquote.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/General/antiquote.scala Sun Jan 08 19:35:14 2017 +0100 @@ -7,9 +7,6 @@ package isabelle -import scala.util.parsing.input.CharSequenceReader - - object Antiquote { sealed abstract class Antiquote { def source: String } @@ -50,7 +47,7 @@ def read(input: CharSequence): List[Antiquote] = { - Parsers.parseAll(Parsers.rep(Parsers.antiquote), new CharSequenceReader(input)) match { + Parsers.parseAll(Parsers.rep(Parsers.antiquote), Scan.char_reader(input)) match { case Parsers.Success(xs, _) => xs case Parsers.NoSuccess(_, next) => error("Malformed quotation/antiquotation source" + diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/General/scan.scala Sun Jan 08 19:35:14 2017 +0100 @@ -10,7 +10,8 @@ import scala.annotation.tailrec import scala.collection.{IndexedSeq, Traversable, TraversableOnce} import scala.collection.immutable.PagedSeq -import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader} +import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, + Reader, CharSequenceReader} import scala.util.parsing.combinator.RegexParsers import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream} @@ -489,4 +490,10 @@ val stream_length = connection.getContentLength make_byte_reader(stream, stream_length) } + + + /* plain text reader */ + + def char_reader(text: CharSequence): CharSequenceReader = + new CharSequenceReader(text) } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/Isar/token.scala Sun Jan 08 19:35:14 2017 +0100 @@ -128,18 +128,15 @@ /* explode */ def explode(keywords: Keyword.Keywords, inp: CharSequence): List[Token] = - { - val in: input.Reader[Char] = new input.CharSequenceReader(inp) - Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), in) match { + Parsers.parseAll(Parsers.rep(Parsers.token(keywords)), Scan.char_reader(inp)) match { case Parsers.Success(tokens, _) => tokens case _ => error("Unexpected failure of tokenizing input:\n" + inp.toString) } - } def explode_line(keywords: Keyword.Keywords, inp: CharSequence, context: Scan.Line_Context) : (List[Token], Scan.Line_Context) = { - var in: input.Reader[Char] = new input.CharSequenceReader(inp) + var in: input.Reader[Char] = Scan.char_reader(inp) val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { @@ -180,7 +177,7 @@ val offset: Symbol.Offset, val file: String, val id: String) - extends scala.util.parsing.input.Position + extends input.Position { def column = 0 def lineContents = "" @@ -210,7 +207,7 @@ override def toString: String = Position.here(position(), delimited = false) } - abstract class Reader extends scala.util.parsing.input.Reader[Token] + abstract class Reader extends input.Reader[Token] private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader { diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/ML/ml_lex.scala --- a/src/Pure/ML/ml_lex.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/ML/ml_lex.scala Sun Jan 08 19:35:14 2017 +0100 @@ -8,7 +8,7 @@ import scala.collection.mutable -import scala.util.parsing.input.{Reader, CharSequenceReader} +import scala.util.parsing.input.Reader object ML_Lex @@ -265,17 +265,15 @@ /* tokenize */ def tokenize(input: CharSequence): List[Token] = - { - Parsers.parseAll(Parsers.rep(Parsers.token), new CharSequenceReader(input)) match { + Parsers.parseAll(Parsers.rep(Parsers.token), Scan.char_reader(input)) match { case Parsers.Success(tokens, _) => tokens case _ => error("Unexpected failure of tokenizing input:\n" + input.toString) } - } def tokenize_line(SML: Boolean, input: CharSequence, context: Scan.Line_Context) : (List[Token], Scan.Line_Context) = { - var in: Reader[Char] = new CharSequenceReader(input) + var in: Reader[Char] = Scan.char_reader(input) val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/command.scala Sun Jan 08 19:35:14 2017 +0100 @@ -10,7 +10,6 @@ import scala.collection.mutable import scala.collection.immutable.SortedMap -import scala.util.parsing.input.CharSequenceReader object Command @@ -350,9 +349,8 @@ span.name match { // inlined errors case Thy_Header.THEORY => - val header = - resources.check_thy_reader("", node_name, - new CharSequenceReader(Token.implode(span.content)), Token.Pos.command) + val reader = Scan.char_reader(Token.implode(span.content)) + val header = resources.check_thy_reader("", node_name, reader) val errors = for ((imp, pos) <- header.imports if !can_import(imp)) yield { val msg = diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/document.scala Sun Jan 08 19:35:14 2017 +0100 @@ -160,7 +160,6 @@ case _ => false } } - case class Clear[A, B]() extends Edit[A, B] case class Blob[A, B](blob: Document.Blob) extends Edit[A, B] case class Edits[A, B](edits: List[A]) extends Edit[A, B] @@ -264,8 +263,6 @@ def load_commands_changed(doc_blobs: Blobs): Boolean = load_commands.exists(_.blobs_changed(doc_blobs)) - def clear: Node = new Node(header = header, syntax = syntax) - def init_blob(blob: Blob): Node = new Node(get_blob = Some(blob.unchanged)) def update_header(new_header: Node.Header): Node = @@ -467,6 +464,41 @@ } + /* model */ + + trait Model + { + def session: Session + def is_stable: Boolean + def snapshot(): Snapshot + + def node_name: Document.Node.Name + def is_theory: Boolean = node_name.is_theory + override def toString: String = node_name.toString + + def node_required: Boolean + def get_blob: Option[Document.Blob] + + def node_header: Node.Header + def node_edits( + text_edits: List[Text.Edit], perspective: Node.Perspective_Text): List[Edit_Text] = + { + val edits: List[Node.Edit[Text.Edit, Text.Perspective]] = + get_blob match { + case None => + List( + Document.Node.Deps( + if (session.resources.loaded_theories(node_name.theory)) + node_header.error("Cannot update finished theory " + quote(node_name.theory)) + else node_header), + Document.Node.Edits(text_edits), perspective) + case Some(blob) => + List(Document.Node.Blob(blob), Document.Node.Edits(text_edits)) + } + edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit)) + } + } + /** global state -- document structure, execution process, editing history **/ @@ -743,14 +775,11 @@ if a == name } yield edits - val is_cleared = rev_pending_changes.exists({ case Node.Clear() => true case _ => false }) val edits = - if (is_cleared) Nil - else - (pending_edits /: rev_pending_changes)({ - case (edits, Node.Edits(es)) => es ::: edits - case (edits, _) => edits - }) + (pending_edits /: rev_pending_changes)({ + case (edits, Node.Edits(es)) => es ::: edits + case (edits, _) => edits + }) lazy val reverse_edits = edits.reverse new Snapshot @@ -764,10 +793,8 @@ /* local node content */ - def convert(offset: Text.Offset) = - if (is_cleared) 0 else (offset /: edits)((i, edit) => edit.convert(i)) - def revert(offset: Text.Offset) = - if (is_cleared) 0 else (offset /: reverse_edits)((i, edit) => edit.revert(i)) + def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) + def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) def convert(range: Text.Range) = range.map(convert(_)) def revert(range: Text.Range) = range.map(revert(_)) diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/line.scala --- a/src/Pure/PIDE/line.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/line.scala Sun Jan 08 19:35:14 2017 +0100 @@ -90,14 +90,21 @@ object Document { def apply(text: String, text_length: Text.Length): Document = - Document(logical_lines(text).map(Line(_)), text_length) + Document(logical_lines(text).map(s => Line(Library.trim_substring(s))), text_length) } sealed case class Document(lines: List[Line], text_length: Text.Length) { - def make_text: String = lines.mkString("", "\n", "") + lazy val text_range: Text.Range = + { + val length = + if (lines.isEmpty) 0 + else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 + Text.Range(0, length) + } + lazy val text: String = lines.mkString("", "\n", "") - override def toString: String = make_text + override def toString: String = text override def equals(that: Any): Boolean = that match { @@ -136,18 +143,6 @@ } else None } - - lazy val length: Int = - if (lines.isEmpty) 0 - else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 - - def full_range: Text.Range = Text.Range(0, length) - - lazy val blob: (Bytes, Symbol.Text_Chunk) = - { - val text = make_text - (Bytes(text), Symbol.Text_Chunk(text)) - } } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Sun Jan 08 19:35:14 2017 +0100 @@ -26,6 +26,9 @@ val base_syntax: Outer_Syntax, val log: Logger = No_Logger) { + val thy_info = new Thy_Info(this) + + /* document node names */ def node_name(qualifier: String, raw_path: Path): Document.Node.Name = @@ -118,11 +121,12 @@ } def check_thy_reader(qualifier: String, node_name: Document.Node.Name, - reader: Reader[Char], start: Token.Pos): Document.Node.Header = + reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true) + : Document.Node.Header = { - if (reader.source.length > 0) { + if (node_name.is_theory && reader.source.length > 0) { try { - val header = Thy_Header.read(reader, start).decode_symbols + val header = Thy_Header.read(reader, start, strict).decode_symbols val base_name = Long_Name.base_name(node_name.theory) val (name, pos) = header.name @@ -140,16 +144,9 @@ else Document.Node.no_header } - def check_thy(qualifier: String, name: Document.Node.Name, start: Token.Pos) - : Document.Node.Header = - with_thy_reader(name, check_thy_reader(qualifier, name, _, start)) - - def check_file(file: String): Boolean = - try { - if (Url.is_wellformed(file)) Url.is_readable(file) - else (new JFile(file)).isFile - } - catch { case ERROR(_) => false } + def check_thy(qualifier: String, name: Document.Node.Name, + start: Token.Pos = Token.Pos.command, strict: Boolean = true): Document.Node.Header = + with_thy_reader(name, check_thy_reader(qualifier, name, _, start, strict)) /* special header */ diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/session.scala Sun Jan 08 19:35:14 2017 +0100 @@ -242,18 +242,6 @@ resources.base_syntax - /* theory files */ - - def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text = - { - val header1 = - if (resources.loaded_theories(name.theory)) - header.error("Cannot update finished theory " + quote(name.theory)) - else header - (name, Document.Node.Deps(header1)) - } - - /* pipelined change parsing */ private case class Text_Edits( diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/text.scala --- a/src/Pure/PIDE/text.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/text.scala Sun Jan 08 19:35:14 2017 +0100 @@ -139,6 +139,10 @@ { def insert(start: Offset, text: String): Edit = new Edit(true, start, text) def remove(start: Offset, text: String): Edit = new Edit(false, start, text) + def replace(start: Offset, old_text: String, new_text: String): List[Edit] = + if (old_text == new_text) Nil + else if (old_text == "") List(insert(start, new_text)) + else List(remove(start, old_text), insert(start, new_text)) } final class Edit private(val is_insert: Boolean, val start: Offset, val text: String) diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/PIDE/xml.scala --- a/src/Pure/PIDE/xml.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/PIDE/xml.scala Sun Jan 08 19:35:14 2017 +0100 @@ -148,8 +148,6 @@ x } - private def trim_bytes(s: String): String = new String(s.toCharArray) - private def cache_string(x: String): String = if (x == "true") "true" else if (x == "false") "false" @@ -159,7 +157,7 @@ lookup(x) match { case Some(y) => y case None => - val z = trim_bytes(x) + val z = Library.trim_substring(x) if (z.length > max_string) z else store(z) } private def cache_props(x: Properties.T): Properties.T = @@ -167,7 +165,7 @@ else lookup(x) match { case Some(y) => y - case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2)))) + case None => store(x.map(p => (Library.trim_substring(p._1).intern, cache_string(p._2)))) } private def cache_markup(x: Markup): Markup = lookup(x) match { diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/Thy/thy_header.scala Sun Jan 08 19:35:14 2017 +0100 @@ -9,7 +9,7 @@ import scala.annotation.tailrec import scala.collection.mutable -import scala.util.parsing.input.{Reader, CharSequenceReader} +import scala.util.parsing.input.Reader import scala.util.matching.Regex @@ -154,59 +154,27 @@ /* read -- lazy scanning */ - def read(reader: Reader[Char], start: Token.Pos): Thy_Header = + def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header = { val token = Token.Parsers.token(bootstrap_keywords) - val toks = new mutable.ListBuffer[Token] - - @tailrec def scan_to_begin(in: Reader[Char]) - { + def make_tokens(in: Reader[Char]): Stream[Token] = token(in) match { - case Token.Parsers.Success(tok, rest) => - toks += tok - if (!tok.is_begin) scan_to_begin(rest) - case _ => + case Token.Parsers.Success(tok, rest) => tok #:: make_tokens(rest) + case _ => Stream.empty } - } - scan_to_begin(reader) + + val tokens = + if (strict) make_tokens(reader) + else make_tokens(reader).dropWhile(tok => !tok.is_command(Thy_Header.THEORY)) - parse(commit(header), Token.reader(toks.toList, start)) match { + val tokens1 = tokens.takeWhile(tok => !tok.is_begin).toList + val tokens2 = tokens.dropWhile(tok => !tok.is_begin).headOption.toList + + parse(commit(header), Token.reader(tokens1 ::: tokens2, start)) match { case Success(result, _) => result case bad => error(bad.toString) } } - - def read(source: CharSequence, start: Token.Pos): Thy_Header = - read(new CharSequenceReader(source), start) - - - /* line-oriented text */ - - def header_text(doc: Line.Document): String = - { - val keywords = bootstrap_syntax.keywords - val toks = new mutable.ListBuffer[Token] - val iterator = - (for { - (toks, _) <- - doc.lines.iterator.scanLeft((List.empty[Token], Scan.Finished: Scan.Line_Context))( - { - case ((_, ctxt), line) => Token.explode_line(keywords, line.text, ctxt) - }) - tok <- toks.iterator ++ Iterator.single(Token.newline) - } yield tok).dropWhile(tok => !tok.is_command(Thy_Header.THEORY)) - - @tailrec def until_begin - { - if (iterator.hasNext) { - val tok = iterator.next - toks += tok - if (!tok.is_begin) until_begin - } - } - until_begin - Token.implode(toks.toList) - } } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/Thy/thy_syntax.scala Sun Jan 08 19:35:14 2017 +0100 @@ -236,8 +236,6 @@ } edit match { - case (_, Document.Node.Clear()) => node.clear - case (_, Document.Node.Blob(blob)) => node.init_blob(blob) case (name, Document.Node.Edits(text_edits)) => diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/Tools/bibtex.scala Sun Jan 08 19:35:14 2017 +0100 @@ -8,12 +8,32 @@ import scala.collection.mutable -import scala.util.parsing.input.{Reader, CharSequenceReader} import scala.util.parsing.combinator.RegexParsers +import scala.util.parsing.input.Reader object Bibtex { + /** document model **/ + + def check_name(name: String): Boolean = name.endsWith(".bib") + def check_name(name: Document.Node.Name): Boolean = check_name(name.node) + + def document_entries(text: String): List[Text.Info[String]] = + { + val result = new mutable.ListBuffer[Text.Info[String]] + var offset = 0 + for (chunk <- Bibtex.parse(text)) { + val end_offset = offset + chunk.source.length + if (chunk.name != "" && !chunk.is_command) + result += Text.Info(Text.Range(offset, end_offset), chunk.name) + offset = end_offset + } + result.toList + } + + + /** content **/ private val months = List( @@ -383,17 +403,14 @@ /* parse */ def parse(input: CharSequence): List[Chunk] = - { - val in: Reader[Char] = new CharSequenceReader(input) - Parsers.parseAll(Parsers.rep(Parsers.chunk), in) match { + Parsers.parseAll(Parsers.rep(Parsers.chunk), Scan.char_reader(input)) match { case Parsers.Success(result, _) => result case _ => error("Unexpected failure to parse input:\n" + input.toString) } - } def parse_line(input: CharSequence, context: Line_Context): (List[Chunk], Line_Context) = { - var in: Reader[Char] = new CharSequenceReader(input) + var in: Reader[Char] = Scan.char_reader(input) val chunks = new mutable.ListBuffer[Chunk] var ctxt = context while (!in.atEnd) { diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/Tools/build.scala Sun Jan 08 19:35:14 2017 +0100 @@ -137,7 +137,6 @@ (parent.loaded_theories, parent.known_theories, parent.syntax) } val resources = new Resources(loaded_theories0, known_theories0, syntax0) - val thy_info = new Thy_Info(resources) if (verbose || list_files) { val groups = @@ -155,7 +154,7 @@ (resources.node_name( if (global) "" else name, info.dir + Resources.thy_path(thy)), info.pos)) }) - val thy_deps = thy_info.dependencies(name, root_theories) + val thy_deps = resources.thy_info.dependencies(name, root_theories) thy_deps.errors match { case Nil => thy_deps diff -r 5477d6b1222f -r 048aa6ea3d32 src/Pure/library.scala --- a/src/Pure/library.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Pure/library.scala Sun Jan 08 19:35:14 2017 +0100 @@ -139,6 +139,8 @@ def trim_split_lines(s: String): List[String] = split_lines(trim_line(s)).map(trim_line(_)) + def trim_substring(s: String): String = new String(s.toCharArray) + /* quote */ diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/VSCode/extension/src/extension.ts --- a/src/Tools/VSCode/extension/src/extension.ts Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/VSCode/extension/src/extension.ts Sun Jan 08 19:35:14 2017 +0100 @@ -31,7 +31,7 @@ let server_options: ServerOptions = { run: run, debug: run }; let client_options: LanguageClientOptions = { - documentSelector: ["isabelle", "isabelle-ml"] + documentSelector: ["isabelle", "isabelle-ml", "bibtex"] }; let disposable = new LanguageClient("Isabelle", server_options, client_options, false).start(); diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/VSCode/src/document_model.scala --- a/src/Tools/VSCode/src/document_model.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/VSCode/src/document_model.scala Sun Jan 08 19:35:14 2017 +0100 @@ -11,36 +11,39 @@ import java.io.{File => JFile} -import scala.util.parsing.input.CharSequenceReader - 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) + lazy val bibtex_entries: List[Text.Info[String]] = + try { Bibtex.document_entries(text) } + catch { case ERROR(_) => Nil } + } + 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, - pending_edits: Vector[Text.Edit] = Vector.empty, - published_diagnostics: List[Text.Info[Command.Results]] = Nil) + pending_edits: List[Text.Edit] = Nil, + published_diagnostics: List[Text.Info[Command.Results]] = Nil) extends Document.Model { - /* name */ - - override def toString: String = node_name.toString - - def is_theory: Boolean = node_name.is_theory - - /* external file */ def external(b: Boolean): Document_Model = copy(external_file = b) @@ -52,12 +55,7 @@ def node_header: Document.Node.Header = resources.special_header(node_name) getOrElse - { - if (is_theory) - resources.check_thy_reader( - "", node_name, new CharSequenceReader(Thy_Header.header_text(doc)), Token.Pos.command) - else Document.Node.no_header - } + resources.check_thy_reader("", node_name, Scan.char_reader(content.text)) /* perspective */ @@ -83,26 +81,21 @@ def get_blob: Option[Document.Blob] = if (is_theory) None - else { - val (bytes, chunk) = doc.blob - val changed = pending_edits.nonEmpty - Some((Document.Blob(bytes, chunk, changed))) - } + else Some((Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty))) /* edits */ def update_text(text: String): Option[Document_Model] = { + val old_text = content.text val new_text = Line.normalize(text) - val old_text = doc.make_text - if (new_text == old_text) None - else { - val doc1 = Line.Document(new_text, doc.text_length) - val pending_edits1 = - if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits - val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text) - Some(copy(doc = doc1, pending_edits = pending_edits2)) + Text.Edit.replace(0, old_text, new_text) match { + case Nil => None + case edits => + val content1 = Document_Model.Content(Line.Document(new_text, content.doc.text_length)) + val pending_edits1 = pending_edits ::: edits + Some(copy(content = content1, pending_edits = pending_edits1)) } } @@ -110,17 +103,8 @@ { val (reparse, perspective) = node_perspective(doc_blobs) if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { - val edits: List[Document.Edit_Text] = - get_blob match { - case None => - List(session.header_edit(node_name, node_header), - node_name -> Document.Node.Edits(pending_edits.toList), - node_name -> perspective) - case Some(blob) => - List(node_name -> Document.Node.Blob(blob), - node_name -> Document.Node.Edits(pending_edits.toList)) - } - Some((edits, copy(pending_edits = Vector.empty, last_perspective = perspective))) + val edits = node_edits(pending_edits, perspective) + Some((edits, copy(pending_edits = Nil, last_perspective = perspective))) } else None } @@ -141,7 +125,8 @@ def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources] - def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.toList) + def is_stable: Boolean = pending_edits.isEmpty + def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources) } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/VSCode/src/server.scala --- a/src/Tools/VSCode/src/server.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/VSCode/src/server.scala Sun Jan 08 19:35:14 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,8 +314,8 @@ val result = (for ((rendering, offset) <- rendering_offset(node_pos)) yield { - val doc = rendering.model.doc - rendering.caret_focus_ranges(Text.Range(offset, offset + 1), doc.full_range) + 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 channel.write(Protocol.DocumentHighlights.reply(id, result)) diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/VSCode/src/vscode_rendering.scala --- a/src/Tools/VSCode/src/vscode_rendering.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Sun Jan 08 19:35:14 2017 +0100 @@ -34,7 +34,7 @@ Markup.BAD) private val hyperlink_elements = - Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION) + Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION) } class VSCode_Rendering( @@ -47,7 +47,7 @@ def diagnostics: List[Text.Info[Command.Results]] = snapshot.cumulate[Command.Results]( - model.doc.full_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) @@ -90,14 +90,17 @@ } yield { Line.Node_Range(file.getPath, - resources.get_file_content(file) match { - case Some(text) if range.start > 0 => - val chunk = Symbol.Text_Chunk(text) - val doc = Line.Document(text, resources.text_length) - doc.range(chunk.decode(range)) - case _ => - Line.Range(Line.Position((line1 - 1) max 0)) - }) + if (range.start > 0) { + resources.get_file_content(file) match { + case Some(text) => + val chunk = Symbol.Text_Chunk(text) + val doc = Line.Document(text, resources.text_length) + doc.range(chunk.decode(range)) + case _ => + Line.Range(Line.Position((line1 - 1) max 0)) + } + } + else Line.Range(Line.Position((line1 - 1) max 0))) } } @@ -140,6 +143,14 @@ case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => hyperlink_position(props).map(_ :: links) + case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => + val iterator = + for { + Text.Info(entry_range, (entry, model)) <- resources.bibtex_entries_iterator + if entry == name + } yield Line.Node_Range(model.node_name.node, model.content.doc.range(entry_range)) + if (iterator.isEmpty) None else Some((links /: iterator)(_ :+ _)) + case _ => None }) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/VSCode/src/vscode_resources.scala Sun Jan 08 19:35:14 2017 +0100 @@ -11,7 +11,7 @@ import java.io.{File => JFile} -import scala.util.parsing.input.{Reader, CharSequenceReader} +import scala.util.parsing.input.Reader object VSCode_Resources @@ -67,12 +67,33 @@ else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath } + def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file) + def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) + + + /* file content */ + + def read_file_content(file: JFile): Option[String] = + try { Some(Line.normalize(File.read(file))) } + catch { case ERROR(_) => None } + + def get_file_content(file: JFile): Option[String] = + get_model(file) match { + case Some(model) => Some(model.content.text) + case None => read_file_content(file) + } + + def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = + for { + (_, model) <- state.value.models.iterator + Text.Info(range, entry) <- model.content.bibtex_entries.iterator + } yield Text.Info(range, (entry, model)) + override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { val file = node_file(name) get_model(file) match { - case Some(model) => - f(new CharSequenceReader(model.doc.make_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 } @@ -84,9 +105,6 @@ /* document models */ - def get_model(file: JFile): Option[Document_Model] = state.value.models.get(file) - def get_model(name: Document.Node.Name): Option[Document_Model] = get_model(node_file(name)) - def visible_node(name: Document.Node.Name): Boolean = get_model(name) match { case Some(model) => model.node_visible @@ -120,7 +138,7 @@ (for { (file, model) <- st.models.iterator if changed_files(file) && model.external_file - text <- try_read(file) + text <- read_file_content(file) model1 <- model.update_text(text) } yield (file, model1)).toList if (changed_models.isEmpty) (false, st) @@ -131,23 +149,8 @@ }) - /* file content */ - - def try_read(file: JFile): Option[String] = - try { Some(Line.normalize(File.read(file))) } - catch { case ERROR(_) => None } - - def get_file_content(file: JFile): Option[String] = - get_model(file) match { - case Some(model) => Some(model.doc.make_text) - case None => try_read(file) - } - - /* resolve dependencies */ - val thy_info = new Thy_Info(this) - def resolve_dependencies(session: Session, watcher: File_Watcher): (Boolean, Boolean) = { state.change_result(st => @@ -164,7 +167,7 @@ /* auxiliary files */ val stable_tip_version = - if (st.models.forall({ case (_, model) => model.pending_edits.isEmpty })) + if (st.models.forall(entry => entry._2.is_stable)) session.current_state().stable_tip_version else None @@ -182,7 +185,7 @@ node_name <- thy_files.iterator ++ aux_files.iterator file = node_file(node_name) if !st.models.isDefinedAt(file) - text <- { watcher.register_parent(file); try_read(file) } + text <- { watcher.register_parent(file); read_file_content(file) } } yield { val model = Document_Model.init(session, node_name) diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/etc/options --- a/src/Tools/jEdit/etc/options Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/etc/options Sun Jan 08 19:35:14 2017 +0100 @@ -6,11 +6,8 @@ public option jedit_print_mode : string = "" -- "default print modes for output, separated by commas (change requires restart)" -public option jedit_auto_load : bool = false - -- "load all required files automatically to resolve theory imports" - public option jedit_auto_resolve : bool = false - -- "automatically resolve auxiliary files within the editor" + -- "automatically resolve auxiliary files within the document model" public option jedit_reset_font_size : int = 18 -- "reset main text font size" diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/bibtex_jedit.scala --- a/src/Tools/jEdit/src/bibtex_jedit.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/bibtex_jedit.scala Sun Jan 08 19:35:14 2017 +0100 @@ -27,50 +27,13 @@ object Bibtex_JEdit { - /** buffer model **/ - - /* file type */ - - def check(buffer: Buffer): Boolean = - JEdit_Lib.buffer_name(buffer).endsWith(".bib") - - - /* parse entries */ - - def parse_buffer_entries(buffer: Buffer): List[(String, Text.Offset)] = - { - val chunks = - try { Bibtex.parse(JEdit_Lib.buffer_text(buffer)) } - catch { case ERROR(msg) => Output.warning(msg); Nil } - - val result = new mutable.ListBuffer[(String, Text.Offset)] - var offset = 0 - for (chunk <- chunks) { - if (chunk.name != "" && !chunk.is_command) result += ((chunk.name, offset)) - offset += chunk.source.length - } - result.toList - } - - - /* retrieve entries */ - - def entries_iterator(): Iterator[(String, Buffer, Text.Offset)] = - for { - buffer <- JEdit_Lib.jedit_buffers() - model <- PIDE.document_model(buffer).iterator - (name, offset) <- model.bibtex_entries.iterator - } yield (name, buffer, offset) - - - /* completion */ + /** completion **/ def complete(name: String): List[String] = - { - val name1 = name.toLowerCase - (for ((entry, _, _) <- entries_iterator() if entry.toLowerCase.containsSlice(name1)) - yield entry).toList - } + (for { + Text.Info(_, (entry, _)) <- Document_Model.bibtex_entries_iterator() + if entry.toLowerCase.containsSlice(name.toLowerCase) + } yield entry).toList def completion( history: Completion.History, @@ -108,7 +71,7 @@ case text_area: TextArea => text_area.getBuffer match { case buffer: Buffer - if (check(buffer) && buffer.isEditable) => + if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) => val menu = new JMenu("BibTeX entries") for (entry <- Bibtex.entries) { val item = new JMenuItem(entry.kind) diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/document_model.scala --- a/src/Tools/jEdit/src/document_model.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/document_model.scala Sun Jan 08 19:35:14 2017 +0100 @@ -2,8 +2,8 @@ Author: Fabian Immler, TU Munich Author: Makarius -Document model connected to jEdit buffer (node in theory graph or -auxiliary file). +Document model connected to jEdit buffer or external file: content of theory +node or auxiliary file (blob). */ package isabelle.jedit @@ -12,95 +12,323 @@ import isabelle._ import scala.collection.mutable -import scala.util.parsing.input.CharSequenceReader -import org.gjt.sp.jedit.jEdit +import org.gjt.sp.jedit.{jEdit, View} import org.gjt.sp.jedit.Buffer import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer} object Document_Model { - /* document model of buffer */ + /* document models */ + + sealed case class State( + models: Map[Document.Node.Name, Document_Model] = Map.empty, + buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty) + { + def models_iterator: Iterator[Document_Model] = + for ((_, model) <- models.iterator) yield model + + def file_models_iterator: Iterator[File_Model] = + for { + (_, model) <- models.iterator + if model.isInstanceOf[File_Model] + } yield model.asInstanceOf[File_Model] + + def buffer_models_iterator: Iterator[Buffer_Model] = + for ((_, model) <- buffer_models.iterator) yield model + - private val key = "PIDE.document_model" + def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer) + : (Buffer_Model, State) = + { + val old_model = + models.get(node_name) match { + case Some(file_model: File_Model) => Some(file_model) + case Some(buffer_model: Buffer_Model) => Some(buffer_model.exit()) + case _ => None + } + val buffer_model = Buffer_Model(session, node_name, buffer).init(old_model) + (buffer_model, + copy(models = models + (node_name -> buffer_model), + buffer_models = buffer_models + (buffer -> buffer_model))) + } + + def close_buffer(buffer: JEditBuffer): State = + { + buffer_models.get(buffer) match { + case None => this + case Some(buffer_model) => + val file_model = buffer_model.exit() + copy(models = models + (file_model.node_name -> file_model), + buffer_models = buffer_models - buffer) + } + } - def apply(buffer: Buffer): Option[Document_Model] = + def provide_file(session: Session, node_name: Document.Node.Name, text: String): State = + if (models.isDefinedAt(node_name)) this + else { + val edit = Text.Edit.insert(0, text) + val model = File_Model(session, node_name, File_Content(text), pending_edits = List(edit)) + copy(models = models + (node_name -> model)) + } + } + + private val state = Synchronized(State()) // owned by GUI thread + + def get_models(): Map[Document.Node.Name, Document_Model] = state.value.models + def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name) + def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer) + + def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] = + for { + model <- state.value.models_iterator + Text.Info(range, entry) <- model.bibtex_entries.iterator + } yield Text.Info(range, (entry, model)) + + + /* syntax */ + + def syntax_changed(names: List[Document.Node.Name]) { - buffer.getProperty(key) match { - case model: Document_Model => Some(model) - case _ => None + GUI_Thread.require {} + + val models = state.value.models + for (name <- names.iterator; model <- models.get(name)) { + model match { case buffer_model: Buffer_Model => buffer_model.syntax_changed() case _ => } } } + + /* init and exit */ + + def init(session: Session, node_name: Document.Node.Name, buffer: Buffer): Buffer_Model = + { + GUI_Thread.require {} + state.change_result(st => + st.buffer_models.get(buffer) match { + case Some(buffer_model) if buffer_model.node_name == node_name => + buffer_model.init_token_marker + (buffer_model, st) + case _ => + val res = st.close_buffer(buffer).open_buffer(session, node_name, buffer) + buffer.propertiesChanged + res + }) + } + def exit(buffer: Buffer) { GUI_Thread.require {} - apply(buffer) match { - case None => - case Some(model) => - model.deactivate() - buffer.unsetProperty(key) + state.change(st => + if (st.buffer_models.isDefinedAt(buffer)) { + val res = st.close_buffer(buffer) buffer.propertiesChanged + res + } + else st) + } + + def provide_files(session: Session, files: List[(Document.Node.Name, String)]) + { + GUI_Thread.require {} + state.change(st => + (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) }) + } + + + /* required nodes */ + + def required_nodes(): Set[Document.Node.Name] = + (for { + model <- state.value.models_iterator + if model.node_required + } yield model.node_name).toSet + + def node_required(name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false) + { + GUI_Thread.require {} + + val changed = + state.change_result(st => + st.models.get(name) match { + case None => (false, st) + case Some(model) => + val required = if (toggle) !model.node_required else set + model match { + case model1: File_Model if required != model1.node_required => + (true, st.copy(models = st.models + (name -> model1.copy(node_required = required)))) + case model1: Buffer_Model if required != model1.node_required => + model1.set_node_required(required); (true, st) + case _ => (false, st) + } + }) + if (changed) { + PIDE.options_changed() + PIDE.editor.flush() } } - def init(session: Session, buffer: Buffer, node_name: Document.Node.Name, - old_model: Option[Document_Model]): Document_Model = + def view_node_required(view: View, toggle: Boolean = false, set: Boolean = false): Unit = + Document_Model.get(view.getBuffer).foreach(model => + node_required(model.node_name, toggle = toggle, set = set)) + + + /* flushed edits */ + + def flush_edits(hidden: Boolean): (Document.Blobs, List[Document.Edit_Text]) = { GUI_Thread.require {} - val model = - old_model match { - case Some(old) if old.node_name == node_name => old - case _ => - apply(buffer).map(_.deactivate) - val model = new Document_Model(session, buffer, node_name) - buffer.setProperty(key, model) - model.activate() - buffer.propertiesChanged - model - } - model.init_token_marker - model + state.change_result(st => + { + val doc_blobs = + Document.Blobs( + (for { + model <- st.models_iterator + blob <- model.get_blob + } yield (model.node_name -> blob)).toMap) + + val buffer_edits = + (for { + model <- st.buffer_models_iterator + edit <- model.flush_edits(doc_blobs, hidden).iterator + } yield edit).toList + + val file_edits = + (for { + model <- st.file_models_iterator + change <- model.flush_edits(doc_blobs, hidden) + } yield change).toList + + val edits = buffer_edits ::: file_edits.flatMap(_._1) + + ((doc_blobs, edits), + st.copy( + models = (st.models /: file_edits) { case (ms, (_, m)) => ms + (m.node_name -> m) })) + }) + } + + + /* file content */ + + sealed case class File_Content(text: String) + { + lazy val bytes: Bytes = Bytes(Symbol.encode(text)) + lazy val chunk: Symbol.Text_Chunk = Symbol.Text_Chunk(text) + lazy val bibtex_entries: List[Text.Info[String]] = + try { Bibtex.document_entries(text) } + catch { case ERROR(msg) => Output.warning(msg); Nil } } } +sealed abstract class Document_Model extends Document.Model +{ + /* content */ -class Document_Model(val session: Session, val buffer: Buffer, val node_name: Document.Node.Name) -{ - override def toString: String = node_name.toString + def bibtex_entries: List[Text.Info[String]] + /* perspective */ + + def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = Nil + + def node_perspective( + doc_blobs: Document.Blobs, hidden: Boolean): (Boolean, Document.Node.Perspective_Text) = + { + GUI_Thread.require {} + + if (Isabelle.continuous_checking && is_theory) { + val snapshot = this.snapshot() + + val reparse = snapshot.node.load_commands_changed(doc_blobs) + val perspective = + if (hidden) Text.Perspective.empty + else { + val view_ranges = document_view_ranges(snapshot) + val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) + Text.Perspective(view_ranges ::: load_ranges) + } + val overlays = PIDE.editor.node_overlays(node_name) + + (reparse, Document.Node.Perspective(node_required, perspective, overlays)) + } + else (false, Document.Node.no_perspective_text) + } +} + +case class File_Model( + session: Session, + node_name: Document.Node.Name, + content: Document_Model.File_Content, + node_required: Boolean = false, + last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text, + pending_edits: List[Text.Edit] = Nil) extends Document_Model +{ /* header */ - def is_theory: Boolean = node_name.is_theory + def node_header: Document.Node.Header = + PIDE.resources.special_header(node_name) getOrElse + PIDE.resources.check_thy_reader("", node_name, Scan.char_reader(content.text), strict = false) + + + /* content */ + + def node_position(offset: Text.Offset): Line.Node_Position = + Line.Node_Position(node_name.node, + Line.Position.zero.advance(content.text.substring(0, offset), Text.Length)) + + def get_blob: Option[Document.Blob] = + if (is_theory) None + else Some(Document.Blob(content.bytes, content.chunk, pending_edits.nonEmpty)) + + def bibtex_entries: List[Text.Info[String]] = + if (Bibtex.check_name(node_name)) content.bibtex_entries else Nil + + + /* edits */ + + def update_text(text: String): Option[File_Model] = + Text.Edit.replace(0, content.text, text) match { + case Nil => None + case edits => + val content1 = Document_Model.File_Content(text) + val pending_edits1 = pending_edits ::: edits + Some(copy(content = content1, pending_edits = pending_edits1)) + } + + def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean) + : Option[(List[Document.Edit_Text], File_Model)] = + { + val (reparse, perspective) = node_perspective(doc_blobs, hidden) + if (reparse || pending_edits.nonEmpty || last_perspective != perspective) { + val edits = node_edits(pending_edits, perspective) + Some((edits, copy(last_perspective = perspective, pending_edits = Nil))) + } + else None + } + + + /* snapshot */ + + def is_stable: Boolean = pending_edits.isEmpty + def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits) +} + +case class Buffer_Model(session: Session, node_name: Document.Node.Name, buffer: Buffer) + extends Document_Model +{ + /* header */ def node_header(): Document.Node.Header = { GUI_Thread.require {} PIDE.resources.special_header(node_name) getOrElse - { - if (is_theory) { - JEdit_Lib.buffer_lock(buffer) { - Token_Markup.line_token_iterator( - Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst( - { - case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start - }) - match { - case Some(offset) => - val length = buffer.getLength - offset - PIDE.resources.check_thy_reader("", node_name, - new CharSequenceReader(buffer.getSegment(offset, length)), Token.Pos.command) - case None => - Document.Node.no_header - } - } + JEdit_Lib.buffer_lock(buffer) { + PIDE.resources.check_thy_reader( + "", node_name, JEdit_Lib.buffer_reader(buffer), strict = false) } - else Document.Node.no_header - } } @@ -109,39 +337,16 @@ // owned by GUI thread private var _node_required = false def node_required: Boolean = _node_required - def node_required_=(b: Boolean) - { - GUI_Thread.require {} - if (_node_required != b && is_theory) { - _node_required = b - PIDE.options_changed() - PIDE.editor.flush() - } - } + def set_node_required(b: Boolean) { GUI_Thread.require { _node_required = b } } - def node_perspective(hidden: Boolean, doc_blobs: Document.Blobs) - : (Boolean, Document.Node.Perspective_Text) = + override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] = { GUI_Thread.require {} - if (Isabelle.continuous_checking && is_theory) { - val snapshot = this.snapshot() - - val document_view_ranges = - for { - doc_view <- PIDE.document_views(buffer) - range <- doc_view.perspective(snapshot).ranges - } yield range - - val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_)) - val reparse = snapshot.node.load_commands_changed(doc_blobs) - - (reparse, - Document.Node.Perspective(node_required, - Text.Perspective(if (hidden) Nil else document_view_ranges ::: load_ranges), - PIDE.editor.node_overlays(node_name))) - } - else (false, Document.Node.no_perspective_text) + (for { + doc_view <- PIDE.document_views(buffer).iterator + range <- doc_view.perspective(snapshot).ranges.iterator + } yield range).toList } @@ -151,7 +356,7 @@ private def reset_blob(): Unit = GUI_Thread.require { _blob = None } - def get_blob(): Option[Document.Blob] = + def get_blob: Option[Document.Blob] = GUI_Thread.require { if (is_theory) None else { @@ -159,12 +364,12 @@ _blob match { case Some(x) => x case None => - val bytes = PIDE.resources.file_content(buffer) + val bytes = PIDE.resources.make_file_content(buffer) val chunk = Symbol.Text_Chunk(buffer.getSegment(0, buffer.getLength)) _blob = Some((bytes, chunk)) (bytes, chunk) } - val changed = pending_edits.is_pending() + val changed = pending_edits.nonEmpty Some(Document.Blob(bytes, chunk, changed)) } } @@ -172,18 +377,21 @@ /* bibtex entries */ - private var _bibtex: Option[List[(String, Text.Offset)]] = None // owned by GUI thread + private var _bibtex_entries: Option[List[Text.Info[String]]] = None // owned by GUI thread - private def reset_bibtex(): Unit = GUI_Thread.require { _bibtex = None } + private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None } - def bibtex_entries(): List[(String, Text.Offset)] = + def bibtex_entries: List[Text.Info[String]] = GUI_Thread.require { - if (Bibtex_JEdit.check(buffer)) { - _bibtex match { + if (Bibtex.check_name(node_name)) { + _bibtex_entries match { case Some(entries) => entries case None => - val entries = Bibtex_JEdit.parse_buffer_entries(buffer) - _bibtex = Some(entries) + val text = JEdit_Lib.buffer_text(buffer) + val entries = + try { Bibtex.document_entries(text) } + catch { case ERROR(msg) => Output.warning(msg); Nil } + _bibtex_entries = Some(entries) entries } } @@ -191,110 +399,69 @@ } - /* edits */ - - def node_edits( - clear: Boolean, - text_edits: List[Text.Edit], - perspective: Document.Node.Perspective_Text): List[Document.Edit_Text] = - { - val edits: List[Document.Edit_Text] = - get_blob() match { - case None => - val header_edit = session.header_edit(node_name, node_header()) - if (clear) - List(header_edit, - node_name -> Document.Node.Clear(), - node_name -> Document.Node.Edits(text_edits), - node_name -> perspective) - else - List(header_edit, - node_name -> Document.Node.Edits(text_edits), - node_name -> perspective) - case Some(blob) => - List(node_name -> Document.Node.Blob(blob), - node_name -> Document.Node.Edits(text_edits)) - } - edits.filterNot(_._2.is_void) - } - - /* pending edits */ private object pending_edits { - private var pending_clear = false private val pending = new mutable.ListBuffer[Text.Edit] private var last_perspective = Document.Node.no_perspective_text - def is_pending(): Boolean = synchronized { pending_clear || pending.nonEmpty } - def snapshot(): List[Text.Edit] = synchronized { pending.toList } + def nonEmpty: Boolean = synchronized { pending.nonEmpty } + def get_edits: List[Text.Edit] = synchronized { pending.toList } + def get_last_perspective: Document.Node.Perspective_Text = synchronized { last_perspective } + def set_last_perspective(perspective: Document.Node.Perspective_Text): Unit = + synchronized { last_perspective = perspective } - def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] = + def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = synchronized { GUI_Thread.require {} - val clear = pending_clear - val edits = snapshot() - val (reparse, perspective) = node_perspective(hidden, doc_blobs) - if (clear || reparse || edits.nonEmpty || last_perspective != perspective) { - pending_clear = false + val edits = get_edits + val (reparse, perspective) = node_perspective(doc_blobs, hidden) + if (reparse || edits.nonEmpty || last_perspective != perspective) { pending.clear last_perspective = perspective - node_edits(clear, edits, perspective) + node_edits(edits, perspective) } else Nil } - def edit(clear: Boolean, e: Text.Edit): Unit = synchronized + def edit(edits: List[Text.Edit]): Unit = synchronized { GUI_Thread.require {} reset_blob() - reset_bibtex() + reset_bibtex_entries() for (doc_view <- PIDE.document_views(buffer)) doc_view.rich_text_area.active_reset() - if (clear) { - pending_clear = true - pending.clear - } - pending += e + pending ++= edits PIDE.editor.invoke() } } - def is_stable(): Boolean = !pending_edits.is_pending(); + def is_stable: Boolean = !pending_edits.nonEmpty + def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits) - def snapshot(): Document.Snapshot = - session.snapshot(node_name, pending_edits.snapshot()) - - def flushed_edits(hidden: Boolean, doc_blobs: Document.Blobs): List[Document.Edit_Text] = - pending_edits.flushed_edits(hidden, doc_blobs) + def flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] = + pending_edits.flush_edits(doc_blobs, hidden) /* buffer listener */ private val buffer_listener: BufferListener = new BufferAdapter { - override def bufferLoaded(buffer: JEditBuffer) - { - pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))) - } - override def contentInserted(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, length: Int) { - if (!buffer.isLoading) - pending_edits.edit(false, Text.Edit.insert(offset, buffer.getText(offset, length))) + pending_edits.edit(List(Text.Edit.insert(offset, buffer.getText(offset, length)))) } override def preContentRemoved(buffer: JEditBuffer, start_line: Int, offset: Int, num_lines: Int, removed_length: Int) { - if (!buffer.isLoading) - pending_edits.edit(false, Text.Edit.remove(offset, buffer.getText(offset, removed_length))) + pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length)))) } } @@ -310,7 +477,7 @@ buffer.invalidateCachedFoldLevels } - private def init_token_marker() + def init_token_marker() { Isabelle.buffer_token_marker(buffer) match { case Some(marker) if marker != buffer.getTokenMarker => @@ -321,18 +488,41 @@ } - /* activation */ + /* init */ + + def init(old_model: Option[File_Model]): Buffer_Model = + { + GUI_Thread.require {} - private def activate() - { - pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer))) + old_model match { + case None => + pending_edits.edit(List(Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))) + case Some(file_model) => + set_node_required(file_model.node_required) + pending_edits.set_last_perspective(file_model.last_perspective) + pending_edits.edit( + file_model.pending_edits ::: + Text.Edit.replace(0, file_model.content.text, JEdit_Lib.buffer_text(buffer))) + } + buffer.addBufferListener(buffer_listener) init_token_marker() + + this } - private def deactivate() + + /* exit */ + + def exit(): File_Model = { + GUI_Thread.require {} + buffer.removeBufferListener(buffer_listener) init_token_marker() + + val content = Document_Model.File_Content(JEdit_Lib.buffer_text(buffer)) + File_Model(session, node_name, content, node_required, + pending_edits.get_last_perspective, pending_edits.get_edits) } } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/document_view.scala --- a/src/Tools/jEdit/src/document_view.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/document_view.scala Sun Jan 08 19:35:14 2017 +0100 @@ -45,7 +45,7 @@ } } - def init(model: Document_Model, text_area: JEditTextArea): Document_View = + def init(model: Buffer_Model, text_area: JEditTextArea): Document_View = { exit(text_area) val doc_view = new Document_View(model, text_area) @@ -56,7 +56,7 @@ } -class Document_View(val model: Document_Model, val text_area: JEditTextArea) +class Document_View(val model: Buffer_Model, val text_area: JEditTextArea) { private val session = model.session diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/isabelle.scala --- a/src/Tools/jEdit/src/isabelle.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Sun Jan 08 19:35:14 2017 +0100 @@ -63,7 +63,7 @@ def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] = if (buffer == null) None else - (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match { + (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match { case ("isabelle", Some(model)) => Some(PIDE.session.recent_syntax(model.node_name)) case (mode, _) => mode_syntax(mode) @@ -228,19 +228,9 @@ /* required document nodes */ - private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false) - { - GUI_Thread.require {} - PIDE.document_model(view.getBuffer) match { - case Some(model) => - model.node_required = (if (toggle) !model.node_required else set) - case None => - } - } - - def set_node_required(view: View) { node_required_update(view, set = true) } - def reset_node_required(view: View) { node_required_update(view, set = false) } - def toggle_node_required(view: View) { node_required_update(view, toggle = true) } + def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) } + def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) } + def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) } /* font size */ @@ -329,7 +319,7 @@ { val buffer = text_area.getBuffer if (!snapshot.is_outdated && text != "") { - (snapshot.find_command(id), PIDE.document_model(buffer)) match { + (snapshot.find_command(id), Document_Model.get(buffer)) match { case (Some((node, command)), Some(model)) if command.node_name == model.node_name => node.command_start(command) match { case Some(start) => diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Jan 08 19:35:14 2017 +0100 @@ -178,7 +178,7 @@ override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { val opt_snapshot = - PIDE.document_model(buffer) match { + Document_Model.get(buffer) match { case Some(model) if model.is_theory => Some(model.snapshot) case _ => None } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Jan 08 19:35:14 2017 +0100 @@ -22,27 +22,11 @@ override def session: Session = PIDE.session - // owned by GUI thread - private var removed_nodes = Set.empty[Document.Node.Name] - - def remove_node(name: Document.Node.Name): Unit = - GUI_Thread.require { removed_nodes += name } - - override def flush(hidden: Boolean = false) - { - GUI_Thread.require {} - - val doc_blobs = PIDE.document_blobs() - val models = PIDE.document_models() - - val removed = removed_nodes; removed_nodes = Set.empty - val removed_perspective = - (removed -- models.iterator.map(_.node_name)).toList.map( - name => (name, Document.Node.no_perspective_text)) - - val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective - session.update(doc_blobs, edits) - } + override def flush(hidden: Boolean = false): Unit = + GUI_Thread.require { + val (doc_blobs, edits) = Document_Model.flush_edits(hidden) + session.update(doc_blobs, edits) + } private val delay1_flush = GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } @@ -53,18 +37,11 @@ def invoke(): Unit = delay1_flush.invoke() def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } - def stable_tip_version(): Option[Document.Version] = - GUI_Thread.require { - if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable)) - session.current_state().stable_tip_version - else None - } - def visible_node(name: Document.Node.Name): Boolean = - JEdit_Lib.jedit_buffer(name) match { - case Some(buffer) => JEdit_Lib.jedit_text_areas(buffer).nonEmpty - case None => false - } + (for { + text_area <- JEdit_Lib.jedit_text_areas() + doc_view <- Document_View(text_area) + } yield doc_view.model.node_name).contains(name) /* current situation */ @@ -73,21 +50,16 @@ GUI_Thread.require { jEdit.getActiveView() } override def current_node(view: View): Option[Document.Node.Name] = - GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } + GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } override def current_node_snapshot(view: View): Option[Document.Snapshot] = - GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } + GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) } override def node_snapshot(name: Document.Node.Name): Document.Snapshot = { GUI_Thread.require {} - - JEdit_Lib.jedit_buffer(name) match { - case Some(buffer) => - PIDE.document_model(buffer) match { - case Some(model) => model.snapshot - case None => session.snapshot(name) - } + Document_Model.get(name) match { + case Some(model) => model.snapshot case None => session.snapshot(name) } } @@ -113,7 +85,7 @@ } else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) case _ => - PIDE.document_model(buffer) match { + Document_Model.get(buffer) match { case Some(model) if !model.is_theory => snapshot.version.nodes.commands_loading(model.node_name) match { case cmd :: _ => Some(cmd) @@ -251,12 +223,6 @@ override def toString: String = "URL " + quote(name) } - def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink = - new Hyperlink { - def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset) - override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer)) - } - def hyperlink_file(focus: Boolean, name: String): Hyperlink = hyperlink_file(focus, Line.Node_Position(name)) @@ -266,23 +232,40 @@ override def toString: String = "file " + quote(pos.name) } + def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink = + model match { + case file_model: File_Model => + val pos = + try { file_model.node_position(offset) } + catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } + hyperlink_file(focus, pos) + case buffer_model: Buffer_Model => + new Hyperlink { + def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset) + override def toString: String = "buffer " + quote(model.node_name.node) + } + } + def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset) : Option[Hyperlink] = { for (name <- PIDE.resources.source_file(source_name)) yield { - JEdit_Lib.jedit_buffer(name) match { - case Some(buffer) if offset > 0 => - val pos = - JEdit_Lib.buffer_lock(buffer) { + def hyperlink(pos: Line.Position) = + hyperlink_file(focus, Line.Node_Position(name, pos)) + + if (offset > 0) { + PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { + case Some(text) => + hyperlink( (Line.Position.zero /: - (Symbol.iterator(JEdit_Lib.buffer_text(buffer)). + (Symbol.iterator(text). zipWithIndex.takeWhile(p => p._2 < offset - 1). - map(_._1)))(_.advance(_, Text.Length)) - } - hyperlink_file(focus, Line.Node_Position(name, pos)) - case _ => - hyperlink_file(focus, Line.Node_Position(name, Line.Position((line1 - 1) max 0))) + map(_._1)))(_.advance(_, Text.Length))) + case None => + hyperlink(Line.Position((line1 - 1) max 0)) + } } + else hyperlink(Line.Position((line1 - 1) max 0)) } } diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_lib.scala Sun Jan 08 19:35:14 2017 +0100 @@ -99,7 +99,7 @@ buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } def buffer_reader(buffer: JEditBuffer): CharSequenceReader = - new CharSequenceReader(buffer.getSegment(0, buffer.getLength)) + Scan.char_reader(buffer.getSegment(0, buffer.getLength)) def buffer_mode(buffer: JEditBuffer): String = { diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/jedit_rendering.scala --- a/src/Tools/jEdit/src/jedit_rendering.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_rendering.scala Sun Jan 08 19:35:14 2017 +0100 @@ -413,9 +413,9 @@ case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) => val opt_link = - Bibtex_JEdit.entries_iterator.collectFirst( - { case (a, buffer, offset) if a == name => - PIDE.editor.hyperlink_buffer(true, buffer, offset) }) + Document_Model.bibtex_entries_iterator.collectFirst( + { case Text.Info(entry_range, (entry, model)) if entry == name => + PIDE.editor.hyperlink_model(true, model, entry_range.start) }) opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link)) case _ => None diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/jedit_resources.scala --- a/src/Tools/jEdit/src/jedit_resources.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/jedit_resources.scala Sun Jan 08 19:35:14 2017 +0100 @@ -33,7 +33,7 @@ base_syntax: Outer_Syntax) extends Resources(loaded_theories, known_theories, base_syntax) { - /* document node names */ + /* document node name */ def node_name(buffer: Buffer): Document.Node.Name = { @@ -43,15 +43,21 @@ Document.Node.Name(node, master_dir, theory) } + def node_name(path: String): Document.Node.Name = + { + val vfs = VFSManager.getVFSForPath(path) + val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path + val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("") + val master_dir = if (theory == "") "" else vfs.getParentOfPath(path) + Document.Node.Name(node, master_dir, theory) + } + def theory_node_name(buffer: Buffer): Option[Document.Node.Name] = { val name = node_name(buffer) if (name.is_theory) Some(name) else None } - - /* file-system operations */ - override def append(dir: String, source_path: Path): String = { val path = source_path.expand @@ -67,12 +73,35 @@ } } + + /* file content */ + + def read_file_content(node_name: Document.Node.Name): Option[String] = + { + val name = node_name.node + try { + val text = + if (Url.is_wellformed(name)) Url.read(Url(name)) + else File.read(new JFile(name)) + Some(Symbol.decode(Line.normalize(text))) + } + catch { case ERROR(_) => None } + } + + def get_file_content(node_name: Document.Node.Name): Option[String] = + Document_Model.get(node_name) match { + case Some(model: Buffer_Model) => Some(JEdit_Lib.buffer_text(model.buffer)) + case Some(model: File_Model) => Some(model.content.text) + case None => read_file_content(node_name) + } + override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A = { GUI_Thread.now { - JEdit_Lib.jedit_buffer(name) match { - case Some(buffer) => - JEdit_Lib.buffer_lock(buffer) { Some(f(JEdit_Lib.buffer_reader(buffer))) } + Document_Model.get(name) match { + case Some(model: Buffer_Model) => + JEdit_Lib.buffer_lock(model.buffer) { Some(f(JEdit_Lib.buffer_reader(model.buffer))) } + case Some(model: File_Model) => Some(f(Scan.char_reader(model.content.text))) case None => None } } getOrElse { @@ -86,8 +115,6 @@ } - /* file content */ - private class File_Content_Output(buffer: Buffer) extends ByteArrayOutputStream(buffer.getLength + 1) { @@ -106,7 +133,7 @@ } } - def file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content() + def make_file_content(buffer: Buffer): Bytes = (new File_Content(buffer)).content() /* theory text edits */ @@ -114,14 +141,7 @@ override def commit(change: Session.Change) { if (change.syntax_changed.nonEmpty) - GUI_Thread.later { - val changed = change.syntax_changed.toSet - for { - buffer <- JEdit_Lib.jedit_buffers() - model <- PIDE.document_model(buffer) - if changed(model.node_name) - } model.syntax_changed() - } + GUI_Thread.later { Document_Model.syntax_changed(change.syntax_changed) } if (change.deps_changed || PIDE.options.bool("jedit_auto_resolve") && undefined_blobs(change.version.nodes).nonEmpty) PIDE.deps_changed() diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/plugin.scala Sun Jan 08 19:35:14 2017 +0100 @@ -63,12 +63,6 @@ /* document model and view */ - def document_model(buffer: JEditBuffer): Option[Document_Model] = - buffer match { - case b: Buffer => Document_Model(b) - case _ => None - } - def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area) def document_views(buffer: Buffer): List[Document_View] = @@ -77,24 +71,9 @@ doc_view <- document_view(text_area) } yield doc_view - def document_models(): List[Document_Model] = - for { - buffer <- JEdit_Lib.jedit_buffers().toList - model <- document_model(buffer) - } yield model - - def document_blobs(): Document.Blobs = - Document.Blobs( - (for { - buffer <- JEdit_Lib.jedit_buffers() - model <- document_model(buffer) - blob <- model.get_blob() - } yield (model.node_name -> blob)).toMap) - def exit_models(buffers: List[Buffer]) { GUI_Thread.now { - PIDE.editor.flush() buffers.foreach(buffer => JEdit_Lib.buffer_lock(buffer) { JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) @@ -115,7 +94,7 @@ if (buffer.isLoaded) { JEdit_Lib.buffer_lock(buffer) { val node_name = resources.node_name(buffer) - val model = Document_Model.init(session, buffer, node_name, document_model(buffer)) + val model = Document_Model.init(session, node_name, buffer) for { text_area <- JEdit_Lib.jedit_text_areas(buffer) if document_view(text_area).map(_.model) != Some(model) @@ -132,7 +111,7 @@ def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { - document_model(buffer) match { + Document_Model.get(buffer) match { case Some(model) => Document_View.init(model, text_area) case None => } @@ -151,8 +130,7 @@ def snapshot(view: View): Document.Snapshot = GUI_Thread.now { - val buffer = view.getBuffer - document_model(buffer) match { + Document_Model.get(view.getBuffer) match { case Some(model) => model.snapshot case None => error("No document model for current buffer") } @@ -201,65 +179,54 @@ if (Isabelle.continuous_checking && delay_load_activated() && PerspectiveManager.isPerspectiveEnabled) { - try { - val view = jEdit.getActiveView() - - val buffers = JEdit_Lib.jedit_buffers().toList - if (buffers.forall(_.isLoaded)) { - def loaded_buffer(name: String): Boolean = - buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name) + if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke() + else { + val required_files = + { + val models = Document_Model.get_models() val thys = - for { - buffer <- buffers - model <- PIDE.document_model(buffer) - if model.is_theory - } yield (model.node_name, Position.none) - - val thy_info = new Thy_Info(PIDE.resources) - val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node) + (for ((node_name, model) <- models.iterator if model.is_theory) + yield (node_name, Position.none)).toList + val thy_files = PIDE.resources.thy_info.dependencies("", thys).deps.map(_.name) val aux_files = if (PIDE.options.bool("jedit_auto_resolve")) { - PIDE.editor.stable_tip_version() match { - case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node) + val stable_tip_version = + if (models.forall(p => p._2.is_stable)) + PIDE.session.current_state().stable_tip_version + else None + stable_tip_version match { + case Some(version) => PIDE.resources.undefined_blobs(version.nodes) case None => delay_load.invoke(); Nil } } else Nil - val files = - (thy_files ::: aux_files).filter(file => - !loaded_buffer(file) && PIDE.resources.check_file(file)) - - if (files.nonEmpty) { - if (PIDE.options.bool("jedit_auto_load")) { - files.foreach(file => jEdit.openFile(null: View, file)) - } - else { - val files_list = new ListView(files.sorted) - for (i <- 0 until files.length) - files_list.selection.indices += i + (thy_files ::: aux_files).filterNot(models.isDefinedAt(_)) + } + if (required_files.nonEmpty) { + try { + Standard_Thread.fork("resolve_dependencies") { + val loaded_files = + for { + name <- required_files + text <- PIDE.resources.read_file_content(name) + } yield (name, text) - val answer = - GUI.confirm_dialog(view, - "Auto loading of required files", - JOptionPane.YES_NO_OPTION, - "The following files are required to resolve theory imports.", - "Reload selected files now?", - new ScrollPane(files_list), - new Isabelle.Continuous_Checking) - if (answer == 0) { - files.foreach(file => - if (files_list.selection.items.contains(file)) - jEdit.openFile(null: View, file)) + GUI_Thread.later { + try { + Document_Model.provide_files(PIDE.session, loaded_files) + delay_init.invoke() + } + finally { delay_load_active.change(_ => false) } } } } + catch { case _: Throwable => delay_load_active.change(_ => false) } } - else delay_load.invoke() + else delay_load_active.change(_ => false) } - finally { delay_load_active.change(_ => false) } } } @@ -300,6 +267,8 @@ case Session.Shutdown => GUI_Thread.later { delay_load.revoke() + delay_init.revoke() + PIDE.editor.flush() PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) } @@ -343,14 +312,14 @@ JEdit_Sessions.session_info().open_root).foreach(_.follow(view)) case msg: BufferUpdate - if msg.getWhat == BufferUpdate.LOADED || - msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || - msg.getWhat == BufferUpdate.CLOSING => + if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING => + if (msg.getBuffer != null) { + PIDE.exit_models(List(msg.getBuffer)) + PIDE.editor.invoke_generated() + } - if (msg.getWhat == BufferUpdate.CLOSING) { - val buffer = msg.getBuffer - if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer)) - } + case msg: BufferUpdate + if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED => if (PIDE.session.is_ready) { delay_init.invoke() delay_load.invoke() diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/state_dockable.scala Sun Jan 08 19:35:14 2017 +0100 @@ -64,7 +64,7 @@ { GUI_Thread.require {} - PIDE.document_model(view.getBuffer).map(_.snapshot()) match { + Document_Model.get(view.getBuffer).map(_.snapshot()) match { case Some(snapshot) => (PIDE.editor.current_command(view, snapshot), print_state.get_location) match { case (Some(command1), Some(command2)) if command1.id == command2.id => diff -r 5477d6b1222f -r 048aa6ea3d32 src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Sat Jan 07 09:56:33 2017 +0100 +++ b/src/Tools/jEdit/src/theories_dockable.scala Sun Jan 08 19:35:14 2017 +0100 @@ -38,12 +38,7 @@ val index = peer.locationToIndex(point) if (index >= 0) { if (in_checkbox(peer.indexToLocation(index), point)) { - if (clicks == 1) { - for { - buffer <- JEdit_Lib.jedit_buffer(listData(index)) - model <- PIDE.document_model(buffer) - } model.node_required = !model.node_required - } + if (clicks == 1) Document_Model.node_required(listData(index), toggle = true) } else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node) } @@ -90,18 +85,7 @@ /* component state -- owned by GUI thread */ private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty - private var nodes_required: Set[Document.Node.Name] = Set.empty - - private def update_nodes_required() - { - nodes_required = Set.empty - for { - buffer <- JEdit_Lib.jedit_buffers - model <- PIDE.document_model(buffer) - if model.node_required - } nodes_required += model.node_name - } - update_nodes_required() + private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes() private def in_checkbox(loc0: Point, p: Point): Boolean = Node_Renderer_Component != null && @@ -229,7 +213,7 @@ GUI_Thread.later { continuous_checking.load() logic.load () - update_nodes_required() + nodes_required = Document_Model.required_nodes() status.repaint() }