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