renamed main plugin object to PIDE;
authorwenzelm
Sun Nov 25 20:59:32 2012 +0100 (2012-11-25)
changeset 50205788c8263e634
parent 50204 daeb1674fb91
child 50206 6626bc5ed053
renamed main plugin object to PIDE;
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/graphview_dockable.scala
src/Tools/jEdit/src/info_dockable.scala
src/Tools/jEdit/src/isabelle_actions.scala
src/Tools/jEdit/src/isabelle_logic.scala
src/Tools/jEdit/src/isabelle_options.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/output_dockable.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/protocol_dockable.scala
src/Tools/jEdit/src/raw_output_dockable.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/scala_console.scala
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/syslog_dockable.scala
src/Tools/jEdit/src/text_overview.scala
src/Tools/jEdit/src/token_markup.scala
     1.1 --- a/src/Tools/jEdit/src/document_model.scala	Sun Nov 25 20:31:49 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_model.scala	Sun Nov 25 20:59:32 2012 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4      Swing_Thread.require()
     1.5      JEdit_Lib.buffer_lock(buffer) {
     1.6        Exn.capture {
     1.7 -        Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
     1.8 +        PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
     1.9        } match {
    1.10          case Exn.Res(header) => header
    1.11          case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
    1.12 @@ -86,7 +86,7 @@
    1.13      Swing_Thread.require()
    1.14      Text.Perspective(
    1.15        for {
    1.16 -        doc_view <- Isabelle.document_views(buffer)
    1.17 +        doc_view <- PIDE.document_views(buffer)
    1.18          range <- doc_view.perspective().ranges
    1.19        } yield range)
    1.20    }
    1.21 @@ -115,8 +115,7 @@
    1.22      }
    1.23  
    1.24      private val delay_flush =
    1.25 -      Swing_Thread.delay_last(
    1.26 -        Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() }
    1.27 +      Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) { flush() }
    1.28  
    1.29      def +=(edit: Text.Edit)
    1.30      {
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 20:31:49 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Nov 25 20:59:32 2012 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4  {
     2.5    private val session = model.session
     2.6  
     2.7 -  def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value)
     2.8 +  def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
     2.9  
    2.10    val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
    2.11  
    2.12 @@ -147,7 +147,7 @@
    2.13    /* caret handling */
    2.14  
    2.15    private val delay_caret_update =
    2.16 -    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
    2.17 +    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
    2.18        session.caret_focus.event(Session.Caret_Focus)
    2.19      }
    2.20  
    2.21 @@ -161,8 +161,7 @@
    2.22    private object overview extends Text_Overview(this)
    2.23    {
    2.24      val delay_repaint =
    2.25 -      Swing_Thread.delay_first(
    2.26 -        Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
    2.27 +      Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
    2.28    }
    2.29  
    2.30  
    2.31 @@ -173,8 +172,7 @@
    2.32        react {
    2.33          case _: Session.Raw_Edits =>
    2.34            Swing_Thread.later {
    2.35 -            overview.delay_repaint.postpone(
    2.36 -              Time.seconds(Isabelle.options.real("editor_input_delay")))
    2.37 +            overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
    2.38            }
    2.39  
    2.40          case changed: Session.Commands_Changed =>
     3.1 --- a/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     3.3 @@ -45,7 +45,7 @@
     3.4        new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
     3.5          override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
     3.6          {
     3.7 -          val rendering = Rendering(snapshot, Isabelle.options.value)
     3.8 +          val rendering = Rendering(snapshot, PIDE.options.value)
     3.9            new Pretty_Tooltip(view, parent, rendering, x, y, body)
    3.10            null
    3.11          }
    3.12 @@ -123,9 +123,9 @@
    3.13    {
    3.14      Swing_Thread.require()
    3.15  
    3.16 -    Isabelle.session.global_options += main_actor
    3.17 -    Isabelle.session.commands_changed += main_actor
    3.18 -    Isabelle.session.caret_focus += main_actor
    3.19 +    PIDE.session.global_options += main_actor
    3.20 +    PIDE.session.commands_changed += main_actor
    3.21 +    PIDE.session.caret_focus += main_actor
    3.22      handle_update(do_update, None)
    3.23    }
    3.24  
    3.25 @@ -133,8 +133,8 @@
    3.26    {
    3.27      Swing_Thread.require()
    3.28  
    3.29 -    Isabelle.session.global_options -= main_actor
    3.30 -    Isabelle.session.commands_changed -= main_actor
    3.31 -    Isabelle.session.caret_focus -= main_actor
    3.32 +    PIDE.session.global_options -= main_actor
    3.33 +    PIDE.session.commands_changed -= main_actor
    3.34 +    PIDE.session.caret_focus -= main_actor
    3.35    }
    3.36  }
     4.1 --- a/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/info_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     4.3 @@ -76,8 +76,8 @@
     4.4    {
     4.5      Swing_Thread.require()
     4.6  
     4.7 -    pretty_text_area.resize(Isabelle.font_family(),
     4.8 -      (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
     4.9 +    pretty_text_area.resize(PIDE.font_family(),
    4.10 +      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
    4.11    }
    4.12  
    4.13  
    4.14 @@ -98,7 +98,7 @@
    4.15      Swing_Thread.require()
    4.16  
    4.17      JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
    4.18 -    Isabelle.session.global_options += main_actor
    4.19 +    PIDE.session.global_options += main_actor
    4.20      handle_resize()
    4.21    }
    4.22  
    4.23 @@ -107,7 +107,7 @@
    4.24      Swing_Thread.require()
    4.25  
    4.26      JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
    4.27 -    Isabelle.session.global_options -= main_actor
    4.28 +    PIDE.session.global_options -= main_actor
    4.29      delay_resize.revoke()
    4.30    }
    4.31  
    4.32 @@ -116,7 +116,7 @@
    4.33  
    4.34    private val delay_resize =
    4.35      Swing_Thread.delay_first(
    4.36 -      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
    4.37 +      Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
    4.38  
    4.39    addComponentListener(new ComponentAdapter {
    4.40      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
     5.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 20:31:49 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 20:59:32 2012 +0100
     5.3 @@ -35,13 +35,13 @@
     5.4  
     5.5    def check_buffer(buffer: Buffer)
     5.6    {
     5.7 -    Isabelle.document_model(buffer) match {
     5.8 +    PIDE.document_model(buffer) match {
     5.9        case None =>
    5.10        case Some(model) => model.full_perspective()
    5.11      }
    5.12    }
    5.13  
    5.14 -  def cancel_execution() { Isabelle.session.cancel_execution() }
    5.15 +  def cancel_execution() { PIDE.session.cancel_execution() }
    5.16  
    5.17  
    5.18    /* control styles */
     6.1 --- a/src/Tools/jEdit/src/isabelle_logic.scala	Sun Nov 25 20:31:49 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle_logic.scala	Sun Nov 25 20:59:32 2012 +0100
     6.3 @@ -42,13 +42,13 @@
     6.4        val title = "Logic"
     6.5        def load: Unit =
     6.6        {
     6.7 -        val logic = Isabelle.options.string(opt_name)
     6.8 +        val logic = PIDE.options.string(opt_name)
     6.9          entries.find(_.name == logic) match {
    6.10            case Some(entry) => selection.item = entry
    6.11            case None =>
    6.12          }
    6.13        }
    6.14 -      def save: Unit = Isabelle.options.string(opt_name) = selection.item.name
    6.15 +      def save: Unit = PIDE.options.string(opt_name) = selection.item.name
    6.16      }
    6.17  
    6.18      component.load()
    6.19 @@ -56,7 +56,7 @@
    6.20        component.listenTo(component.selection)
    6.21        component.reactions += { case SelectionChanged(_) => component.save() }
    6.22      }
    6.23 -    component.tooltip = Isabelle.options.value.check_name(opt_name).print_default
    6.24 +    component.tooltip = PIDE.options.value.check_name(opt_name).print_default
    6.25      component
    6.26    }
    6.27  
    6.28 @@ -64,7 +64,7 @@
    6.29    {
    6.30      val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
    6.31      val logic =
    6.32 -      Isabelle.options.string(opt_name) match {
    6.33 +      PIDE.options.string(opt_name) match {
    6.34          case "" => default_logic()
    6.35          case logic => logic
    6.36        }
     7.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 25 20:31:49 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Sun Nov 25 20:59:32 2012 +0100
     7.3 @@ -47,10 +47,10 @@
     7.4        "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
     7.5        "editor_tracing_limit", "editor_update_delay")
     7.6  
     7.7 -  relevant_options.foreach(Isabelle.options.value.check_name _)
     7.8 +  relevant_options.foreach(PIDE.options.value.check_name _)
     7.9  
    7.10    protected val components =
    7.11 -    Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
    7.12 +    PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
    7.13  }
    7.14  
    7.15  
    7.16 @@ -59,12 +59,12 @@
    7.17    // FIXME avoid hard-wired stuff
    7.18    private val predefined =
    7.19      (for {
    7.20 -      (name, opt) <- Isabelle.options.value.options.toList
    7.21 +      (name, opt) <- PIDE.options.value.options.toList
    7.22        if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
    7.23 -    } yield Isabelle.options.make_color_component(opt))
    7.24 +    } yield PIDE.options.make_color_component(opt))
    7.25  
    7.26    assert(!predefined.isEmpty)
    7.27  
    7.28 -  protected val components = Isabelle.options.make_components(predefined, _ => false)
    7.29 +  protected val components = PIDE.options.make_components(predefined, _ => false)
    7.30  }
    7.31  
     8.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Nov 25 20:31:49 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Nov 25 20:59:32 2012 +0100
     8.3 @@ -177,7 +177,7 @@
     8.4  
     8.5  
     8.6  class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
     8.7 -  "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
     8.8 +  "isabelle", PIDE.get_recent_syntax, JEdit_Lib.buffer_node_name)
     8.9  
    8.10  
    8.11  class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
    8.12 @@ -188,8 +188,7 @@
    8.13    "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
    8.14  
    8.15  
    8.16 -class Isabelle_Sidekick_Raw
    8.17 -  extends Isabelle_Sidekick("isabelle-raw", Isabelle.get_recent_syntax)
    8.18 +class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
    8.19  {
    8.20    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    8.21    {
     9.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
     9.3 @@ -47,8 +47,8 @@
     9.4    {
     9.5      Swing_Thread.require()
     9.6  
     9.7 -    pretty_text_area.resize(Isabelle.font_family(),
     9.8 -      (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
     9.9 +    pretty_text_area.resize(PIDE.font_family(),
    9.10 +      (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
    9.11    }
    9.12  
    9.13    private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
    9.14 @@ -116,9 +116,9 @@
    9.15    {
    9.16      Swing_Thread.require()
    9.17  
    9.18 -    Isabelle.session.global_options += main_actor
    9.19 -    Isabelle.session.commands_changed += main_actor
    9.20 -    Isabelle.session.caret_focus += main_actor
    9.21 +    PIDE.session.global_options += main_actor
    9.22 +    PIDE.session.commands_changed += main_actor
    9.23 +    PIDE.session.caret_focus += main_actor
    9.24      handle_update(true, None)
    9.25    }
    9.26  
    9.27 @@ -126,9 +126,9 @@
    9.28    {
    9.29      Swing_Thread.require()
    9.30  
    9.31 -    Isabelle.session.global_options -= main_actor
    9.32 -    Isabelle.session.commands_changed -= main_actor
    9.33 -    Isabelle.session.caret_focus -= main_actor
    9.34 +    PIDE.session.global_options -= main_actor
    9.35 +    PIDE.session.commands_changed -= main_actor
    9.36 +    PIDE.session.caret_focus -= main_actor
    9.37      delay_resize.revoke()
    9.38    }
    9.39  
    9.40 @@ -137,7 +137,7 @@
    9.41  
    9.42    private val delay_resize =
    9.43      Swing_Thread.delay_first(
    9.44 -      Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
    9.45 +      Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
    9.46  
    9.47    addComponentListener(new ComponentAdapter {
    9.48      override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    10.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 20:31:49 2012 +0100
    10.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 20:59:32 2012 +0100
    10.3 @@ -24,7 +24,7 @@
    10.4  import scala.actors.Actor._
    10.5  
    10.6  
    10.7 -object Isabelle
    10.8 +object PIDE
    10.9  {
   10.10    /* plugin instance */
   10.11  
   10.12 @@ -149,7 +149,7 @@
   10.13    /* theory files */
   10.14  
   10.15    private lazy val delay_load =
   10.16 -    Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay")))
   10.17 +    Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_load_delay")))
   10.18      {
   10.19        val view = jEdit.getActiveView()
   10.20  
   10.21 @@ -159,13 +159,13 @@
   10.22            buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
   10.23  
   10.24          val thys =
   10.25 -          for (buffer <- buffers; model <- Isabelle.document_model(buffer))
   10.26 +          for (buffer <- buffers; model <- PIDE.document_model(buffer))
   10.27              yield model.name
   10.28  
   10.29 -        val thy_info = new Thy_Info(Isabelle.thy_load)
   10.30 +        val thy_info = new Thy_Info(PIDE.thy_load)
   10.31          // FIXME avoid I/O in Swing thread!?!
   10.32          val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
   10.33 -          filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
   10.34 +          filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
   10.35  
   10.36          if (!files.isEmpty) {
   10.37            val files_list = new ListView(files.sorted)
   10.38 @@ -199,16 +199,16 @@
   10.39              case Session.Failed =>
   10.40                Swing_Thread.later {
   10.41                  Library.error_dialog(jEdit.getActiveView, "Prover process failure",
   10.42 -                    "Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog()))
   10.43 +                    "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
   10.44                }
   10.45  
   10.46              case Session.Ready =>
   10.47 -              Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
   10.48 -              JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
   10.49 +              PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
   10.50 +              JEdit_Lib.jedit_buffers.foreach(PIDE.init_model)
   10.51                Swing_Thread.later { delay_load.invoke() }
   10.52  
   10.53              case Session.Shutdown =>
   10.54 -              JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
   10.55 +              JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
   10.56                Swing_Thread.later { delay_load.revoke() }
   10.57  
   10.58              case _ =>
   10.59 @@ -225,28 +225,28 @@
   10.60    {
   10.61      Swing_Thread.assert()
   10.62  
   10.63 -    if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) {
   10.64 +    if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
   10.65        message match {
   10.66          case msg: EditorStarted =>
   10.67            Library.error_dialog(null, "Isabelle plugin startup failure",
   10.68 -            Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)),
   10.69 +            Library.scrollable_text(Exn.message(PIDE.startup_failure.get)),
   10.70              "Prover IDE inactive!")
   10.71 -          Isabelle.startup_notified = true
   10.72 +          PIDE.startup_notified = true
   10.73          case _ =>
   10.74        }
   10.75      }
   10.76  
   10.77 -    if (Isabelle.startup_failure.isEmpty) {
   10.78 +    if (PIDE.startup_failure.isEmpty) {
   10.79        message match {
   10.80          case msg: EditorStarted =>
   10.81 -          if (Isabelle.options.bool("jedit_auto_start"))
   10.82 -            Isabelle.session.start(Isabelle_Logic.session_args())
   10.83 +          if (PIDE.options.bool("jedit_auto_start"))
   10.84 +            PIDE.session.start(Isabelle_Logic.session_args())
   10.85  
   10.86          case msg: BufferUpdate
   10.87          if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   10.88 -          if (Isabelle.session.is_ready) {
   10.89 +          if (PIDE.session.is_ready) {
   10.90              val buffer = msg.getBuffer
   10.91 -            if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
   10.92 +            if (buffer != null && !buffer.isLoading) PIDE.init_model(buffer)
   10.93              Swing_Thread.later { delay_load.invoke() }
   10.94            }
   10.95  
   10.96 @@ -262,14 +262,14 @@
   10.97            if (buffer != null && text_area != null) {
   10.98              if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
   10.99                  msg.getWhat == EditPaneUpdate.CREATED) {
  10.100 -              if (Isabelle.session.is_ready)
  10.101 -                Isabelle.init_view(buffer, text_area)
  10.102 +              if (PIDE.session.is_ready)
  10.103 +                PIDE.init_view(buffer, text_area)
  10.104              }
  10.105 -            else Isabelle.exit_view(buffer, text_area)
  10.106 +            else PIDE.exit_view(buffer, text_area)
  10.107            }
  10.108  
  10.109          case msg: PropertiesChanged =>
  10.110 -          Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
  10.111 +          PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
  10.112  
  10.113          case _ =>
  10.114        }
  10.115 @@ -279,12 +279,12 @@
  10.116    override def start()
  10.117    {
  10.118      try {
  10.119 -      Isabelle.plugin = this
  10.120 +      PIDE.plugin = this
  10.121        Isabelle_System.init()
  10.122        Isabelle_System.install_fonts()
  10.123  
  10.124        val init_options = Options.init()
  10.125 -      Swing_Thread.now { Isabelle.options.update(init_options)  }
  10.126 +      Swing_Thread.now { PIDE.options.update(init_options)  }
  10.127  
  10.128        SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
  10.129        if (ModeProvider.instance.isInstanceOf[ModeProvider])
  10.130 @@ -293,28 +293,28 @@
  10.131        val content = Isabelle_Logic.session_content(false)
  10.132        val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
  10.133  
  10.134 -      Isabelle.session = new Session(thy_load) {
  10.135 -        override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
  10.136 -        override def reparse_limit = Isabelle.options.int("editor_reparse_limit")
  10.137 +      PIDE.session = new Session(thy_load) {
  10.138 +        override def output_delay = Time.seconds(PIDE.options.real("editor_output_delay"))
  10.139 +        override def reparse_limit = PIDE.options.int("editor_reparse_limit")
  10.140        }
  10.141  
  10.142 -      Isabelle.session.phase_changed += session_manager
  10.143 -      Isabelle.startup_failure = None
  10.144 +      PIDE.session.phase_changed += session_manager
  10.145 +      PIDE.startup_failure = None
  10.146      }
  10.147      catch {
  10.148        case exn: Throwable =>
  10.149 -        Isabelle.startup_failure = Some(exn)
  10.150 -        Isabelle.startup_notified = false
  10.151 +        PIDE.startup_failure = Some(exn)
  10.152 +        PIDE.startup_notified = false
  10.153      }
  10.154    }
  10.155  
  10.156    override def stop()
  10.157    {
  10.158 -    if (Isabelle.startup_failure.isEmpty)
  10.159 -      Isabelle.options.value.save_prefs()
  10.160 +    if (PIDE.startup_failure.isEmpty)
  10.161 +      PIDE.options.value.save_prefs()
  10.162  
  10.163 -    Isabelle.session.phase_changed -= session_manager
  10.164 -    JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
  10.165 -    Isabelle.session.stop()
  10.166 +    PIDE.session.phase_changed -= session_manager
  10.167 +    JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
  10.168 +    PIDE.session.stop()
  10.169    }
  10.170  }
    11.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 25 20:31:49 2012 +0100
    11.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Nov 25 20:59:32 2012 +0100
    11.3 @@ -25,7 +25,7 @@
    11.4      (String, Rendering) =
    11.5    {
    11.6      val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
    11.7 -    val rendering = Rendering(state.snapshot(), Isabelle.options.value)
    11.8 +    val rendering = Rendering(state.snapshot(), PIDE.options.value)
    11.9      (text, rendering)
   11.10    }
   11.11  
    12.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 20:31:49 2012 +0100
    12.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Nov 25 20:59:32 2012 +0100
    12.3 @@ -68,8 +68,8 @@
    12.4  
    12.5    val pretty_text_area = new Pretty_Text_Area(view)
    12.6    pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
    12.7 -  pretty_text_area.resize(Isabelle.font_family(),
    12.8 -    Isabelle.font_size("jedit_tooltip_font_scale").round)
    12.9 +  pretty_text_area.resize(PIDE.font_family(),
   12.10 +    PIDE.font_size("jedit_tooltip_font_scale").round)
   12.11    pretty_text_area.update(rendering.snapshot, body)
   12.12  
   12.13    pretty_text_area.registerKeyboardAction(action_listener, "close_all",
   12.14 @@ -106,7 +106,7 @@
   12.15  
   12.16    {
   12.17      val font_metrics = pretty_text_area.getPainter.getFontMetrics
   12.18 -    val margin = Isabelle.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
   12.19 +    val margin = PIDE.options.int("jedit_tooltip_margin")  // FIXME via rendering?!
   12.20      val lines =
   12.21        XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
   12.22          (n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
    13.1 --- a/src/Tools/jEdit/src/protocol_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
    13.2 +++ b/src/Tools/jEdit/src/protocol_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
    13.3 @@ -39,6 +39,6 @@
    13.4      }
    13.5    }
    13.6  
    13.7 -  override def init() { Isabelle.session.all_messages += main_actor }
    13.8 -  override def exit() { Isabelle.session.all_messages -= main_actor }
    13.9 +  override def init() { PIDE.session.all_messages += main_actor }
   13.10 +  override def exit() { PIDE.session.all_messages -= main_actor }
   13.11  }
    14.1 --- a/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
    14.2 +++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
    14.3 @@ -37,6 +37,6 @@
    14.4      }
    14.5    }
    14.6  
    14.7 -  override def init() { Isabelle.session.raw_output_messages += main_actor }
    14.8 -  override def exit() { Isabelle.session.raw_output_messages -= main_actor }
    14.9 +  override def init() { PIDE.session.raw_output_messages += main_actor }
   14.10 +  override def exit() { PIDE.session.raw_output_messages -= main_actor }
   14.11  }
    15.1 --- a/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:31:49 2012 +0100
    15.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sun Nov 25 20:59:32 2012 +0100
    15.3 @@ -205,7 +205,7 @@
    15.4          {
    15.5            case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
    15.6            if Path.is_ok(name) =>
    15.7 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    15.8 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    15.9              Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
   15.10  
   15.11            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
   15.12 @@ -304,7 +304,7 @@
   15.13              add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
   15.14            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
   15.15            if Path.is_ok(name) =>
   15.16 -            val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   15.17 +            val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
   15.18              add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
   15.19            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
   15.20            if name == Markup.SORTING || name == Markup.TYPING =>
    16.1 --- a/src/Tools/jEdit/src/scala_console.scala	Sun Nov 25 20:31:49 2012 +0100
    16.2 +++ b/src/Tools/jEdit/src/scala_console.scala	Sun Nov 25 20:59:32 2012 +0100
    16.3 @@ -124,7 +124,7 @@
    16.4      interp.setContextClassLoader
    16.5      interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
    16.6      interp.bind("console", "console.Console", console)
    16.7 -    interp.interpret("import isabelle.jedit.Isabelle")
    16.8 +    interp.interpret("import isabelle.jedit.PIDE")
    16.9  
   16.10      interpreters += (console -> interp)
   16.11    }
   16.12 @@ -139,9 +139,9 @@
   16.13      out.print(null,
   16.14       "This shell evaluates Isabelle/Scala expressions.\n\n" +
   16.15       "The following special toplevel bindings are provided:\n" +
   16.16 -     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
   16.17 -     "  console   -- jEdit Console plugin\n" +
   16.18 -     "  Isabelle  -- Isabelle plugin (e.g. Isabelle.session, Isabelle.document_model)\n")
   16.19 +     "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
   16.20 +     "  console -- jEdit Console plugin\n" +
   16.21 +     "  PIDE    -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.document_model)\n")
   16.22    }
   16.23  
   16.24    override def printPrompt(console: Console, out: Output)
    17.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
    17.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
    17.3 @@ -41,7 +41,7 @@
    17.4  
    17.5    /* controls */
    17.6  
    17.7 -  private val session_phase = new Label(Isabelle.session.phase.toString)
    17.8 +  private val session_phase = new Label(PIDE.session.phase.toString)
    17.9    session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   17.10    session_phase.tooltip = "Prover status"
   17.11  
   17.12 @@ -89,10 +89,10 @@
   17.13            var end = size.width - insets.right
   17.14            for {
   17.15              (n, color) <- List(
   17.16 -              (st.unprocessed, Isabelle.options.color_value("unprocessed1_color")),
   17.17 -              (st.running, Isabelle.options.color_value("running_color")),
   17.18 -              (st.warned, Isabelle.options.color_value("warning_color")),
   17.19 -              (st.failed, Isabelle.options.color_value("error_color"))) }
   17.20 +              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
   17.21 +              (st.running, PIDE.options.color_value("running_color")),
   17.22 +              (st.warned, PIDE.options.color_value("warning_color")),
   17.23 +              (st.failed, PIDE.options.color_value("error_color"))) }
   17.24            {
   17.25              gfx.setColor(color)
   17.26              val v = (n * w / st.total) max (if (n > 0) 2 else 0)
   17.27 @@ -121,7 +121,7 @@
   17.28    private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
   17.29    {
   17.30      Swing_Thread.now {
   17.31 -      val snapshot = Isabelle.session.snapshot()
   17.32 +      val snapshot = PIDE.session.snapshot()
   17.33  
   17.34        val iterator =
   17.35          restriction match {
   17.36 @@ -130,7 +130,7 @@
   17.37          }
   17.38        val nodes_status1 =
   17.39          (nodes_status /: iterator)({ case (status, (name, node)) =>
   17.40 -            if (Isabelle.thy_load.loaded_theories(name.theory)) status
   17.41 +            if (PIDE.thy_load.loaded_theories(name.theory)) status
   17.42              else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
   17.43  
   17.44        if (nodes_status != nodes_status1) {
   17.45 @@ -161,15 +161,15 @@
   17.46  
   17.47    override def init()
   17.48    {
   17.49 -    Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
   17.50 -    Isabelle.session.global_options += main_actor
   17.51 -    Isabelle.session.commands_changed += main_actor; handle_update()
   17.52 +    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
   17.53 +    PIDE.session.global_options += main_actor
   17.54 +    PIDE.session.commands_changed += main_actor; handle_update()
   17.55    }
   17.56  
   17.57    override def exit()
   17.58    {
   17.59 -    Isabelle.session.phase_changed -= main_actor
   17.60 -    Isabelle.session.global_options -= main_actor
   17.61 -    Isabelle.session.commands_changed -= main_actor
   17.62 +    PIDE.session.phase_changed -= main_actor
   17.63 +    PIDE.session.global_options -= main_actor
   17.64 +    PIDE.session.commands_changed -= main_actor
   17.65    }
   17.66  }
    18.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
    18.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
    18.3 @@ -24,7 +24,7 @@
    18.4    private class Symbol_Component(val symbol: String) extends Button
    18.5    {
    18.6      private val decoded = Symbol.decode(symbol)
    18.7 -    private val font_size = Isabelle.font_size("jedit_font_scale").round
    18.8 +    private val font_size = PIDE.font_size("jedit_font_scale").round
    18.9  
   18.10      font =
   18.11        Symbol.fonts.get(symbol) match {
   18.12 @@ -71,8 +71,8 @@
   18.13        add(results_panel, BorderPanel.Position.Center)
   18.14        listenTo(search)
   18.15        val delay_search =
   18.16 -        Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
   18.17 -          val max_results = Isabelle.options.int("jedit_symbols_search_limit") max 0
   18.18 +        Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
   18.19 +          val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
   18.20            results_panel.contents.clear
   18.21            val results =
   18.22              (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)
    19.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Sun Nov 25 20:31:49 2012 +0100
    19.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Sun Nov 25 20:59:32 2012 +0100
    19.3 @@ -24,7 +24,7 @@
    19.4    private def update_syslog()
    19.5    {
    19.6      Swing_Thread.later {
    19.7 -      val text = Isabelle.session.current_syslog()
    19.8 +      val text = PIDE.session.current_syslog()
    19.9        if (text != syslog.text) syslog.text = text
   19.10      }
   19.11    }
   19.12 @@ -47,12 +47,12 @@
   19.13  
   19.14    override def init()
   19.15    {
   19.16 -    Isabelle.session.syslog_messages += main_actor
   19.17 +    PIDE.session.syslog_messages += main_actor
   19.18      update_syslog()
   19.19    }
   19.20  
   19.21    override def exit()
   19.22    {
   19.23 -    Isabelle.session.syslog_messages -= main_actor
   19.24 +    PIDE.session.syslog_messages -= main_actor
   19.25    }
   19.26  }
    20.1 --- a/src/Tools/jEdit/src/text_overview.scala	Sun Nov 25 20:31:49 2012 +0100
    20.2 +++ b/src/Tools/jEdit/src/text_overview.scala	Sun Nov 25 20:59:32 2012 +0100
    20.3 @@ -54,7 +54,7 @@
    20.4    private var cached_colors: List[(Color, Int, Int)] = Nil
    20.5  
    20.6    private var last_snapshot = Document.State.init.snapshot()
    20.7 -  private var last_options = Isabelle.options.value
    20.8 +  private var last_options = PIDE.options.value
    20.9    private var last_relevant_range = Text.Range(0)
   20.10    private var last_line_count = 0
   20.11    private var last_char_count = 0
    21.1 --- a/src/Tools/jEdit/src/token_markup.scala	Sun Nov 25 20:31:49 2012 +0100
    21.2 +++ b/src/Tools/jEdit/src/token_markup.scala	Sun Nov 25 20:59:32 2012 +0100
    21.3 @@ -265,7 +265,7 @@
    21.4    /* mode provider */
    21.5  
    21.6    private val markers = Map(
    21.7 -    "isabelle" -> new Token_Markup.Marker(true, Isabelle.get_recent_syntax()),
    21.8 +    "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
    21.9      "isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
   21.10      "isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))
   21.11