# HG changeset patch
# User wenzelm
# Date 1497377799 -7200
# Node ID 2d12a730a380e38f1fdfe436b8de1e2df21fd6ff
# Parent  441f95b05944f7f36281fbbe2c5e9b6b07661f61
clarified modules;

diff -r 441f95b05944 -r 2d12a730a380 src/Pure/PIDE/editor.scala
--- 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
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/active.scala
--- 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 {
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/debugger_dockable.scala
--- 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())
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/document_model.scala
--- 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()
     }
   }
 
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/document_view.scala
--- 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()
     }
   }
 
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/documentation_dockable.scala
--- 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 _ =>
     }
   }
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/jedit_editor.scala
--- 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)
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/jedit_rendering.scala
--- 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
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/output_dockable.scala
--- 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()
     }
   }
 
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/plugin.scala
--- 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
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/query_dockable.scala
--- 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)))
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/rich_text_area.scala
--- 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
     }
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- 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 =>
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/sledgehammer_dockable.scala
--- 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)))
 
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/state_dockable.scala
--- 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()
         }
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/theories_dockable.scala
--- 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
diff -r 441f95b05944 -r 2d12a730a380 src/Tools/jEdit/src/timing_dockable.scala
--- 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)) }
   }