diff --git a/src/Tools/jEdit/src/document_model.scala b/src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala
+++ b/src/Tools/jEdit/src/document_model.scala
@@ -1,698 +1,700 @@
/* Title: Tools/jEdit/src/document_model.scala
Author: Fabian Immler, TU Munich
Author: Makarius
Document model connected to jEdit buffer or external file: content of theory
node or auxiliary file (blob).
*/
package isabelle.jedit
import isabelle._
import java.io.{File => JFile}
import scala.collection.mutable
import scala.annotation.tailrec
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.Buffer
import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
object Document_Model
{
/* document models */
sealed case class State(
models: Map[Document.Node.Name, Document_Model] = Map.empty,
buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
overlays: Document.Overlays = Document.Overlays.empty)
{
def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
for {
(node_name, model) <- models.iterator
if model.isInstanceOf[File_Model]
} yield (node_name, model.asInstanceOf[File_Model])
def document_blobs: Document.Blobs =
Document.Blobs(
(for {
(node_name, model) <- models.iterator
blob <- model.get_blob
} yield (node_name -> blob)).toMap)
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 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.init(session, node_name, 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 document_blobs(): Document.Blobs = state.value.document_blobs
/* bibtex */
def bibtex_entries_iterator(): Iterator[Text.Info[(String, Document_Model)]] =
Bibtex.entries_iterator(state.value.models)
def bibtex_completion(history: Completion.History, rendering: Rendering, caret: Text.Offset)
: Option[Completion.Result] =
Bibtex.completion(history, rendering, caret, state.value.models)
/* overlays */
def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
state.value.overlays(name)
def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
/* sync external files */
def sync_files(changed_files: Set[JFile]): Boolean =
{
state.change_result(st =>
{
val changed_models =
(for {
(node_name, model) <- st.file_models_iterator
file <- model.file if changed_files(file)
text <- PIDE.resources.read_file_content(node_name)
if model.content.text != text
} yield {
val content = Document_Model.File_Content(text)
val edits = Text.Edit.replace(0, model.content.text, text)
(node_name, model.copy(content = content, pending_edits = model.pending_edits ::: edits))
}).toList
if (changed_models.isEmpty) (false, st)
- else (true, st.copy(models = (st.models /: changed_models)(_ + _)))
+ else (true, st.copy(models = changed_models.foldLeft(st.models)(_ + _)))
})
}
/* syntax */
def syntax_changed(names: List[Document.Node.Name]): Unit =
{
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): Unit =
{
GUI_Thread.require {}
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)]): Unit =
{
GUI_Thread.require {}
state.change(st =>
- (st /: files) { case (st1, (node_name, text)) => st1.provide_file(session, node_name, text) })
+ files.foldLeft(st) {
+ case (st1, (node_name, text)) => st1.provide_file(session, node_name, text)
+ })
}
/* required nodes */
def required_nodes(): Set[Document.Node.Name] =
(for {
(node_name, model) <- state.value.models.iterator
if model.node_required
} yield node_name).toSet
def node_required(
name: Document.Node.Name, toggle: Boolean = false, set: Boolean = false): Unit =
{
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.plugin.options_changed()
PIDE.editor.flush()
}
}
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, purge: Boolean): (Document.Blobs, List[Document.Edit_Text]) =
{
GUI_Thread.require {}
state.change_result(st =>
{
val doc_blobs = st.document_blobs
val buffer_edits =
(for {
(_, model) <- st.buffer_models.iterator
edit <- model.flush_edits(doc_blobs, hidden).iterator
} yield edit).toList
val file_edits =
(for {
(node_name, model) <- st.file_models_iterator
(edits, model1) <- model.flush_edits(doc_blobs, hidden)
} yield (edits, node_name -> model1)).toList
val model_edits = buffer_edits ::: file_edits.flatMap(_._1)
val purge_edits =
if (purge) {
val purged =
(for ((node_name, model) <- st.file_models_iterator)
yield (node_name -> model.purge_edits(doc_blobs))).toList
val imports =
{
val open_nodes =
(for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
val touched_nodes = model_edits.map(_._1)
val pending_nodes = for ((node_name, None) <- purged) yield node_name
(open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
}
val retain = PIDE.resources.dependencies(imports).theories.toSet
for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
yield edit
}
else Nil
val st1 = st.copy(models = st.models ++ file_edits.map(_._2) -- purge_edits.map(_._1))
PIDE.plugin.file_watcher.purge(
(for {
(_, model) <- st1.file_models_iterator
file <- model.file
} yield file.getParentFile).toSet)
((doc_blobs, model_edits ::: purge_edits), st1)
})
}
/* 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.entries(text) }
catch { case ERROR(_) => Nil }
}
/* HTTP preview */
private val plain_text_prefix = "plain_text="
def open_preview(view: View, plain_text: Boolean): Unit =
{
Document_Model.get(view.getBuffer) match {
case Some(model) =>
val name = model.node_name
val url =
PIDE.plugin.http_server.url + PIDE.plugin.http_root + "/preview?" +
(if (plain_text) plain_text_prefix else "") + Url.encode(name.node)
PIDE.editor.hyperlink_url(url).follow(view)
case _ =>
}
}
def http_handlers(http_root: String): List[HTTP.Handler] =
{
val fonts_root = http_root + "/fonts"
val preview_root = http_root + "/preview"
val html =
HTTP.get(preview_root, arg =>
for {
query <- Library.try_unprefix(preview_root + "?", arg.uri.toString).map(Url.decode)
name = Library.perhaps_unprefix(plain_text_prefix, query)
model <- get(PIDE.resources.node_name(name))
}
yield {
val snapshot = model.await_stable_snapshot()
val html_context = Presentation.html_context(fonts_url = HTML.fonts_dir(fonts_root))
val document =
Presentation.html_document(
PIDE.resources, snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix))
HTTP.Response.html(document.content)
})
List(HTTP.fonts(fonts_root), html)
}
}
sealed abstract class Document_Model extends Document.Model
{
/* 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)
}
/* snapshot */
@tailrec final def await_stable_snapshot(): Document.Snapshot =
{
val snapshot = this.snapshot()
if (snapshot.is_outdated) {
PIDE.options.seconds("editor_output_delay").sleep
await_stable_snapshot()
}
else snapshot
}
}
object File_Model
{
def empty(session: Session): File_Model =
File_Model(session, Document.Node.Name.empty, None, Document_Model.File_Content(""),
false, Document.Node.no_perspective_text, Nil)
def init(session: Session,
node_name: Document.Node.Name,
text: String,
node_required: Boolean = false,
last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
pending_edits: List[Text.Edit] = Nil): File_Model =
{
val file = JEdit_Lib.check_file(node_name.node)
file.foreach(PIDE.plugin.file_watcher.register_parent(_))
val content = Document_Model.File_Content(text)
val node_required1 = node_required || File_Format.registry.is_theory(node_name)
File_Model(session, node_name, file, content, node_required1, last_perspective, pending_edits)
}
}
case class File_Model(
session: Session,
node_name: Document.Node.Name,
file: Option[JFile],
content: Document_Model.File_Content,
node_required: Boolean,
last_perspective: Document.Node.Perspective_Text,
pending_edits: List[Text.Edit]) extends Document_Model
{
/* text */
def get_text(range: Text.Range): Option[String] =
range.try_substring(content.text)
/* header */
def node_header: Document.Node.Header =
PIDE.resources.special_header(node_name) getOrElse
PIDE.resources.check_thy(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)))
def get_blob: Option[Document.Blob] =
if (is_theory) None
else Some(Document.Blob(content.bytes, content.text, content.chunk, pending_edits.nonEmpty))
def bibtex_entries: List[Text.Info[String]] =
if (Bibtex.is_bibtex(node_name.node)) 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(node_header, pending_edits, perspective)
Some((edits, copy(last_perspective = perspective, pending_edits = Nil)))
}
else None
}
def purge_edits(doc_blobs: Document.Blobs): Option[List[Document.Edit_Text]] =
if (pending_edits.nonEmpty ||
!File_Format.registry.is_theory(node_name) &&
(node_required || !Document.Node.is_no_perspective_text(last_perspective))) None
else {
val text_edits = List(Text.Edit.remove(0, content.text))
Some(node_edits(Document.Node.no_header, text_edits, Document.Node.no_perspective_text))
}
/* 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
{
/* text */
def get_text(range: Text.Range): Option[String] =
JEdit_Lib.get_text(buffer, range)
/* header */
def node_header(): Document.Node.Header =
{
GUI_Thread.require {}
PIDE.resources.special_header(node_name) getOrElse
JEdit_Lib.buffer_lock(buffer) {
PIDE.resources.check_thy(node_name, JEdit_Lib.buffer_reader(buffer), strict = false)
}
}
/* perspective */
// owned by GUI thread
private var _node_required = false
def node_required: Boolean = _node_required
def set_node_required(b: Boolean): Unit = GUI_Thread.require { _node_required = b }
def document_view_iterator: Iterator[Document_View] =
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
doc_view <- Document_View.get(text_area)
} yield doc_view
override def document_view_ranges(snapshot: Document.Snapshot): List[Text.Range] =
{
GUI_Thread.require {}
(for {
doc_view <- document_view_iterator
range <- doc_view.perspective(snapshot).ranges.iterator
} yield range).toList
}
/* blob */
// owned by GUI thread
private var _blob: Option[(Bytes, String, Symbol.Text_Chunk)] = None
private def reset_blob(): Unit = GUI_Thread.require { _blob = None }
def get_blob: Option[Document.Blob] =
GUI_Thread.require {
if (is_theory) None
else {
val (bytes, text, chunk) =
_blob match {
case Some(x) => x
case None =>
val bytes = PIDE.resources.make_file_content(buffer)
val text = buffer.getText(0, buffer.getLength)
val chunk = Symbol.Text_Chunk(text)
val x = (bytes, text, chunk)
_blob = Some(x)
x
}
val changed = pending_edits.nonEmpty
Some(Document.Blob(bytes, text, chunk, changed))
}
}
/* bibtex entries */
// owned by GUI thread
private var _bibtex_entries: Option[List[Text.Info[String]]] = None
private def reset_bibtex_entries(): Unit = GUI_Thread.require { _bibtex_entries = None }
def bibtex_entries: List[Text.Info[String]] =
GUI_Thread.require {
if (Bibtex.is_bibtex(node_name.node)) {
_bibtex_entries match {
case Some(entries) => entries
case None =>
val text = JEdit_Lib.buffer_text(buffer)
val entries =
try { Bibtex.entries(text) }
catch { case ERROR(msg) => Output.warning(msg); Nil }
_bibtex_entries = Some(entries)
entries
}
}
else Nil
}
/* pending edits */
private object pending_edits
{
private val pending = new mutable.ListBuffer[Text.Edit]
private var last_perspective = Document.Node.no_perspective_text
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 flush_edits(doc_blobs: Document.Blobs, hidden: Boolean): List[Document.Edit_Text] =
synchronized {
GUI_Thread.require {}
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(node_header(), edits, perspective)
}
else Nil
}
def edit(edits: List[Text.Edit]): Unit = synchronized
{
GUI_Thread.require {}
reset_blob()
reset_bibtex_entries()
for (doc_view <- document_view_iterator)
doc_view.rich_text_area.active_reset()
pending ++= edits
PIDE.editor.invoke()
}
}
def is_stable: Boolean = !pending_edits.nonEmpty
def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits.get_edits)
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 contentInserted(buffer: JEditBuffer,
start_line: Int, offset: Int, num_lines: Int, length: Int): Unit =
{
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): Unit =
{
pending_edits.edit(List(Text.Edit.remove(offset, buffer.getText(offset, removed_length))))
}
}
/* syntax */
def syntax_changed(): Unit =
{
JEdit_Lib.buffer_line_manager(buffer).setFirstInvalidLineContext(0)
for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
invoke(text_area)
buffer.invalidateCachedFoldLevels()
}
def init_token_marker(): Unit =
{
Isabelle.buffer_token_marker(buffer) match {
case Some(marker) if marker != buffer.getTokenMarker =>
buffer.setTokenMarker(marker)
syntax_changed()
case _ =>
}
}
/* init */
def init(old_model: Option[File_Model]): Buffer_Model =
{
GUI_Thread.require {}
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
}
/* exit */
def exit(): File_Model =
{
GUI_Thread.require {}
buffer.removeBufferListener(buffer_listener)
init_token_marker()
File_Model.init(session, node_name, JEdit_Lib.buffer_text(buffer), node_required,
pending_edits.get_last_perspective, pending_edits.get_edits)
}
}
diff --git a/src/Tools/jEdit/src/isabelle_sidekick.scala b/src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala
@@ -1,267 +1,267 @@
/* Title: Tools/jEdit/src/isabelle_sidekick.scala
Author: Fabian Immler, TU Munich
Author: Makarius
SideKick parsers for Isabelle proof documents.
*/
package isabelle.jedit
import isabelle._
import javax.swing.tree.DefaultMutableTreeNode
import javax.swing.text.Position
import javax.swing.{JLabel, Icon}
import org.gjt.sp.jedit.Buffer
import sidekick.{SideKickParser, SideKickParsedData, IAsset}
object Isabelle_Sidekick
{
def int_to_pos(offset: Text.Offset): Position =
new Position { def getOffset = offset; override def toString: String = offset.toString }
def root_data(buffer: Buffer): SideKickParsedData =
{
val data = new SideKickParsedData(buffer.getName)
data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
data
}
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
{
private val css = GUI.imitate_font_css(GUI.label_font())
protected var _name = text
protected var _start = int_to_pos(range.start)
protected var _end = int_to_pos(range.stop)
override def getIcon: Icon = null
override def getShortString: String =
{
val n = keyword.length
val s =
_name.indexOf(keyword) match {
case i if i >= 0 && n > 0 =>
HTML.output(_name.substring(0, i)) +
"" + HTML.output(keyword) + "" +
HTML.output(_name.substring(i + n))
case _ => HTML.output(_name)
}
"" + s + ""
}
override def getLongString: String = _name
override def getName: String = _name
override def setName(name: String): Unit = _name = name
override def getStart: Position = _start
override def setStart(start: Position): Unit = _start = start
override def getEnd: Position = _end
override def setEnd(end: Position): Unit = _end = end
override def toString: String = _name
}
class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
{
for ((_, entry) <- tree.branches) {
val node = swing_node(Text.Info(entry.range, entry.markup))
swing_markup_tree(entry.subtree, node, swing_node)
parent.add(node)
}
}
}
class Isabelle_Sidekick(name: String) extends SideKickParser(name)
{
override def supportsCompletion = false
/* parsing */
@volatile protected var stopped = false
override def stop() = { stopped = true }
def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
{
stopped = false
// FIXME lock buffer (!??)
val data = Isabelle_Sidekick.root_data(buffer)
val syntax = Isabelle.buffer_syntax(buffer)
val ok =
if (syntax.isDefined) {
val ok = parser(buffer, syntax.get, data)
if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true }
else ok
}
else false
if (!ok) data.root.add(new DefaultMutableTreeNode(""))
data
}
}
class Isabelle_Sidekick_Structure(
name: String,
node_name: Buffer => Option[Document.Node.Name],
parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
extends Isabelle_Sidekick(name)
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
def make_tree(
parent: DefaultMutableTreeNode,
offset: Text.Offset,
documents: List[Document_Structure.Document]): Unit =
{
- (offset /: documents) { case (i, document) =>
+ documents.foldLeft(offset) { case (i, document) =>
document match {
case Document_Structure.Block(name, text, body) =>
val range = Text.Range(i, i + document.length)
val node =
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
parent.add(node)
make_tree(node, i, body)
case _ =>
}
i + document.length
}
}
node_name(buffer) match {
case Some(name) =>
make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
true
case None =>
false
}
}
}
class Isabelle_Sidekick_Default extends
Isabelle_Sidekick_Structure("isabelle",
PIDE.resources.theory_node_name, Document_Structure.parse_sections)
class Isabelle_Sidekick_Context extends
Isabelle_Sidekick_Structure("isabelle-context",
PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
class Isabelle_Sidekick_Options extends
Isabelle_Sidekick_Structure("isabelle-options",
_ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
class Isabelle_Sidekick_Root extends
Isabelle_Sidekick_Structure("isabelle-root",
_ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
class Isabelle_Sidekick_ML extends
Isabelle_Sidekick_Structure("isabelle-ml",
buffer => Some(PIDE.resources.node_name(buffer)),
(_, _, text) => Document_Structure.parse_ml_sections(false, text))
class Isabelle_Sidekick_SML extends
Isabelle_Sidekick_Structure("isabelle-sml",
buffer => Some(PIDE.resources.node_name(buffer)),
(_, _, text) => Document_Structure.parse_ml_sections(true, text))
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
val opt_snapshot =
Document_Model.get(buffer) match {
case Some(model) if model.is_theory => Some(model.snapshot)
case _ => None
}
opt_snapshot match {
case Some(snapshot) =>
for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
val markup =
snapshot.state.command_markup(
snapshot.version, command, Command.Markup_Index.markup,
command.range, Markup.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, data.root,
(info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Asset(command.toString, range) {
override def getShortString: String = content
override def getLongString: String = info_text
override def toString: String = quote(content) + " " + range.toString
})
})
}
true
case None => false
}
}
}
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
{
private val Heading1 = """^New in (.*)\w*$""".r
private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
var offset = 0
var end_offset = 0
var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
var start2: Option[(Int, String)] = None
def close1: Unit =
start1 match {
case Some((start_offset, s, body)) =>
val node = make_node(s, start_offset, end_offset)
body.foreach(node.add(_))
data.root.add(node)
start1 = None
case None =>
}
def close2: Unit =
start2 match {
case Some((start_offset, s)) =>
start1 match {
case Some((start_offset1, s1, body)) =>
val node = make_node(s, start_offset, end_offset)
start1 = Some((start_offset1, s1, body :+ node))
case None =>
}
start2 = None
case None =>
}
for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
line match {
case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
case Heading2(s) => close2; start2 = Some((offset, s))
case _ =>
}
offset += line.length + 1
if (!line.forall(Character.isSpaceChar)) end_offset = offset
}
if (!stopped) { close2; close1 }
true
}
}
diff --git a/src/Tools/jEdit/src/jedit_editor.scala b/src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala
+++ b/src/Tools/jEdit/src/jedit_editor.scala
@@ -1,323 +1,322 @@
/* Title: Tools/jEdit/src/jedit_editor.scala
Author: Makarius
PIDE editor operations for jEdit.
*/
package isabelle.jedit
import isabelle._
import java.io.{File => JFile}
import org.gjt.sp.jedit.{jEdit, View, Buffer}
import org.gjt.sp.jedit.browser.VFSBrowser
import org.gjt.sp.jedit.io.{VFSManager, VFSFile}
class JEdit_Editor extends Editor[View]
{
/* session */
override def session: Session = PIDE.session
def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit =
GUI_Thread.require {
val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge)
session.update(doc_blobs, edits)
}
override def flush(): Unit = flush_edits()
def purge(): Unit = flush_edits(purge = true)
private val delay1_flush =
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() }
private val delay2_flush =
Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() }
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
def shutdown(): Unit =
GUI_Thread.require {
delay1_flush.revoke()
delay2_flush.revoke()
Document_Model.flush_edits(hidden = false, purge = false)
}
def visible_node(name: Document.Node.Name): Boolean =
(for {
text_area <- JEdit_Lib.jedit_text_areas()
doc_view <- Document_View.get(text_area)
} yield doc_view.model.node_name).contains(name)
/* current situation */
override def current_node(view: View): Option[Document.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 { Document_Model.get(view.getBuffer).map(_.snapshot()) }
override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
{
GUI_Thread.require {}
Document_Model.get(name) match {
case Some(model) => model.snapshot
case None => session.snapshot(name)
}
}
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] =
{
GUI_Thread.require {}
val text_area = view.getTextArea
val buffer = view.getBuffer
Document_View.get(text_area) match {
case Some(doc_view) if doc_view.model.is_theory =>
snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
case _ =>
Document_Model.get(buffer) match {
case Some(model) if !model.is_theory =>
snapshot.version.nodes.commands_loading(model.node_name).headOption
case _ => None
}
}
}
/* overlays */
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
Document_Model.node_overlays(name)
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
Document_Model.insert_overlay(command, fn, args)
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
Document_Model.remove_overlay(command, fn, args)
/* navigation */
def push_position(view: View): Unit =
{
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
if (navigator != null) {
try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
catch { case _: NoSuchMethodException => }
}
}
def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset): Unit =
{
GUI_Thread.require {}
push_position(view)
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
try { view.getTextArea.moveCaretPosition(offset) }
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
}
def goto_file(focus: Boolean, view: View, name: String): Unit =
goto_file(focus, view, Line.Node_Position.offside(name))
def goto_file(focus: Boolean, view: View, pos: Line.Node_Position): Unit =
{
GUI_Thread.require {}
push_position(view)
val name = pos.name
val line = pos.line
val column = pos.column
JEdit_Lib.jedit_buffer(name) match {
case Some(buffer) =>
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer)
val text_area = view.getTextArea
try {
val line_start = text_area.getBuffer.getLineStartOffset(line)
text_area.moveCaretPosition(line_start)
if (column > 0) text_area.moveCaretPosition(line_start + column)
}
catch {
case _: ArrayIndexOutOfBoundsException =>
case _: IllegalArgumentException =>
}
case None =>
val is_dir =
try {
val vfs = VFSManager.getVFSForPath(name)
val vfs_file = vfs._getFile((), name, view)
vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY
}
catch { case ERROR(_) => false }
if (is_dir) VFSBrowser.browseDirectory(view, name)
else if (!Isabelle_System.open_external_file(name)) {
val args =
if (line <= 0) Array(name)
else if (column <= 0) Array(name, "+line:" + (line + 1))
else Array(name, "+line:" + (line + 1) + "," + (column + 1))
jEdit.openFiles(view, null, args)
}
}
}
def goto_doc(view: View, path: Path): Unit =
{
if (path.is_file)
goto_file(true, view, File.platform_path(path))
else {
Isabelle_Thread.fork(name = "documentation") {
try { Doc.view(path) }
catch {
case exn: Throwable =>
GUI_Thread.later {
GUI.error_dialog(view,
"Documentation error", GUI.scrollable_text(Exn.message(exn)))
}
}
}
}
}
/* hyperlinks */
def hyperlink_doc(name: String): Option[Hyperlink] =
Doc.contents().collectFirst({
case doc: Doc.Text_File if doc.name == name => doc.path
case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
new Hyperlink {
override val external: Boolean = !path.is_file
def follow(view: View): Unit = goto_doc(view, path)
override def toString: String = "doc " + quote(name)
})
def hyperlink_url(name: String): Hyperlink =
new Hyperlink {
override val external = true
def follow(view: View): Unit =
Isabelle_Thread.fork(name = "hyperlink_url") {
try { Isabelle_System.open(Url.escape_name(name)) }
catch {
case exn: Throwable =>
GUI_Thread.later {
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn)))
}
}
}
override def toString: String = "URL " + quote(name)
}
def hyperlink_file(focus: Boolean, name: String): Hyperlink =
hyperlink_file(focus, Line.Node_Position.offside(name))
def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink =
new Hyperlink {
def follow(view: View): Unit = goto_file(focus, view, pos)
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 {
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(text).
- zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_)))
+ Symbol.iterator(text).zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1).
+ foldLeft(Line.Position.zero)(_.advance(_)))
case None =>
hyperlink(Line.Position((line1 - 1) max 0))
}
}
else hyperlink(Line.Position((line1 - 1) max 0))
}
}
override def hyperlink_command(
focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
: Option[Hyperlink] =
{
if (snapshot.is_outdated) None
else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _))
}
def is_hyperlink_position(snapshot: Document.Snapshot,
text_offset: Text.Offset, pos: Position.T): Boolean =
{
pos match {
case Position.Item_Id(id, range) if range.start > 0 =>
snapshot.find_command(id) match {
case Some((node, command)) if snapshot.get_node(command.node_name) eq node =>
node.command_start(command) match {
case Some(start) => text_offset == start + command.chunk.decode(range.start)
case None => false
}
case _ => false
}
case _ => false
}
}
def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
: Option[Hyperlink] =
pos match {
case Position.Item_File(name, line, range) =>
hyperlink_source_file(focus, name, line, range.start)
case Position.Item_Id(id, range) =>
hyperlink_command(focus, snapshot, id, range.start)
case _ => None
}
def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T)
: Option[Hyperlink] =
pos match {
case Position.Item_Def_File(name, line, range) =>
hyperlink_source_file(focus, name, line, range.start)
case Position.Item_Def_Id(id, range) =>
hyperlink_command(focus, snapshot, id, range.start)
case _ => None
}
/* dispatcher thread */
override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body)
override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body)
override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body)
override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body)
}
diff --git a/src/Tools/jEdit/src/jedit_rendering.scala b/src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala
+++ b/src/Tools/jEdit/src/jedit_rendering.scala
@@ -1,428 +1,428 @@
/* Title: Tools/jEdit/src/jedit_rendering.scala
Author: Makarius
Isabelle/jEdit-specific implementation of quasi-abstract rendering and
markup interpretation.
*/
package isabelle.jedit
import isabelle._
import java.awt.Color
import javax.swing.Icon
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
import org.gjt.sp.jedit.jEdit
import scala.collection.immutable.SortedMap
object JEdit_Rendering
{
/* make rendering */
def apply(snapshot: Document.Snapshot, model: Document_Model, options: Options): JEdit_Rendering =
new JEdit_Rendering(snapshot, model, options)
def text(snapshot: Document.Snapshot, formatted_body: XML.Body,
results: Command.Results = Command.Results.empty): (String, JEdit_Rendering) =
{
val command = Command.rich_text(Document_ID.make(), results, formatted_body)
val snippet = snapshot.snippet(command)
val model = File_Model.empty(PIDE.session)
val rendering = apply(snippet, model, PIDE.options.value)
(command.source, rendering)
}
/* popup window bounds */
def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8
/* Isabelle/Isar token markup */
private val command_style: Map[String, Byte] =
{
import JEditToken._
Map[String, Byte](
Keyword.THY_END -> KEYWORD2,
Keyword.PRF_ASM -> KEYWORD3,
Keyword.PRF_ASM_GOAL -> KEYWORD3
).withDefaultValue(KEYWORD1)
}
private val token_style: Map[Token.Kind.Value, Byte] =
{
import JEditToken._
Map[Token.Kind.Value, Byte](
Token.Kind.KEYWORD -> KEYWORD2,
Token.Kind.IDENT -> NULL,
Token.Kind.LONG_IDENT -> NULL,
Token.Kind.SYM_IDENT -> NULL,
Token.Kind.VAR -> NULL,
Token.Kind.TYPE_IDENT -> NULL,
Token.Kind.TYPE_VAR -> NULL,
Token.Kind.NAT -> NULL,
Token.Kind.FLOAT -> NULL,
Token.Kind.SPACE -> NULL,
Token.Kind.STRING -> LITERAL1,
Token.Kind.ALT_STRING -> LITERAL2,
Token.Kind.VERBATIM -> COMMENT3,
Token.Kind.CARTOUCHE -> COMMENT3,
Token.Kind.INFORMAL_COMMENT -> COMMENT1,
Token.Kind.FORMAL_COMMENT -> COMMENT1,
Token.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
}
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
else if (token.is_delimiter) JEditToken.OPERATOR
else token_style(token.kind)
/* Isabelle/ML token markup */
private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] =
{
import JEditToken._
Map[ML_Lex.Kind.Value, Byte](
ML_Lex.Kind.KEYWORD -> NULL,
ML_Lex.Kind.IDENT -> NULL,
ML_Lex.Kind.LONG_IDENT -> NULL,
ML_Lex.Kind.TYPE_VAR -> NULL,
ML_Lex.Kind.WORD -> DIGIT,
ML_Lex.Kind.INT -> DIGIT,
ML_Lex.Kind.REAL -> DIGIT,
ML_Lex.Kind.CHAR -> LITERAL2,
ML_Lex.Kind.STRING -> LITERAL1,
ML_Lex.Kind.SPACE -> NULL,
ML_Lex.Kind.INFORMAL_COMMENT -> COMMENT1,
ML_Lex.Kind.FORMAL_COMMENT -> COMMENT1,
ML_Lex.Kind.ANTIQ -> NULL,
ML_Lex.Kind.ANTIQ_START -> LITERAL4,
ML_Lex.Kind.ANTIQ_STOP -> LITERAL4,
ML_Lex.Kind.ANTIQ_OTHER -> NULL,
ML_Lex.Kind.ANTIQ_STRING -> NULL,
ML_Lex.Kind.ANTIQ_ALT_STRING -> NULL,
ML_Lex.Kind.ANTIQ_CARTOUCHE -> NULL,
ML_Lex.Kind.ERROR -> INVALID
).withDefaultValue(NULL)
}
def ml_token_markup(token: ML_Lex.Token): Byte =
if (!token.is_keyword) ml_token_style(token.kind)
else if (token.is_delimiter) JEditToken.OPERATOR
else if (ML_Lex.keywords2(token.source)) JEditToken.KEYWORD2
else if (ML_Lex.keywords3(token.source)) JEditToken.KEYWORD3
else JEditToken.KEYWORD1
/* markup elements */
private val indentation_elements =
Markup.Elements(Markup.Command_Indent.name)
private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
private val highlight_elements =
Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.DOC, Markup.URL,
Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.FREE, Markup.SKOLEM,
Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name)
private val hyperlink_elements =
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.EXPORT_PATH, Markup.DOC, Markup.URL,
Markup.POSITION, Markup.CITATION)
private val gutter_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
private val squiggly_elements =
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR)
private val line_background_elements =
Markup.Elements(Markup.WRITELN_MESSAGE, Markup.STATE_MESSAGE, Markup.INFORMATION_MESSAGE,
Markup.TRACING_MESSAGE, Markup.WARNING_MESSAGE, Markup.LEGACY_MESSAGE,
Markup.ERROR_MESSAGE)
private val separator_elements =
Markup.Elements(Markup.SEPARATOR)
private val bullet_elements =
Markup.Elements(Markup.BULLET, Markup.ML_BREAKPOINT)
private val fold_depth_elements =
Markup.Elements(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
}
class JEdit_Rendering(snapshot: Document.Snapshot, model: Document_Model, options: Options)
extends Rendering(snapshot, options, PIDE.session)
{
override def get_text(range: Text.Range): Option[String] = model.get_text(range)
/* colors */
def color(s: String): Color =
if (s == "main_color") main_color
else Color_Value(options.string(s))
def color(c: Rendering.Color.Value): Color = _rendering_colors(c)
lazy val _rendering_colors: Map[Rendering.Color.Value, Color] =
Rendering.Color.values.iterator.map(c => c -> color(c.toString + "_color")).toMap
val main_color = jEdit.getColorProperty("view.fgColor")
val outdated_color = color("outdated_color")
val bullet_color = color("bullet_color")
val tooltip_color = color("tooltip_color")
val spell_checker_color = color("spell_checker_color")
val entity_ref_color = color("entity_ref_color")
val breakpoint_disabled_color = color("breakpoint_disabled_color")
val breakpoint_enabled_color = color("breakpoint_enabled_color")
val caret_debugger_color = color("caret_debugger_color")
val highlight_color = color("highlight_color")
val hyperlink_color = color("hyperlink_color")
val active_hover_color = color("active_hover_color")
val caret_invisible_color = color("caret_invisible_color")
val completion_color = color("completion_color")
val search_color = color("search_color")
/* indentation */
def indentation(range: Text.Range): Int =
snapshot.select(range, JEdit_Rendering.indentation_elements, _ =>
{
case Text.Info(_, XML.Elem(Markup.Command_Indent(i), _)) => Some(i)
case _ => None
}).headOption.map(_.info).getOrElse(0)
/* breakpoints */
def breakpoint(range: Text.Range): Option[(Command, Long)] =
if (snapshot.is_outdated) None
else
snapshot.select(range, JEdit_Rendering.breakpoint_elements, command_states =>
{
case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
command_states match {
case st :: _ => Some((st.command, breakpoint))
case _ => None
}
case _ => None
}).headOption.map(_.info)
/* caret focus */
def entity_ref(range: Text.Range, focus: Rendering.Focus): List[Text.Info[Color]] =
snapshot.select(range, Rendering.entity_elements, _ =>
{
case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Ref(i)), _))
if focus(i) => Some(entity_ref_color)
case _ => None
})
/* highlighted area */
def highlight(range: Text.Range): Option[Text.Info[Color]] =
snapshot.select(range, JEdit_Rendering.highlight_elements, _ =>
{
case info => Some(Text.Info(snapshot.convert(info.range), highlight_color))
}).headOption.map(_.info)
/* hyperlinks */
def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
val file = perhaps_append_file(snapshot.node_name, name)
val link = PIDE.editor.hyperlink_file(true, file)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Export_Path(name), _))) =>
val link = PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Doc(name), _))) =>
PIDE.editor.hyperlink_doc(name).map(link =>
(links :+ Text.Info(snapshot.convert(info_range), link)))
case (links, Text.Info(info_range, XML.Elem(Markup.Url(name), _))) =>
val link = PIDE.editor.hyperlink_url(name)
Some(links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) =>
val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props)
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
case (links, Text.Info(info_range, XML.Elem(Markup.Citation(name), _))) =>
val opt_link =
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
}) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
}
def hyperlink_entity(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
range, Vector.empty, Rendering.entity_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>
val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props)
opt_link.map(link => links :+ Text.Info(snapshot.convert(info_range), link))
case _ => None
}) match { case Text.Info(_, _ :+ info) :: _ => Some(info) case _ => None }
}
/* active elements */
def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
snapshot.select(range, Rendering.active_elements, command_states =>
{
case Text.Info(info_range, elem) =>
if (elem.name == Markup.DIALOG) {
elem match {
case Protocol.Dialog(_, serial, _)
if !command_states.exists(st => st.results.defined(serial)) =>
Some(Text.Info(snapshot.convert(info_range), elem))
case _ => None
}
}
else Some(Text.Info(snapshot.convert(info_range), elem))
}).headOption.map(_.info)
/* tooltips */
def tooltip_margin: Int = options.int("jedit_tooltip_margin")
override def timing_threshold: Double = options.real("jedit_timing_threshold")
def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[XML.Body]] =
{
val elements = if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements
tooltips(elements, range).map(info => info.map(Pretty.fbreaks))
}
lazy val tooltip_close_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_close_icon"))
lazy val tooltip_detach_icon: Icon = JEdit_Lib.load_icon(options.string("tooltip_detach_icon"))
/* gutter */
private def gutter_message_pri(msg: XML.Tree): Int =
if (Protocol.is_error(msg)) Rendering.error_pri
else if (Protocol.is_legacy(msg)) Rendering.legacy_pri
else if (Protocol.is_warning(msg)) Rendering.warning_pri
else if (Protocol.is_information(msg)) Rendering.information_pri
else 0
private lazy val gutter_message_content = Map(
Rendering.information_pri ->
(JEdit_Lib.load_icon(options.string("gutter_information_icon")),
color(Rendering.Color.information_message)),
Rendering.warning_pri ->
(JEdit_Lib.load_icon(options.string("gutter_warning_icon")),
color(Rendering.Color.warning_message)),
Rendering.legacy_pri ->
(JEdit_Lib.load_icon(options.string("gutter_legacy_icon")),
color(Rendering.Color.legacy_message)),
Rendering.error_pri ->
(JEdit_Lib.load_icon(options.string("gutter_error_icon")),
color(Rendering.Color.error_message)))
def gutter_content(range: Text.Range): Option[(Icon, Color)] =
{
val pris =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.gutter_elements, _ =>
{
case (pri, Text.Info(_, elem)) => Some(pri max gutter_message_pri(elem))
case _ => None
}).map(_.info)
- gutter_message_content.get((0 /: pris)(_ max _))
+ gutter_message_content.get(pris.foldLeft(0)(_ max _))
}
/* message output */
def squiggly_underline(range: Text.Range): List[Text.Info[Rendering.Color.Value]] =
message_underline_color(JEdit_Rendering.squiggly_elements, range)
def line_background(range: Text.Range): Option[(Rendering.Color.Value, Boolean)] =
{
val results =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.line_background_elements, _ =>
{
case (pri, Text.Info(_, elem)) => Some(pri max Rendering.message_pri(elem.name))
})
- val pri = (0 /: results) { case (p1, Text.Info(_, p2)) => p1 max p2 }
+ val pri = results.foldLeft(0) { case (p1, Text.Info(_, p2)) => p1 max p2 }
Rendering.message_background_color.get(pri).map(message_color =>
{
val is_separator =
snapshot.cumulate[Boolean](range, false, JEdit_Rendering.separator_elements, _ =>
{
case _ => Some(true)
}).exists(_.info)
(message_color, is_separator)
})
}
/* text color */
def text_color(range: Text.Range, current_color: Color): List[Text.Info[Color]] =
{
if (current_color == Syntax_Style.hidden_color) List(Text.Info(range, current_color))
else
snapshot.cumulate(range, current_color, Rendering.text_color_elements, _ =>
{
case (_, Text.Info(_, elem)) => Rendering.text_color.get(elem.name).map(color)
})
}
/* virtual bullets */
def bullet(range: Text.Range): List[Text.Info[Color]] =
snapshot.select(range, JEdit_Rendering.bullet_elements, _ =>
{
case Text.Info(_, Protocol.ML_Breakpoint(breakpoint)) =>
PIDE.session.debugger.active_breakpoint_state(breakpoint).map(b =>
if (b) breakpoint_enabled_color else breakpoint_disabled_color)
case _ => Some(bullet_color)
})
/* text folds */
def fold_depth(range: Text.Range): List[Text.Info[Int]] =
snapshot.cumulate[Int](range, 0, JEdit_Rendering.fold_depth_elements, _ =>
{
case (depth, _) => Some(depth + 1)
})
}
diff --git a/src/Tools/jEdit/src/pretty_tooltip.scala b/src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala
@@ -1,290 +1,291 @@
/* Title: Tools/jEdit/src/pretty_tooltip.scala
Author: Makarius
Tooltip based on Pretty_Text_Area.
*/
package isabelle.jedit
import isabelle._
import java.awt.{Color, Point, BorderLayout, Dimension}
import java.awt.event.{FocusAdapter, FocusEvent}
import javax.swing.{JPanel, JComponent, SwingUtilities, JLayeredPane}
import javax.swing.border.LineBorder
import scala.swing.{FlowPanel, Label}
import scala.swing.event.MouseClicked
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.textarea.TextArea
object Pretty_Tooltip
{
/* tooltip hierarchy */
// owned by GUI thread
private var stack: List[Pretty_Tooltip] = Nil
private def hierarchy(tip: Pretty_Tooltip): Option[(List[Pretty_Tooltip], List[Pretty_Tooltip])] =
{
GUI_Thread.require {}
if (stack.contains(tip)) Some(stack.span(_ != tip))
else None
}
private def descendant(parent: JComponent): Option[Pretty_Tooltip] =
GUI_Thread.require { stack.find(tip => tip.original_parent == parent) }
def apply(
view: View,
parent: JComponent,
location: Point,
rendering: JEdit_Rendering,
results: Command.Results,
info: Text.Info[XML.Body]): Unit =
{
GUI_Thread.require {}
stack match {
case top :: _ if top.results == results && top.info == info =>
case _ =>
GUI.layered_pane(parent) match {
case None =>
case Some(layered) =>
val (old, rest) =
GUI.ancestors(parent).collectFirst({ case x: Pretty_Tooltip => x }) match {
case Some(tip) => hierarchy(tip).getOrElse((stack, Nil))
case None => (stack, Nil)
}
old.foreach(_.hide_popup)
val loc = SwingUtilities.convertPoint(parent, location, layered)
val tip = new Pretty_Tooltip(view, layered, parent, loc, rendering, results, info)
stack = tip :: rest
tip.show_popup
}
}
}
/* pending event and active state */ // owned by GUI thread
private var pending: Option[() => Unit] = None
private var active = true
private val pending_delay =
Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
pending match {
case Some(body) => pending = None; body()
case None =>
}
}
def invoke(body: () => Unit): Unit =
GUI_Thread.require {
if (active) {
pending = Some(body)
pending_delay.invoke()
}
}
def revoke(): Unit =
GUI_Thread.require {
pending = None
pending_delay.revoke()
}
private lazy val reactivate_delay =
Delay.last(PIDE.options.seconds("jedit_tooltip_delay"), gui = true) {
active = true
}
private def deactivate(): Unit =
GUI_Thread.require {
revoke()
active = false
reactivate_delay.invoke()
}
/* dismiss */
private lazy val focus_delay = Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true)
{
dismiss_unfocused()
}
def dismiss_unfocused(): Unit =
{
stack.span(tip => !tip.pretty_text_area.isFocusOwner) match {
case (Nil, _) =>
case (unfocused, rest) =>
deactivate()
unfocused.foreach(_.hide_popup)
stack = rest
}
}
def dismiss(tip: Pretty_Tooltip): Unit =
{
deactivate()
hierarchy(tip) match {
case Some((old, _ :: rest)) =>
rest match {
case top :: _ => top.request_focus
case Nil => JEdit_Lib.request_focus_view()
}
old.foreach(_.hide_popup)
tip.hide_popup
stack = rest
case _ =>
}
}
def dismiss_descendant(parent: JComponent): Unit =
descendant(parent).foreach(dismiss)
def dismissed_all(): Boolean =
{
deactivate()
if (stack.isEmpty) false
else {
JEdit_Lib.request_focus_view()
stack.foreach(_.hide_popup)
stack = Nil
true
}
}
}
class Pretty_Tooltip private(
view: View,
layered: JLayeredPane,
val original_parent: JComponent,
location: Point,
rendering: JEdit_Rendering,
private val results: Command.Results,
private val info: Text.Info[XML.Body]) extends JPanel(new BorderLayout)
{
tip =>
GUI_Thread.require {}
/* controls */
private val close = new Label {
icon = rendering.tooltip_close_icon
tooltip = "Close tooltip window"
listenTo(mouse.clicks)
reactions += { case _: MouseClicked => Pretty_Tooltip.dismiss(tip) }
}
private val detach = new Label {
icon = rendering.tooltip_detach_icon
tooltip = "Detach tooltip window"
listenTo(mouse.clicks)
reactions += {
case _: MouseClicked =>
Info_Dockable(view, rendering.snapshot, results, info.info)
Pretty_Tooltip.dismiss(tip)
}
}
private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach) {
background = rendering.tooltip_color
}
/* text area */
val pretty_text_area: Pretty_Text_Area =
new Pretty_Text_Area(view, () => Pretty_Tooltip.dismiss(tip), true) {
override def get_background() = Some(rendering.tooltip_color)
}
pretty_text_area.addFocusListener(new FocusAdapter {
override def focusGained(e: FocusEvent): Unit =
{
tip_border(true)
Pretty_Tooltip.focus_delay.invoke()
}
override def focusLost(e: FocusEvent): Unit =
{
tip_border(false)
Pretty_Tooltip.focus_delay.invoke()
}
})
pretty_text_area.resize(Font_Info.main(PIDE.options.real("jedit_popup_font_scale")))
/* main content */
def tip_border(has_focus: Boolean): Unit =
{
tip.setBorder(new LineBorder(if (has_focus) Color.BLACK else Color.GRAY))
tip.repaint()
}
tip_border(true)
override def getFocusTraversalKeysEnabled = false
tip.setBackground(rendering.tooltip_color)
tip.add(controls.peer, BorderLayout.NORTH)
tip.add(pretty_text_area)
/* popup */
private val popup =
{
val screen = GUI.screen_location(layered, location)
val size =
{
val bounds = JEdit_Rendering.popup_bounds
val w_max = layered.getWidth min (screen.bounds.width * bounds).toInt
val h_max = layered.getHeight min (screen.bounds.height * bounds).toInt
val painter = pretty_text_area.getPainter
val geometry = JEdit_Lib.window_geometry(tip, painter)
val metric = JEdit_Lib.pretty_metric(painter)
val margin =
((rendering.tooltip_margin * metric.average) min
((w_max - geometry.deco_width) / metric.unit).toInt) max 20
val formatted = Pretty.formatted(info.info, margin = margin, metric = metric)
val lines =
XML.traverse_text(formatted)(if (XML.text_length(formatted) == 0) 0 else 1)(
(n: Int, s: String) => n + s.iterator.count(_ == '\n'))
val h = painter.getLineHeight * lines + geometry.deco_height
val margin1 =
- if (h <= h_max)
- (0.0 /: split_lines(XML.content(formatted)))({ case (m, line) => m max metric(line) })
+ if (h <= h_max) {
+ split_lines(XML.content(formatted)).foldLeft(0.0)({ case (m, line) => m max metric(line) })
+ }
else margin
val w = (metric.unit * (margin1 + metric.average)).round.toInt + geometry.deco_width
new Dimension(w min w_max, h min h_max)
}
new Popup(layered, tip, screen.relative(layered, size), size)
}
private def show_popup: Unit =
{
popup.show
pretty_text_area.requestFocus
pretty_text_area.update(rendering.snapshot, results, info.info)
}
private def hide_popup: Unit = popup.hide
private def request_focus: Unit = pretty_text_area.requestFocus
}
diff --git a/src/Tools/jEdit/src/text_structure.scala b/src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala
+++ b/src/Tools/jEdit/src/text_structure.scala
@@ -1,354 +1,354 @@
/* Title: Tools/jEdit/src/text_structure.scala
Author: Makarius
Text structure based on Isabelle/Isar outer syntax.
*/
package isabelle.jedit
import isabelle._
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
import org.gjt.sp.jedit.buffer.JEditBuffer
import org.gjt.sp.jedit.Buffer
object Text_Structure
{
/* token navigator */
class Navigator(syntax: Outer_Syntax, buffer: JEditBuffer, comments: Boolean)
{
val limit: Int = PIDE.options.value.int("jedit_structure_limit") max 0
def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
{
val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
}
def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
{
val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
}
}
/* indentation */
object Indent_Rule extends IndentRule
{
private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
private val keyword_close = Keyword.proof_close
def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
actions: java.util.List[IndentAction]): Unit =
{
Isabelle.buffer_syntax(buffer) match {
case Some(syntax) =>
val keywords = syntax.keywords
val nav = new Navigator(syntax, buffer, true)
val indent_size = buffer.getIndentSize
def line_indent(line: Int): Int =
if (line < 0 || line >= buffer.getLineCount) 0
else buffer.getCurrentIndentForLine(line, null)
def line_head(line: Int): Option[Text.Info[Token]] =
nav.iterator(line, 1).nextOption()
def head_is_quasi_command(line: Int): Boolean =
line_head(line) match {
case None => false
case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
}
val prev_line: Int =
Range.inclusive(current_line - 1, 0, -1).find(line =>
Token_Markup.Line_Context.before(buffer, line).get_context == Scan.Finished &&
(!Token_Markup.Line_Context.after(buffer, line).structure.improper ||
Token_Markup.Line_Context.after(buffer, line).structure.blank)) getOrElse -1
def prev_line_command: Option[Token] =
nav.reverse_iterator(prev_line, 1).
collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
def prev_line_span: Iterator[Token] =
nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
def prev_span: Iterator[Token] =
nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
val script_indent: Text.Info[Token] => Int =
{
val opt_rendering: Option[JEdit_Rendering] =
if (PIDE.options.value.bool("jedit_indent_script"))
GUI_Thread.now {
(for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
doc_view <- Document_View.get(text_area)
} yield doc_view.get_rendering).nextOption()
}
else None
val limit = PIDE.options.value.int("jedit_indent_script_limit")
(info: Text.Info[Token]) =>
opt_rendering match {
case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) =>
(rendering.indentation(info.range) min limit) max 0
case _ => 0
}
}
def indent_indent(tok: Token): Int =
if (keywords.is_command(tok, keyword_open)) indent_size
else if (keywords.is_command(tok, keyword_close)) - indent_size
else 0
def indent_offset(tok: Token): Int =
if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
else 0
def indent_structure: Int =
nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
{ case ((ind, _), Text.Info(range, tok)) =>
val ind1 = ind + indent_indent(tok)
if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) {
val line = buffer.getLineOfOffset(range.start)
line_head(line) match {
case Some(info) if info.info == tok =>
(ind1 + indent_offset(tok) + line_indent(line), true)
case _ => (ind1, false)
}
}
else (ind1, false)
}).collectFirst({ case (i, true) => i }).getOrElse(0)
def indent_brackets: Int =
- (0 /: prev_line_span)(
+ prev_line_span.foldLeft(0)(
{ case (i, tok) =>
if (tok.is_open_bracket) i + indent_size
else if (tok.is_close_bracket) i - indent_size
else i })
def indent_extra: Int =
if (prev_span.exists(keywords.is_quasi_command)) indent_size
else 0
val indent =
if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished)
line_indent(current_line)
else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
else {
line_head(current_line) match {
case Some(info) =>
val tok = info.info
if (tok.is_begin ||
keywords.is_before_command(tok) ||
keywords.is_command(tok, Keyword.theory)) 0
else if (keywords.is_command(tok, Keyword.proof_enclose))
indent_structure + script_indent(info) - indent_offset(tok)
else if (keywords.is_command(tok, Keyword.proof))
(indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
else if (tok.is_command) indent_structure - indent_offset(tok)
else {
prev_line_command match {
case None =>
val extra =
(keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
case (true, true) | (false, false) => 0
case (true, false) => - indent_extra
case (false, true) => indent_extra
}
line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
case Some(prev_tok) =>
indent_structure + indent_brackets + indent_size - indent_offset(tok) -
indent_offset(prev_tok) - indent_indent(prev_tok)
}
}
case None =>
prev_line_command match {
case None =>
val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
line_indent(prev_line) + indent_brackets + extra
case Some(prev_tok) =>
indent_structure + indent_brackets + indent_size -
indent_offset(prev_tok) - indent_indent(prev_tok)
}
}
}
actions.clear()
actions.add(new IndentAction.AlignOffset(indent max 0))
case None =>
}
}
}
def line_content(buffer: JEditBuffer, keywords: Keyword.Keywords,
range: Text.Range, ctxt: Scan.Line_Context): (List[Token], Scan.Line_Context) =
{
val text = JEdit_Lib.get_text(buffer, range).getOrElse("")
val (toks, ctxt1) = Token.explode_line(keywords, text, ctxt)
val toks1 = toks.filterNot(_.is_space)
(toks1, ctxt1)
}
def split_line_content(buffer: JEditBuffer, keywords: Keyword.Keywords, line: Int, caret: Int)
: (List[Token], List[Token]) =
{
val line_range = JEdit_Lib.line_range(buffer, line)
val ctxt0 = Token_Markup.Line_Context.before(buffer, line).get_context
val (toks1, ctxt1) = line_content(buffer, keywords, Text.Range(line_range.start, caret), ctxt0)
val (toks2, _) = line_content(buffer, keywords, Text.Range(caret, line_range.stop), ctxt1)
(toks1, toks2)
}
/* structure matching */
object Matcher extends StructureMatcher
{
private def find_block(
open: Token => Boolean,
close: Token => Boolean,
reset: Token => Boolean,
restrict: Token => Boolean,
it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
{
val range1 = it.next().range
it.takeWhile(info => !info.info.is_command || restrict(info.info)).
scanLeft((range1, 1))(
{ case ((r, d), Text.Info(range, tok)) =>
if (open(tok)) (range, d + 1)
else if (close(tok)) (range, d - 1)
else if (reset(tok)) (range, 0)
else (r, d) }
).collectFirst({ case (range2, 0) => (range1, range2) })
}
private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
{
val buffer = text_area.getBuffer
val caret_line = text_area.getCaretLine
val caret = text_area.getCaretPosition
Isabelle.buffer_syntax(text_area.getBuffer) match {
case Some(syntax) =>
val keywords = syntax.keywords
val nav = new Navigator(syntax, buffer, false)
def caret_iterator(): Iterator[Text.Info[Token]] =
nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
def reverse_caret_iterator(): Iterator[Text.Info[Token]] =
nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
nav.iterator(caret_line, 1).find(info => info.range.touches(caret))
match {
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
find_block(
keywords.is_command(_, Keyword.proof_goal),
keywords.is_command(_, Keyword.qed),
keywords.is_command(_, Keyword.qed_global),
t =>
keywords.is_command(t, Keyword.diag) ||
keywords.is_command(t, Keyword.proof),
caret_iterator())
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) =>
find_block(
keywords.is_command(_, Keyword.proof_goal),
keywords.is_command(_, Keyword.qed),
_ => false,
t =>
keywords.is_command(t, Keyword.diag) ||
keywords.is_command(t, Keyword.proof),
caret_iterator())
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) =>
reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory))
match {
case Some(Text.Info(range2, tok))
if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2))
case _ => None
}
case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) =>
find_block(
keywords.is_command(_, Keyword.qed),
t =>
keywords.is_command(t, Keyword.proof_goal) ||
keywords.is_command(t, Keyword.theory_goal),
_ => false,
t =>
keywords.is_command(t, Keyword.diag) ||
keywords.is_command(t, Keyword.proof) ||
keywords.is_command(t, Keyword.theory_goal),
reverse_caret_iterator())
case Some(Text.Info(range1, tok)) if tok.is_begin =>
find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
case Some(Text.Info(range1, tok)) if tok.is_end =>
find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator())
match {
case Some((_, range2)) =>
reverse_caret_iterator().
dropWhile(info => info.range != range2).
dropWhile(info => info.range == range2).
find(info => info.info.is_command || info.info.is_begin)
match {
case Some(Text.Info(range3, tok)) =>
if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3))
else Some((range1, range2))
case None => None
}
case None => None
}
case _ => None
}
case None => None
}
}
def getMatch(text_area: TextArea): StructureMatcher.Match =
find_pair(text_area) match {
case Some((_, range)) =>
val line = text_area.getBuffer.getLineOfOffset(range.start)
new StructureMatcher.Match(Matcher, line, range.start, line, range.stop)
case None => null
}
def selectMatch(text_area: TextArea): Unit =
{
def get_span(offset: Text.Offset): Option[Text.Range] =
for {
syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
} yield span.range
find_pair(text_area) match {
case Some((r1, r2)) =>
(get_span(r1.start), get_span(r2.start)) match {
case (Some(range1), Some(range2)) =>
val start = range1.start min range2.start
val stop = range1.stop max range2.stop
text_area.moveCaretPosition(stop, false)
if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
text_area.addToSelection(new Selection.Range(start, stop))
case _ =>
}
case None =>
}
}
}
}
diff --git a/src/Tools/jEdit/src/theories_dockable.scala b/src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala
+++ b/src/Tools/jEdit/src/theories_dockable.scala
@@ -1,270 +1,270 @@
/* Title: Tools/jEdit/src/theories_dockable.scala
Author: Makarius
Dockable window for theories managed by prover.
*/
package isabelle.jedit
import isabelle._
import isabelle.jedit_base.Dockable
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
ScrollPane, Component, CheckBox, BorderPanel}
import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
import javax.swing.{JList, BorderFactory, UIManager}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}
class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* status */
private val status = new ListView(Nil: List[Document.Node.Name]) {
background =
{
// enforce default value
val c = UIManager.getDefaults.getColor("Panel.background")
new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
}
listenTo(mouse.clicks)
listenTo(mouse.moves)
reactions += {
case MouseClicked(_, point, _, clicks, _) =>
val index = peer.locationToIndex(point)
if (index >= 0) {
if (in_checkbox(peer.indexToLocation(index), point)) {
if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
}
else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
}
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
val index_location = peer.indexToLocation(index)
if (index >= 0 && in_checkbox(index_location, point))
tooltip = "Mark as required for continuous checking"
else if (index >= 0 && in_label(index_location, point)) {
val name = listData(index)
val st = nodes_status.overall_node_status(name)
tooltip =
"theory " + quote(name.theory) +
(if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
}
else tooltip = null
}
}
status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
status.peer.setVisibleRowCount(0)
status.selection.intervalMode = ListView.IntervalMode.Single
set_content(new ScrollPane(status))
/* controls */
def phase_text(phase: Session.Phase): String = "Prover: " + phase.print
private val session_phase = new Label(phase_text(PIDE.session.phase))
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Status of prover session"
private def handle_phase(phase: Session.Phase): Unit =
{
GUI_Thread.require {}
session_phase.text = " " + phase_text(phase) + " "
}
private val purge = new Button("Purge") {
tooltip = "Restrict document model to theories required for open editor buffers"
reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
}
private val continuous_checking = new Isabelle.Continuous_Checking
continuous_checking.focusable = false
private val logic = JEdit_Sessions.logic_selector(PIDE.options, true)
private val controls =
Wrap_Panel(List(purge, continuous_checking, session_phase, logic))
add(controls.peer, BorderLayout.NORTH)
/* component state -- owned by GUI thread */
private var nodes_status = Document_Status.Nodes_Status.empty
private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
geometry match {
case Some((loc, size)) =>
loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
case None => false
}
private def in_checkbox(loc0: Point, p: Point): Boolean =
Node_Renderer_Component != null && in(Node_Renderer_Component.checkbox_geometry, loc0, p)
private def in_label(loc0: Point, p: Point): Boolean =
Node_Renderer_Component != null && in(Node_Renderer_Component.label_geometry, loc0, p)
private object Node_Renderer_Component extends BorderPanel
{
opaque = true
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
var node_name = Document.Node.Name.empty
var checkbox_geometry: Option[(Point, Dimension)] = None
val checkbox = new CheckBox {
opaque = false
override def paintComponent(gfx: Graphics2D): Unit =
{
super.paintComponent(gfx)
if (location != null && size != null)
checkbox_geometry = Some((location, size))
}
}
var label_geometry: Option[(Point, Dimension)] = None
val label = new Label {
background = view.getTextArea.getPainter.getBackground
foreground = view.getTextArea.getPainter.getForeground
opaque = false
xAlignment = Alignment.Leading
override def paintComponent(gfx: Graphics2D): Unit =
{
def paint_segment(x: Int, w: Int, color: Color): Unit =
{
gfx.setColor(color)
gfx.fillRect(x, 0, w, size.height)
}
paint_segment(0, size.width, background)
nodes_status.get(node_name) match {
case Some(node_status) =>
val segments =
List(
(node_status.unprocessed, PIDE.options.color_value("unprocessed1_color")),
(node_status.running, PIDE.options.color_value("running_color")),
(node_status.warned, PIDE.options.color_value("warning_color")),
(node_status.failed, PIDE.options.color_value("error_color"))
).filter(_._1 > 0)
- ((size.width - 2) /: segments)({ case (last, (n, color)) =>
+ segments.foldLeft(size.width - 2)({ case (last, (n, color)) =>
val w = (n * ((size.width - 4) - segments.length) / node_status.total) max 4
paint_segment(last - w, w, color)
last - w - 1
})
case None =>
paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
}
super.paintComponent(gfx)
if (location != null && size != null)
label_geometry = Some((location, size))
}
}
def label_border(name: Document.Node.Name): Unit =
{
val st = nodes_status.overall_node_status(name)
val color =
if (st == Document_Status.Overall_Node_Status.failed)
PIDE.options.color_value("error_color")
else label.foreground
val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 2
val thickness2 = 3 - thickness1
label.border =
BorderFactory.createCompoundBorder(
BorderFactory.createLineBorder(color, thickness1),
BorderFactory.createEmptyBorder(thickness2, thickness2, thickness2, thickness2))
}
layout(checkbox) = BorderPanel.Position.West
layout(label) = BorderPanel.Position.Center
}
private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
{
def componentFor(list: ListView[_ <: isabelle.Document.Node.Name], isSelected: Boolean,
focused: Boolean, name: Document.Node.Name, index: Int): Component =
{
val component = Node_Renderer_Component
component.node_name = name
component.checkbox.selected = nodes_required.contains(name)
component.label_border(name)
component.label.text = name.theory_base_name
component
}
}
status.renderer = new Node_Renderer
private def handle_update(
domain: Option[Set[Document.Node.Name]] = None, trim: Boolean = false): Unit =
{
GUI_Thread.require {}
val snapshot = PIDE.session.snapshot()
val (nodes_status_changed, nodes_status1) =
nodes_status.update(
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
nodes_status = nodes_status1
if (nodes_status_changed) {
status.listData =
(for {
(name, node_status) <- nodes_status1.present.iterator
if !node_status.is_suppressed && node_status.total > 0
} yield name).toList
}
}
/* main */
private val main =
Session.Consumer[Any](getClass.getName) {
case phase: Session.Phase =>
GUI_Thread.later { handle_phase(phase) }
case _: Session.Global_Options =>
GUI_Thread.later {
continuous_checking.load()
logic.load ()
nodes_required = Document_Model.required_nodes()
status.repaint()
}
case changed: Session.Commands_Changed =>
GUI_Thread.later { handle_update(domain = Some(changed.nodes), trim = changed.assignment) }
}
override def init(): Unit =
{
PIDE.session.phase_changed += main
PIDE.session.global_options += main
PIDE.session.commands_changed += main
handle_phase(PIDE.session.phase)
handle_update()
}
override def exit(): Unit =
{
PIDE.session.phase_changed -= main
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
}
}
diff --git a/src/Tools/jEdit/src/timing_dockable.scala b/src/Tools/jEdit/src/timing_dockable.scala
--- a/src/Tools/jEdit/src/timing_dockable.scala
+++ b/src/Tools/jEdit/src/timing_dockable.scala
@@ -1,225 +1,225 @@
/* Title: Tools/jEdit/src/timing_dockable.scala
Author: Makarius
Dockable window for timing information.
*/
package isabelle.jedit
import isabelle._
import isabelle.jedit_base.Dockable
import scala.swing.{Label, ListView, Alignment, ScrollPane, Component, TextField}
import scala.swing.event.{MouseClicked, ValueChanged}
import java.awt.{BorderLayout, Graphics2D, Insets, Color}
import javax.swing.{JList, BorderFactory}
import javax.swing.border.{BevelBorder, SoftBevelBorder}
import org.gjt.sp.jedit.{View, jEdit}
class Timing_Dockable(view: View, position: String) extends Dockable(view, position)
{
/* entry */
private object Entry
{
object Ordering extends scala.math.Ordering[Entry]
{
def compare(entry1: Entry, entry2: Entry): Int =
entry2.timing compare entry1.timing
}
object Renderer_Component extends Label
{
opaque = false
xAlignment = Alignment.Leading
border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
var entry: Entry = null
override def paintComponent(gfx: Graphics2D): Unit =
{
def paint_rectangle(color: Color): Unit =
{
val size = peer.getSize()
val insets = border.getBorderInsets(peer)
val x = insets.left
val y = insets.top
val w = size.width - x - insets.right
val h = size.height - y - insets.bottom
gfx.setColor(color)
gfx.fillRect(x, y, w, h)
}
entry match {
case theory_entry: Theory_Entry if theory_entry.current =>
paint_rectangle(view.getTextArea.getPainter.getSelectionColor)
case _: Command_Entry =>
paint_rectangle(view.getTextArea.getPainter.getMultipleSelectionColor)
case _ =>
}
super.paintComponent(gfx)
}
}
class Renderer extends ListView.Renderer[Entry]
{
def componentFor(list: ListView[_ <: Timing_Dockable.this.Entry],
isSelected: Boolean, focused: Boolean, entry: Entry, index: Int): Component =
{
val component = Renderer_Component
component.entry = entry
component.text = entry.print
component
}
}
}
private abstract class Entry
{
def timing: Double
def print: String
def follow(snapshot: Document.Snapshot): Unit
}
private case class Theory_Entry(name: Document.Node.Name, timing: Double, current: Boolean)
extends Entry
{
def print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
def follow(snapshot: Document.Snapshot): Unit =
PIDE.editor.goto_file(true, view, name.node)
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
{
def print: String =
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot): Unit =
PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view))
}
/* timing view */
private val timing_view = new ListView(Nil: List[Entry]) {
listenTo(mouse.clicks)
reactions += {
case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
val index = peer.locationToIndex(point)
if (index >= 0) listData(index).follow(PIDE.session.snapshot())
}
}
timing_view.peer.setLayoutOrientation(JList.VERTICAL_WRAP)
timing_view.peer.setVisibleRowCount(0)
timing_view.selection.intervalMode = ListView.IntervalMode.Single
timing_view.renderer = new Entry.Renderer
set_content(new ScrollPane(timing_view))
/* timing threshold */
private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
private val threshold_tooltip = "Threshold for timing display (seconds)"
private val threshold_label = new Label("Threshold: ") {
tooltip = threshold_tooltip
}
private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
reactions += {
case _: ValueChanged =>
text match {
case Value.Double(x) if x >= 0.0 => timing_threshold = x
case _ =>
}
handle_update()
}
tooltip = threshold_tooltip
verifier = ((s: String) =>
s match { case Value.Double(x) => x >= 0.0 case _ => false })
}
private val controls = Wrap_Panel(List(threshold_label, threshold_value))
add(controls.peer, BorderLayout.NORTH)
/* component state -- owned by GUI thread */
private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
private def make_entries(): List[Entry] =
{
GUI_Thread.require {}
val name =
Document_View.get(view.getTextArea) match {
case None => Document.Node.Name.empty
case Some(doc_view) => doc_view.model.node_name
}
val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
val theories =
(for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
yield Theory_Entry(node_name, node_timing.total, false)).sorted(Entry.Ordering)
val commands =
(for ((command, command_timing) <- timing.command_timings.toList)
yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
theories.flatMap(entry =>
if (entry.name == name) entry.copy(current = true) :: commands
else List(entry))
}
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None): Unit =
{
GUI_Thread.require {}
val snapshot = PIDE.session.snapshot()
- val iterator =
- restriction match {
+ val nodes_timing1 =
+ (restriction match {
case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
case None => snapshot.version.nodes.iterator
- }
- val nodes_timing1 =
- (nodes_timing /: iterator)({ case (timing1, (name, node)) =>
- if (PIDE.resources.session_base.loaded_theory(name)) timing1
- else {
- val node_timing =
- Document_Status.Overall_Timing.make(
- snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
- timing1 + (name -> node_timing)
- }
})
+ .foldLeft(nodes_timing)(
+ { case (timing1, (name, node)) =>
+ if (PIDE.resources.session_base.loaded_theory(name)) timing1
+ else {
+ val node_timing =
+ Document_Status.Overall_Timing.make(
+ snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
+ timing1 + (name -> node_timing)
+ }
+ })
nodes_timing = nodes_timing1
val entries = make_entries()
if (timing_view.listData.toList != entries) timing_view.listData = entries
}
/* main */
private val main =
Session.Consumer[Session.Commands_Changed](getClass.getName) {
case changed =>
GUI_Thread.later { handle_update(Some(changed.nodes)) }
}
override def init(): Unit =
{
PIDE.session.commands_changed += main
handle_update()
}
override def exit(): Unit =
{
PIDE.session.commands_changed -= main
}
}