--- a/src/Pure/PIDE/editor.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Pure/PIDE/editor.scala Tue Jun 13 20:16:39 2017 +0200
@@ -9,19 +9,32 @@
abstract class Editor[Context]
{
+ /* session */
+
def session: Session
def flush(hidden: Boolean = false, purge: Boolean = false): Unit
def invoke(): Unit
- def invoke_generated(): Unit
- def current_context: Context
def current_node(context: Context): Option[Document.Node.Name]
def current_node_snapshot(context: Context): Option[Document.Snapshot]
def node_snapshot(name: Document.Node.Name): Document.Snapshot
def current_command(context: Context, snapshot: Document.Snapshot): Option[Command]
- def node_overlays(name: Document.Node.Name): Document.Node.Overlays
- def insert_overlay(command: Command, fn: String, args: List[String]): Unit
- def remove_overlay(command: Command, fn: String, args: List[String]): Unit
+
+ /* overlays */
+
+ private val overlays = Synchronized(Document.Overlays.empty)
+
+ def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+ overlays.value(name)
+
+ def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+ overlays.change(_.insert(command, fn, args))
+
+ def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+ overlays.change(_.remove(command, fn, args))
+
+
+ /* hyperlinks */
abstract class Hyperlink {
def external: Boolean = false
--- a/src/Tools/jEdit/src/active.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/active.scala Tue Jun 13 20:16:39 2017 +0200
@@ -51,7 +51,7 @@
case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
val link =
props match {
- case Position.Id(id) => JEdit_Editor.hyperlink_command(true, snapshot, id)
+ case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
case _ => None
}
GUI_Thread.later {
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -87,7 +87,7 @@
{
GUI_Thread.require {}
- val new_snapshot = JEdit_Editor.current_node_snapshot(view).getOrElse(current_snapshot)
+ val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
val (new_threads, new_output) = debugger.status(tree_selection())
if (new_threads != current_threads)
@@ -306,7 +306,7 @@
debugger.set_focus(c)
for {
pos <- c.debug_position
- link <- JEdit_Editor.hyperlink_position(false, current_snapshot, pos)
+ link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
} link.follow(view)
}
JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
--- a/src/Tools/jEdit/src/document_model.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/document_model.scala Tue Jun 13 20:16:39 2017 +0200
@@ -184,7 +184,7 @@
})
if (changed) {
PIDE.plugin.options_changed()
- JEdit_Editor.flush()
+ PIDE.editor.flush()
}
}
@@ -273,7 +273,7 @@
{
Document_Model.get(view.getBuffer) match {
case Some(model) if model.is_theory =>
- JEdit_Editor.hyperlink_url(
+ PIDE.editor.hyperlink_url(
PIDE.plugin.http_server.url.toString + PIDE.plugin.http_root + "/preview/" +
model.node_name.theory).follow(view)
case _ =>
@@ -333,10 +333,10 @@
if (hidden) Text.Perspective.empty
else {
val view_ranges = document_view_ranges(snapshot)
- val load_ranges = snapshot.commands_loading_ranges(JEdit_Editor.visible_node(_))
+ val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
Text.Perspective(view_ranges ::: load_ranges)
}
- val overlays = JEdit_Editor.node_overlays(node_name)
+ val overlays = PIDE.editor.node_overlays(node_name)
(reparse, Document.Node.Perspective(node_required, perspective, overlays))
}
@@ -570,7 +570,7 @@
doc_view.rich_text_area.active_reset()
pending ++= edits
- JEdit_Editor.invoke()
+ PIDE.editor.invoke()
}
}
--- a/src/Tools/jEdit/src/document_view.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/document_view.scala Tue Jun 13 20:16:39 2017 +0200
@@ -77,7 +77,7 @@
{
val view = text_area.getView
if (view != null && view.getTextArea == text_area) {
- JEdit_Editor.current_command(view, snapshot) match {
+ PIDE.editor.current_command(view, snapshot) match {
case Some(command) =>
snapshot.node.command_start(command) match {
case Some(start) => List(snapshot.convert(command.proper_range + start))
@@ -111,7 +111,7 @@
start: Array[Int], end: Array[Int], y: Int, line_height: Int)
{
// no robust_body
- JEdit_Editor.invoke_generated()
+ PIDE.editor.invoke_generated()
}
}
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -54,9 +54,9 @@
{
node.getUserObject match {
case Text_File(_, path) =>
- JEdit_Editor.goto_file(true, view, File.platform_path(path))
+ PIDE.editor.goto_file(true, view, File.platform_path(path))
case Documentation(_, _, path) =>
- JEdit_Editor.goto_doc(view, path)
+ PIDE.editor.goto_doc(view, path)
case _ =>
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Jun 13 20:16:39 2017 +0200
@@ -48,9 +48,6 @@
/* current situation */
- override def current_context: View =
- GUI_Thread.require { jEdit.getActiveView() }
-
override def current_node(view: View): Option[Document.Node.Name] =
GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) }
@@ -86,20 +83,6 @@
}
- /* overlays */
-
- private val overlays = Synchronized(Document.Overlays.empty)
-
- override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
- overlays.value(name)
-
- override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
- overlays.change(_.insert(command, fn, args))
-
- override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
- overlays.change(_.remove(command, fn, args))
-
-
/* navigation */
def push_position(view: View)
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Jun 13 20:16:39 2017 +0200
@@ -228,37 +228,37 @@
/* hyperlinks */
- def hyperlink(range: Text.Range): Option[Text.Info[JEdit_Editor.Hyperlink]] =
+ def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
{
- snapshot.cumulate[Vector[Text.Info[JEdit_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 = JEdit_Editor.hyperlink_file(true, file)
+ 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.Doc(name), _))) =>
- JEdit_Editor.hyperlink_doc(name).map(link =>
+ 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 = JEdit_Editor.hyperlink_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 = JEdit_Editor.hyperlink_def_position(true, snapshot, 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 = JEdit_Editor.hyperlink_position(true, snapshot, 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 =>
- JEdit_Editor.hyperlink_model(true, model, entry_range.start) })
+ 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/output_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -47,11 +47,11 @@
GUI_Thread.require {}
for {
- snapshot <- JEdit_Editor.current_node_snapshot(view)
+ snapshot <- PIDE.editor.current_node_snapshot(view)
if follow && !snapshot.is_outdated
} {
val (command, results) =
- JEdit_Editor.current_command(view, snapshot) match {
+ PIDE.editor.current_command(view, snapshot) match {
case Some(command) => (command, snapshot.command_results(command))
case None => (Command.empty, Command.Results.empty)
}
@@ -77,8 +77,8 @@
if (output_state != b) {
PIDE.options.bool("editor_output_state") = b
PIDE.session.update_options(PIDE.options.value)
- JEdit_Editor.flush(hidden = true)
- JEdit_Editor.flush()
+ PIDE.editor.flush(hidden = true)
+ PIDE.editor.flush()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Tue Jun 13 20:16:39 2017 +0200
@@ -55,6 +55,8 @@
def options: JEdit_Options = plugin.options
def resources: JEdit_Resources = plugin.resources
def session: Session = plugin.session
+
+ val editor = JEdit_Editor
}
class Plugin extends EBPlugin
@@ -172,7 +174,7 @@
GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() }
private def file_watcher_action(changed: Set[JFile]): Unit =
- if (Document_Model.sync_files(changed)) JEdit_Editor.invoke_generated()
+ if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
lazy val file_watcher: File_Watcher =
File_Watcher(file_watcher_action _, options.seconds("editor_load_delay"))
@@ -210,7 +212,7 @@
GUI_Thread.later {
delay_load.revoke()
delay_init.revoke()
- JEdit_Editor.flush()
+ PIDE.editor.flush()
exit_models(JEdit_Lib.jedit_buffers().toList)
}
@@ -234,7 +236,7 @@
def init_models()
{
GUI_Thread.now {
- JEdit_Editor.flush()
+ PIDE.editor.flush()
for {
buffer <- JEdit_Lib.jedit_buffers()
@@ -253,7 +255,7 @@
else delay_init.invoke()
}
- JEdit_Editor.invoke_generated()
+ PIDE.editor.invoke_generated()
}
}
@@ -310,14 +312,14 @@
Keymap_Merge.check_dialog(view)
- JEdit_Editor.hyperlink_position(true, Document.Snapshot.init,
+ PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
if (msg.getBuffer != null) {
exit_models(List(msg.getBuffer))
- JEdit_Editor.invoke_generated()
+ PIDE.editor.invoke_generated()
}
case msg: BufferUpdate
--- a/src/Tools/jEdit/src/query_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -77,7 +77,7 @@
private val process_indicator = new Process_Indicator
val query_operation =
- new Query_Operation(JEdit_Editor, view, "find_theorems",
+ new Query_Operation(PIDE.editor, view, "find_theorems",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -143,7 +143,7 @@
private val process_indicator = new Process_Indicator
val query_operation =
- new Query_Operation(JEdit_Editor, view, "find_consts",
+ new Query_Operation(PIDE.editor, view, "find_consts",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -226,7 +226,7 @@
private val process_indicator = new Process_Indicator
val query_operation =
- new Query_Operation(JEdit_Editor, view, "print_operation",
+ new Query_Operation(PIDE.editor, view, "print_operation",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
--- a/src/Tools/jEdit/src/rich_text_area.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Jun 13 20:16:39 2017 +0200
@@ -162,7 +162,7 @@
(rendering: JEdit_Rendering) => rendering.highlight _, None)
private val hyperlink_area =
- new Active_Area[JEdit_Editor.Hyperlink](
+ new Active_Area[PIDE.editor.Hyperlink](
(rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
private val active_area =
@@ -374,7 +374,7 @@
c <- PIDE.session.debugger.focus().iterator
pos <- c.debug_position.iterator
} yield pos).toList
- if (debug_positions.exists(JEdit_Editor.is_hyperlink_position(rendering.snapshot, offset, _)))
+ if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
rendering.caret_debugger_color
else rendering.caret_invisible_color
}
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -82,10 +82,10 @@
private def handle_update(follow: Boolean)
{
val (new_snapshot, new_command, new_results, new_id) =
- JEdit_Editor.current_node_snapshot(view) match {
+ PIDE.editor.current_node_snapshot(view) match {
case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
- JEdit_Editor.current_command(view, snapshot) match {
+ PIDE.editor.current_command(view, snapshot) match {
case Some(cmd) =>
(snapshot, cmd, snapshot.command_results(cmd), cmd.id)
case None =>
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -49,7 +49,7 @@
}
private val sledgehammer =
- new Query_Operation(JEdit_Editor, view, "sledgehammer", consume_status _,
+ new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
--- a/src/Tools/jEdit/src/state_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -31,7 +31,7 @@
override def detach_operation = pretty_text_area.detach_operation
private val print_state =
- new Query_Operation(JEdit_Editor, view, "print_state", _ => (),
+ new Query_Operation(PIDE.editor, view, "print_state", _ => (),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
@@ -66,7 +66,7 @@
Document_Model.get(view.getBuffer).map(_.snapshot()) match {
case Some(snapshot) =>
- (JEdit_Editor.current_command(view, snapshot), print_state.get_location) match {
+ (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
case (Some(command1), Some(command2)) if command1.id == command2.id =>
case _ => update_request()
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -40,7 +40,7 @@
if (in_checkbox(peer.indexToLocation(index), point)) {
if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
}
- else if (clicks == 2) JEdit_Editor.goto_file(true, view, listData(index).node)
+ else if (clicks == 2) PIDE.editor.goto_file(true, view, listData(index).node)
}
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
@@ -76,7 +76,7 @@
private val purge = new Button("Purge") {
tooltip = "Restrict document model to theories required for open editor buffers"
- reactions += { case ButtonClicked(_) => JEdit_Editor.purge() }
+ reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
}
private val continuous_checking = new Isabelle.Continuous_Checking
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 13 15:11:01 2017 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Jun 13 20:16:39 2017 +0200
@@ -88,7 +88,7 @@
{
def print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
- def follow(snapshot: Document.Snapshot) { JEdit_Editor.goto_file(true, view, name.node) }
+ def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
}
private case class Command_Entry(command: Command, timing: Double) extends Entry
@@ -96,7 +96,7 @@
def print: String =
" " + Time.print_seconds(timing) + "s command " + quote(command.span.name)
def follow(snapshot: Document.Snapshot)
- { JEdit_Editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
+ { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
}