# HG changeset patch # User wenzelm # Date 1489524234 -3600 # Node ID 848965b5befc7057879d83aa70da89469c59dbbd # Parent e955b33f432c7be270e01d610842e16662ef8f59 clarified singleton module; diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/active.scala --- 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 { diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/debugger_dockable.scala --- 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()) diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/document_model.scala --- 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() } } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/document_view.scala --- 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() } } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/documentation_dockable.scala --- 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 _ => } } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/jedit_editor.scala --- 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 */ diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/jedit_rendering.scala --- 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 diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/output_dockable.scala --- 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() } } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/plugin.scala --- 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 diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/query_dockable.scala --- 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))) diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/rich_text_area.scala --- 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 } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/simplifier_trace_dockable.scala --- 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 => diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/sledgehammer_dockable.scala --- 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))) diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/state_dockable.scala --- 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() } diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/theories_dockable.scala --- 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 diff -r e955b33f432c -r 848965b5befc src/Tools/jEdit/src/timing_dockable.scala --- 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)) } }