src/Tools/jEdit/src/active.scala
author wenzelm
Thu Jul 18 20:53:22 2013 +0200 (2013-07-18 ago)
changeset 52697 6fb98a20c349
parent 52531 21f8e0e151f5
child 53497 07bb77881b8d
permissions -rw-r--r--
explicit padding on command boundary for "auto" generated sendback -- do not replace the corresponding goal command, but append to it;
wenzelm@50450
     1
/*  Title:      Tools/jEdit/src/active.scala
wenzelm@49492
     2
    Author:     Makarius
wenzelm@49492
     3
wenzelm@50450
     4
Active areas within the document.
wenzelm@49492
     5
*/
wenzelm@49492
     6
wenzelm@49492
     7
package isabelle.jedit
wenzelm@49492
     8
wenzelm@49492
     9
wenzelm@49492
    10
import isabelle._
wenzelm@49492
    11
wenzelm@49493
    12
import org.gjt.sp.jedit.View
wenzelm@49492
    13
wenzelm@49492
    14
wenzelm@50450
    15
object Active
wenzelm@49492
    16
{
wenzelm@50450
    17
  def action(view: View, text: String, elem: XML.Elem)
wenzelm@49492
    18
  {
wenzelm@49492
    19
    Swing_Thread.require()
wenzelm@49492
    20
wenzelm@49492
    21
    Document_View(view.getTextArea) match {
wenzelm@49492
    22
      case Some(doc_view) =>
wenzelm@49492
    23
        doc_view.rich_text_area.robust_body() {
wenzelm@50215
    24
          val text_area = doc_view.text_area
wenzelm@49492
    25
          val model = doc_view.model
wenzelm@49492
    26
          val buffer = model.buffer
wenzelm@49492
    27
          val snapshot = model.snapshot()
wenzelm@49493
    28
wenzelm@52697
    29
          def try_replace_command(padding: Boolean, exec_id: Document_ID.Exec, s: String)
wenzelm@50452
    30
          {
wenzelm@50452
    31
            snapshot.state.execs.get(exec_id).map(_.command) match {
wenzelm@50452
    32
              case Some(command) =>
wenzelm@50452
    33
                snapshot.node.command_start(command) match {
wenzelm@50452
    34
                  case Some(start) =>
wenzelm@50452
    35
                    JEdit_Lib.buffer_edit(buffer) {
wenzelm@52697
    36
                      val range = command.proper_range + start
wenzelm@52697
    37
                      if (padding) {
wenzelm@52697
    38
                        val pad =
wenzelm@52697
    39
                          JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
wenzelm@52697
    40
                            match {
wenzelm@52697
    41
                              case None => ""
wenzelm@52697
    42
                              case Some(s) => if (Symbol.is_blank(s)) "" else " "
wenzelm@52697
    43
                            }
wenzelm@52697
    44
                        buffer.insert(start + range.length, pad + s)
wenzelm@52697
    45
                      }
wenzelm@52697
    46
                      else {
wenzelm@52697
    47
                        buffer.remove(start, range.length)
wenzelm@52697
    48
                        buffer.insert(start, s)
wenzelm@52697
    49
                      }
wenzelm@50452
    50
                    }
wenzelm@50452
    51
                  case None =>
wenzelm@50452
    52
                }
wenzelm@50452
    53
              case None =>
wenzelm@50452
    54
            }
wenzelm@50452
    55
          }
wenzelm@50452
    56
wenzelm@50164
    57
          if (!snapshot.is_outdated) {
wenzelm@50715
    58
            // FIXME avoid hard-wired stuff
wenzelm@50715
    59
wenzelm@50450
    60
            elem match {
wenzelm@50715
    61
              case XML.Elem(Markup(Markup.BROWSER, _), body) =>
wenzelm@50715
    62
                default_thread_pool.submit(() =>
wenzelm@50715
    63
                  {
wenzelm@50715
    64
                    val graph_file = File.tmp_file("graph")
wenzelm@50715
    65
                    File.write(graph_file, XML.content(body))
wenzelm@50715
    66
                    Isabelle_System.bash_env(null,
wenzelm@50715
    67
                      Map("GRAPH_FILE" -> Isabelle_System.posix_path(graph_file)),
wenzelm@50715
    68
                      "\"$ISABELLE_TOOL\" browser -c \"$GRAPH_FILE\" &")
wenzelm@50715
    69
                  })
wenzelm@50715
    70
wenzelm@50715
    71
              case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
wenzelm@50452
    72
                default_thread_pool.submit(() =>
wenzelm@50452
    73
                  {
wenzelm@50452
    74
                    val graph =
wenzelm@50452
    75
                      Exn.capture {
wenzelm@50452
    76
                        isabelle.graphview.Model.decode_graph(body)
wenzelm@50452
    77
                          .transitive_reduction_acyclic
wenzelm@50452
    78
                      }
wenzelm@50452
    79
                    Swing_Thread.later { Graphview_Dockable(view, snapshot, graph) }
wenzelm@50452
    80
                  })
wenzelm@50450
    81
wenzelm@50500
    82
              case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
wenzelm@50500
    83
                props match {
wenzelm@50500
    84
                  case Position.Id(exec_id) =>
wenzelm@52697
    85
                    try_replace_command(props.exists(_ == Markup.PADDING_COMMAND), exec_id, text)
wenzelm@50500
    86
                  case _ =>
wenzelm@50500
    87
                    if (props.exists(_ == Markup.PADDING_LINE))
wenzelm@50500
    88
                      Isabelle.insert_line_padding(text_area, text)
wenzelm@50500
    89
                    else text_area.setSelectedText(text)
wenzelm@50500
    90
                }
wenzelm@50500
    91
wenzelm@52081
    92
              case Protocol.Dialog(id, serial, result) =>
wenzelm@52081
    93
                model.session.dialog_result(id, serial, result)
wenzelm@52081
    94
wenzelm@50215
    95
              case _ =>
wenzelm@50164
    96
            }
wenzelm@49492
    97
          }
wenzelm@49492
    98
        }
wenzelm@49492
    99
      case None =>
wenzelm@49492
   100
    }
wenzelm@49492
   101
  }
wenzelm@49492
   102
}
wenzelm@49492
   103