--- a/src/Tools/jEdit/src/document_model.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Sun Nov 25 20:59:32 2012 +0100
@@ -68,7 +68,7 @@
Swing_Thread.require()
JEdit_Lib.buffer_lock(buffer) {
Exn.capture {
- Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
+ PIDE.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
} match {
case Exn.Res(header) => header
case Exn.Exn(exn) => Document.Node.bad_header(Exn.message(exn))
@@ -86,7 +86,7 @@
Swing_Thread.require()
Text.Perspective(
for {
- doc_view <- Isabelle.document_views(buffer)
+ doc_view <- PIDE.document_views(buffer)
range <- doc_view.perspective().ranges
} yield range)
}
@@ -115,8 +115,7 @@
}
private val delay_flush =
- Swing_Thread.delay_last(
- Time.seconds(Isabelle.options.real("editor_input_delay"))) { flush() }
+ Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) { flush() }
def +=(edit: Text.Edit)
{
--- a/src/Tools/jEdit/src/document_view.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/document_view.scala Sun Nov 25 20:59:32 2012 +0100
@@ -67,7 +67,7 @@
{
private val session = model.session
- def get_rendering(): Rendering = Rendering(model.snapshot(), Isabelle.options.value)
+ def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _, false)
@@ -147,7 +147,7 @@
/* caret handling */
private val delay_caret_update =
- Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
+ Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
session.caret_focus.event(Session.Caret_Focus)
}
@@ -161,8 +161,7 @@
private object overview extends Text_Overview(this)
{
val delay_repaint =
- Swing_Thread.delay_first(
- Time.seconds(Isabelle.options.real("editor_update_delay"))) { repaint() }
+ Swing_Thread.delay_first(Time.seconds(PIDE.options.real("editor_update_delay"))) { repaint() }
}
@@ -173,8 +172,7 @@
react {
case _: Session.Raw_Edits =>
Swing_Thread.later {
- overview.delay_repaint.postpone(
- Time.seconds(Isabelle.options.real("editor_input_delay")))
+ overview.delay_repaint.postpone(Time.seconds(PIDE.options.real("editor_input_delay")))
}
case changed: Session.Commands_Changed =>
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -45,7 +45,7 @@
new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
- val rendering = Rendering(snapshot, Isabelle.options.value)
+ val rendering = Rendering(snapshot, PIDE.options.value)
new Pretty_Tooltip(view, parent, rendering, x, y, body)
null
}
@@ -123,9 +123,9 @@
{
Swing_Thread.require()
- Isabelle.session.global_options += main_actor
- Isabelle.session.commands_changed += main_actor
- Isabelle.session.caret_focus += main_actor
+ PIDE.session.global_options += main_actor
+ PIDE.session.commands_changed += main_actor
+ PIDE.session.caret_focus += main_actor
handle_update(do_update, None)
}
@@ -133,8 +133,8 @@
{
Swing_Thread.require()
- Isabelle.session.global_options -= main_actor
- Isabelle.session.commands_changed -= main_actor
- Isabelle.session.caret_focus -= main_actor
+ PIDE.session.global_options -= main_actor
+ PIDE.session.commands_changed -= main_actor
+ PIDE.session.caret_focus -= main_actor
}
}
--- a/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -76,8 +76,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Isabelle.font_family(),
- (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(PIDE.font_family(),
+ (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
}
@@ -98,7 +98,7 @@
Swing_Thread.require()
JEdit_Lib.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
- Isabelle.session.global_options += main_actor
+ PIDE.session.global_options += main_actor
handle_resize()
}
@@ -107,7 +107,7 @@
Swing_Thread.require()
JEdit_Lib.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
- Isabelle.session.global_options -= main_actor
+ PIDE.session.global_options -= main_actor
delay_resize.revoke()
}
@@ -116,7 +116,7 @@
private val delay_resize =
Swing_Thread.delay_first(
- Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
+ Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/isabelle_actions.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_actions.scala Sun Nov 25 20:59:32 2012 +0100
@@ -35,13 +35,13 @@
def check_buffer(buffer: Buffer)
{
- Isabelle.document_model(buffer) match {
+ PIDE.document_model(buffer) match {
case None =>
case Some(model) => model.full_perspective()
}
}
- def cancel_execution() { Isabelle.session.cancel_execution() }
+ def cancel_execution() { PIDE.session.cancel_execution() }
/* control styles */
--- a/src/Tools/jEdit/src/isabelle_logic.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_logic.scala Sun Nov 25 20:59:32 2012 +0100
@@ -42,13 +42,13 @@
val title = "Logic"
def load: Unit =
{
- val logic = Isabelle.options.string(opt_name)
+ val logic = PIDE.options.string(opt_name)
entries.find(_.name == logic) match {
case Some(entry) => selection.item = entry
case None =>
}
}
- def save: Unit = Isabelle.options.string(opt_name) = selection.item.name
+ def save: Unit = PIDE.options.string(opt_name) = selection.item.name
}
component.load()
@@ -56,7 +56,7 @@
component.listenTo(component.selection)
component.reactions += { case SelectionChanged(_) => component.save() }
}
- component.tooltip = Isabelle.options.value.check_name(opt_name).print_default
+ component.tooltip = PIDE.options.value.check_name(opt_name).print_default
component
}
@@ -64,7 +64,7 @@
{
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
val logic =
- Isabelle.options.string(opt_name) match {
+ PIDE.options.string(opt_name) match {
case "" => default_logic()
case logic => logic
}
--- a/src/Tools/jEdit/src/isabelle_options.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Nov 25 20:59:32 2012 +0100
@@ -47,10 +47,10 @@
"editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
"editor_tracing_limit", "editor_update_delay")
- relevant_options.foreach(Isabelle.options.value.check_name _)
+ relevant_options.foreach(PIDE.options.value.check_name _)
protected val components =
- Isabelle.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
+ PIDE.options.make_components(List(Isabelle_Logic.logic_selector(false)), relevant_options)
}
@@ -59,12 +59,12 @@
// FIXME avoid hard-wired stuff
private val predefined =
(for {
- (name, opt) <- Isabelle.options.value.options.toList
+ (name, opt) <- PIDE.options.value.options.toList
if (name.endsWith("_color") && opt.section == "Rendering of Document Content")
- } yield Isabelle.options.make_color_component(opt))
+ } yield PIDE.options.make_color_component(opt))
assert(!predefined.isEmpty)
- protected val components = Isabelle.options.make_components(predefined, _ => false)
+ protected val components = PIDE.options.make_components(predefined, _ => false)
}
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Sun Nov 25 20:59:32 2012 +0100
@@ -177,7 +177,7 @@
class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
- "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
+ "isabelle", PIDE.get_recent_syntax, JEdit_Lib.buffer_node_name)
class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
@@ -188,8 +188,7 @@
"isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
-class Isabelle_Sidekick_Raw
- extends Isabelle_Sidekick("isabelle-raw", Isabelle.get_recent_syntax)
+class Isabelle_Sidekick_Raw extends Isabelle_Sidekick("isabelle-raw", PIDE.get_recent_syntax)
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
--- a/src/Tools/jEdit/src/output_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -47,8 +47,8 @@
{
Swing_Thread.require()
- pretty_text_area.resize(Isabelle.font_family(),
- (Isabelle.font_size("jedit_font_scale") * zoom_factor / 100).round)
+ pretty_text_area.resize(PIDE.font_family(),
+ (PIDE.font_size("jedit_font_scale") * zoom_factor / 100).round)
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]])
@@ -116,9 +116,9 @@
{
Swing_Thread.require()
- Isabelle.session.global_options += main_actor
- Isabelle.session.commands_changed += main_actor
- Isabelle.session.caret_focus += main_actor
+ PIDE.session.global_options += main_actor
+ PIDE.session.commands_changed += main_actor
+ PIDE.session.caret_focus += main_actor
handle_update(true, None)
}
@@ -126,9 +126,9 @@
{
Swing_Thread.require()
- Isabelle.session.global_options -= main_actor
- Isabelle.session.commands_changed -= main_actor
- Isabelle.session.caret_focus -= main_actor
+ PIDE.session.global_options -= main_actor
+ PIDE.session.commands_changed -= main_actor
+ PIDE.session.caret_focus -= main_actor
delay_resize.revoke()
}
@@ -137,7 +137,7 @@
private val delay_resize =
Swing_Thread.delay_first(
- Time.seconds(Isabelle.options.real("editor_update_delay"))) { handle_resize() }
+ Time.seconds(PIDE.options.real("editor_update_delay"))) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
--- a/src/Tools/jEdit/src/plugin.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Sun Nov 25 20:59:32 2012 +0100
@@ -24,7 +24,7 @@
import scala.actors.Actor._
-object Isabelle
+object PIDE
{
/* plugin instance */
@@ -149,7 +149,7 @@
/* theory files */
private lazy val delay_load =
- Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_load_delay")))
+ Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_load_delay")))
{
val view = jEdit.getActiveView()
@@ -159,13 +159,13 @@
buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
val thys =
- for (buffer <- buffers; model <- Isabelle.document_model(buffer))
+ for (buffer <- buffers; model <- PIDE.document_model(buffer))
yield model.name
- val thy_info = new Thy_Info(Isabelle.thy_load)
+ val thy_info = new Thy_Info(PIDE.thy_load)
// FIXME avoid I/O in Swing thread!?!
val files = thy_info.dependencies(true, thys).deps.map(_._1.node).
- filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file))
+ filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file))
if (!files.isEmpty) {
val files_list = new ListView(files.sorted)
@@ -199,16 +199,16 @@
case Session.Failed =>
Swing_Thread.later {
Library.error_dialog(jEdit.getActiveView, "Prover process failure",
- "Isabelle Syslog", Library.scrollable_text(Isabelle.session.current_syslog()))
+ "Isabelle Syslog", Library.scrollable_text(PIDE.session.current_syslog()))
}
case Session.Ready =>
- Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
- JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
+ PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
+ JEdit_Lib.jedit_buffers.foreach(PIDE.init_model)
Swing_Thread.later { delay_load.invoke() }
case Session.Shutdown =>
- JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
+ JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
Swing_Thread.later { delay_load.revoke() }
case _ =>
@@ -225,28 +225,28 @@
{
Swing_Thread.assert()
- if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) {
+ if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) {
message match {
case msg: EditorStarted =>
Library.error_dialog(null, "Isabelle plugin startup failure",
- Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)),
+ Library.scrollable_text(Exn.message(PIDE.startup_failure.get)),
"Prover IDE inactive!")
- Isabelle.startup_notified = true
+ PIDE.startup_notified = true
case _ =>
}
}
- if (Isabelle.startup_failure.isEmpty) {
+ if (PIDE.startup_failure.isEmpty) {
message match {
case msg: EditorStarted =>
- if (Isabelle.options.bool("jedit_auto_start"))
- Isabelle.session.start(Isabelle_Logic.session_args())
+ if (PIDE.options.bool("jedit_auto_start"))
+ PIDE.session.start(Isabelle_Logic.session_args())
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
- if (Isabelle.session.is_ready) {
+ if (PIDE.session.is_ready) {
val buffer = msg.getBuffer
- if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
+ if (buffer != null && !buffer.isLoading) PIDE.init_model(buffer)
Swing_Thread.later { delay_load.invoke() }
}
@@ -262,14 +262,14 @@
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED) {
- if (Isabelle.session.is_ready)
- Isabelle.init_view(buffer, text_area)
+ if (PIDE.session.is_ready)
+ PIDE.init_view(buffer, text_area)
}
- else Isabelle.exit_view(buffer, text_area)
+ else PIDE.exit_view(buffer, text_area)
}
case msg: PropertiesChanged =>
- Isabelle.session.global_options.event(Session.Global_Options(Isabelle.options.value))
+ PIDE.session.global_options.event(Session.Global_Options(PIDE.options.value))
case _ =>
}
@@ -279,12 +279,12 @@
override def start()
{
try {
- Isabelle.plugin = this
+ PIDE.plugin = this
Isabelle_System.init()
Isabelle_System.install_fonts()
val init_options = Options.init()
- Swing_Thread.now { Isabelle.options.update(init_options) }
+ Swing_Thread.now { PIDE.options.update(init_options) }
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
if (ModeProvider.instance.isInstanceOf[ModeProvider])
@@ -293,28 +293,28 @@
val content = Isabelle_Logic.session_content(false)
val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax)
- Isabelle.session = new Session(thy_load) {
- override def output_delay = Time.seconds(Isabelle.options.real("editor_output_delay"))
- override def reparse_limit = Isabelle.options.int("editor_reparse_limit")
+ PIDE.session = new Session(thy_load) {
+ override def output_delay = Time.seconds(PIDE.options.real("editor_output_delay"))
+ override def reparse_limit = PIDE.options.int("editor_reparse_limit")
}
- Isabelle.session.phase_changed += session_manager
- Isabelle.startup_failure = None
+ PIDE.session.phase_changed += session_manager
+ PIDE.startup_failure = None
}
catch {
case exn: Throwable =>
- Isabelle.startup_failure = Some(exn)
- Isabelle.startup_notified = false
+ PIDE.startup_failure = Some(exn)
+ PIDE.startup_notified = false
}
}
override def stop()
{
- if (Isabelle.startup_failure.isEmpty)
- Isabelle.options.value.save_prefs()
+ if (PIDE.startup_failure.isEmpty)
+ PIDE.options.value.save_prefs()
- Isabelle.session.phase_changed -= session_manager
- JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
- Isabelle.session.stop()
+ PIDE.session.phase_changed -= session_manager
+ JEdit_Lib.jedit_buffers.foreach(PIDE.exit_model)
+ PIDE.session.stop()
}
}
--- a/src/Tools/jEdit/src/pretty_text_area.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sun Nov 25 20:59:32 2012 +0100
@@ -25,7 +25,7 @@
(String, Rendering) =
{
val (text, state) = Pretty_Text_Area.document_state(base_snapshot, formatted_body)
- val rendering = Rendering(state.snapshot(), Isabelle.options.value)
+ val rendering = Rendering(state.snapshot(), PIDE.options.value)
(text, rendering)
}
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sun Nov 25 20:59:32 2012 +0100
@@ -68,8 +68,8 @@
val pretty_text_area = new Pretty_Text_Area(view)
pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
- pretty_text_area.resize(Isabelle.font_family(),
- Isabelle.font_size("jedit_tooltip_font_scale").round)
+ pretty_text_area.resize(PIDE.font_family(),
+ PIDE.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, body)
pretty_text_area.registerKeyboardAction(action_listener, "close_all",
@@ -106,7 +106,7 @@
{
val font_metrics = pretty_text_area.getPainter.getFontMetrics
- val margin = Isabelle.options.int("jedit_tooltip_margin") // FIXME via rendering?!
+ val margin = PIDE.options.int("jedit_tooltip_margin") // FIXME via rendering?!
val lines =
XML.traverse_text(Pretty.formatted(body, margin, Pretty.font_metric(font_metrics)))(0)(
(n: Int, s: String) => n + s.iterator.filter(_ == '\n').length)
--- a/src/Tools/jEdit/src/protocol_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/protocol_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -39,6 +39,6 @@
}
}
- override def init() { Isabelle.session.all_messages += main_actor }
- override def exit() { Isabelle.session.all_messages -= main_actor }
+ override def init() { PIDE.session.all_messages += main_actor }
+ override def exit() { PIDE.session.all_messages -= main_actor }
}
--- a/src/Tools/jEdit/src/raw_output_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -37,6 +37,6 @@
}
}
- override def init() { Isabelle.session.raw_output_messages += main_actor }
- override def exit() { Isabelle.session.raw_output_messages -= main_actor }
+ override def init() { PIDE.session.raw_output_messages += main_actor }
+ override def exit() { PIDE.session.raw_output_messages -= main_actor }
}
--- a/src/Tools/jEdit/src/rendering.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sun Nov 25 20:59:32 2012 +0100
@@ -205,7 +205,7 @@
{
case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
- val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+ val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
Text.Info(snapshot.convert(info_range), Hyperlink(jedit_file, 0, 0)) :: links
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _)))
@@ -304,7 +304,7 @@
add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
if Path.is_ok(name) =>
- val jedit_file = Isabelle.thy_load.append(snapshot.node_name.dir, Path.explode(name))
+ val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
add(prev, r, (true, XML.Text("file " + quote(jedit_file))))
case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
if name == Markup.SORTING || name == Markup.TYPING =>
--- a/src/Tools/jEdit/src/scala_console.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/scala_console.scala Sun Nov 25 20:59:32 2012 +0100
@@ -124,7 +124,7 @@
interp.setContextClassLoader
interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
interp.bind("console", "console.Console", console)
- interp.interpret("import isabelle.jedit.Isabelle")
+ interp.interpret("import isabelle.jedit.PIDE")
interpreters += (console -> interp)
}
@@ -139,9 +139,9 @@
out.print(null,
"This shell evaluates Isabelle/Scala expressions.\n\n" +
"The following special toplevel bindings are provided:\n" +
- " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
- " console -- jEdit Console plugin\n" +
- " Isabelle -- Isabelle plugin (e.g. Isabelle.session, Isabelle.document_model)\n")
+ " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
+ " console -- jEdit Console plugin\n" +
+ " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.document_model)\n")
}
override def printPrompt(console: Console, out: Output)
--- a/src/Tools/jEdit/src/session_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -41,7 +41,7 @@
/* controls */
- private val session_phase = new Label(Isabelle.session.phase.toString)
+ private val session_phase = new Label(PIDE.session.phase.toString)
session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
session_phase.tooltip = "Prover status"
@@ -89,10 +89,10 @@
var end = size.width - insets.right
for {
(n, color) <- List(
- (st.unprocessed, Isabelle.options.color_value("unprocessed1_color")),
- (st.running, Isabelle.options.color_value("running_color")),
- (st.warned, Isabelle.options.color_value("warning_color")),
- (st.failed, Isabelle.options.color_value("error_color"))) }
+ (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
+ (st.running, PIDE.options.color_value("running_color")),
+ (st.warned, PIDE.options.color_value("warning_color")),
+ (st.failed, PIDE.options.color_value("error_color"))) }
{
gfx.setColor(color)
val v = (n * w / st.total) max (if (n > 0) 2 else 0)
@@ -121,7 +121,7 @@
private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
{
Swing_Thread.now {
- val snapshot = Isabelle.session.snapshot()
+ val snapshot = PIDE.session.snapshot()
val iterator =
restriction match {
@@ -130,7 +130,7 @@
}
val nodes_status1 =
(nodes_status /: iterator)({ case (status, (name, node)) =>
- if (Isabelle.thy_load.loaded_theories(name.theory)) status
+ if (PIDE.thy_load.loaded_theories(name.theory)) status
else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
if (nodes_status != nodes_status1) {
@@ -161,15 +161,15 @@
override def init()
{
- Isabelle.session.phase_changed += main_actor; handle_phase(Isabelle.session.phase)
- Isabelle.session.global_options += main_actor
- Isabelle.session.commands_changed += main_actor; handle_update()
+ PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
+ PIDE.session.global_options += main_actor
+ PIDE.session.commands_changed += main_actor; handle_update()
}
override def exit()
{
- Isabelle.session.phase_changed -= main_actor
- Isabelle.session.global_options -= main_actor
- Isabelle.session.commands_changed -= main_actor
+ PIDE.session.phase_changed -= main_actor
+ PIDE.session.global_options -= main_actor
+ PIDE.session.commands_changed -= main_actor
}
}
--- a/src/Tools/jEdit/src/symbols_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -24,7 +24,7 @@
private class Symbol_Component(val symbol: String) extends Button
{
private val decoded = Symbol.decode(symbol)
- private val font_size = Isabelle.font_size("jedit_font_scale").round
+ private val font_size = PIDE.font_size("jedit_font_scale").round
font =
Symbol.fonts.get(symbol) match {
@@ -71,8 +71,8 @@
add(results_panel, BorderPanel.Position.Center)
listenTo(search)
val delay_search =
- Swing_Thread.delay_last(Time.seconds(Isabelle.options.real("editor_input_delay"))) {
- val max_results = Isabelle.options.int("jedit_symbols_search_limit") max 0
+ Swing_Thread.delay_last(Time.seconds(PIDE.options.real("editor_input_delay"))) {
+ val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
results_panel.contents.clear
val results =
(searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)
--- a/src/Tools/jEdit/src/syslog_dockable.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/syslog_dockable.scala Sun Nov 25 20:59:32 2012 +0100
@@ -24,7 +24,7 @@
private def update_syslog()
{
Swing_Thread.later {
- val text = Isabelle.session.current_syslog()
+ val text = PIDE.session.current_syslog()
if (text != syslog.text) syslog.text = text
}
}
@@ -47,12 +47,12 @@
override def init()
{
- Isabelle.session.syslog_messages += main_actor
+ PIDE.session.syslog_messages += main_actor
update_syslog()
}
override def exit()
{
- Isabelle.session.syslog_messages -= main_actor
+ PIDE.session.syslog_messages -= main_actor
}
}
--- a/src/Tools/jEdit/src/text_overview.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala Sun Nov 25 20:59:32 2012 +0100
@@ -54,7 +54,7 @@
private var cached_colors: List[(Color, Int, Int)] = Nil
private var last_snapshot = Document.State.init.snapshot()
- private var last_options = Isabelle.options.value
+ private var last_options = PIDE.options.value
private var last_relevant_range = Text.Range(0)
private var last_line_count = 0
private var last_char_count = 0
--- a/src/Tools/jEdit/src/token_markup.scala Sun Nov 25 20:31:49 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala Sun Nov 25 20:59:32 2012 +0100
@@ -265,7 +265,7 @@
/* mode provider */
private val markers = Map(
- "isabelle" -> new Token_Markup.Marker(true, Isabelle.get_recent_syntax()),
+ "isabelle" -> new Token_Markup.Marker(true, PIDE.get_recent_syntax()),
"isabelle-options" -> new Token_Markup.Marker(false, Some(Options.options_syntax)),
"isabelle-root" -> new Token_Markup.Marker(false, Some(Build.root_syntax)))