src/Tools/jEdit/src/isabelle.scala
changeset 52815 eaad5fe7bb1b
parent 51533 3f6280aedbcc
child 52816 c608e0ade554
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 18:08:12 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 31 19:59:14 2013 +0200
     1.3 @@ -57,6 +57,60 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  /* continuous checking */
     1.8 +
     1.9 +  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    1.10 +
    1.11 +  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
    1.12 +
    1.13 +  def continuous_checking_=(b: Boolean)
    1.14 +  {
    1.15 +    Swing_Thread.require()
    1.16 +
    1.17 +    if (continuous_checking != b) {
    1.18 +      PIDE.options.bool(CONTINUOUS_CHECKING) = b
    1.19 +      PIDE.options_changed()
    1.20 +
    1.21 +      PIDE.session.update(
    1.22 +        (List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) {
    1.23 +          case (edits, buffer) =>
    1.24 +            JEdit_Lib.buffer_lock(buffer) {
    1.25 +              PIDE.document_model(buffer) match {
    1.26 +                case Some(model) => model.flushed_edits() ::: edits
    1.27 +                case None => edits
    1.28 +              }
    1.29 +            }
    1.30 +        }
    1.31 +      )
    1.32 +    }
    1.33 +  }
    1.34 +
    1.35 +  def set_continuous_checking() { continuous_checking = true }
    1.36 +  def reset_continuous_checking() { continuous_checking = false }
    1.37 +  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    1.38 +
    1.39 +
    1.40 +  /* required document nodes */
    1.41 +
    1.42 +  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
    1.43 +  {
    1.44 +    Swing_Thread.require()
    1.45 +    PIDE.document_model(view.getBuffer) match {
    1.46 +      case Some(model) =>
    1.47 +        val b = if (toggle) !model.node_required else set
    1.48 +        if (model.node_required != b) {
    1.49 +          model.node_required = b
    1.50 +          PIDE.options_changed()
    1.51 +        }
    1.52 +      case None =>
    1.53 +    }
    1.54 +  }
    1.55 +
    1.56 +  def set_node_required(view: View) { node_required_update(view, set = true) }
    1.57 +  def reset_node_required(view: View) { node_required_update(view, set = false) }
    1.58 +  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    1.59 +
    1.60 +
    1.61    /* font size */
    1.62  
    1.63    def change_font_size(view: View, change: Int => Int)