# HG changeset patch # User wenzelm # Date 1353873572 -3600 # Node ID 788c8263e6342a94744a43290032b7672dd48a76 # Parent daeb1674fb9180703b0ea49217083492dbfd0530 renamed main plugin object to PIDE; diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/document_model.scala --- 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) { diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/document_view.scala --- 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 => diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/graphview_dockable.scala --- 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 } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/info_dockable.scala --- 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() } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/isabelle_actions.scala --- 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 */ diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/isabelle_logic.scala --- 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 } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/isabelle_options.scala --- 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) } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/isabelle_sidekick.scala --- 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 = { diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/output_dockable.scala --- 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() } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/plugin.scala --- 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() } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/pretty_text_area.scala --- 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) } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/protocol_dockable.scala --- 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 } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/raw_output_dockable.scala --- 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 } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/rendering.scala --- 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 => diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/scala_console.scala --- 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) diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/session_dockable.scala --- 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 } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/symbols_dockable.scala --- 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) diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/syslog_dockable.scala --- 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 } } diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/text_overview.scala --- 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 diff -r daeb1674fb91 -r 788c8263e634 src/Tools/jEdit/src/token_markup.scala --- 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)))