diff --git a/src/Pure/System/getopts.scala b/src/Pure/System/getopts.scala --- a/src/Pure/System/getopts.scala +++ b/src/Pure/System/getopts.scala @@ -1,72 +1,72 @@ /* Title: Pure/System/getopts.scala Author: Makarius Support for command-line options as in GNU bash. */ package isabelle import scala.annotation.tailrec object Getopts { def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts = { val options = option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) { case (m, (s, f)) => val (a, entry) = - if (s.size == 1) (s(0), (false, f)) - else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f)) + if (s.length == 1) (s(0), (false, f)) + else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f)) else error("Bad option specification: " + quote(s)) if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString)) else m + (a -> entry) } new Getopts(usage_text, options) } } class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)]) { def usage(): Nothing = { Output.writeln(usage_text, stdout = true) sys.exit(1) } private def is_option(opt: Char): Boolean = options.isDefinedAt(opt) private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1 private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1 private def print_option(opt: Char): String = quote("-" + opt.toString) private def option(opt: Char, opt_arg: List[Char]): Unit = try { options(opt)._2.apply(opt_arg.mkString) } catch { case ERROR(msg) => cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt)) } @tailrec private def getopts(args: List[List[Char]]): List[List[Char]] = args match { case List('-', '-') :: rest_args => rest_args case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty => option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args) case List('-', opt) :: rest_args if is_option0(opt) => option(opt, Nil); getopts(rest_args) case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty => option(opt, opt_arg); getopts(rest_args) case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) => option(opt, opt_arg); getopts(rest_args) case List(List('-', opt)) if is_option1(opt) => Output.error_message("Command-line option " + print_option(opt) + " requires an argument") usage() case ('-' :: opt :: _) :: _ if !is_option(opt) => if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt)) usage() case _ => args } def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString) def apply(args: Array[String]): List[String] = apply(args.toList) } diff --git a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala --- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala +++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala @@ -1,305 +1,308 @@ /* Title: Tools/jEdit/src/isabelle_sidekick.scala Author: Fabian Immler, TU Munich Author: Makarius SideKick parsers for Isabelle proof documents. */ package isabelle.jedit_main import isabelle._ import isabelle.jedit._ import javax.swing.tree.DefaultMutableTreeNode import javax.swing.text.Position -import javax.swing.{JLabel, Icon} +import javax.swing.Icon import org.gjt.sp.jedit.Buffer import sidekick.{SideKickParser, SideKickParsedData, IAsset} object Isabelle_Sidekick { def int_to_pos(offset: Text.Offset): Position = - new Position { def getOffset = offset; override def toString: String = offset.toString } + new Position { + def getOffset: Text.Offset = offset + override def toString: String = offset.toString + } def root_data(buffer: Buffer): SideKickParsedData = { val data = new SideKickParsedData(buffer.getName) data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength)) data } class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset { private val css = GUI.imitate_font_css(GUI.label_font()) - protected var _name = text - protected var _start = int_to_pos(range.start) - protected var _end = int_to_pos(range.stop) + protected var _name: String = text + protected var _start: Position = int_to_pos(range.start) + protected var _end: Position = int_to_pos(range.stop) override def getIcon: Icon = null override def getShortString: String = { val n = keyword.length val s = _name.indexOf(keyword) match { case i if i >= 0 && n > 0 => HTML.output(_name.substring(0, i)) + "" + HTML.output(keyword) + "" + HTML.output(_name.substring(i + n)) case _ => HTML.output(_name) } "" + s + "" } override def getLongString: String = _name override def getName: String = _name override def setName(name: String): Unit = _name = name override def getStart: Position = _start override def setStart(start: Position): Unit = _start = start override def getEnd: Position = _end override def setEnd(end: Position): Unit = _end = end override def toString: String = _name } class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range) def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode, swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit = { for ((_, entry) <- tree.branches) { val node = swing_node(Text.Info(entry.range, entry.markup)) swing_markup_tree(entry.subtree, node, swing_node) parent.add(node) } } } class Isabelle_Sidekick(name: String) extends SideKickParser(name) { override def supportsCompletion = false /* parsing */ @volatile protected var stopped = false - override def stop() = { stopped = true } + override def stop(): Unit = { stopped = true } def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { stopped = false // FIXME lock buffer (!??) val data = Isabelle_Sidekick.root_data(buffer) val syntax = Isabelle.buffer_syntax(buffer) val ok = if (syntax.isDefined) { val ok = parser(buffer, syntax.get, data) if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true } else ok } else false if (!ok) data.root.add(new DefaultMutableTreeNode("")) data } } class Isabelle_Sidekick_Structure( name: String, node_name: Buffer => Option[Document.Node.Name], parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document]) extends Isabelle_Sidekick(name) { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { def make_tree( parent: DefaultMutableTreeNode, offset: Text.Offset, documents: List[Document_Structure.Document]): Unit = { documents.foldLeft(offset) { case (i, document) => document match { case Document_Structure.Block(name, text, body) => val range = Text.Range(i, i + document.length) val node = new DefaultMutableTreeNode( new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range)) parent.add(node) make_tree(node, i, body) case _ => } i + document.length } } node_name(buffer) match { case Some(name) => make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer))) true case None => false } } } class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name, Document_Structure.parse_sections) class Isabelle_Sidekick_Context extends Isabelle_Sidekick_Structure("isabelle-context", PIDE.resources.theory_node_name, Document_Structure.parse_blocks) class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections) class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections) class Isabelle_Sidekick_ML extends Isabelle_Sidekick_Structure("isabelle-ml", buffer => Some(PIDE.resources.node_name(buffer)), (_, _, text) => Document_Structure.parse_ml_sections(false, text)) class Isabelle_Sidekick_SML extends Isabelle_Sidekick_Structure("isabelle-sml", buffer => Some(PIDE.resources.node_name(buffer)), (_, _, text) => Document_Structure.parse_ml_sections(true, text)) class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup") { override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { val opt_snapshot = Document_Model.get(buffer) match { case Some(model) if model.is_theory => Some(model.snapshot()) case _ => None } opt_snapshot match { case Some(snapshot) => for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) { val markup = snapshot.state.command_markup( snapshot.version, command, Command.Markup_Index.markup, command.range, Markup.Elements.full) Isabelle_Sidekick.swing_markup_tree(markup, data.root, (info: Text.Info[List[XML.Elem]]) => { val range = info.range + command_start val content = command.source(info.range).replace('\n', ' ') val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString new DefaultMutableTreeNode( new Isabelle_Sidekick.Asset(command.toString, range) { override def getShortString: String = content override def getLongString: String = info_text override def toString: String = quote(content) + " " + range.toString }) }) } true case None => false } } } class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news") { private val Heading1 = """^New in (.*)\w*$""".r private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode = new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop))) override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = { var offset = 0 var end_offset = 0 var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None var start2: Option[(Int, String)] = None - def close1: Unit = + def close1(): Unit = start1 match { case Some((start_offset, s, body)) => val node = make_node(s, start_offset, end_offset) body.foreach(node.add(_)) data.root.add(node) start1 = None case None => } - def close2: Unit = + def close2(): Unit = start2 match { case Some((start_offset, s)) => start1 match { case Some((start_offset1, s1, body)) => val node = make_node(s, start_offset, end_offset) start1 = Some((start_offset1, s1, body :+ node)) case None => } start2 = None case None => } for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) { line match { - case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector())) - case Heading2(s) => close2; start2 = Some((offset, s)) + case Heading1(s) => close2(); close1(); start1 = Some((offset, s, Vector())) + case Heading2(s) => close2(); start2 = Some((offset, s)) case _ => } offset += line.length + 1 if (!line.forall(Character.isSpaceChar)) end_offset = offset } - if (!stopped) { close2; close1 } + if (!stopped) { close2(); close1() } true } } class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex") { override def supportsCompletion = false private class Asset(label: String, label_html: String, range: Text.Range, source: String) extends Isabelle_Sidekick.Asset(label, range) { override def getShortString: String = label_html override def getLongString: String = source } def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData = { val data = Isabelle_Sidekick.root_data(buffer) try { var offset = 0 for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) { val kind = chunk.kind val name = chunk.name val source = chunk.source if (kind != "") { val label = kind + (if (name == "") "" else " " + name) val label_html = "" + HTML.output(kind) + "" + (if (name == "") "" else " " + HTML.output(name)) + "" val range = Text.Range(offset, offset + source.length) val asset = new Asset(label, label_html, range, source) data.root.add(new DefaultMutableTreeNode(asset)) } offset += source.length } data } catch { case ERROR(msg) => Output.warning(msg); null } } } diff --git a/src/Tools/jEdit/jedit_main/scala_console.scala b/src/Tools/jEdit/jedit_main/scala_console.scala --- a/src/Tools/jEdit/jedit_main/scala_console.scala +++ b/src/Tools/jEdit/jedit_main/scala_console.scala @@ -1,182 +1,182 @@ /* Title: Tools/jEdit/jedit_main/scala_console.scala Author: Makarius Scala instance of Console plugin. */ package isabelle.jedit_main import isabelle._ import isabelle.jedit._ import console.{Console, ConsolePane, Shell, Output} import org.gjt.sp.jedit.JARClassLoader import java.io.{OutputStream, Writer, PrintWriter} class Scala_Console extends Shell("Scala") { /* global state -- owned by GUI thread */ @volatile private var interpreters = Map.empty[Console, Interpreter] @volatile private var global_console: Console = null @volatile private var global_out: Output = null @volatile private var global_err: Output = null private val console_stream = new OutputStream { val buf = new StringBuilder(100) override def flush(): Unit = { val s = buf.synchronized { val s = buf.toString; buf.clear(); s } val str = UTF8.decode_permissive(s) GUI_Thread.later { if (global_out == null) java.lang.System.out.print(str) else global_out.writeAttrs(null, str) } Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output } override def close(): Unit = flush() def write(byte: Int): Unit = { val c = byte.toChar buf.synchronized { buf.append(c) } if (c == '\n') flush() } } private val console_writer = new Writer { def flush(): Unit = console_stream.flush() def close(): Unit = console_stream.flush() def write(cbuf: Array[Char], off: Int, len: Int): Unit = { if (len > 0) { UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) } } } private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = { global_console = console global_out = out global_err = if (err == null) out else err try { scala.Console.withErr(console_stream) { scala.Console.withOut(console_stream) { e } } } finally { - console_stream.flush + console_stream.flush() global_console = null global_out = null global_err = null } } private def report_error(str: String): Unit = { if (global_console == null || global_err == null) isabelle.Output.writeln(str) else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } /* interpreter thread */ private abstract class Request private case class Start(console: Console) extends Request private case class Execute(console: Console, out: Output, err: Output, command: String) extends Request private class Interpreter { private val running = Synchronized[Option[Thread]](None) def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt }) private val interp = Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). interpreter( print_writer = new PrintWriter(console_writer, true), class_loader = new JARClassLoader) val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") { case Start(console) => interp.bind("view", "org.gjt.sp.jedit.View", console.getView) interp.bind("console", "console.Console", console) interp.interpret("import isabelle._; import isabelle.jedit._") true case Execute(console, out, err, command) => with_console(console, out, err) { try { running.change(_ => Some(Thread.currentThread())) interp.interpret(command) } finally { running.change(_ => None) Exn.Interrupt.dispose() } GUI_Thread.later { if (err != null) err.commandDone() out.commandDone() } true } } } /* jEdit console methods */ override def openConsole(console: Console): Unit = { val interp = new Interpreter interp.thread.send(Start(console)) interpreters += (console -> interp) } override def closeConsole(console: Console): Unit = { interpreters.get(console) match { case Some(interp) => interp.interrupt() interp.thread.shutdown() interpreters -= console case None => } } override def printInfoMessage(out: Output): Unit = { out.print(null, "This shell evaluates Isabelle/Scala expressions.\n\n" + "The contents of package isabelle and isabelle.jedit are imported.\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" + " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") } override def printPrompt(console: Console, out: Output): Unit = { out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") } override def execute( console: Console, input: String, out: Output, err: Output, command: String): Unit = { interpreters(console).thread.send(Execute(console, out, err, command)) } override def stop(console: Console): Unit = interpreters.get(console).foreach(_.interrupt()) } diff --git a/src/Tools/jEdit/src/main.scala b/src/Tools/jEdit/src/main.scala --- a/src/Tools/jEdit/src/main.scala +++ b/src/Tools/jEdit/src/main.scala @@ -1,142 +1,142 @@ /* Title: src/Tools/jEdit/src/main.scala Author: Makarius Main Isabelle application entry point. */ package isabelle.jedit import isabelle._ import org.gjt.sp.jedit.{MiscUtilities, jEdit} object Main { /* main entry point */ def main(args: Array[String]): Unit = { if (args.nonEmpty && args(0) == "-init") { Isabelle_System.init() } else { val start = { try { Isabelle_System.init() Isabelle_Fonts.init() GUI.init_lafs() /* ROOTS template */ { val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS") if (!roots.is_file) File.write(roots, """# Additional session root directories # # * each line contains one directory entry in Isabelle path notation, e.g. # # $ISABELLE_HOME/../AFP/thys # # for a copy of AFP put side-by-side to the Isabelle distribution # # * Isabelle/jEdit provides formal markup for C-hover-click and completion # # * lines starting with "#" are stripped # # * changes require restart of the Isabelle application # #:mode=text:encoding=UTF-8: #$ISABELLE_HOME/../AFP/thys """) } /* settings directory */ val settings_dir = Path.explode("$JEDIT_SETTINGS") val properties = settings_dir + Path.explode("properties") if (properties.is_file) { val props1 = split_lines(File.read(properties)) val props2 = props1.filterNot(_.startsWith("plugin-blacklist.isabelle_jedit")) if (props1 != props2) File.write(properties, cat_lines(props2)) } Isabelle_System.make_directory(settings_dir + Path.explode("DockableWindowManager")) if (!(settings_dir + Path.explode("perspective.xml")).is_file) { File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"), """""") File.write(settings_dir + Path.explode("perspective.xml"), XML.header + """ """) } Scala_Project.plugin_contexts().foreach(isabelle.setup.Build.build(_, false)) /* args */ val jedit_settings = "-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS")) val jedit_server = System.getProperty("isabelle.jedit_server") match { case null | "" => "-noserver" case name => "-server=" + name } val jedit_options = Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +") val more_args = { args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match { case Nil | List("--") => args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy"))) - case List(":") => args.slice(0, args.size - 1) + case List(":") => args.slice(0, args.length - 1) case _ => args } } /* environment */ for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) { MiscUtilities.putenv(name, File.platform_path(Isabelle_System.getenv(name))) } MiscUtilities.putenv("ISABELLE_ROOT", null) /* properties */ System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME"))) System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME"))) System.setProperty("scala.color", "false") /* main startup */ () => jEdit.main(Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args) } catch { case exn: Throwable => GUI.init_laf() GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn))) sys.exit(2) } } start() } } } 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,501 +1,501 @@ /* 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 = + 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 (Isabelle.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())) } case Session.Ready if !shutting_down.value => init_models() if (!Isabelle.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) Isabelle.continuous_checking = true } } 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) != Some(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_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 msg: 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 msg: 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 msg: 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() val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root)) /* 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() } }