--- 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 ***
--- 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>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
+ 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>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
--- 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" +
--- 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)
}
--- 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
{
--- 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) {
--- 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 =
--- 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(_))
--- 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))
- }
}
--- 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 */
--- 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(
--- 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)
--- 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 {
--- 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)
- }
}
--- 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)) =>
--- 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) {
--- 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
--- 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 */
--- 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();
--- 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)
}
--- 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))
--- 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 }
}
--- 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)
--- 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"
--- 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)
--- 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)
}
}
--- 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
--- 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) =>
--- 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
}
--- 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))
}
}
--- 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 =
{
--- 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
--- 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()
--- 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()
--- 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 =>
--- 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()
}