src/Tools/jEdit/src/jedit/TheoryView.scala

 
 class TheoryView (text_area: JEditTextArea)
     extends TextAreaExtension with Text with BufferListener {
 
   private val buffer = text_area.getBuffer
+  private val prover = Isabelle.prover_setup(buffer).get.prover
   buffer.addBufferListener(this)
 
 
   private var col: Text.Changed = null
 

 
   col_timer.stop
   col_timer.setRepeats(true)
 
 
-  private val phase_overview = new PhaseOverviewPanel(Isabelle.prover(buffer))
+  private val phase_overview = new PhaseOverviewPanel(prover)
 
 
   /* activation */
 
   Isabelle.plugin.font_changed += (_ => update_font())

     }
   }
 
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
-      val cmd = Isabelle.prover(buffer).document.getNextCommandContaining(e.getDot)
+      val cmd = prover.document.getNextCommandContaining(e.getDot)
       if (cmd != null && cmd.start <= e.getDot &&
-          Isabelle.prover_setup(buffer).selected_state != cmd)
-        Isabelle.prover_setup(buffer).selected_state = cmd
+          Isabelle.prover_setup(buffer).get.selected_state != cmd)
+        Isabelle.prover_setup(buffer).get.selected_state = cmd
     }
   }
 
   def activate() = {
     text_area.addCaretListener(selected_state_controller)

 
 
   /* painting */
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint_all())
-  Isabelle.prover(buffer).command_info += (_ => repaint_delay.delay_or_ignore())
+  prover.command_info += (_ => repaint_delay.delay_or_ignore())
 
   private def from_current(pos: Int) =
     if (col != null && col.start <= pos)
       if (pos < col.start + col.added) col.start
       else pos - col.added + col.removed

     if (text_area != null && status != Command.Status.REMOVE && status != Command.Status.REMOVED) {
       val start = text_area.getLineOfOffset(to_current(cmd.start))
       val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
       text_area.invalidateLineRange(start, stop)
 
-      if (Isabelle.prover_setup(buffer).selected_state == cmd)
-        Isabelle.prover_setup(buffer).selected_state = cmd  // update State view
+      if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
+        Isabelle.prover_setup(buffer).get.selected_state = cmd  // update State view
     }
   }
 
   def repaint_all() =
   {

     screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) =
   {
     val saved_color = gfx.getColor
 
     val metrics = text_area.getPainter.getFontMetrics
-    var e = Isabelle.prover(buffer).document.getNextCommandContaining(from_current(start))
+    var e = prover.document.getNextCommandContaining(from_current(start))
 
     // encolor phase
     while (e != null && to_current(e.start) < end) {
       val begin = start max to_current(e.start)
       val finish = end - 1 min to_current(e.stop)