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