1/* Title: Tools/jEdit/src/jedit_editor.scala 2 Author: Makarius 3 4PIDE editor operations for jEdit. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12 13import java.io.{File => JFile} 14 15import org.gjt.sp.jedit.{jEdit, View, Buffer} 16import org.gjt.sp.jedit.browser.VFSBrowser 17 18 19class JEdit_Editor extends Editor[View] 20{ 21 /* session */ 22 23 override def session: Session = PIDE.session 24 25 def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit = 26 GUI_Thread.require { 27 val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge) 28 session.update(doc_blobs, edits) 29 } 30 override def flush(): Unit = flush_edits() 31 def purge() { flush_edits(purge = true) } 32 33 private val delay1_flush = 34 GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } 35 36 private val delay2_flush = 37 GUI_Thread.delay_first(PIDE.options.seconds("editor_generated_input_delay")) { flush() } 38 39 def invoke(): Unit = delay1_flush.invoke() 40 def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } 41 42 def shutdown(): Unit = 43 GUI_Thread.require { 44 delay1_flush.revoke() 45 delay2_flush.revoke() 46 Document_Model.flush_edits(hidden = false, purge = false) 47 } 48 49 def visible_node(name: Document.Node.Name): Boolean = 50 (for { 51 text_area <- JEdit_Lib.jedit_text_areas() 52 doc_view <- Document_View.get(text_area) 53 } yield doc_view.model.node_name).contains(name) 54 55 56 /* current situation */ 57 58 override def current_node(view: View): Option[Document.Node.Name] = 59 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } 60 61 override def current_node_snapshot(view: View): Option[Document.Snapshot] = 62 GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) } 63 64 override def node_snapshot(name: Document.Node.Name): Document.Snapshot = 65 { 66 GUI_Thread.require {} 67 Document_Model.get(name) match { 68 case Some(model) => model.snapshot 69 case None => session.snapshot(name) 70 } 71 } 72 73 override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = 74 { 75 GUI_Thread.require {} 76 77 val text_area = view.getTextArea 78 val buffer = view.getBuffer 79 80 Document_View.get(text_area) match { 81 case Some(doc_view) if doc_view.model.is_theory => 82 snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) 83 case _ => 84 Document_Model.get(buffer) match { 85 case Some(model) if !model.is_theory => 86 snapshot.version.nodes.commands_loading(model.node_name).headOption 87 case _ => None 88 } 89 } 90 } 91 92 93 /* overlays */ 94 95 override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = 96 Document_Model.node_overlays(name) 97 98 override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = 99 Document_Model.insert_overlay(command, fn, args) 100 101 override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = 102 Document_Model.remove_overlay(command, fn, args) 103 104 105 /* navigation */ 106 107 def push_position(view: View) 108 { 109 val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin") 110 if (navigator != null) { 111 try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) } 112 catch { case _: NoSuchMethodException => } 113 } 114 } 115 116 def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset) 117 { 118 GUI_Thread.require {} 119 120 push_position(view) 121 122 if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) 123 try { view.getTextArea.moveCaretPosition(offset) } 124 catch { 125 case _: ArrayIndexOutOfBoundsException => 126 case _: IllegalArgumentException => 127 } 128 } 129 130 def goto_file(focus: Boolean, view: View, name: String): Unit = 131 goto_file(focus, view, Line.Node_Position.offside(name)) 132 133 def goto_file(focus: Boolean, view: View, pos: Line.Node_Position) 134 { 135 GUI_Thread.require {} 136 137 push_position(view) 138 139 val name = pos.name 140 val line = pos.line 141 val column = pos.column 142 143 JEdit_Lib.jedit_buffer(name) match { 144 case Some(buffer) => 145 if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) 146 val text_area = view.getTextArea 147 148 try { 149 val line_start = text_area.getBuffer.getLineStartOffset(line) 150 text_area.moveCaretPosition(line_start) 151 if (column > 0) text_area.moveCaretPosition(line_start + column) 152 } 153 catch { 154 case _: ArrayIndexOutOfBoundsException => 155 case _: IllegalArgumentException => 156 } 157 158 case None if (new JFile(name)).isDirectory => 159 VFSBrowser.browseDirectory(view, name) 160 161 case None => 162 val args = 163 if (line <= 0) Array(name) 164 else if (column <= 0) Array(name, "+line:" + (line + 1)) 165 else Array(name, "+line:" + (line + 1) + "," + (column + 1)) 166 jEdit.openFiles(view, null, args) 167 } 168 } 169 170 def goto_doc(view: View, path: Path) 171 { 172 if (path.is_file) 173 goto_file(true, view, File.platform_path(path)) 174 else { 175 Standard_Thread.fork("documentation") { 176 try { Doc.view(path) } 177 catch { 178 case exn: Throwable => 179 GUI_Thread.later { 180 GUI.error_dialog(view, 181 "Documentation error", GUI.scrollable_text(Exn.message(exn))) 182 } 183 } 184 } 185 } 186 } 187 188 189 /* hyperlinks */ 190 191 def hyperlink_doc(name: String): Option[Hyperlink] = 192 Doc.contents().collectFirst({ 193 case doc: Doc.Text_File if doc.name == name => doc.path 194 case doc: Doc.Doc if doc.name == name => doc.path}).map(path => 195 new Hyperlink { 196 override val external = !path.is_file 197 def follow(view: View): Unit = goto_doc(view, path) 198 override def toString: String = "doc " + quote(name) 199 }) 200 201 def hyperlink_url(name: String): Hyperlink = 202 new Hyperlink { 203 override val external = true 204 def follow(view: View): Unit = 205 Standard_Thread.fork("hyperlink_url") { 206 try { Isabelle_System.open(Url.escape(name)) } 207 catch { 208 case exn: Throwable => 209 GUI_Thread.later { 210 GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) 211 } 212 } 213 } 214 override def toString: String = "URL " + quote(name) 215 } 216 217 def hyperlink_file(focus: Boolean, name: String): Hyperlink = 218 hyperlink_file(focus, Line.Node_Position.offside(name)) 219 220 def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink = 221 new Hyperlink { 222 def follow(view: View): Unit = goto_file(focus, view, pos) 223 override def toString: String = "file " + quote(pos.name) 224 } 225 226 def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink = 227 model match { 228 case file_model: File_Model => 229 val pos = 230 try { file_model.node_position(offset) } 231 catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } 232 hyperlink_file(focus, pos) 233 case buffer_model: Buffer_Model => 234 new Hyperlink { 235 def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset) 236 override def toString: String = "buffer " + quote(model.node_name.node) 237 } 238 } 239 240 def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset) 241 : Option[Hyperlink] = 242 { 243 for (name <- PIDE.resources.source_file(source_name)) yield { 244 def hyperlink(pos: Line.Position) = 245 hyperlink_file(focus, Line.Node_Position(name, pos)) 246 247 if (offset > 0) { 248 PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { 249 case Some(text) => 250 hyperlink( 251 (Line.Position.zero /: 252 (Symbol.iterator(text). 253 zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))) 254 case None => 255 hyperlink(Line.Position((line1 - 1) max 0)) 256 } 257 } 258 else hyperlink(Line.Position((line1 - 1) max 0)) 259 } 260 } 261 262 override def hyperlink_command( 263 focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) 264 : Option[Hyperlink] = 265 { 266 if (snapshot.is_outdated) None 267 else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _)) 268 } 269 270 def is_hyperlink_position(snapshot: Document.Snapshot, 271 text_offset: Text.Offset, pos: Position.T): Boolean = 272 { 273 pos match { 274 case Position.Item_Id(id, range) if range.start > 0 => 275 snapshot.find_command(id) match { 276 case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => 277 node.command_start(command) match { 278 case Some(start) => text_offset == start + command.chunk.decode(range.start) 279 case None => false 280 } 281 case _ => false 282 } 283 case _ => false 284 } 285 } 286 287 def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) 288 : Option[Hyperlink] = 289 pos match { 290 case Position.Item_File(name, line, range) => 291 hyperlink_source_file(focus, name, line, range.start) 292 case Position.Item_Id(id, range) => 293 hyperlink_command(focus, snapshot, id, range.start) 294 case _ => None 295 } 296 297 def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) 298 : Option[Hyperlink] = 299 pos match { 300 case Position.Item_Def_File(name, line, range) => 301 hyperlink_source_file(focus, name, line, range.start) 302 case Position.Item_Def_Id(id, range) => 303 hyperlink_command(focus, snapshot, id, range.start) 304 case _ => None 305 } 306 307 308 /* dispatcher thread */ 309 310 override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body) 311 override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body) 312 override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body) 313 override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body) 314} 315