diff --git a/src/Pure/PIDE/session.scala b/src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala +++ b/src/Pure/PIDE/session.scala @@ -1,753 +1,756 @@ /* Title: Pure/PIDE/session.scala Author: Makarius Options: :folding=explicit: PIDE editor session, potentially with running prover process. */ package isabelle import scala.collection.immutable.Queue import scala.collection.mutable import scala.annotation.tailrec object Session { /* outlets */ object Consumer { def apply[A](name: String)(consume: A => Unit): Consumer[A] = new Consumer[A](name, consume) } final class Consumer[-A] private(val name: String, val consume: A => Unit) class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) { private val consumers = Synchronized[List[Consumer[A]]](Nil) def += (c: Consumer[A]): Unit = consumers.change(Library.update(c)) def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c)) def post(a: A): Unit = { for (c <- consumers.value.iterator) { dispatcher.send(() => try { c.consume(a) } catch { case exn: Throwable => Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.message(exn)) }) } } } /* change */ sealed case class Change( previous: Document.Version, syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name], version: Document.Version) case object Change_Flush /* events */ //{{{ case class Command_Timing(props: Properties.T) case class Theory_Timing(props: Properties.T) case class Runtime_Statistics(props: Properties.T) case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String) case class Commands_Changed( assignment: Boolean, nodes: Set[Document.Node.Name], commands: Set[Command]) sealed abstract class Phase { def print: String = this match { case Terminated(result) => if (result.ok) "finished" else "failed" case _ => Word.lowercase(this.toString) } } case object Inactive extends Phase // stable case object Startup extends Phase // transient case object Ready extends Phase // metastable case object Shutdown extends Phase // transient case class Terminated(result: Process_Result) extends Phase // stable //}}} /* syslog */ - private[Session] class Syslog(limit: Int) { - private var queue = Queue.empty[XML.Elem] + class Syslog(limit: Int) { + private var queue = Queue.empty[String] private var length = 0 - def += (msg: XML.Elem): Unit = synchronized { + def += (msg: String): Unit = synchronized { queue = queue.enqueue(msg) length += 1 if (length > limit) queue = queue.dequeue._2 } - def content: String = synchronized { - cat_lines(queue.iterator.map(XML.content)) + + def content(): String = synchronized { + cat_lines(queue.iterator) + (if (length > limit) "\n(A total of " + length + " messages...)" else "") } + + override def toString: String = "Syslog(" + length + ")" } /* protocol handlers */ type Protocol_Function = Prover.Protocol_Output => Boolean type Protocol_Functions = List[(String, Protocol_Function)] abstract class Protocol_Handler extends Isabelle_System.Service { def init(session: Session): Unit = {} def exit(): Unit = {} def functions: Protocol_Functions = Nil def prover_options(options: Options): Options = options } } class Session(_session_options: => Options, val resources: Resources) extends Document.Session { session => val init_time: Time = Time.now() val cache: Term.Cache = Term.Cache.make() def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none /* global flags */ @volatile var timing: Boolean = false @volatile var verbose: Boolean = false /* dynamic session options */ def session_options: Options = _session_options def output_delay: Time = session_options.seconds("editor_output_delay") def consolidate_delay: Time = session_options.seconds("editor_consolidate_delay") def prune_delay: Time = session_options.seconds("editor_prune_delay") def prune_size: Int = session_options.int("editor_prune_size") def syslog_limit: Int = session_options.int("editor_syslog_limit") def reparse_limit: Int = session_options.int("editor_reparse_limit") /* dispatcher */ private val dispatcher = Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true } def assert_dispatcher[A](body: => A): A = { assert(dispatcher.check_thread()) body } def require_dispatcher[A](body: => A): A = { require(dispatcher.check_thread(), "not on dispatcher thread") body } def send_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread()) body else dispatcher.send(() => body) } def send_wait_dispatcher(body: => Unit): Unit = { if (dispatcher.check_thread()) body else dispatcher.send_wait(() => body) } /* outlets */ val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher) val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) val commands_changed = new Session.Outlet[Session.Commands_Changed](dispatcher) val phase_changed = new Session.Outlet[Session.Phase](dispatcher) val syslog_messages = new Session.Outlet[Prover.Output](dispatcher) val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher) val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher) val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher) val all_messages = new Session.Outlet[Prover.Message](dispatcher) // potential bottle-neck! /** main protocol manager **/ /* internal messages */ private case class Start(start_prover: Prover.Receiver => Prover) private case object Stop private case class Get_State(promise: Promise[Document.State]) private case class Cancel_Exec(exec_id: Document_ID.Exec) private case class Protocol_Command_Raw(name: String, args: List[Bytes]) private case class Protocol_Command_Args(name: String, args: List[String]) private case class Update_Options(options: Options) private case object Consolidate_Execution private case object Prune_History /* phase */ private def post_phase(new_phase: Session.Phase): Session.Phase = { phase_changed.post(new_phase) new_phase } private val _phase = Synchronized[Session.Phase](Session.Inactive) private def phase_=(new_phase: Session.Phase): Unit = _phase.change(_ => post_phase(new_phase)) def phase: Session.Phase = _phase.value def is_ready: Boolean = phase == Session.Ready /* syslog */ - private val syslog = new Session.Syslog(syslog_limit) - def syslog_content(): String = syslog.content + def make_syslog(): Session.Syslog = new Session.Syslog(syslog_limit) + + val syslog: Session.Syslog = make_syslog() /* pipelined change parsing */ private case class Text_Edits( previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], consolidate: List[Document.Node.Name], version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) true } /* buffered changes */ private object change_buffer { private var assignment: Boolean = false private var nodes: Set[Document.Node.Name] = Set.empty private var commands: Set[Command] = Set.empty def flush(): Unit = synchronized { if (assignment || nodes.nonEmpty || commands.nonEmpty) commands_changed.post(Session.Commands_Changed(assignment, nodes, commands)) if (nodes.nonEmpty) consolidation.update(more_nodes = nodes) assignment = false nodes = Set.empty commands = Set.empty } private val delay_flush = Delay.first(output_delay) { flush() } def invoke(assign: Boolean, edited_nodes: List[Document.Node.Name], cmds: List[Command]): Unit = synchronized { assignment |= assign for (node <- edited_nodes) { nodes += node } for (command <- cmds) { nodes += command.node_name command.blobs_names.foreach(nodes += _) commands += command } delay_flush.invoke() } def shutdown(): Unit = { delay_flush.revoke() flush() } } /* postponed changes */ private object postponed_changes { private var postponed: List[Session.Change] = Nil def store(change: Session.Change): Unit = synchronized { postponed ::= change } def flush(state: Document.State): List[Session.Change] = synchronized { val (assigned, unassigned) = postponed.partition(change => state.is_assigned(change.previous)) postponed = unassigned assigned.reverse } } /* node consolidation */ private object consolidation { private val delay = Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) } private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty) private val state = Synchronized(init_state) def exit(): Unit = { delay.revoke() state.change(_ => None) } def update(more_nodes: Set[Document.Node.Name] = Set.empty): Unit = { val active = state.change_result(st => (st.isDefined, st.map(nodes => if (nodes.isEmpty) more_nodes else nodes ++ more_nodes))) if (active) delay.invoke() } def flush(): Set[Document.Node.Name] = state.change_result(st => if (st.isDefined) (st.get, init_state) else (Set.empty, None)) } /* prover process */ private object prover { private val variable = Synchronized[Option[Prover]](None) def defined: Boolean = variable.value.isDefined def get: Prover = variable.value.get def set(p: Prover): Unit = variable.change(_ => Some(p)) def reset(): Unit = variable.change(_ => None) def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None }) } /* file formats and protocol handlers */ private lazy val file_formats: File_Format.Session = File_Format.registry.start_session(session) private val protocol_handlers = Protocol_Handlers.init(session) def get_protocol_handler[C <: Session.Protocol_Handler](c: Class[C]): Option[C] = protocol_handlers.get(c.getName) match { case Some(h) if Library.is_subclass(h.getClass, c) => Some(h.asInstanceOf[C]) case _ => None } def init_protocol_handler(handler: Session.Protocol_Handler): Unit = protocol_handlers.init(handler) def prover_options(options: Options): Options = protocol_handlers.prover_options(file_formats.prover_options(options)) /* debugger */ private val debugger_handler = new Debugger.Handler(this) init_protocol_handler(debugger_handler) def debugger: Debugger = debugger_handler.debugger /* manager thread */ private lazy val delay_prune = Delay.first(prune_delay) { manager.send(Prune_History) } private val manager: Consumer_Thread[Any] = { /* global state */ val global_state = Synchronized(Document.State.init) /* raw edits */ def handle_raw_edits( doc_blobs: Document.Blobs = Document.Blobs.empty, edits: List[Document.Edit_Text] = Nil, consolidate: List[Document.Node.Name] = Nil): Unit = { //{{{ require(prover.defined, "prover process not defined (handle_raw_edits)") if (edits.nonEmpty) prover.get.discontinue_execution() val previous = global_state.value.history.tip.version val version = Future.promise[Document.Version] global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) //}}} } /* resulting changes */ def handle_change(change: Session.Change): Unit = { //{{{ require(prover.defined, "prover process not defined (handle_change)") // define commands { val id_commands = new mutable.ListBuffer[Command] def id_command(command: Command): Unit = { for { (name, digest) <- command.blobs_defined if !global_state.value.defined_blob(digest) } { change.version.nodes(name).get_blob match { case Some(blob) => global_state.change(_.define_blob(digest)) prover.get.define_blob(digest, blob.bytes) case None => Output.error_message("Missing blob " + quote(name.toString)) } } if (!global_state.value.defined_command(command.id)) { global_state.change(_.define_command(command)) id_commands += command } } for { (_, edit) <- change.doc_edits } { edit.foreach({ case (c1, c2) => c1.foreach(id_command); c2.foreach(id_command) }) } if (id_commands.nonEmpty) { prover.get.define_commands_bulk(resources, id_commands.toList) } } val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) //}}} } /* prover output */ def handle_output(output: Prover.Output): Unit = { //{{{ def bad_output(): Unit = { if (verbose) Output.warning("Ignoring bad prover output: " + output.message.toString) } def change_command(f: Document.State => (Command.State, Document.State)): Unit = { try { val st = global_state.change_result(f) if (!st.command.span.is_theory) { change_buffer.invoke(false, Nil, List(st.command)) } } catch { case _: Document.State.Fail => bad_output() } } output match { case msg: Prover.Protocol_Output => val handled = protocol_handlers.invoke(msg) if (!handled) { msg.properties match { case Protocol.Command_Timing(props, state_id, timing) if prover.defined => command_timings.post(Session.Command_Timing(props)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, cache.elem(message), cache)) case Markup.Theory_Timing(props) => theory_timings.post(Session.Theory_Timing(props)) case Markup.Task_Statistics(props) => task_statistics.post(Session.Task_Statistics(props)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val entry = Export.make_entry(Sessions.DRAFT, args, msg.chunk, cache) change_command(_.add_export(id, (args.serial, entry))) case Protocol.Loading_Theory(node_name, id) => val blobs_info = build_blobs_info(node_name) try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) } catch { case _: Document.State.Fail => bad_output() } case List(Markup.Commands_Accepted.THIS) => msg.text match { case Protocol.Commands_Accepted(ids) => ids.foreach(id => change_command(_.accumulate(id, Protocol.Commands_Accepted.message, cache))) case _ => bad_output() } case List(Markup.Assign_Update.THIS) => msg.text match { case Protocol.Assign_Update(id, edited, update) => try { val (edited_nodes, cmds) = global_state.change_result(_.assign(id, edited, update)) change_buffer.invoke(true, edited_nodes, cmds) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } delay_prune.invoke() case List(Markup.Removed_Versions.THIS) => msg.text match { case Protocol.Removed(removed) => try { global_state.change(_.removed_versions(removed)) manager.send(Session.Change_Flush) } catch { case _: Document.State.Fail => bad_output() } case _ => bad_output() } case _ => bad_output() } } case _ => output.properties match { case Position.Id(state_id) => change_command(_.accumulate(state_id, output.message, cache)) case _ if output.is_init => val init_ok = try { Isabelle_System.make_services(classOf[Session.Protocol_Handler]) .foreach(init_protocol_handler) true } catch { case exn: Throwable => prover.get.protocol_command("Prover.stop", "1", Exn.message(exn)) false } if (init_ok) { prover.get.options(prover_options(session_options)) prover.get.init_session(resources) phase = Session.Ready debugger.ready() } case Markup.Process_Result(result) if output.is_exit => if (prover.defined) protocol_handlers.exit() for (id <- global_state.value.theories.keys) { val snapshot = global_state.change_result(_.end_theory(id)) finished_theories.post(snapshot) } file_formats.stop_session phase = Session.Terminated(result) prover.reset() case _ => raw_output_messages.post(output) } } //}}} } /* main thread */ Consumer_Thread.fork[Any]("Session.manager", daemon = true) { case arg: Any => //{{{ arg match { case output: Prover.Output => if (output.is_syslog) { - syslog += output.message + syslog += XML.content(output.message) syslog_messages.post(output) } if (output.is_stdout || output.is_stderr) raw_output_messages.post(output) else handle_output(output) all_messages.post(output) case input: Prover.Input => all_messages.post(input) case Start(start_prover) if !prover.defined => prover.set(start_prover(manager.send(_))) case Stop => consolidation.exit() delay_prune.revoke() if (prover.defined) { global_state.change(_ => Document.State.init) prover.get.terminate() } case Get_State(promise) => promise.fulfill(global_state.value) case Consolidate_Execution => if (prover.defined) { val state = global_state.value state.stable_tip_version match { case None => consolidation.update() case Some(version) => val consolidate = consolidation.flush().iterator.filter(name => !resources.session_base.loaded_theory(name) && !state.node_consolidated(version, name) && state.node_maybe_consolidated(version, name)).toList if (consolidate.nonEmpty) handle_raw_edits(consolidate = consolidate) } } case Prune_History => if (prover.defined) { val old_versions = global_state.change_result(_.remove_versions(prune_size)) if (old_versions.nonEmpty) prover.get.remove_versions(old_versions) } case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(prover_options(options)) handle_raw_edits() } global_options.post(Session.Global_Options(options)) case Cancel_Exec(exec_id) if prover.defined => prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) case Protocol_Command_Raw(name, args) if prover.defined => prover.get.protocol_command_raw(name, args) case Protocol_Command_Args(name, args) if prover.defined => prover.get.protocol_command_args(name, args) case change: Session.Change if prover.defined => val state = global_state.value if (!state.removing_versions && state.is_assigned(change.previous)) handle_change(change) else postponed_changes.store(change) case Session.Change_Flush if prover.defined => val state = global_state.value if (!state.removing_versions) postponed_changes.flush(state).foreach(handle_change) case bad => if (verbose) Output.warning("Ignoring bad message: " + bad.toString) } true //}}} } } /* main operations */ def get_state(): Document.State = { if (manager.is_active()) { val promise = Future.promise[Document.State] manager.send_wait(Get_State(promise)) promise.join } else Document.State.init } def snapshot(name: Document.Node.Name = Document.Node.Name.empty, pending_edits: List[Text.Edit] = Nil): Document.Snapshot = get_state().snapshot(name, pending_edits) def recent_syntax(name: Document.Node.Name): Outer_Syntax = get_state().recent_finished.version.get_finished.nodes(name).syntax getOrElse resources.session_base.overall_syntax @tailrec final def await_stable_snapshot(): Document.Snapshot = { val snapshot = this.snapshot() if (snapshot.is_outdated) { output_delay.sleep() await_stable_snapshot() } else snapshot } def start(start_prover: Prover.Receiver => Prover): Unit = { file_formats _phase.change( { case Session.Inactive => manager.send(Start(start_prover)) post_phase(Session.Startup) case phase => error("Cannot start prover in phase " + quote(phase.print)) }) } def stop(): Process_Result = { val was_ready = _phase.guarded_access( { case Session.Startup | Session.Shutdown => None case Session.Terminated(_) => Some((false, phase)) case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) case Session.Ready => Some((true, post_phase(Session.Shutdown))) }) if (was_ready) manager.send(Stop) prover.await_reset() change_parser.shutdown() change_buffer.shutdown() manager.shutdown() dispatcher.shutdown() phase match { case Session.Terminated(result) => result case phase => error("Bad session phase after shutdown: " + quote(phase.print)) } } def protocol_command_raw(name: String, args: List[Bytes]): Unit = manager.send(Protocol_Command_Raw(name, args)) def protocol_command_args(name: String, args: List[String]): Unit = manager.send(Protocol_Command_Args(name, args)) def protocol_command(name: String, args: String*): Unit = protocol_command_args(name, args.toList) def cancel_exec(exec_id: Document_ID.Exec): Unit = manager.send(Cancel_Exec(exec_id)) def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit = if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) def update_options(options: Options): Unit = manager.send_wait(Update_Options(options)) def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit = manager.send(Session.Dialog_Result(id, serial, result)) } diff --git a/src/Pure/System/isabelle_process.scala b/src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala +++ b/src/Pure/System/isabelle_process.scala @@ -1,80 +1,80 @@ /* Title: Pure/System/isabelle_process.scala Author: Makarius Isabelle process wrapper. */ package isabelle import java.util.{Map => JMap} import java.io.{File => JFile} object Isabelle_Process { def start( session: Session, options: Options, sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", raw_ml_system: Boolean = false, use_prelude: List[String] = Nil, eval_main: String = "", modes: List[String] = Nil, cwd: JFile = null, env: JMap[String, String] = Isabelle_System.settings() ): Isabelle_Process = { val channel = System_Channel() val process = try { val channel_options = options.string.update("system_channel_address", channel.address). string.update("system_channel_password", channel.password) ML_Process(channel_options, sessions_structure, store, logic = logic, raw_ml_system = raw_ml_system, use_prelude = use_prelude, eval_main = eval_main, modes = modes, cwd = cwd, env = env) } catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } val isabelle_process = new Isabelle_Process(session, process) process.stdin.close() session.start(receiver => new Prover(receiver, session.cache, channel, process)) isabelle_process } } class Isabelle_Process private(session: Session, process: Bash.Process) { private val startup = Future.promise[String] private val terminated = Future.promise[Process_Result] session.phase_changed += Session.Consumer(getClass.getName) { case Session.Ready => startup.fulfill("") case Session.Terminated(result) => if (!result.ok && !startup.is_finished) { - val syslog = session.syslog_content() + val syslog = session.syslog.content() val err = "Session startup failed" + (if (syslog.isEmpty) "" else ":\n" + syslog) startup.fulfill(err) } terminated.fulfill(result) case _ => } def await_startup(): Isabelle_Process = startup.join match { case "" => this case err => session.stop(); error(err) } def await_shutdown(): Process_Result = { val result = terminated.join session.stop() result } def terminate(): Unit = process.terminate() } diff --git a/src/Tools/jEdit/src/main_plugin.scala b/src/Tools/jEdit/src/main_plugin.scala --- a/src/Tools/jEdit/src/main_plugin.scala +++ b/src/Tools/jEdit/src/main_plugin.scala @@ -1,482 +1,482 @@ /* Title: Tools/jEdit/src/main_plugin.scala Author: Makarius Main plumbing for PIDE infrastructure as jEdit plugin. */ package isabelle.jedit import isabelle._ import javax.swing.JOptionPane import java.io.{File => JFile} import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager} import org.gjt.sp.jedit.textarea.JEditTextArea import org.gjt.sp.jedit.syntax.ModeProvider import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged, ViewUpdate} import org.gjt.sp.util.SyntaxUtilities import org.gjt.sp.util.Log object PIDE { /* semantic document content */ def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now { val buffer = JEdit_Lib.jedit_view(view).getBuffer Document_Model.get(buffer).map(_.snapshot()) } def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now { val text_area = JEdit_Lib.jedit_view(view).getTextArea Document_View.get(text_area).map(_.get_rendering()) } def snapshot(view: View = null): Document.Snapshot = maybe_snapshot(view) getOrElse error("No document model for current buffer") def rendering(view: View = null): JEdit_Rendering = maybe_rendering(view) getOrElse error("No document view for current text area") /* plugin instance */ @volatile var _plugin: Main_Plugin = null def plugin: Main_Plugin = if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin") else _plugin def options: JEdit_Options = plugin.options def resources: JEdit_Resources = plugin.resources def session: Session = plugin.session object editor extends JEdit_Editor } class Main_Plugin extends EBPlugin { /* options */ private var _options: JEdit_Options = null private def init_options(): Unit = _options = new JEdit_Options(Options.init()) def options: JEdit_Options = _options /* resources */ private var _resources: JEdit_Resources = null private def init_resources(): Unit = _resources = JEdit_Resources(options.value) def resources: JEdit_Resources = _resources /* session */ private var _session: Session = null private def init_session(): Unit = _session = new Session(options.value, resources) def session: Session = _session /* misc support */ val completion_history = new Completion.History_Variable val spell_checker = new Spell_Checker_Variable /* global changes */ def options_changed(): Unit = { session.global_options.post(Session.Global_Options(options.value)) delay_load.invoke() } def deps_changed(): Unit = { delay_load.invoke() } /* theory files */ lazy val delay_init: Delay = Delay.last(options.seconds("editor_load_delay"), gui = true) { init_models() } private val delay_load_active = Synchronized(false) private def delay_load_activated(): Boolean = delay_load_active.guarded_access(a => Some((!a, true))) private def delay_load_action(): Unit = { if (JEdit_Options.continuous_checking() && delay_load_activated() && PerspectiveManager.isPerspectiveEnabled) { if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke() else { val required_files = { val models = Document_Model.get_models() val thys = (for ((node_name, model) <- models.iterator if model.is_theory) yield (node_name, Position.none)).toList val thy_files1 = resources.dependencies(thys).theories val thy_files2 = (for { (name, _) <- models.iterator thy_name <- resources.make_theory_name(name) } yield thy_name).toList val aux_files = if (options.bool("jedit_auto_resolve")) { val stable_tip_version = if (models.forall(p => p._2.is_stable)) session.get_state().stable_tip_version else None stable_tip_version match { case Some(version) => resources.undefined_blobs(version.nodes) case None => delay_load.invoke(); Nil } } else Nil (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt) } if (required_files.nonEmpty) { try { Isabelle_Thread.fork(name = "resolve_dependencies") { val loaded_files = for { name <- required_files text <- resources.read_file_content(name) } yield (name, text) GUI_Thread.later { try { Document_Model.provide_files(session, loaded_files) delay_init.invoke() } finally { delay_load_active.change(_ => false) } } } } catch { case _: Throwable => delay_load_active.change(_ => false) } } else delay_load_active.change(_ => false) } } } private lazy val delay_load = Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() } private def file_watcher_action(changed: Set[JFile]): Unit = if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated() lazy val file_watcher: File_Watcher = File_Watcher(file_watcher_action, options.seconds("editor_load_delay")) /* session phase */ val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit") { case Session.Terminated(result) if !result.ok => GUI_Thread.later { GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error", - "Isabelle Syslog", GUI.scrollable_text(session.syslog_content())) + "Isabelle Syslog", GUI.scrollable_text(session.syslog.content())) } case Session.Ready if !shutting_down.value => init_models() if (!JEdit_Options.continuous_checking()) { GUI_Thread.later { val answer = GUI.confirm_dialog(jEdit.getActiveView, "Continuous checking of PIDE document", JOptionPane.YES_NO_OPTION, "Continuous checking is presently disabled:", "editor buffers will remain inactive!", "Enable continuous checking now?") if (answer == 0) JEdit_Options.continuous_checking.set() } } delay_load.invoke() case Session.Shutdown => GUI_Thread.later { delay_load.revoke() delay_init.revoke() PIDE.editor.shutdown() exit_models(JEdit_Lib.jedit_buffers().toList) } case _ => } /* document model and view */ def exit_models(buffers: List[Buffer]): Unit = { GUI_Thread.now { buffers.foreach(buffer => JEdit_Lib.buffer_lock(buffer) { JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) Document_Model.exit(buffer) }) } } def init_models(): Unit = { GUI_Thread.now { PIDE.editor.flush() for { buffer <- JEdit_Lib.jedit_buffers() if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED) } { if (buffer.isLoaded) { JEdit_Lib.buffer_lock(buffer) { val node_name = resources.node_name(buffer) val model = Document_Model.init(session, node_name, buffer) for { text_area <- JEdit_Lib.jedit_text_areas(buffer) if !Document_View.get(text_area).map(_.model).contains(model) } Document_View.init(model, text_area) } } else delay_init.invoke() } PIDE.editor.invoke_generated() } } def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { Document_Model.get(buffer) match { case Some(model) => Document_View.init(model, text_area) case None => } } } def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit = GUI_Thread.now { JEdit_Lib.buffer_lock(buffer) { Document_View.exit(text_area) } } /* main plugin plumbing */ @volatile private var startup_failure: Option[Throwable] = None @volatile private var startup_notified = false private def init_editor(view: View): Unit = { Keymap_Merge.check_dialog(view) Session_Build.check_dialog(view) } private def init_title(view: View): Unit = { val title = proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") + "/" + PIDE.resources.session_base.session_name val marker = "\u200B" val old_title = view.getViewConfig.title if (old_title == null || old_title.startsWith(marker)) { view.setUserTitle(marker + title) } } override def handleMessage(message: EBMessage): Unit = { GUI_Thread.assert {} if (startup_failure.isDefined && !startup_notified) { message match { case _: EditorStarted => GUI.error_dialog(null, "Isabelle plugin startup failure", GUI.scrollable_text(Exn.message(startup_failure.get)), "Prover IDE inactive!") startup_notified = true case _ => } } if (startup_failure.isEmpty) { message match { case _: EditorStarted => if (resources.session_errors.nonEmpty) { GUI.warning_dialog(jEdit.getActiveView, "Bad session structure: may cause problems with theory imports", GUI.scrollable_text(cat_lines(resources.session_errors))) } jEdit.propertiesChanged() val view = jEdit.getActiveView() init_editor(view) PIDE.editor.hyperlink_position(true, Document.Snapshot.init, JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view)) case msg: ViewUpdate if msg.getWhat == ViewUpdate.CREATED && msg.getView != null => init_title(msg.getView) case msg: BufferUpdate if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING => if (msg.getBuffer != null) { exit_models(List(msg.getBuffer)) PIDE.editor.invoke_generated() } case msg: BufferUpdate if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED => if (session.is_ready) { delay_init.invoke() delay_load.invoke() } case msg: EditPaneUpdate if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || msg.getWhat == EditPaneUpdate.CREATED || msg.getWhat == EditPaneUpdate.DESTROYED => val edit_pane = msg.getEditPane val buffer = edit_pane.getBuffer val text_area = edit_pane.getTextArea if (buffer != null && text_area != null) { if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || msg.getWhat == EditPaneUpdate.CREATED) { if (session.is_ready) init_view(buffer, text_area) } else { Isabelle.dismissed_popups(text_area.getView) exit_view(buffer, text_area) } if (msg.getWhat == EditPaneUpdate.CREATED) Completion_Popup.Text_Area.init(text_area) if (msg.getWhat == EditPaneUpdate.DESTROYED) Completion_Popup.Text_Area.exit(text_area) } case _: PropertiesChanged => for { view <- JEdit_Lib.jedit_views() edit_pane <- JEdit_Lib.jedit_edit_panes(view) } { val buffer = edit_pane.getBuffer val text_area = edit_pane.getTextArea if (buffer != null && text_area != null) init_view(buffer, text_area) } spell_checker.update(options.value) session.update_options(options.value) case _ => } } } /* mode provider */ private var orig_mode_provider: ModeProvider = null private var pide_mode_provider: ModeProvider = null def init_mode_provider(): Unit = { orig_mode_provider = ModeProvider.instance if (orig_mode_provider.isInstanceOf[ModeProvider]) { pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider) ModeProvider.instance = pide_mode_provider } } def exit_mode_provider(): Unit = { if (ModeProvider.instance == pide_mode_provider) ModeProvider.instance = orig_mode_provider } /* HTTP server */ val http_root: String = "/" + UUID.random().toString val http_server: HTTP.Server = HTTP.server(services = Document_Model.Preview_Service :: HTTP.isabelle_services) /* start and stop */ private val shutting_down = Synchronized(false) override def start(): Unit = { /* strict initialization */ init_options() init_resources() init_session() PIDE._plugin = this /* non-strict initialization */ try { completion_history.load() spell_checker.update(options.value) JEdit_Lib.jedit_views().foreach(init_title) Syntax_Style.set_extender(Syntax_Style.Main_Extender) init_mode_provider() JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init) http_server.start() startup_failure = None } catch { case exn: Throwable => startup_failure = Some(exn) startup_notified = false Log.log(Log.ERROR, this, exn) } shutting_down.change(_ => false) val view = jEdit.getActiveView() if (view != null) init_editor(view) } override def stop(): Unit = { http_server.stop() Syntax_Style.set_extender(Syntax_Style.Base_Extender) exit_mode_provider() JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit) if (startup_failure.isEmpty) { options.value.save_prefs() completion_history.value.save() } exit_models(JEdit_Lib.jedit_buffers().toList) shutting_down.change(_ => true) session.stop() file_watcher.shutdown() PIDE.editor.shutdown() Document_Model.reset() } } diff --git a/src/Tools/jEdit/src/syslog_dockable.scala b/src/Tools/jEdit/src/syslog_dockable.scala --- a/src/Tools/jEdit/src/syslog_dockable.scala +++ b/src/Tools/jEdit/src/syslog_dockable.scala @@ -1,43 +1,43 @@ /* Title: Tools/jEdit/src/syslog_dockable.scala Author: Makarius Dockable window for syslog. */ package isabelle.jedit import isabelle._ import scala.swing.{TextArea, ScrollPane} import org.gjt.sp.jedit.View class Syslog_Dockable(view: View, position: String) extends Dockable(view, position) { /* GUI components */ private val syslog = new TextArea() private def syslog_delay = Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { - val text = PIDE.session.syslog_content() + val text = PIDE.session.syslog.content() if (text != syslog.text) syslog.text = text } set_content(new ScrollPane(syslog)) /* main */ private val main = Session.Consumer[Prover.Output](getClass.getName) { case _ => syslog_delay.invoke() } override def init(): Unit = { PIDE.session.syslog_messages += main syslog_delay.invoke() } override def exit(): Unit = { PIDE.session.syslog_messages -= main } }