--- a/src/Tools/jEdit/src/active.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/active.scala Tue Mar 14 21:43:54 2017 +0100
@@ -51,7 +51,7 @@
case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
val link =
props match {
- case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
+ case Position.Id(id) => JEdit_Editor.hyperlink_command(true, snapshot, id)
case _ => None
}
GUI_Thread.later {
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -85,7 +85,7 @@
{
GUI_Thread.require {}
- val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
+ val new_snapshot = JEdit_Editor.current_node_snapshot(view).getOrElse(current_snapshot)
val (new_threads, new_output) = PIDE.debugger.status(tree_selection())
if (new_threads != current_threads)
@@ -304,7 +304,7 @@
PIDE.debugger.set_focus(c)
for {
pos <- c.debug_position
- link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
+ link <- JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Tue Mar 14 21:43:54 2017 +0100
@@ -183,7 +183,7 @@
})
if (changed) {
PIDE.plugin.options_changed()
- PIDE.editor.flush()
+ JEdit_Editor.flush()
}
}
@@ -290,10 +290,10 @@
if (hidden) Text.Perspective.empty
else {
val view_ranges = document_view_ranges(snapshot)
- val load_ranges = snapshot.commands_loading_ranges(PIDE.editor.visible_node(_))
+ val load_ranges = snapshot.commands_loading_ranges(JEdit_Editor.visible_node(_))
Text.Perspective(view_ranges ::: load_ranges)
}
- val overlays = PIDE.editor.node_overlays(node_name)
+ val overlays = JEdit_Editor.node_overlays(node_name)
(reparse, Document.Node.Perspective(node_required, perspective, overlays))
}
@@ -515,7 +515,7 @@
doc_view.rich_text_area.active_reset()
pending ++= edits
- PIDE.editor.invoke()
+ JEdit_Editor.invoke()
}
}
--- a/src/Tools/jEdit/src/document_view.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Tue Mar 14 21:43:54 2017 +0100
@@ -77,7 +77,7 @@
{
val view = text_area.getView
if (view != null && view.getTextArea == text_area) {
- PIDE.editor.current_command(view, snapshot) match {
+ JEdit_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
- PIDE.editor.invoke_generated()
+ JEdit_Editor.invoke_generated()
}
}
--- a/src/Tools/jEdit/src/documentation_dockable.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/documentation_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -54,9 +54,9 @@
{
node.getUserObject match {
case Text_File(_, path) =>
- PIDE.editor.goto_file(true, view, File.platform_path(path))
+ JEdit_Editor.goto_file(true, view, File.platform_path(path))
case Documentation(_, _, path) =>
- PIDE.editor.goto_doc(view, path)
+ JEdit_Editor.goto_doc(view, path)
case _ =>
}
}
--- a/src/Tools/jEdit/src/jedit_editor.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Tue Mar 14 21:43:54 2017 +0100
@@ -16,7 +16,7 @@
import org.gjt.sp.jedit.browser.VFSBrowser
-class JEdit_Editor extends Editor[View]
+object JEdit_Editor extends Editor[View]
{
/* session */
--- a/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Tue Mar 14 21:43:54 2017 +0100
@@ -298,37 +298,37 @@
/* hyperlinks */
- def hyperlink(range: Text.Range): Option[Text.Info[PIDE.editor.Hyperlink]] =
+ def hyperlink(range: Text.Range): Option[Text.Info[JEdit_Editor.Hyperlink]] =
{
- snapshot.cumulate[Vector[Text.Info[PIDE.editor.Hyperlink]]](
+ snapshot.cumulate[Vector[Text.Info[JEdit_Editor.Hyperlink]]](
range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
val file = PIDE.resources.append_file(snapshot.node_name.master_dir, name)
- val link = PIDE.editor.hyperlink_file(true, file)
+ val link = JEdit_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), _))) =>
- PIDE.editor.hyperlink_doc(name).map(link =>
+ JEdit_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)
+ val link = JEdit_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)
+ val opt_link = JEdit_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)
+ val opt_link = JEdit_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) })
+ JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -47,11 +47,11 @@
GUI_Thread.require {}
for {
- snapshot <- PIDE.editor.current_node_snapshot(view)
+ snapshot <- JEdit_Editor.current_node_snapshot(view)
if follow && !snapshot.is_outdated
} {
val (command, results) =
- PIDE.editor.current_command(view, snapshot) match {
+ JEdit_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)
- PIDE.editor.flush(hidden = true)
- PIDE.editor.flush()
+ JEdit_Editor.flush(hidden = true)
+ JEdit_Editor.flush()
}
}
--- a/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Tue Mar 14 21:43:54 2017 +0100
@@ -43,8 +43,6 @@
def debugger: Debugger = session.debugger
- lazy val editor = new JEdit_Editor
-
/* current document content */
@@ -175,7 +173,7 @@
GUI_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) { delay_load_action() }
private def file_watcher_action(changed: Set[JFile]): Unit =
- if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
+ if (Document_Model.sync_files(changed)) JEdit_Editor.invoke_generated()
lazy val file_watcher: File_Watcher =
File_Watcher(file_watcher_action _, PIDE.options.seconds("editor_load_delay"))
@@ -214,7 +212,7 @@
GUI_Thread.later {
delay_load.revoke()
delay_init.revoke()
- PIDE.editor.flush()
+ JEdit_Editor.flush()
exit_models(JEdit_Lib.jedit_buffers().toList)
}
@@ -238,7 +236,7 @@
def init_models()
{
GUI_Thread.now {
- PIDE.editor.flush()
+ JEdit_Editor.flush()
for {
buffer <- JEdit_Lib.jedit_buffers()
@@ -257,7 +255,7 @@
else delay_init.invoke()
}
- PIDE.editor.invoke_generated()
+ JEdit_Editor.invoke_generated()
}
}
@@ -314,14 +312,14 @@
Keymap_Merge.check_dialog(view)
- PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
+ JEdit_Editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.session_info().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))
- PIDE.editor.invoke_generated()
+ JEdit_Editor.invoke_generated()
}
case msg: BufferUpdate
--- a/src/Tools/jEdit/src/query_dockable.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -77,7 +77,7 @@
private val process_indicator = new Process_Indicator
val query_operation =
- new Query_Operation(PIDE.editor, view, "find_theorems",
+ new Query_Operation(JEdit_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(PIDE.editor, view, "find_consts",
+ new Query_Operation(JEdit_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(PIDE.editor, view, "print_operation",
+ new Query_Operation(JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala Tue Mar 14 21:43:54 2017 +0100
@@ -162,7 +162,7 @@
(rendering: JEdit_Rendering) => rendering.highlight _, None)
private val hyperlink_area =
- new Active_Area[PIDE.editor.Hyperlink](
+ new Active_Area[JEdit_Editor.Hyperlink](
(rendering: JEdit_Rendering) => rendering.hyperlink _, Some(Cursor.HAND_CURSOR))
private val active_area =
@@ -374,7 +374,7 @@
c <- PIDE.debugger.focus().iterator
pos <- c.debug_position.iterator
} yield pos).toList
- if (debug_positions.exists(PIDE.editor.is_hyperlink_position(rendering.snapshot, offset, _)))
+ if (debug_positions.exists(JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -82,10 +82,10 @@
private def handle_update(follow: Boolean)
{
val (new_snapshot, new_command, new_results, new_id) =
- PIDE.editor.current_node_snapshot(view) match {
+ JEdit_Editor.current_node_snapshot(view) match {
case Some(snapshot) =>
if (follow && !snapshot.is_outdated) {
- PIDE.editor.current_command(view, snapshot) match {
+ JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -49,7 +49,7 @@
}
private val sledgehammer =
- new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
+ new Query_Operation(JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -31,7 +31,7 @@
override def detach_operation = pretty_text_area.detach_operation
private val print_state =
- new Query_Operation(PIDE.editor, view, "print_state", _ => (),
+ new Query_Operation(JEdit_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) =>
- (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
+ (JEdit_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 Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -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) PIDE.editor.goto_file(true, view, listData(index).node)
+ else if (clicks == 2) JEdit_Editor.goto_file(true, view, listData(index).node)
}
case MouseMoved(_, point, _) =>
val index = peer.locationToIndex(point)
@@ -73,7 +73,7 @@
private val purge = new Button("Purge") {
tooltip = "Restrict document model to theories required for open editor buffers"
- reactions += { case ButtonClicked(_) => PIDE.editor.purge() }
+ reactions += { case ButtonClicked(_) => JEdit_Editor.purge() }
}
private val continuous_checking = new Isabelle.Continuous_Checking
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 14 21:36:27 2017 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Mar 14 21:43:54 2017 +0100
@@ -88,7 +88,7 @@
{
def print: String =
Time.print_seconds(timing) + "s theory " + quote(name.theory)
- def follow(snapshot: Document.Snapshot) { PIDE.editor.goto_file(true, view, name.node) }
+ def follow(snapshot: Document.Snapshot) { JEdit_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)
- { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
+ { JEdit_Editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) }
}